OAI/Analysis/CircleDomains/Probability/CompactMeasureDensity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The compact-family plan has the actual nonnegative Borel L² density of its barycenter. The identity is proved on Borel sets, not just tests.

  1. lemma OAI.CircleDomainRigidity.L2_ofReal_energy_eq line 17
  2. lemma OAI.CircleDomainRigidity.compactMeasureBarycenter_eq_withDensity line 36
  3. lemma OAI.CircleDomainRigidity.exists_compact_measure_density_plan line 77