OAI/Geometry/RCD/Sobolev/QuadraticCutoffIdentity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.bounded_product_bound line 17
2. theorem OAI.RegularPointCoordinates.coordinateQuadratic_cutoff_energy line 30

   Source documentation

   Testing the quadratic model against an actual cutoff times a bounded Sobolev function is legitimate in every harmonic coordinate equation.

   theorem coordinateQuadratic_cutoff_energy {n : ℕ} {Ω : Set X}
       (u : Fin n → SobolevSpace μ hQ) (C D E L : ℝ≥0)
       (hu : ∀ j, IsSobolevHarmonicOn μ hQ Ω (u j))
       (hub : ∀ j, ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (u j) x| ≤ C)
       (c w : SobolevSpace μ hQ) (χ : X → ℝ)
       (hχ : LipschitzWith L χ) (hcpt : HasCompactSupport χ)
       (hbound : ∀ x, |χ x| ≤ E) (hnonneg : ∀ x, 0 ≤ χ x)
       (hsupp : tsupport χ ⊆ Ω) (hcrep : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
       (hw : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ w x| ≤ D) :
       energyForm μ hQ (coordinateQuadratic μ hQ u C) (SobolevSpace.product μ hQ c w E D) =
         -(∫ x, SobolevSpace.toLp μ hQ (SobolevSpace.product μ hQ c w E D) x *
           (∑ j, localGamma μ hQ (u j) (u j) x) ∂μ) := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.coordinateQuadratic, OAI.RegularPointCoordinates.SobolevSpace.product, OAI.RegularPointCoordinates.localGamma

3. theorem OAI.RegularPointCoordinates.coordinateQuadratic_cutoff_cross line 68

   Source documentation

   The exact cross-term identity used in qualitative convergence of the distance gradient. The quadratic model's source is the actual Gram trace.

   theorem coordinateQuadratic_cutoff_cross {n : ℕ} {Ω : Set X}
       (u : Fin n → SobolevSpace μ hQ) (C D E L : ℝ≥0)
       (hu : ∀ j, IsSobolevHarmonicOn μ hQ Ω (u j))
       (hub : ∀ j, ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (u j) x| ≤ C)
       (c w : SobolevSpace μ hQ) (χ : X → ℝ)
       (hχ : LipschitzWith L χ) (hcpt : HasCompactSupport χ)
       (hbound : ∀ x, |χ x| ≤ E) (hnonneg : ∀ x, 0 ≤ χ x)
       (hsupp : tsupport χ ⊆ Ω) (hcrep : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
       (hw : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ w x| ≤ D) :
       (∫ x, SobolevSpace.toLp μ hQ c x *
         localGamma μ hQ w (coordinateQuadratic μ hQ u C) x ∂μ) =
         -(∫ x, SobolevSpace.toLp μ hQ (SobolevSpace.product μ hQ c w E D) x *
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.coordinateQuadratic, OAI.RegularPointCoordinates.SobolevSpace.product