OAI/Geometry/RCD/Coordinates/FramedRadialEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.LocalHessianPairing.cast_right_mixed line 16
2. theorem OAI.RegularPointCoordinates.framed_radial_fit_energy line 26

   Source documentation

   Applying the energy estimate in a normalized coordinate frame keeps its source term in the inverse-frame norm of the original covector. The radial function and the fitted affine function remain the original ones.

   theorem framed_radial_fit_energy {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [IsFiniteMeasureOnCompacts (hausdorff n X)]
       (hhessian : LocalPoissonHessianInput hX) (hgradient : LocalHarmonicL2GradientInput hX)
       (hn : 2 ≤ n) {κ₀ : ℝ} (hκ₀ : 0 ≤ κ₀) :
       ∃ Cg : ℝ, 1 ≤ Cg ∧ ∀ {κ r0 B J C A ε Cχ Lbase : ℝ},
         0 ≤ κ → -κ ≤ K → 0 ≤ B → 0 ≤ J → 0 ≤ A → 0 ≤ ε → 0 ≤ Cχ →
         ∀ (p : X) (S : DyadicDistanceSources (hausdorff n X) hX.quadratic n κ p r0)
           (T : DyadicDistanceReplacements (hausdorff n X) hX.quadratic S B J C) (i : ℕ),
         distanceSourceRadius r0 i ≤ 1 → -κ₀ ≤ K * (distanceSourceRadius r0 i / 64) ^ 2 →
         ∀ (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
           (N : Euclidean n ≃L[ℝ] Euclidean n),
         (∀ j, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianInput, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.distanceSourceRadius, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsSobolevHarmonicOn