OAI/Geometry/RCD/Sobolev/RadialCutoffEnergyIdentity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact energy normalization for a physical interior cutoff

  1. theorem OAI.RegularPointCoordinates.nested_cutoff_integral_region line 14
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.radial_cutoff_energy_identity line 26