Commit 2025-05-25 13:18 3537c251

View on Github →

chore(*): use gcongr&positivity (#25128)

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/Analysis/Analytic/ChangeOrigin.lean

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Mul.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean

modified theorem SzemerediRegularity.stepBound_mono

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean

Modified Mathlib/NumberTheory/SelbergSieve.lean

added def Mathlib.Meta.Positivity.evalBoundingSieveWeights

Modified Mathlib/NumberTheory/SiegelsLemma.lean

Modified Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean

Modified Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleNumber.lean

Modified Mathlib/NumberTheory/Zsqrtd/Basic.lean

modified theorem Zsqrtd.sqLe_of_le