SplittingConstruction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The disjoint-component selection obstruction

This combines the abstract mass argument with the exact mass identities for a finite mixture of a central measure and its injective branch pushforwards.

theorem OAI.Problem356.Splitting.no_preserving_splitMeasure_selection line 25

Source documentation

A finite family of disjoint injective branches with strictly smaller outer coefficients cannot support any preserving deterministic selector.

theorem no_preserving_splitMeasure_selection [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))
    (hInj : ∀ i, Set.InjOn (H i) B)
    (himage : ∀ i S, MeasurableSet S → S ⊆ B →
      MeasurableSet (H i '' S))
    (hCentral : ∀ i, Disjoint B (H i '' B))
    (hPair : Pairwise fun i j => Disjoint (H i '' B) (H j '' B))
    (hdc : d < c) :
…