OAI/Geometry/RCD/Sobolev/CutoffGaugeEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact energy transfer through a radial cutoff and constant gauge

Tests supported on the inner ball see the original energy, independently of the outer radial realization and the chosen additive constant.

  1. theorem OAI.RegularPointCoordinates.cutoff_gauge_weighted_energy line 18