OAI/Analysis/HenonEmden/Gradients.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HenonLaneEmden.WeakPDE.kernelDir line 17
2. lemma OAI.HenonLaneEmden.WeakPDE.hasFDerivAt_kernel line 21
3. lemma OAI.HenonLaneEmden.WeakPDE.dir_kernel line 36
4. lemma OAI.HenonLaneEmden.WeakPDE.kernelDir_bound line 42
5. lemma OAI.HenonLaneEmden.WeakPDE.measurable_kernelDir line 60
6. lemma OAI.HenonLaneEmden.WeakPDE.locallyIntegrable_kernelDir line 63
7. lemma OAI.HenonLaneEmden.WeakPDE.integral_kernel_dir_off_zero line 72
8. lemma OAI.HenonLaneEmden.WeakPDE.kernel_cutoff_derivative_tendsto_zero line 100
9. lemma OAI.HenonLaneEmden.WeakPDE.kernel_dir_cutoff_tendsto_zero line 164
10. lemma OAI.HenonLaneEmden.WeakPDE.integral_kernel_dir line 191
11. lemma OAI.HenonLaneEmden.WeakPDE.kernelDir_shift_bound line 237
12. lemma OAI.HenonLaneEmden.WeakPDE.hasLineDerivAt_far_rawPotential line 263
13. lemma OAI.HenonLaneEmden.WeakPDE.contDiff_mul_cutoff line 319
14. lemma OAI.HenonLaneEmden.WeakPDE.rawPotential_eq_convolve line 331
15. lemma OAI.HenonLaneEmden.WeakPDE.integrable_kernelDir_local line 337
16. lemma OAI.HenonLaneEmden.WeakPDE.dir_rawPotential_local line 346
17. lemma OAI.HenonLaneEmden.WeakPDE.hasLineDerivAt_rawPotential_local line 366
18. lemma OAI.HenonLaneEmden.WeakPDE.hasLineDerivAt_rawPotential line 380
19. lemma OAI.HenonLaneEmden.IsSolution.gradient_u line 432