OAI/Geometry/RCD/Harmonic/AffineCommutatorResidual.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.normalized_radial_derivative_norm_le line 18
2. theorem OAI.RegularPointCoordinates.normalized_affine_commutator_bound line 31

   Source documentation

   All five terms in the exact coefficient identity are controlled by the two actual W12 fits and the full-mass commutator error.

   theorem normalized_affine_commutator_bound {n : ℕ}
       (Ω : Set X) (hfin : μ Ω ≠ ∞) (f v η : SobolevSpace μ hQ)
       {Cf Cv eg dg eh dh k : ℝ}
       (hCf : 0 ≤ Cf) (hCv : 0 ≤ Cv) (hdg : 0 ≤ dg) (hdh : 0 ≤ dh)
       (heg : 0 ≤ eg) (heh : 0 ≤ eh)
       (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ Cf ^ 2)
       (hv : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ v v x ≤ Cv ^ 2)
       (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
       (U G H : Euclidean n →L[ℝ] SobolevSpace μ hQ)
       (hG : ∀ a, SobolevSpace.toLp μ hQ (G a) =ᵐ[μ.restrict Ω] localGamma μ hQ f (U a))
       (hH : ∀ a, SobolevSpace.toLp μ hQ (H a) =ᵐ[μ.restrict Ω] localGamma μ hQ v (U a))
       (A B : Euclidean n →L[ℝ] Euclidean n) (c : Euclidean n →L[ℝ] ℝ)
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.Euclidean