HarmonicMeanConstruction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The published harmonic mean-value input from RCD calculus

The local level-set iteration proves Jiang's half-ball L² estimate at unit rescaled curvature. A fixed-radius interior cover and the CD ball-volume comparison give the stated estimate for every bounded curvature parameter.

theorem OAI.RegularPointCoordinates.small_radius_curvature line 24
theorem OAI.RegularPointCoordinates.target_norm_le_of_ball_volume line 37
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.harmonicMeanValueInput line 65
Source documentation
The precise half-ball harmonic L²-to-L∞ input is a theorem of the retained RCD structure, with no mean-value or gradient assumption.
```
theorem NoncollapsedRCD.harmonicMeanValueInput {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) : LocalHarmonicL2MeanValueInput hX := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput