OAI/Analysis/CoulombTransport/CoulombCalculus.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem356.CoulombCalculus.pairCost line 16

    Source documentation

    The real-valued radial Coulomb interaction, used only away from the origin.

    def pairCost (x : E) : ℝ := ‖x‖⁻¹
  2. def OAI.Problem356.CoulombCalculus.pairGradient line 19

    Source documentation

    The gradient of the real radial Coulomb interaction.

    def pairGradient (x : E) : E := -(‖x‖ ^ 3)⁻¹ • x
  3. lemma OAI.Problem356.CoulombCalculus.hasFDerivAt_norm_explicit line 21
  4. lemma OAI.Problem356.CoulombCalculus.hasFDerivAt_pairCost line 34
  5. lemma OAI.Problem356.CoulombCalculus.contDiffAt_pairCost line 43
  6. def OAI.Problem356.CoulombCalculus.pairHessian line 48

    Source documentation

    The Hessian of the real radial Coulomb interaction.

    def pairHessian (x : E) : E →L[ℝ] E :=
…
  7. lemma OAI.Problem356.CoulombCalculus.hasFDerivAt_radialFactor line 52
  8. lemma OAI.Problem356.CoulombCalculus.hasFDerivAt_pairGradient line 65
  9. lemma OAI.Problem356.CoulombCalculus.contDiffAt_pairGradient line 72
  10. lemma OAI.Problem356.CoulombCalculus.pairCost_neg line 78
  11. lemma OAI.Problem356.CoulombCalculus.pairGradient_neg line 81
  12. lemma OAI.Problem356.CoulombCalculus.pairHessian_neg line 84
  13. lemma OAI.Problem356.CoulombCalculus.pairHessian_apply line 88
  14. lemma OAI.Problem356.CoulombCalculus.pairHessian_apply_self line 93
  15. lemma OAI.Problem356.CoulombCalculus.pairHessian_apply_orthogonal line 101
  16. lemma OAI.Problem356.CoulombCalculus.pairHessian_symmetric line 105
  17. lemma OAI.Problem356.CoulombCalculus.pairHessian_smul_pos line 112
  18. lemma OAI.Problem356.CoulombCalculus.pairHessian_apply_of_norm_eq_one line 119
  19. lemma OAI.Problem356.CoulombCalculus.pairHessian_injective line 123
  20. lemma OAI.Problem356.CoulombCalculus.pairHessian_isInvertible line 135
  21. lemma OAI.Problem356.CoulombCalculus.fderiv_pairCost line 143
  22. lemma OAI.Problem356.CoulombCalculus.hasFDerivAt_fderiv_pairCost line 148
  23. lemma OAI.Problem356.CoulombCalculus.secondFDeriv_pairCost_apply line 156
  24. lemma OAI.Problem356.CoulombCalculus.pairHessian_quadratic_lower line 161