OAI/Geometry/RCD/Sobolev/SmallRadiusPoissonMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Poisson source control of transport means at every physical radius

The full shifted mass is constructed from the actual positive source. The balanced estimate uses the radius-dependent centered action bound.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.small_radius_poisson_mean_estimate line 26