GluedCertificate.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem356.componentContact line 16

Source documentation

A contact triple on a finite union, with its ordered component labels.

def componentContact {ι : Type uIndex} (U : ι → Set E3)
    (Good : (ι × (ι × ι)) → Prop)
    (Contact : (ι × (ι × ι)) → Triple → Prop) (t : Triple) : Prop :=
…

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

theorem OAI.Problem356.exists_glued_component_certificate line 25

Source documentation

Local good-type certificates and strict bad-center gaps produce an actual bounded, measurable supporting potential on disjoint small component balls, with the precise union of the prescribed contact sets.

theorem exists_glued_component_certificate {ι : 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 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)) <
…

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