OAI/Analysis/CircleDomains/Probability/ProbabilityImageLifting.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Lift a probability supported on the image of a standard Borel code map. A measurable range section and countable measure evaluations suffice as a target encoding, with no probability-space topology hypothesis.

  1. theorem OAI.CircleDomainRigidity.exists_probability_lift_of_measurable_injection line 13
  2. theorem OAI.CircleDomainRigidity.measurePlanLifting line 38

    Source documentation

    The exact published probability-lifting input for finite-measure images.

    theorem measurePlanLifting (A Z : Type*) [MeasurableSpace A] [StandardBorelSpace A]
    [TopologicalSpace Z] [PolishSpace Z] [MeasurableSpace Z] [BorelSpace Z] :
    MeasurePlanLifting A Z := by
…

    Mentions: OAI.CircleDomainRigidity.MeasurePlanLifting