LocalSplitting.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The local-homeomorphism selection obstruction

The local branch maps need not be measurable away from their source. Extending them by a constant, then using concentration of the reference measure, gives the exact obstruction stated for the original maps and their pushforwards.

theorem OAI.Problem356.LocalSplitting.no_preserving_local_branch_selection line 29

Source documentation

Local homeomorphic branches on disjoint components cannot admit a measure-preserving deterministic selector when the central weight is larger.

theorem no_preserving_local_branch_selection
    (z : α) (e : ι → OpenPartialHomeomorph α α)
    {ν : Measure α} [IsFiniteMeasure ν] {B : Set α} {c d : ℝ≥0∞}
    (hν : ν univ ≠ 0) (hB : MeasurableSet B)
    (hfull : ∀ᵐ x ∂ν, x ∈ B)
    (hSource : ∀ i, B ⊆ (e i).source)
    (hCentral : ∀ i, Disjoint B (e i '' B))
    (hPair : Pairwise fun i j => Disjoint (e i '' B) (e j '' B))
    (hdc : d < c) :
    ¬ ∃ T : α → α, Measurable T ∧
      Measure.map T (splitMeasure ν c (fun _ => d) (fun i => e i)) =
        splitMeasure ν c (fun _ => d) (fun i => e i) ∧
…

theorem OAI.Problem356.LocalSplitting.no_preserving_four_local_branches line 77

Source documentation

The coefficients and four branches used by the Coulomb counterexample.

theorem no_preserving_four_local_branches
    (z : α) (e : Fin 4 → OpenPartialHomeomorph α α)
    {ν : Measure α} [IsProbabilityMeasure ν] {B : Set α}
    (hB : MeasurableSet B) (hfull : ∀ᵐ x ∂ν, x ∈ B)
    (hSource : ∀ i, B ⊆ (e i).source)
    (hCentral : ∀ i, Disjoint B (e i '' B))
    (hPair : Pairwise fun i j => Disjoint (e i '' B) (e j '' B)) :
    ¬ ∃ T : α → α, Measurable T ∧
      Measure.map T (splitMeasure ν (1 / 3) (fun _ => 1 / 6) (fun i => e i)) =
        splitMeasure ν (1 / 3) (fun _ => 1 / 6) (fun i => e i) ∧
      (∀ᵐ x ∂ν, ∃ i, T x = e i x) := by
…