OAI/Analysis/HenonEmden/LocalizationIntegral.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HenonLaneEmden.measurable_localError line 13
  2. lemma OAI.HenonLaneEmden.localError_nonneg line 18
  3. lemma OAI.HenonLaneEmden.closeConstant_nonneg line 19
  4. lemma OAI.HenonLaneEmden.farLocalConstant_nonneg line 22
  5. def OAI.HenonLaneEmden.localFarSum line 26
  6. lemma OAI.HenonLaneEmden.localFarSum_nonneg line 29
  7. lemma OAI.HenonLaneEmden.localError_global line 33
  8. def OAI.HenonLaneEmden.localizationConstant line 43
  9. lemma OAI.HenonLaneEmden.localizationConstant_nonneg line 45
  10. lemma OAI.HenonLaneEmden.IsSolution.localFarSum_bound line 51
  11. lemma OAI.HenonLaneEmden.IsSolution.localError_bound line 72