OAI/Analysis/CircleDomains/Probability/CompactMeasureBarycenter.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual barycenter measure of a law on a compact family. Both its finite mass and its nonnegative continuous test integrals follow from the measurable measure-valued inclusion, not an assumed identity.

  1. def OAI.CircleDomainRigidity.compactMeasureBarycenter line 18
  2. lemma OAI.CircleDomainRigidity.measurable_compactMeasure_inclusion line 22
  3. lemma OAI.CircleDomainRigidity.compactMeasureBarycenter_apply line 27
  4. lemma OAI.CircleDomainRigidity.compactMeasureBarycenter_finite line 32
  5. lemma OAI.CircleDomainRigidity.compactMeasureBarycenter_lintegral line 49
  6. lemma OAI.CircleDomainRigidity.compactMeasureBarycenter_integral_nonneg line 55