OAI/Geometry/RCD/Transport/LocalizedPlanEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local energy control along a bounded-compression plan

The squared endpoint difference only uses energy on the region containing the paths. This localization is needed for the interior Poincare input.

  1. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_integrated_square_on line 20