OAI/Analysis/HenonEmden/RadialODE.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HenonLaneEmden.RadialODE.pow_le_self line 23
2. lemma OAI.HenonLaneEmden.RadialODE.sample_flux line 27
3. lemma OAI.HenonLaneEmden.RadialODE.flux_nonpos line 39
4. lemma OAI.HenonLaneEmden.RadialODE.flux_tendsto_zero line 52
5. lemma OAI.HenonLaneEmden.RadialODE.positive_radial_flux_lower line 74
6. lemma OAI.HenonLaneEmden.RadialODE.radial_source_integral_bound line 125
7. lemma OAI.HenonLaneEmden.SphereCalculus.continuous_meanD_global line 155
8. lemma OAI.HenonLaneEmden.SphereCalculus.spherical_source_integral_bound line 164
9. lemma OAI.HenonLaneEmden.SphereCalculus.spherical_source_lintegral_bound line 205
10. lemma OAI.HenonLaneEmden.SphereCalculus.kernel_source_polar line 233
11. lemma OAI.HenonLaneEmden.SphereCalculus.smooth_newton_lower_at_zero line 261