OAI/Analysis/HenonEmden/Interaction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HenonLaneEmden.newtonKernel line 14

    Source documentation

    The Newton kernel, including its harmless diagonal convention.

    def newtonKernel (n : ℕ) (z : Space n × Space n) : ℝ :=
…

    Mentions: OAI.HenonLaneEmden.Space

  2. lemma OAI.HenonLaneEmden.measurable_newtonKernel line 17
  3. lemma OAI.HenonLaneEmden.newtonKernel_symm line 19
  4. lemma OAI.HenonLaneEmden.newtonKernel_nonneg line 22
  5. lemma OAI.HenonLaneEmden.IsSolution.newton_potential_u line 26
  6. lemma OAI.HenonLaneEmden.IsSolution.newton_potential_u_ae line 51
  7. def OAI.HenonLaneEmden.interaction line 59
  8. instance OAI.HenonLaneEmden.interaction_sigmaFinite line 63
  9. lemma OAI.HenonLaneEmden.lintegral_interaction line 69
  10. lemma OAI.HenonLaneEmden.lintegral_interaction_left line 76
  11. lemma OAI.HenonLaneEmden.lintegral_interaction_right line 90
  12. lemma OAI.HenonLaneEmden.IsSolution.interaction_left line 105
  13. lemma OAI.HenonLaneEmden.IsSolution.interaction_right line 116