OAI/Analysis/HenonEmden/NearLocalization.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HenonLaneEmden.measurable_radialFactor line 15
  2. lemma OAI.HenonLaneEmden.measurable_fluxFactor line 17
  3. lemma OAI.HenonLaneEmden.eta_nonneg line 22
  4. lemma OAI.HenonLaneEmden.eta_gap_bounds line 25
  5. def OAI.HenonLaneEmden.pairGap line 28
  6. def OAI.HenonLaneEmden.localError line 29
  7. def OAI.HenonLaneEmden.closeConstant line 31
  8. lemma OAI.HenonLaneEmden.pairGap_bounds line 33
  9. lemma OAI.HenonLaneEmden.pairGap_power_le line 35
  10. lemma OAI.HenonLaneEmden.close_pair_gaps line 43
  11. lemma OAI.HenonLaneEmden.close_power_bound line 63
  12. lemma OAI.HenonLaneEmden.flux_close_estimate line 77
  13. lemma OAI.HenonLaneEmden.localError_close line 107