RegularPairGradient.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Harmonic residual gradients in the common regular neighborhood

theorem OAI.RegularPointCoordinates.regular_pair_projection_gradient line 18

Source documentation

The actual sharp projection bound supplies an actual Sobolev residual and a uniform physical gradient estimate, in the same centered heat frame.

theorem regular_pair_projection_gradient {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    (hgradient : LocalHarmonicL2GradientInput hX) (hn : 2 ≤ n)
    {P : ℝ} (hP : 0 < P) :
    ∃ Q : ℝ, 0 < Q ∧
    ∀ {base first center : X} {a κ B J C A Cχ enlargement zeta eta Cg D Ca : ℝ}
      {ker : ℝ → X → X → ℝ}
      {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker},
    0 ≤ κ →
    ∀ (e : RegularProjectionEnvironment hX base hk a κ B J C A Cχ enlargement zeta eta),
    center ∈ ball base (e.heat.radius / 32) →
    ∀ (d1 : RegularCenterRadialData hX e.heat κ B J C A Cχ eta Cg D Ca first)
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment, OAI.RegularPointCoordinates.RegularCenterRadialData