OAI/Analysis/CircleDomains/Transfer/FiniteRealChartIntersections.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite generic intersections on a bounded physical chart follow from the actual L2 occupation density and the coordinate's differential energy. No simplicity of the sampled path is needed.

  1. theorem OAI.CircleDomainRigidity.mean_real_chart_circle_count_finite line 23
  2. theorem OAI.CircleDomainRigidity.ae_real_chart_circle_count_finite line 79