ActualGeometryConclusion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.FiveComponentGeometry.ennreal_graph_contact line 19

theorem OAI.Problem356.FiveComponentGeometry.fullConclusion_of_five_component_certificate line 35

Source documentation

The actual five-component certificate discharges every local-geometry input, after choosing a sufficiently small common central ball.

theorem fullConclusion_of_five_component_certificate
    (C₁ : ChartsAt (point 1)) (C₂ : ChartsAt (point 3))
    (hout₁ : ∀ s ∈ C₁.charts.central.source,
      s ∉ ball (0 : E3) (1 / 4) ∧ C₁.charts.opposite s ∉ ball (0 : E3) (1 / 4))
    (hout₂ : ∀ s ∈ C₂.charts.central.source,
      s ∉ ball (0 : E3) (1 / 4) ∧ C₂.charts.opposite s ∉ ball (0 : E3) (1 / 4))
    {R : ℝ} (hR : 0 < R)
    (hdisj : Pairwise (fun i j : Fin 5 => Disjoint (ball (point i) R) (ball (point j) R)))
    {u : E3 → ℝ} (hu : Measurable u) {M : ℝ} (hM : 0 ≤ M)
    (hubound : ∀ x, |u x| ≤ M)
    (hueq : ∀ i x, x ∈ ball (point i) R → u x = potentials C₁ C₂ i x)
    (hcert : ∀ x ∈ ⋃ i : Fin 5, ball (point i) R,
…

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

theorem OAI.Problem356.FiveComponentGeometry.exists_full_coulomb_conclusion line 188
Source documentation
The unconditional witness: the actual separated local Coulomb charts and their global certificate supply all inputs of the construction.
```
theorem exists_full_coulomb_conclusion :
    ∃ rho : E3 → ℝ, HasFullCoulombConclusion rho := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.HasFullCoulombConclusion