OAI/Geometry/RCD/Sobolev/DyadicRadialEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.dyadic_radial_value_energy line 24

   Source documentation

   The same centered affine fit controls values of the genuine distance radial derivative and gradients of its genuine Poisson counterpart. Both errors use the same summable Poisson envelope and the same frame.

   theorem dyadic_radial_value_energy {K : ℝ} (m : ℕ)
       (hX : NoncollapsedRCD K (m + 2) X) [IsFiniteMeasureOnCompacts (hausdorff (m + 2) X)]
       (hhessian : LocalPoissonHessianInput hX)
       {a κ r0 B J C A Cχ L δ : ℝ} {p : X}
       (ha : 0 ≤ a) (hκ : 0 ≤ κ) (hK : -κ ≤ K)
       (hB : 0 ≤ B) (hJ : 0 ≤ J) (hA : 0 ≤ A) (hCχ : 0 ≤ Cχ)
       (hr01 : r0 ≤ 1) (hscale : a * (3 * r0) ≤ 1)
       (hBG : BallVolumeComparison (hausdorff (m + 2) X) (comparisonModelVolume (m + 1) a))
       (S : DyadicDistanceSources (hausdorff (m + 2) X) hX.quadratic (m + 2) κ p r0)
       (T : DyadicDistanceReplacements (hausdorff (m + 2) X) hX.quadratic S B J C)
       (hP : Summable (normalizedPoissonDefect (hausdorff (m + 2) X) hX.quadratic S))
       (hquarter : ∀ t : ℝ, 0 < t → t ≤ r0 →
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianInput, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.normalizedPoissonDefect