ActualRadialEnergy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Interior energy of the actual Poisson radial fits

theorem OAI.RegularPointCoordinates.actual_radial_fit_energy line 22

Source documentation

The actual Poisson radial derivative has an interior gradient fit controlled by the distance value fit and the original Poisson defect. The harmonic gradient constant is chosen before all centers and scales.

theorem actual_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χ : ℝ},
      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),
      (∀ j, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic
        (ball p (distanceSourceRadius r0 i / 4)) (u j)) →
…

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.IsSobolevHarmonicOn