OAI/Analysis/CircleDomains/Probability/FiniteMeasureTightControl.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The tightness estimate in the measure-modulus duality argument. A finite Borel reference measure admits arbitrarily cheap L² densities which charge every measure outside a compact set by at least one.

  1. lemma OAI.CircleDomainRigidity.exists_compact_finiteMeasure_control line 14