Commit 2025-05-08 15:46 f2b9c384

View on Github →

chore(*): use notation for Real.sqrt (#24684) Also golf a couple of proofs using gcongr and positivity.

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

Modified Mathlib/Analysis/CStarAlgebra/Module/Defs.lean

Modified Mathlib/Analysis/Complex/AbelLimit.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Isometric.lean

modified theorem CFC.norm_sqrt

Modified Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean

modified theorem Real.abs_mulExpNegMulSq_le

Modified Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

modified theorem Complex.abs_cpow_inv_two_im

modified theorem Complex.cpow_inv_two_re

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

modified theorem Real.abs_sin_half

modified theorem Real.cos_half

modified theorem Real.tan_pi_div_six

modified theorem Real.tan_pi_div_three

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean

Modified Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean

Modified Mathlib/Data/Complex/Norm.lean

modified theorem Complex.norm_add_mul_I

modified theorem Complex.norm_def

modified theorem Complex.norm_eq_sqrt_sq_add_sq

modified theorem Complex.norm_le_sqrt_two_mul_max

Modified Mathlib/Data/Real/GoldenRatio.lean

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

Modified Mathlib/MeasureTheory/Measure/FiniteMeasureExt.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean

Modified Mathlib/Probability/Distributions/Gaussian.lean

Modified Mathlib/Topology/ContinuousMap/ContinuousSqrt.lean