OAI/Analysis/CoulombTransport/GluedCertificateForward.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem356.exists_glued_component_certificate_forward line 16

   Source documentation

   The finite gluing construction only needs forward contact localization. The explicit contact candidates may be shown saturated separately, so no converse from the chosen global contact predicate is required here.

   theorem exists_glued_component_certificate_forward {ι : Type uIndex} [Fintype ι]
       (p : ι → E3) (hp : Function.Injective p)
       (V : ι → Set E3) (hV : ∀ i, IsOpen (V i)) (hpV : ∀ i, p i ∈ V i)
       (v : ι → E3 → ℝ) (hv : ∀ i, ContinuousOn (v i) (V i))
       (Good : (ι × (ι × ι)) → Prop) (Contact : Triple → Prop)
       (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 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