RegularMeanPinching.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Directional pinching for the canonical inverse mean Gram

theorem OAI.RegularPointCoordinates.pinching_mean_radius line 19
Source documentation
The mean normalization in the mass estimate is on the existing dyadic sequence, fifteen indices after the source index.
```
theorem pinching_mean_radius (r : ℝ) (i : ℕ) :
    3 * (distanceSourceRadius r i / 49152) = r / (2 : ℝ) ^ (i + 15) := by
…
```
Mentions: OAI.RegularPointCoordinates.distanceSourceRadius
theorem OAI.RegularPointCoordinates.regular_pair_mean_pinching line 29
Source documentation
The actual local mass matrix uses the inverse of the original mean Gram. The exact normalization used in its proof has disappeared from the quadratic estimate, and the physical mass scaling has been cancelled.
```
theorem regular_pair_mean_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