CompactMeasureL2Plan.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The compact-family plan has an actual L² representing function on bounded continuous tests. Positivity and Borel-set barycenter identities are established separately from this linear representation step.

lemma OAI.CircleDomainRigidity.exists_compact_measure_L2_test_plan line 16