ContactSelectionAE.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

From permuted contact triples to deterministic branch selection

The central component is disjoint from every outer branch image. Therefore, when a contact triple is written with its first coordinate in the central component, its second coordinate must be an outer branch of that same point. The statements are independent of the analytic construction of the branches.

def OAI.Problem356.ContactSelection.BranchContact line 25
Source documentation
A deliberately broad contact relation: any pair of outer branches is allowed. A more precise geometric contact set can imply this relation.
```
def BranchContact (B : Set α) (H : ι → α → α) (t : α × (α × α)) : Prop :=
…
```
theorem OAI.Problem356.ContactSelection.second_eq_outer_of_perm line 31
Source documentation
Removing the unique central entry of a permuted triple leaves two outer entries. Neither injectivity nor pairwise disjointness of the outer images is required for this step.
```
theorem second_eq_outer_of_perm {B : Set α} {a b c x y z : α}
    (ha : a ∈ B) (hy : y ∉ B) (hz : z ∉ B)
    (hp : List.Perm [a, b, c] [x, y, z]) : b = y ∨ b = z := by
…
```
theorem OAI.Problem356.ContactSelection.second_selects_of_contact line 46
theorem OAI.Problem356.ContactSelection.second_selects_of_contact_disjoint line 62

theorem OAI.Problem356.ContactSelection.ae_selects_of_ae_contact line 74

Source documentation

Transfer the contact relation from the marginal to a central component measure, and then extract the branch selected by the second graph map.

theorem ae_selects_of_ae_contact {μ ν : Measure α} {B : Set α}
    {H : ι → α → α} {T₂ T₃ : α → α}
    (hac : ν ≪ μ) (hB : ∀ᵐ x ∂ν, x ∈ B)
    (houter : ∀ i, Disjoint B (H i '' B))
    (hcontact : ∀ᵐ x ∂μ, BranchContact B H (x, (T₂ x, T₃ x))) :
    ∀ᵐ x ∂ν, ∃ i, T₂ x = H i x := by
…

Mentions: OAI.Problem356.ContactSelection.BranchContact

theorem OAI.Problem356.ContactSelection.absolutelyContinuous_of_smul_le line 85
Source documentation
A positive-weight component is absolutely continuous with respect to any measure dominating it, including the five-component branch mixture.
```
theorem absolutelyContinuous_of_smul_le {μ ν : Measure α} {a : ℝ≥0∞}
    (ha : a ≠ 0) (hdom : a • ν ≤ μ) : ν ≪ μ :=
…
```
theorem OAI.Problem356.ContactSelection.ae_selects_of_smul_le_of_ae_contact line 89