CoulombLocalCertificate.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.LocalGeometry.statePotential_center_value line 19
theorem OAI.Problem356.LocalGeometry.localSupporting_value_center line 28
Source documentation
The branch value vanishes at the center, as required to glue the five local potentials with values 5/2,0,0,0,0.
```
theorem localSupporting_value_center {a : E} (ha : ‖a‖ = 1)
    (C : LocalSupportingCharts (jointPotential a) (stationary a) a (0, -a)) :
    C.value a = 0 := by
…
```
Mentions: OAI.Problem356.LocalGeometry.LocalSupportingCharts

theorem OAI.Problem356.LocalGeometry.local_coulomb_supporting line 36

Source documentation

Restore the central and opposite quadratic potentials in the local supporting inequality. This is the literal three-point Coulomb formula.

theorem local_coulomb_supporting {a : E}
    (C : LocalSupportingCharts (jointPotential a) (stationary a) a (0, -a))
    {x y z : E}
    (hy : y ∈ Metric.ball a C.parameterRadius)
    (hx : x ∈ Metric.ball (0 : E) C.stateRadius)
    (hz : z ∈ Metric.ball (-a) C.stateRadius) :
    ((5 : ℝ) / 2 - 10 * ‖x‖ ^ 2) + C.value y +
        ((5 : ℝ) / 4 * ⟪a, z + a⟫ - 10 * ‖z + a‖ ^ 2) ≤
      ‖x - y‖⁻¹ + ‖x - z‖⁻¹ + ‖y - z‖⁻¹ := by
…

Mentions: OAI.Problem356.LocalGeometry.LocalSupportingCharts

theorem OAI.Problem356.LocalGeometry.local_coulomb_contact line 55

Source documentation

Equality in the supporting inequality is exactly the stationary branch, not merely inclusion of the branch in the contact set.

theorem local_coulomb_contact {a : E}
    (C : LocalSupportingCharts (jointPotential a) (stationary a) a (0, -a))
    {x y z : E}
    (hy : y ∈ Metric.ball a C.parameterRadius)
    (hx : x ∈ Metric.ball (0 : E) C.stateRadius)
    (hz : z ∈ Metric.ball (-a) C.stateRadius) :
    (‖x - y‖⁻¹ + ‖x - z‖⁻¹ + ‖y - z‖⁻¹ =
      ((5 : ℝ) / 2 - 10 * ‖x‖ ^ 2) + C.value y +
        ((5 : ℝ) / 4 * ⟪a, z + a⟫ - 10 * ‖z + a‖ ^ 2)) ↔
      x = C.charts.central y ∧ z = C.charts.opposite y := by
…

Mentions: OAI.Problem356.LocalGeometry.LocalSupportingCharts