Splitting.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The deterministic-selection mass obstruction

A preserving map cannot carry a positive-mass selection set into a target whose prescribed mass is a strictly smaller multiple of the same reference mass. This is the measure-theoretic obstruction in the Coulomb construction.

theorem OAI.Problem356.Splitting.reference_mass_zero_of_compression line 26

Source documentation

Preservation and a strict compression of the reference mass force the selected set to have reference measure zero.

theorem reference_mass_zero_of_compression
    {μ ν : Measure α} {T : α → α} {S A : Set α} {c d : ℝ≥0∞}
    (hT : Measurable T) (hpres : Measure.map T μ = μ)
    (hA : MeasurableSet A) (hsub : S ⊆ T ⁻¹' A)
    (hsource : μ S = c * ν S) (htarget : μ A = d * ν S)
    (hdc : d < c) (hfinite : ν S ≠ ⊤) : ν S = 0 := by
…

theorem OAI.Problem356.Splitting.not_preserving_of_countable_compression line 44

Source documentation

No preserving map can implement a countable almost-everywhere selection whose source and target masses have a uniformly strict reversed ratio.

theorem not_preserving_of_countable_compression [Countable ι]
    {μ ν : Measure α} [IsFiniteMeasure ν]
    {T : α → α} {S A : ι → Set α} {c d : ℝ≥0∞}
    (hν : ν Set.univ ≠ 0)
    (hA : ∀ i, MeasurableSet (A i))
    (hsub : ∀ i, S i ⊆ T ⁻¹' A i)
    (hsource : ∀ i, μ (S i) = c * ν (S i))
    (htarget : ∀ i, μ (A i) = d * ν (S i))
    (hdc : d < c)
    (hcover : ∀ᵐ x ∂ν, ∃ i, x ∈ S i) :
    ¬ (Measurable T ∧ Measure.map T μ = μ) := by
…

theorem OAI.Problem356.Splitting.no_preserving_branch_selection line 70

Source documentation

The branch-selection formulation. The hypotheses about selected-set masses are exactly those supplied by disjoint weighted pushforward components. No regularity beyond measurability is imposed on the selector.

theorem no_preserving_branch_selection [Countable ι] [MeasurableEq α]
    {μ ν : Measure α} [IsFiniteMeasure ν] {B : Set α}
    {H : ι → α → α} {c d : ℝ≥0∞}
    (hν : ν Set.univ ≠ 0) (hB : MeasurableSet B)
    (hfull : ∀ᵐ x ∂ν, x ∈ B)
    (hH : ∀ i, Measurable (H i))
    (himage : ∀ i S, MeasurableSet S → S ⊆ B →
      MeasurableSet (H i '' S))
    (hsource : ∀ S, MeasurableSet S → S ⊆ B → μ S = c * ν S)
    (htarget : ∀ i S, MeasurableSet S → S ⊆ B →
      μ (H i '' S) = d * ν S)
    (hdc : d < c) :
…