FiveComponentGeometry.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Problem356.FiveComponentGeometry.ChartsAt line 16
def OAI.Problem356.FiveComponentGeometry.potentials line 21
Source documentation
The actual five local potentials of the Coulomb construction, with the same central quadratic for both branches.
```
def potentials (C₁ : ChartsAt (point 1)) (C₂ : ChartsAt (point 3)) :
    Fin 5 → E3 → ℝ :=
…
```
Mentions: OAI.Problem356.FiveComponentGeometry.ChartsAt, OAI.Problem356.E3
def OAI.Problem356.FiveComponentGeometry.domains line 31
Source documentation
Preliminary domains are unrestricted for the polynomial potentials and are the actual chart sources for the two supporting-value potentials.
```
def domains (C₁ : ChartsAt (point 1)) (C₂ : ChartsAt (point 3)) : Fin 5 → Set E3 :=
…
```
Mentions: OAI.Problem356.FiveComponentGeometry.ChartsAt, OAI.Problem356.E3
lemma OAI.Problem356.FiveComponentGeometry.norm_point_one line 34
lemma OAI.Problem356.FiveComponentGeometry.norm_point_three line 38
lemma OAI.Problem356.FiveComponentGeometry.point_two_eq_neg line 42
lemma OAI.Problem356.FiveComponentGeometry.point_four_eq_neg line 47
lemma OAI.Problem356.FiveComponentGeometry.domains_open line 52
lemma OAI.Problem356.FiveComponentGeometry.point_mem_domains line 62
lemma OAI.Problem356.FiveComponentGeometry.continuousOn_potentials line 72
lemma OAI.Problem356.FiveComponentGeometry.potentials_center_values line 84

lemma OAI.Problem356.FiveComponentGeometry.strict_center_gap line 102

Source documentation

The actual potentials have the strict bad-type gap supplied by the finite center certificate.

lemma strict_center_gap (C₁ : ChartsAt (point 1)) (C₂ : ChartsAt (point 3))
    (i j k : Fin 5) (h : ¬ Good i j k) :
    ENNReal.ofReal (potentials C₁ C₂ i (point i) +
      potentials C₁ C₂ j (point j) + potentials C₁ C₂ k (point k)) <
      coulombCost (point i, (point j, point k)) := by
…

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

theorem OAI.Problem356.FiveComponentGeometry.ennreal_local_certificate line 123

Source documentation

The real local certificate has the exact extended-valued interpretation on any collision-free triple in its three component balls.

theorem ennreal_local_certificate {a : E3} (C : ChartsAt a) {x y z : E3}
    (hy : y ∈ ball a C.parameterRadius)
    (hx : x ∈ ball (0 : E3) C.stateRadius)
    (hz : z ∈ ball (-a) C.stateRadius)
    (hxy : 0 < dist x y) (hxz : 0 < dist x z) (hyz : 0 < dist y z) :
    ENNReal.ofReal (((5 : ℝ) / 2 - 10 * ‖x‖ ^ 2) + C.value y +
      ((5 : ℝ) / 4 * ⟪a, z + a⟫_ℝ - 10 * ‖z + a‖ ^ 2)) ≤ coulombCost (x, (y, z)) ∧
    (ENNReal.ofReal (((5 : ℝ) / 2 - 10 * ‖x‖ ^ 2) + C.value y +
      ((5 : ℝ) / 4 * ⟪a, z + a⟫_ℝ - 10 * ‖z + a‖ ^ 2)) = coulombCost (x, (y, z)) ↔
      x = C.charts.central y ∧ z = C.charts.opposite y) := by
…

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

def OAI.Problem356.FiveComponentGeometry.branchContact line 152
Source documentation
Symmetric union of the two actual local branch graphs. The parameter remains in the corresponding chart source.
```
def branchContact (C₁ : ChartsAt (point 1)) (C₂ : ChartsAt (point 3)) (t : Triple) : Prop :=
…
```
Mentions: OAI.Problem356.FiveComponentGeometry.ChartsAt, OAI.Problem356.Triple
lemma OAI.Problem356.FiveComponentGeometry.branchContact_perm line 158