RegularPairPinching.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.RegularPointCoordinates.regular_pair_pinching line 21
Source documentation
The sharp projection estimate and the constructed radial fits imply full directional pinching, with a uniform constant and source tolerance. The direction is expressed in the actual exact mean-Gram frame on the mass-test ball.
```
theorem regular_pair_pinching {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    (hhessian : LocalPoissonHessianInput hX) (hcutoff : LocalGoodCutoffInput hX)
    (haction : LocalPoissonHessianActionInput hX)
    (hgradient : LocalHarmonicL2GradientInput hX)
    (hmean : LocalHarmonicL2MeanValueInput hX) (hn : 2 ≤ n)
    {A B J Cχ Cg D Ca P : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hJ : 0 ≤ J)
    (hCχ : 0 ≤ Cχ) (hP : 0 < P) :
    ∃ Cpin tau : ℝ, 0 < Cpin ∧ 0 < tau ∧
    ∀ {base first center : X} {a C enlargement zeta eta : ℝ}
      {ker : ℝ → X → X → ℝ}
      {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianInput, OAI.RegularPointCoordinates.LocalGoodCutoffInput, OAI.RegularPointCoordinates.LocalPoissonHessianActionInput, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.tau, OAI.RegularPointCoordinates.IsContinuousHeatKernel