OAI/Analysis/HenonEmden/WeakForm.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HenonLaneEmden.WeakPDE.integrable_mul_compact line 17
  2. def OAI.HenonLaneEmden.WeakPDE.dir line 26
  3. lemma OAI.HenonLaneEmden.WeakPDE.tsupport_dir_subset line 29
  4. lemma OAI.HenonLaneEmden.WeakPDE.compactSupport_dir line 33
  5. lemma OAI.HenonLaneEmden.WeakPDE.contDiffOn_dir line 37
  6. lemma OAI.HenonLaneEmden.WeakPDE.differentiableAt_dir line 43
  7. lemma OAI.HenonLaneEmden.WeakPDE.dir_dir line 50
  8. lemma OAI.HenonLaneEmden.WeakPDE.integral_laplacian_test line 61
  9. lemma OAI.HenonLaneEmden.WeakPDE.ibp_compact_on line 128
  10. lemma OAI.HenonLaneEmden.WeakPDE.weighted_second_ibp line 141
  11. lemma OAI.HenonLaneEmden.WeakPDE.radial_ode_of_weak line 194
  12. lemma OAI.HenonLaneEmden.WeakPDE.continuousOn_laplacian line 232
  13. lemma OAI.HenonLaneEmden.WeakPDE.laplacian_zero_of_notMem_tsupport line 246
  14. lemma OAI.HenonLaneEmden.WeakPDE.tsupport_laplacian_subset line 252
  15. lemma OAI.HenonLaneEmden.WeakPDE.compactSupport_laplacian line 258
  16. lemma OAI.HenonLaneEmden.WeakPDE.continuous_laplacian line 262