FiveComponentGlobal.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.FiveComponentGeometry.exists_global_certificate_of_canonical line 17

Source documentation

The actual two canonical local certificates glue into one globally bounded potential on the five disjoint component balls.

theorem exists_global_certificate_of_canonical
    (C₁ : ChartsAt (point 1)) (C₂ : ChartsAt (point 3))
    (W : Fin 5 → Set E3) (hW : ∀ i, IsOpen (W i))
    (hpW : ∀ i, point i ∈ W i) (hWD : ∀ i, W i ⊆ domains C₁ C₂ i)
    (h012 : LocalTypeCertificate W (potentials C₁ C₂) (branchContact C₁ C₂) 0 1 2)
    (h034 : LocalTypeCertificate W (potentials C₁ C₂) (branchContact C₁ C₂) 0 3 4) :
    ∃ r M : ℝ, 0 < r ∧ 0 < M ∧
      let U := fun i => ball (point i) r
…

Mentions: OAI.Problem356.FiveComponentGeometry.ChartsAt, OAI.Problem356.E3, OAI.Problem356.FiveComponentGeometry.domains, OAI.Problem356.FiveComponentGeometry.potentials, OAI.Problem356.FiveComponentGeometry.branchContact

lemma OAI.Problem356.FiveComponentGeometry.ennreal_graph_equality line 45

Source documentation

Every collision-free raw branch triple saturates the local potential.

lemma ennreal_graph_equality {a : E3} (C : ChartsAt a) {y : E3}
    (hy : y ∈ C.charts.central.source)
    (hxy : 0 < dist (C.charts.central y) y)
    (hxz : 0 < dist (C.charts.central y) (C.charts.opposite y))
    (hyz : 0 < dist y (C.charts.opposite y)) :
    ENNReal.ofReal (((5 : ℝ) / 2 - 10 * ‖C.charts.central y‖ ^ 2) + C.value y +
      ((5 : ℝ) / 4 * ⟪a, C.charts.opposite y + a⟫_ℝ -
        10 * ‖C.charts.opposite y + a‖ ^ 2)) =
      coulombCost (C.charts.central y, (y, C.charts.opposite y)) := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.FiveComponentGeometry.ChartsAt, OAI.Problem356.coulombCost

lemma OAI.Problem356.FiveComponentGeometry.ne_of_disjoint_components line 59

theorem OAI.Problem356.FiveComponentGeometry.glued_saturation_left line 68

Source documentation

Saturation on the first raw branch, after gluing.

theorem glued_saturation_left (C₁ : ChartsAt (point 1)) (C₂ : ChartsAt (point 3))
    {U : Fin 5 → Set E3} (hUD : ∀ i, U i ⊆ domains C₁ C₂ i)
    (hdisj : Pairwise (fun i j => Disjoint (U i) (U j)))
    {x y z : E3} (hx : x ∈ U 0) (hy : y ∈ U 1) (hz : z ∈ U 2)
    (hX : x = C₁.charts.central y) (hZ : z = C₁.charts.opposite y) :
    let u := ComponentPotential.glue U (potentials C₁ C₂)
…

Mentions: OAI.Problem356.FiveComponentGeometry.ChartsAt, OAI.Problem356.E3, OAI.Problem356.FiveComponentGeometry.domains, OAI.Problem356.ComponentPotential.glue, OAI.Problem356.FiveComponentGeometry.potentials

theorem OAI.Problem356.FiveComponentGeometry.glued_saturation_right line 86

Source documentation

Saturation on the second raw branch, after gluing.

theorem glued_saturation_right (C₁ : ChartsAt (point 1)) (C₂ : ChartsAt (point 3))
    {U : Fin 5 → Set E3} (hUD : ∀ i, U i ⊆ domains C₁ C₂ i)
    (hdisj : Pairwise (fun i j => Disjoint (U i) (U j)))
    {x y z : E3} (hx : x ∈ U 0) (hy : y ∈ U 3) (hz : z ∈ U 4)
    (hX : x = C₂.charts.central y) (hZ : z = C₂.charts.opposite y) :
    let u := ComponentPotential.glue U (potentials C₁ C₂)
…

theorem OAI.Problem356.FiveComponentGeometry.exists_global_certificate line 106
Source documentation
The concrete two Coulomb charts admit a globally bounded measurable certificate on five disjoint component balls, with contact only on their actual symmetric graph union.
```
theorem exists_global_certificate
    (C₁ : ChartsAt (point 1)) (C₂ : ChartsAt (point 3)) :
    ∃ r M : ℝ, 0 < r ∧ 0 < M ∧
      let U := fun i => ball (point i) r
…
```
Mentions: OAI.Problem356.FiveComponentGeometry.ChartsAt