BranchInterfaces.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem356.BranchSeparation.pairwise_components_of_disjoint_branches line 14
Source documentation
The disjointness assumptions supplied by the local branch construction are exactly pairwise disjointness of the five labelled components.
```
lemma pairwise_components_of_disjoint_branches {B : Set E3} {H : Fin 4 → E3 → E3}
    (hcentral : ∀ i, Disjoint B (H i '' B))
    (houter : Pairwise fun i j => Disjoint (H i '' B) (H j '' B)) :
    Pairwise fun i j => Disjoint (components B H i) (components B H j) := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.BranchSeparation.components

theorem OAI.Problem356.BranchSeparation.compact_support_and_separation_of_branches line 35

Source documentation

Compact support and uniform separation follow directly from the local central/outer disjointness interface used by counterexample assembly.

theorem compact_support_and_separation_of_branches
    {nu : Measure E3} {K B : Set E3} (hK : IsCompact K) (hKB : K ⊆ B)
    (hnu : ∀ᵐ x ∂nu, x ∈ K) {H : Fin 4 → E3 → E3}
    (hH : ∀ i, Measurable (H i)) (hcont : ∀ i, ContinuousOn (H i) K)
    (hcentral : ∀ i, Disjoint B (H i '' B))
    (houter : Pairwise fun i j => Disjoint (H i '' B) (H j '' B)) :
    (∃ S : Set E3, IsCompact S ∧
      ∀ᵐ x ∂branchMarginal nu (H 0) (H 1) (H 2) (H 3), x ∈ S) ∧
    (∃ eta : ℝ, 0 < eta ∧
      ∀ᵐ t ∂branchCoupling nu (H 0) (H 1) (H 2) (H 3),
        CoulombEstimates.Separated eta t) :=
…

Mentions: OAI.Problem356.E3, OAI.Problem356.branchMarginal, OAI.Problem356.branchCoupling, OAI.Problem356.CoulombEstimates.Separated