OAI/Geometry/RCD/Sobolev/QuadraticGradientComparison.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.weighted_gamma_integrable line 18
2. theorem OAI.RegularPointCoordinates.gamma_sub_right line 24

   Distinct definitions of this name: OAI/Geometry/RCD/Harmonic/CompactMixedTransfer.lean:13 (different declaration text). Qualify references as OAI.RegularPointCoordinates.gamma_sub_right@path.

3. theorem OAI.RegularPointCoordinates.weighted_difference_energy line 32

   Source documentation

   Polarization keeps the signed cross term until after integration.

   theorem weighted_difference_energy (c q H : SobolevSpace μ hQ) (C : ℝ≥0)
       (hc : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ c x| ≤ C) :
       (∫ x, SobolevSpace.toLp μ hQ c x * localGamma μ hQ (q - H) (q - H) x ∂μ) =
         (∫ x, SobolevSpace.toLp μ hQ c x * localGamma μ hQ q q x ∂μ) -
         (∫ x, SobolevSpace.toLp μ hQ c x * localGamma μ hQ H H x ∂μ) -
         2 * ∫ x, SobolevSpace.toLp μ hQ c x * localGamma μ hQ (q - H) H x ∂μ := by
   …

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

4. theorem OAI.RegularPointCoordinates.coordinateQuadratic_difference_energy line 61

   Source documentation

   The gradient error between squared distance and the quadratic coordinate model is expressed using value errors and the actual Gram trace. This is the integration-by-parts step in qualitative convergence.

   theorem coordinateQuadratic_difference_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 q : 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 (q - coordinateQuadratic μ hQ u C) x| ≤ D) :
       let H := coordinateQuadratic μ hQ u C
   …

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