PartitionTransport.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.PartitionTransport.exists_map_eq_sum_of_partition line 18

Source documentation

Gluing measurable transports on a countable measurable partition gives the sum of their restricted pushforwards. The partition need only cover almost everywhere.

theorem exists_map_eq_sum_of_partition [Countable ι] [Nonempty ι]
    (μ : Measure α) (B : ι → Set α)
    (hB : ∀ i, MeasurableSet (B i))
    (hdisj : Pairwise fun i j => Disjoint (B i) (B j))
    (hcover : ∀ᵐ x ∂μ, x ∈ ⋃ i, B i)
    (T : ι → α → β) (hT : ∀ i, Measurable (T i)) :
    ∃ f : α → β, Measurable f ∧
      (∀ i, EqOn f (T i) (B i)) ∧
      Measure.map f μ = Measure.sum (fun i => Measure.map (T i) (μ.restrict (B i))) := by
…

theorem OAI.Problem356.PartitionTransport.exists_map_eq_of_partition line 46

Source documentation

Prescribed laws on partition pieces can be glued into a transport to their sum.

theorem exists_map_eq_of_partition [Countable ι] [Nonempty ι]
    (μ : Measure α) (B : ι → Set α)
    (hB : ∀ i, MeasurableSet (B i))
    (hdisj : Pairwise fun i j => Disjoint (B i) (B j))
    (hcover : ∀ᵐ x ∂μ, x ∈ ⋃ i, B i)
    (T : ι → α → β) (hT : ∀ i, Measurable (T i))
    (ν : ι → Measure β)
    (hmap : ∀ i, Measure.map (T i) (μ.restrict (B i)) = ν i) :
    ∃ f : α → β, Measurable f ∧
      (∀ i, EqOn f (T i) (B i)) ∧ Measure.map f μ = Measure.sum ν := by
…

theorem OAI.Problem356.PartitionTransport.exists_map_eq_finset_sum_of_partition line 62

Source documentation

The finite form, using the usual finite sum of target measures.

theorem exists_map_eq_finset_sum_of_partition [Fintype ι] [Nonempty ι]
    (μ : Measure α) (B : ι → Set α)
    (hB : ∀ i, MeasurableSet (B i))
    (hdisj : Pairwise fun i j => Disjoint (B i) (B j))
    (hcover : ∀ᵐ x ∂μ, x ∈ ⋃ i, B i)
    (T : ι → α → β) (hT : ∀ i, Measurable (T i))
    (ν : ι → Measure β)
    (hmap : ∀ i, Measure.map (T i) (μ.restrict (B i)) = ν i) :
    ∃ f : α → β, Measurable f ∧
      (∀ i, EqOn f (T i) (B i)) ∧ Measure.map f μ = ∑ i, ν i := by
…

theorem OAI.Problem356.PartitionTransport.map_eq_sum_dirac_of_partition line 77

Source documentation

The pushforward law of a label that is constant almost everywhere on each partition piece is the atomic measure with those piece masses.

theorem map_eq_sum_dirac_of_partition [Countable ι]
    (μ : Measure α) (B : ι → Set α)
    (hB : ∀ i, MeasurableSet (B i))
    (hdisj : Pairwise fun i j => Disjoint (B i) (B j))
    (hcover : ∀ᵐ x ∂μ, x ∈ ⋃ i, B i)
    (L : α → β) (hL : Measurable L) (label : ι → β)
    (hlabel : ∀ i, ∀ᵐ x ∂μ.restrict (B i), L x = label i) :
    Measure.map L μ = Measure.sum (fun i => μ (B i) • Measure.dirac (label i)) := by
…

theorem OAI.Problem356.PartitionTransport.map_restrict_eq_of_eqOn line 99

Source documentation

An exact agreement on a measurable piece gives equality of restricted laws.

theorem map_restrict_eq_of_eqOn (μ : Measure α) {B : Set α}
    (hB : MeasurableSet B) {f g : α → β} (heq : EqOn f g B) :
    Measure.map f (μ.restrict B) = Measure.map g (μ.restrict B) := by
…

theorem OAI.Problem356.PartitionTransport.exists_pair_maps_with_label_law line 109

Source documentation

Glue two families of transports simultaneously. Their marginal laws and joint finite-cell law are all explicit. This is the graph-plan step in the cellwise approximation construction.

theorem exists_pair_maps_with_label_law [Countable ι] [Nonempty ι]
    {κ : Type uKappa} [MeasurableSpace κ]
    (μ : Measure α) (B : ι → Set α)
    (hB : ∀ i, MeasurableSet (B i))
    (hdisj : Pairwise fun i j => Disjoint (B i) (B j))
    (hcover : ∀ᵐ x ∂μ, x ∈ ⋃ i, B i)
    (T₂ T₃ : ι → α → α)
    (hT₂ : ∀ i, Measurable (T₂ i)) (hT₃ : ∀ i, Measurable (T₃ i))
    (ν₂ ν₃ : ι → Measure α)
    (hmap₂ : ∀ i, Measure.map (T₂ i) (μ.restrict (B i)) = ν₂ i)
    (hmap₃ : ∀ i, Measure.map (T₃ i) (μ.restrict (B i)) = ν₃ i)
    (hsum₂ : Measure.sum ν₂ = μ) (hsum₃ : Measure.sum ν₃ = μ)
…

theorem OAI.Problem356.PartitionTransport.sum_normalized_restrict_eq line 158

Source documentation

Redistributing weights to the normalized restrictions of a finite partition preserves the measure when the weights have the prescribed marginal sums. Zero-mass cells require no positivity assumption.

theorem sum_normalized_restrict_eq [Fintype ι]
    {κ : Type uKappa} [Fintype κ] [DecidableEq κ]
    (μ : Measure α) [IsFiniteMeasure μ] (A : κ → Set α)
    (hA : ∀ j, MeasurableSet (A j))
    (hdisj : Pairwise fun i j => Disjoint (A i) (A j))
    (hcover : ∀ᵐ x ∂μ, x ∈ ⋃ j, A j)
    (label : ι → κ) (w : ι → ℝ≥0∞)
    (hweights : ∀ j, ∑ i ∈ Finset.univ.filter (fun i => label i = j), w i = μ (A j)) :
    (∑ i, (w i / μ (A (label i))) • μ.restrict (A (label i))) = μ := by
…