OAI/Analysis/CoulombTransport/TriplePermutation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem356.TriplePermutation.pair_symm line 12
2. lemma OAI.Problem356.TriplePermutation.cost_swap_first line 15
3. lemma OAI.Problem356.TriplePermutation.cost_swap_last line 21
4. lemma OAI.Problem356.TriplePermutation.cost_rotate line 27
5. lemma OAI.Problem356.TriplePermutation.cost_eq_of_same_first line 33
6. lemma OAI.Problem356.TriplePermutation.cost_eq_of_perm line 44

   Source documentation

   The extended Coulomb cost is invariant under every permutation, including triples with coincident points and infinite cost.

   lemma cost_eq_of_perm {x y z a b c : E3}
       (h : List.Perm [x, y, z] [a, b, c]) :
       coulombCost (x, (y, z)) = coulombCost (a, (b, c)) := by
   …

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

7. lemma OAI.Problem356.TriplePermutation.real_sum_eq_of_perm line 61

   Source documentation

   A common signed potential sum is invariant under the same permutation.

   lemma real_sum_eq_of_perm {x y z a b c : E3} (u : E3 → ℝ)
       (h : List.Perm [x, y, z] [a, b, c]) :
       u x + u y + u z = u a + u b + u c := by
   …

   Mentions: OAI.Problem356.E3

8. lemma OAI.Problem356.TriplePermutation.ennreal_sum_eq_of_perm line 69

   Source documentation

   The same invariance is available after shifting to a nonnegative potential.

   lemma ennreal_sum_eq_of_perm {x y z a b c : E3} (u : E3 → ℝ≥0∞)
       (h : List.Perm [x, y, z] [a, b, c]) :
       u x + u y + u z = u a + u b + u c := by
   …

   Mentions: OAI.Problem356.E3

9. lemma OAI.Problem356.TriplePermutation.certificate_iff_of_perm line 77

   Source documentation

   An ordered supporting certificate can be transported to any of its six orders.

   lemma certificate_iff_of_perm {x y z a b c : E3} (u : E3 → ℝ)
       (h : List.Perm [x, y, z] [a, b, c]) :
       (ENNReal.ofReal (u x + u y + u z) ≤ coulombCost (x, (y, z))) ↔
         ENNReal.ofReal (u a + u b + u c) ≤ coulombCost (a, (b, c)) := by
   …

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

10. lemma OAI.Problem356.TriplePermutation.contact_iff_of_perm line 84

    Source documentation

    The equality relation is transported at the same time as the inequality.

    lemma contact_iff_of_perm {x y z a b c : E3} (u : E3 → ℝ)
        (h : List.Perm [x, y, z] [a, b, c]) :
        (ENNReal.ofReal (u x + u y + u z) = coulombCost (x, (y, z))) ↔
          ENNReal.ofReal (u a + u b + u c) = coulombCost (a, (b, c)) := by
    …

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