RegularPinchingFrame.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The exact interior frame used to test full directional mass

def OAI.RegularPointCoordinates.pinchingFrameVolumeRatio line 15
Source documentation
The volume loss from the radial normalization ball to the mass-test ball.
```
def pinchingFrameVolumeRatio (n : ℕ) : ℝ :=
…
```

theorem OAI.RegularPointCoordinates.regular_pinching_frame line 22

Source documentation

The same actual harmonic coordinates admit a bounded exact frame on three times the mass radius, with a gradient bound on the cutoff support.

theorem regular_pinching_frame {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    {base 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}
    (e : RegularProjectionEnvironment hX base hk a κ B J C A Cχ enlargement zeta eta)
    (hcenter : center ∈ ball base (e.heat.radius / 32))
    (d : RegularCenterRadialData hX e.heat κ B J C A Cχ eta Cg D Ca center)
    (hzeta : 0 ≤ zeta) (hzeta1 : zeta ≤ 1)
    (hsmall : (n : ℝ) ^ 2 * (pinchingFrameVolumeRatio n * zeta) ≤ 1 / 2)
    (i : ℕ) :
    let μ := hausdorff n X
…

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