OAI/Analysis/CoulombIonization/FieldAnalysis/RadialPower.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombPDE.second_deriv_nonpos_of_localMax line 28
  2. lemma OAI.CoulombPDE.second_deriv_line line 42
  3. lemma OAI.CoulombPDE.second_fderiv_nonpos_of_localMax line 62
  4. lemma OAI.CoulombPDE.laplacian_nonpos_of_localMax line 75
  5. lemma OAI.CoulombPDE.laplacian_norm_sq line 83
  6. theorem OAI.CoulombPDE.compact_maximum_principle line 93
  7. theorem OAI.CoulombPDE.semilinear_comparison line 139
  8. lemma OAI.CoulombPDE.differentiableAt_deriv_of_contDiffAt line 156
  9. lemma OAI.CoulombPDE.second_deriv_norm_sq_comp line 163
  10. lemma OAI.CoulombPDE.laplacian_norm_sq_comp line 197
  11. def OAI.CoulombPDE.radialPower line 211
  12. lemma OAI.CoulombPDE.radialPower_contDiffAt line 214
  13. lemma OAI.CoulombPDE.laplacian_radialPower line 218
  14. theorem OAI.CoulombPDE.annular_maximum_principle line 243
  15. theorem OAI.CoulombPDE.punctured_ball_maximum_principle line 275
  16. lemma OAI.CoulombPDE.radialPower_add line 291
  17. lemma OAI.CoulombPDE.radialPower_pos line 296
  18. lemma OAI.CoulombPDE.radialPower_rpow line 300
  19. lemma OAI.CoulombPDE.radialPower_nonneg line 305
  20. lemma OAI.CoulombPDE.exists_small_rpow_bound line 308
  21. lemma OAI.CoulombPDE.exists_small_radialPower_bound line 319
  22. lemma OAI.CoulombPDE.exists_small_exponent line 329
  23. lemma OAI.CoulombPDE.rpow_three_halves line 338
  24. lemma OAI.CoulombPDE.rpow_three_halves_lower line 343
  25. lemma OAI.CoulombPDE.rpow_three_halves_upper line 349
  26. abbrev OAI.CoulombPDE.Space line 355
  27. lemma OAI.CoulombPDE.radial_laplacian_three line 357
  28. def OAI.CoulombPDE.radialCombination line 366
  29. lemma OAI.CoulombPDE.radialCombination_contDiffAt line 369
  30. lemma OAI.CoulombPDE.radialCombination_laplacian line 374
  31. def OAI.CoulombPDE.reaction line 393
  32. lemma OAI.CoulombPDE.reaction_monotone line 395
  33. lemma OAI.CoulombPDE.radialCombination_factor line 400
  34. lemma OAI.CoulombPDE.radial_scaled_reaction line 406
  35. lemma OAI.CoulombPDE.upper_barrier_laplacian line 411