AtomlessTransport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.Transport.exists_uniform_map line 17

Source documentation

Every atomless standard Borel probability admits a uniform random variable.

theorem exists_uniform_map {X : Type uX} [MeasurableSpace X]
    [StandardBorelSpace X] (μ : Measure X) [IsProbabilityMeasure μ]
    [NullSingletonClass μ] :
    ∃ f : X → I, Measurable f ∧ Measure.map f μ = volume := by
…

theorem OAI.Problem356.Transport.exists_measurable_transport line 35

Source documentation

A singleton-null standard Borel probability can be transported measurably to any probability on a nonempty standard Borel target.

theorem exists_measurable_transport {X : Type uX} {Y : Type uY}
    [MeasurableSpace X] [StandardBorelSpace X]
    [MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y]
    (μ : Measure X) (ν : Measure Y)
    [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] [NullSingletonClass μ] :
    ∃ Q : X → Y, Measurable Q ∧ Measure.map Q μ = ν := by
…

theorem OAI.Problem356.Transport.exists_measurable_transport_finite line 47

Source documentation

Equal finite masses can be transported provided the source has no point atoms.

theorem exists_measurable_transport_finite {X : Type uX} {Y : Type uY}
    [MeasurableSpace X] [StandardBorelSpace X]
    [MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y]
    (μ : Measure X) (ν : Measure Y)
    [IsFiniteMeasure μ] [IsFiniteMeasure ν] [NullSingletonClass μ]
    (hmass : μ univ = ν univ) :
    ∃ Q : X → Y, Measurable Q ∧ Measure.map Q μ = ν := by
…

theorem OAI.Problem356.Transport.exists_measurable_transport_restrict line 81

Source documentation

A restricted atomless measure can be redistributed proportionally over any positive-mass target cell. The input cell is allowed to have mass zero.

theorem exists_measurable_transport_restrict {X : Type uX}
    [MeasurableSpace X] [StandardBorelSpace X] [Nonempty X]
    (μ : Measure X) [IsFiniteMeasure μ] [NullSingletonClass μ]
    (A B : Set X) (hA : μ A ≠ 0) :
    ∃ Q : X → X, Measurable Q ∧
      Measure.map Q (μ.restrict B) = (μ B / μ A) • μ.restrict A := by
…

theorem OAI.Problem356.Transport.exists_measurable_transport_restrict_mem line 97

Source documentation

The transport to a measurable target cell can be chosen to take every value inside that cell, by resetting outputs on a source-null set.

theorem exists_measurable_transport_restrict_mem {X : Type uX}
    [MeasurableSpace X] [StandardBorelSpace X] [Nonempty X]
    (μ : Measure X) [IsFiniteMeasure μ] [NullSingletonClass μ]
    (A B : Set X) (hAm : MeasurableSet A) (hA : μ A ≠ 0) :
    ∃ Q : X → X, Measurable Q ∧
      Measure.map Q (μ.restrict B) = (μ B / μ A) • μ.restrict A ∧
      ∀ x, Q x ∈ A := by
…