OAI/Geometry/RCD/Coordinates/TwoCenterCommutatorFit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.norm_le_sqrt_mul_of_sq_le line 14
2. theorem OAI.RegularPointCoordinates.normalized_commutator_fit_norm line 25

   Source documentation

   A normalized integral commutator bound is precisely the L2 error required by the affine coefficient identity, for the chosen representatives.

   theorem normalized_commutator_fit_norm (Ω : Set X) (hfin : μ Ω ≠ ∞)
       (f v u g h : SobolevSpace μ hQ) {Cf Cv E r : ℝ}
       (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ Cf)
       (hv : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ v v x ≤ Cv)
       (hh : SobolevSpace.toLp μ hQ h =ᵐ[μ.restrict Ω] localGamma μ hQ v u)
       (hE : 0 ≤ E) (hr : 0 ≤ r)
       (he : (μ.real Ω)⁻¹ * (∫ x in Ω,
         (localGamma μ hQ v g x - localGamma μ hQ f h x - localGamma μ hQ v u x) ^ 2 ∂μ) ≤ E * r ^ 2) :
       ‖normalizeLocalL2 μ Ω hfin (localRadialDerivative μ hQ Ω v hv g -
         localRadialDerivative μ hQ Ω f hf h - SobolevSpace.restrictLp μ hQ Ω h)‖ ≤ Real.sqrt E * r := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.localRadialDerivative, OAI.RegularPointCoordinates.SobolevSpace.restrictLp

3. theorem OAI.RegularPointCoordinates.two_center_affine_commutator_bound line 43

   Source documentation

   This is the quantitative affine residual of the actual two-center argument. Its hypotheses are the two radial fits and the separately proved full Poisson-mass commutator estimate, all on the same region.

   theorem two_center_affine_commutator_bound {n : ℕ}
       (Ω : Set X) (hfin : μ Ω ≠ ∞) (fz fx η : SobolevSpace μ hQ)
       {Cf Cv Ez Ex Dz Dx K : ℝ}
       (hCf : 0 ≤ Cf) (hCv : 0 ≤ Cv)
       (hEz : 0 ≤ Ez) (hEx : 0 ≤ Ex) (hDz : 0 ≤ Dz) (hDx : 0 ≤ Dx) (hK : 0 ≤ K)
       (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ fz fz x ≤ Cf ^ 2)
       (hv : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ (fz - fx) (fz - fx) x ≤ Cv ^ 2)
       (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
       (U Gz Gx : Euclidean n →L[ℝ] SobolevSpace μ hQ)
       (hGz : ∀ a, SobolevSpace.toLp μ hQ (Gz a) =ᵐ[μ.restrict Ω] localGamma μ hQ fz (U a))
       (hGx : ∀ a, SobolevSpace.toLp μ hQ (Gx a) =ᵐ[μ.restrict Ω] localGamma μ hQ fx (U a))
       (Az Ax : Euclidean n →L[ℝ] Euclidean n) (c : Euclidean n →L[ℝ] ℝ)
   …

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