OAI/Analysis/HenonEmden/UniformBounds.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HenonLaneEmden.UniformTail.shifted_rpow_le line 16
  2. lemma OAI.HenonLaneEmden.UniformTail.uniform_shifted_tail line 30
  3. def OAI.HenonLaneEmden.UniformTail.tailNumber line 53
  4. lemma OAI.HenonLaneEmden.UniformTail.tailNumber_nonneg line 56
  5. lemma OAI.HenonLaneEmden.UniformTail.truncated_potential_bound line 63
  6. lemma OAI.HenonLaneEmden.UniformTail.local_kernel_mass_le line 103
  7. lemma OAI.HenonLaneEmden.UniformTail.local_potential_bound line 120
  8. def OAI.HenonLaneEmden.sourceMeasure line 157
  9. lemma OAI.HenonLaneEmden.IsSolution.sourceMeasure_ball line 160
  10. lemma OAI.HenonLaneEmden.IsSolution.uniform_source_tail_g line 169
  11. instance OAI.HenonLaneEmden.sourceMeasure_sigmaFinite line 187
  12. lemma OAI.HenonLaneEmden.lintegral_sourceMeasure line 190
  13. lemma OAI.HenonLaneEmden.IsSolution.sourceMeasure_potential_u_ae line 195
  14. def OAI.HenonLaneEmden.kernelMass line 211
  15. lemma OAI.HenonLaneEmden.kernelMass_nonneg line 214
  16. lemma OAI.HenonLaneEmden.lintegral_kernelMass line 217
  17. def OAI.HenonLaneEmden.uniformTailConstant line 226
  18. def OAI.HenonLaneEmden.uniformMassConstant line 229
  19. lemma OAI.HenonLaneEmden.IsSolution.uniform_u_mass line 233
  20. lemma OAI.HenonLaneEmden.IsSolution.uniform_g_truncated line 269