OAI/Analysis/HenonEmden/InteractionBounds.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.HenonLaneEmden.integrable_integral_le_of_lintegral_leline 15 - lemma
OAI.HenonLaneEmden.IsSolution.lintegral_weight_leftline 24 - lemma
OAI.HenonLaneEmden.IsSolution.lintegral_weight_rightline 36 - lemma
OAI.HenonLaneEmden.IsSolution.weight_leftline 48 - lemma
OAI.HenonLaneEmden.IsSolution.weight_rightline 59 - lemma
OAI.HenonLaneEmden.IsSolution.farWeight_boundline 70 - lemma
OAI.HenonLaneEmden.IsSolution.farWeight_swap_boundline 78 - lemma
OAI.HenonLaneEmden.cutoff_far_exponentsline 90