OAI/Geometry/RCD/Heat/SmallRadiusOriginalMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Original-potential means at the physical source scale

The balanced Young estimate retains the product of volume and shifted mass. Its action coefficient is uniform in the center and has fourth-order radius scaling, as required for shrinking balls.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.small_radius_original_mean_estimate line 27