CellwiseLift.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.Transport.exists_measurable_lift_preserving_label line 20

Source documentation

A finite atomless source admits a lift to any finite law with that source as marginal, while preserving any prescribed countable measurable label almost everywhere. This permits cellwise approximation without splitting a three-index mass table.

theorem exists_measurable_lift_preserving_label
    {X : Type uX} {Y : Type uY} {ι : Type uIndex} [MeasurableSpace X] [StandardBorelSpace X]
    [MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y]
    [MeasurableSpace ι] [MeasurableSingletonClass ι] [Countable ι] [Nonempty ι]
    (μ : Measure X) (ν : Measure Y) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    [NullSingletonClass μ] (f : Y → X) (hf : Measurable f)
    (hmarg : ν.map f = μ) (p : X → ι) (hp : Measurable p) :
    ∃ Q : X → Y, Measurable Q ∧ μ.map Q = ν ∧
      ∀ᵐ x ∂μ, p (f (Q x)) = p x := by
…

theorem OAI.Problem356.Transport.exists_measurable_lift_close line 76

Source documentation

A lift can preserve the source coordinate to arbitrary precision whenever that source has compact support. Only the first marginal is approximated; the entire target law is transported exactly.

theorem exists_measurable_lift_close
    {X : Type uX} {Y : Type uY} [MetricSpace X] [MeasurableSpace X] [BorelSpace X]
    [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y]
    (μ : Measure X) (ν : Measure Y) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    [NullSingletonClass μ] (f : Y → X) (hf : Measurable f) (hmarg : ν.map f = μ)
    {K : Set X} (hK : IsCompact K) (hfull : μ Kᶜ = 0)
    {δ : ℝ} (hδ : 0 < δ) :
    ∃ Q : X → Y, Measurable Q ∧ μ.map Q = ν ∧
      ∀ᵐ x ∂μ, dist x (f (Q x)) < δ := by
…