ComponentCertificate.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.finite_bad_component_neighborhoods line 18

Source documentation

Every bad center type with a strict extended-valued cost gap retains that gap on small component balls. The finite index set may include repeated-center types, since extended-valued Coulomb cost is continuous at collisions.

theorem finite_bad_component_neighborhoods {ι : Type uIndex}
    (s : Finset (ι × (ι × ι))) (p : ι → E3) (v : ι → E3 → ℝ)
    (hv : ∀ i, ContinuousAt (v i) (p i))
    (hgap : ∀ a ∈ s,
      ENNReal.ofReal (v a.1 (p a.1) + v a.2.1 (p a.2.1) + v a.2.2 (p a.2.2)) <
        coulombCost (p a.1, (p a.2.1, p a.2.2))) :
    ∃ r : ℝ, 0 < r ∧ ∀ a ∈ s, ∀ x y z : E3,
      x ∈ ball (p a.1) r → y ∈ ball (p a.2.1) r → z ∈ ball (p a.2.2) r →
      ENNReal.ofReal (v a.1 x + v a.2.1 y + v a.2.2 z) <
        coulombCost (x, (y, z)) := by
…

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

theorem OAI.Problem356.continuousAt_component_sum line 50

Source documentation

Continuity of the sum of the three local potentials in one component type.

theorem continuousAt_component_sum {ι : Type uIndex} (p : ι → E3) (v : ι → E3 → ℝ)
    (hv : ∀ i, ContinuousAt (v i) (p i)) (a : ι × (ι × ι)) :
    ContinuousAt
      (fun t : Triple => ENNReal.ofReal (v a.1 t.1 + v a.2.1 t.2.1 + v a.2.2 t.2.2))
      (p a.1, (p a.2.1, p a.2.2)) := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.Triple

theorem OAI.Problem356.finite_component_certificate line 72

Source documentation

The local-to-global finite-type certificate step. Local supporting inequalities and exact contact sets are needed only at the good types; strict gaps at every other center type are enough for all remaining types. A single radius works for the inequalities and exact equality characterization.

theorem finite_component_certificate {ι : Type uIndex} [Fintype ι]
    (p : ι → E3) (v : ι → E3 → ℝ)
    (Good : (ι × (ι × ι)) → Prop)
    (Contact : (ι × (ι × ι)) → Triple → Prop)
    (hv : ∀ i, ContinuousAt (v i) (p i))
    (hgood : ∀ a, Good a → ∀ᶠ t in nhds (p a.1, (p a.2.1, p a.2.2)),
      ENNReal.ofReal (v a.1 t.1 + v a.2.1 t.2.1 + v a.2.2 t.2.2) ≤ coulombCost t ∧
      (ENNReal.ofReal (v a.1 t.1 + v a.2.1 t.2.1 + v a.2.2 t.2.2) =
        coulombCost t ↔ Contact a t))
    (hbad : ∀ a, ¬ Good a →
      ENNReal.ofReal (v a.1 (p a.1) + v a.2.1 (p a.2.1) + v a.2.2 (p a.2.2)) <
        coulombCost (p a.1, (p a.2.1, p a.2.2))) :
…

Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.coulombCost

theorem OAI.Problem356.componentPotential_supporting_inequality line 109

Source documentation

Once all ordered component types have been certified, the glued potential satisfies the supporting inequality on the entire component union.

theorem componentPotential_supporting_inequality {ι : Type uIndex} [Fintype ι]
    (U : ι → Set E3) (v : ι → E3 → ℝ)
    (hdisj : Pairwise (fun i j => Disjoint (U i) (U j)))
    (hlocal : ∀ i j k, ∀ x ∈ U i, ∀ y ∈ U j, ∀ z ∈ U k,
      ENNReal.ofReal (v i x + v j y + v k z) ≤ coulombCost (x, (y, z)))
    {x y z : E3} (hx : x ∈ ⋃ i, U i) (hy : y ∈ ⋃ i, U i)
    (hz : z ∈ ⋃ i, U i) :
    ENNReal.ofReal (ComponentPotential.glue U v x + ComponentPotential.glue U v y +
      ComponentPotential.glue U v z) ≤ coulombCost (x, (y, z)) := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.coulombCost, OAI.Problem356.ComponentPotential.glue

theorem OAI.Problem356.componentPotential_contact_good line 127

Source documentation

Strict inequalities on bad ordered component types exclude those types from the contact set of the glued potential.

theorem componentPotential_contact_good {ι : Type uIndex} [Fintype ι]
    (U : ι → Set E3) (v : ι → E3 → ℝ)
    (hdisj : Pairwise (fun i j => Disjoint (U i) (U j)))
    (Good : ι → ι → ι → Prop)
    (hbad : ∀ i j k, ¬ Good i j k → ∀ x ∈ U i, ∀ y ∈ U j, ∀ z ∈ U k,
      ENNReal.ofReal (v i x + v j y + v k z) < coulombCost (x, (y, z)))
    {i j k : ι} {x y z : E3} (hx : x ∈ U i) (hy : y ∈ U j) (hz : z ∈ U k)
    (hcontact : ENNReal.ofReal (ComponentPotential.glue U v x + ComponentPotential.glue U v y +
      ComponentPotential.glue U v z) = coulombCost (x, (y, z))) : Good i j k := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.coulombCost, OAI.Problem356.ComponentPotential.glue