GoodTypePermutation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem356.GoodTypePermutation.LocalTypeCertificate line 13
Source documentation
A supporting certificate on an ordered component product, with the one-way contact localization needed for excluding deterministic optimizers.
```
def LocalTypeCertificate (U : Fin 5 → Set E3) (v : Fin 5 → E3 → ℝ)
    (Contact : Triple → Prop) (i j k : Fin 5) : Prop :=
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.Triple

theorem OAI.Problem356.GoodTypePermutation.LocalTypeCertificate.swap_first line 24

Source documentation

Contact localization is transported along a swap of the first two entries.

theorem LocalTypeCertificate.swap_first {i j k : Fin 5}
    (h : LocalTypeCertificate U v Contact i j k)
    (hperm : ∀ {x y z a b c : E3}, List.Perm [x, y, z] [a, b, c] →
      Contact (x, (y, z)) → Contact (a, (b, c))) :
    LocalTypeCertificate U v Contact j i k := by
…

Mentions: OAI.Problem356.GoodTypePermutation.LocalTypeCertificate, OAI.Problem356.E3

theorem OAI.Problem356.GoodTypePermutation.LocalTypeCertificate.swap_last line 35

Source documentation

Contact localization is transported along a swap of the last two entries.

theorem LocalTypeCertificate.swap_last {i j k : Fin 5}
    (h : LocalTypeCertificate U v Contact i j k)
    (hperm : ∀ {x y z a b c : E3}, List.Perm [x, y, z] [a, b, c] →
      Contact (x, (y, z)) → Contact (a, (b, c))) :
    LocalTypeCertificate U v Contact i k j := by
…

Mentions: OAI.Problem356.GoodTypePermutation.LocalTypeCertificate, OAI.Problem356.E3

theorem OAI.Problem356.GoodTypePermutation.certificate_of_good line 48

Source documentation

The two canonical component orders supply every good component type. No converse from the abstract contact predicate to equality is assumed.

theorem certificate_of_good
    (hperm : ∀ {x y z a b c : E3}, List.Perm [x, y, z] [a, b, c] →
      Contact (x, (y, z)) → Contact (a, (b, c)))
    (h012 : LocalTypeCertificate U v Contact 0 1 2)
    (h034 : LocalTypeCertificate U v Contact 0 3 4)
    (i j k : Fin 5) (hgood : CenterCertificate.Good i j k) :
    LocalTypeCertificate U v Contact i j k := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.GoodTypePermutation.LocalTypeCertificate, OAI.Problem356.CenterCertificate.Good

theorem OAI.Problem356.GoodTypePermutation.eventually_certificate_of_good line 69

Source documentation

Neighborhood form directly usable by a finite component gluing argument.

theorem eventually_certificate_of_good
    (p : Fin 5 → E3) (hU : ∀ i, U i ∈ nhds (p i))
    (hperm : ∀ {x y z a b c : E3}, List.Perm [x, y, z] [a, b, c] →
      Contact (x, (y, z)) → Contact (a, (b, c)))
    (h012 : LocalTypeCertificate U v Contact 0 1 2)
    (h034 : LocalTypeCertificate U v Contact 0 3 4)
    (i j k : Fin 5) (hgood : CenterCertificate.Good i j k) :
    ∀ᶠ t : Triple in nhds (p i, (p j, p k)),
      ENNReal.ofReal (v i t.1 + v j t.2.1 + v k t.2.2) ≤ coulombCost t ∧
      (ENNReal.ofReal (v i t.1 + v j t.2.1 + v k t.2.2) = coulombCost t →
        Contact t) := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.GoodTypePermutation.LocalTypeCertificate, OAI.Problem356.CenterCertificate.Good, OAI.Problem356.Triple, OAI.Problem356.coulombCost