OAI/Analysis/HenonEmden/FarInteraction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HenonLaneEmden.farWeight line 13
2. lemma OAI.HenonLaneEmden.measurable_farWeight line 16
3. lemma OAI.HenonLaneEmden.farWeight_nonneg line 24
4. lemma OAI.HenonLaneEmden.far_power_bound line 29
5. lemma OAI.HenonLaneEmden.IsSolution.truncated_newton_bound line 36
6. def OAI.HenonLaneEmden.truncatedConstant line 57
7. def OAI.HenonLaneEmden.farConstant line 61
8. lemma OAI.HenonLaneEmden.truncatedConstant_nonneg line 65
9. lemma OAI.HenonLaneEmden.farConstant_nonneg line 66
10. lemma OAI.HenonLaneEmden.IsSolution.far_inner_bound line 70
11. lemma OAI.HenonLaneEmden.IsSolution.far_interaction_bound line 109
12. lemma OAI.HenonLaneEmden.lintegral_interaction_swap line 137