OAI/Geometry/RCD/Harmonic/HarmonicInteriorMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Harmonic mean bounds on every strict interior fraction

The fixed half-ball estimate and nearby-ball volume comparison suffice. The constants depend only on the curvature bound and interior fraction.

  1. theorem OAI.RegularPointCoordinates.harmonic_target_norm_le_of_ball_volume line 18
  2. theorem OAI.RegularPointCoordinates.harmonic_interior_mean_bound line 44