ActualRadialPairing.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The genuine Poisson radial derivative in every coordinate covector

theorem OAI.RegularPointCoordinates.actual_distance_radial_pairing line 19

Source documentation

The common published Hessian span supplies the actual radial Sobolev function in every covector, with the full shifted mass budget.

theorem actual_distance_radial_pairing {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [IsFiniteMeasureOnCompacts (hausdorff n X)]
    (hhessian : LocalPoissonHessianInput hX)
    {κ r0 B J C A ε Cχ : ℝ} (hκ : 0 ≤ κ) (hK : -κ ≤ K)
    (hA : 0 ≤ A) (hε : 0 ≤ ε) (hCχ : 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 : ℕ)
    (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
    (hu : ∀ j, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic
      (ball p (distanceSourceRadius r0 i / 4)) (u j))
    (hgrad : ∀ j, ∀ᵐ x ∂(hausdorff n X).restrict (ball p (distanceSourceRadius r0 i / 4)),
      localGamma (hausdorff n X) hX.quadratic (u j) (u j) x ≤ (1 + ε) ^ 2)
…

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