OAI/Analysis/CoulombTransport/RealCounterexampleAssembly.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem356.coulombCost_pos_realAssembly line 13
2. lemma OAI.Problem356.triplePotential_shifted_contact_iff line 22

   Source documentation

   For the strictly positive Coulomb cost, the shifted and signed contact conditions are equivalent; no nonnegativity assumption on the signed sum is needed.

   lemma triplePotential_shifted_contact_iff {u : E3 → ℝ} {M : ℝ} {t : Triple}
       (hM : 0 ≤ M)
       (h1 : -M ≤ u (tripleFst t)) (h2 : -M ≤ u (tripleSnd t))
       (h3 : -M ≤ u (tripleThd t)) :
       (triplePotential (shiftedPotential u M) t =
         coulombCost t + ENNReal.ofReal (3 * M)) ↔
       ENNReal.ofReal (u (tripleFst t) + u (tripleSnd t) + u (tripleThd t)) =
         coulombCost t :=
   …

   Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.tripleFst, OAI.Problem356.tripleSnd, OAI.Problem356.tripleThd, OAI.Problem356.triplePotential, OAI.Problem356.shiftedPotential, OAI.Problem356.coulombCost

3. theorem OAI.Problem356.hasCoulombCounterexample_of_real_branches line 32