OAI/Analysis/HenonEmden/SourceMass.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HenonLaneEmden.IsSolution.rawPotential_lower_u line 29
  2. lemma OAI.HenonLaneEmden.IsSolution.potential_constant_u line 39
  3. lemma OAI.HenonLaneEmden.WeakPDE.rawPotential_ball_lower line 56
  4. lemma OAI.HenonLaneEmden.WeakPDE.ball_integral_dilation line 81
  5. lemma OAI.HenonLaneEmden.WeakPDE.locallyIntegrable_norm_power line 95
  6. lemma OAI.HenonLaneEmden.WeakPDE.integral_weight_ball_scaling line 104
  7. lemma OAI.HenonLaneEmden.WeakPDE.integral_weight_ball_pos line 111
  8. def OAI.HenonLaneEmden.sourceMass line 130
  9. def OAI.HenonLaneEmden.lowerMass line 132
  10. def OAI.HenonLaneEmden.weightMass line 134
  11. def OAI.HenonLaneEmden.ballConstant line 136
  12. lemma OAI.HenonLaneEmden.ballConstant_pos line 138
  13. lemma OAI.HenonLaneEmden.weightMass_pos line 141
  14. lemma OAI.HenonLaneEmden.lowerMass_eq line 148
  15. lemma OAI.HenonLaneEmden.IsSolution.sourceMass_g_pos line 154
  16. lemma OAI.HenonLaneEmden.IsSolution.lowerMass_g_pos line 169
  17. lemma OAI.HenonLaneEmden.IsSolution.lowerMass_g_le line 176
  18. lemma OAI.HenonLaneEmden.integral_source_ge_lower line 188
  19. lemma OAI.HenonLaneEmden.IsSolution.lowerMass_g_coupling line 211