OAI/Analysis/CircleDomains/Probability/CompactFiniteMeasureMeasurability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Only the measurable inclusion of a compact weak family is needed for Riesz representation. No replacement of the evaluation sigma algebra is made.

  1. lemma OAI.CircleDomainRigidity.measurable_measure_of_continuous_finite line 13
  2. lemma OAI.CircleDomainRigidity.compact_finiteMeasure_measurable_le_borel line 30
  3. lemma OAI.CircleDomainRigidity.measurable_finiteMeasure_integral line 44