OAI/Analysis/NodalLength/Potential.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpNodal.Profiles.regularizedLog line 86
  2. def OAI.SharpNodal.Profiles.logDenom line 88
  3. lemma OAI.SharpNodal.Profiles.logDenom_pos line 90
  4. lemma OAI.SharpNodal.Profiles.smooth_logDenom line 94
  5. lemma OAI.SharpNodal.Profiles.partial_logDenom line 97
  6. lemma OAI.SharpNodal.Profiles.smooth_regularizedLog line 105
  7. lemma OAI.SharpNodal.Profiles.partial_regularizedLog line 108
  8. lemma OAI.SharpNodal.Profiles.partial2_regularizedLog line 120
  9. lemma OAI.SharpNodal.Profiles.laplacian_regularizedLog line 137
  10. lemma OAI.SharpNodal.Profiles.integral_mul_laplacian line 147
  11. lemma OAI.SharpNodal.Profiles.regularizedLog_distribution line 162
  12. lemma OAI.SharpNodal.Profiles.plane_radial_ball_integral line 176
  13. lemma OAI.SharpNodal.Profiles.log_norm_integrableOn_ball line 199
  14. lemma OAI.SharpNodal.Profiles.regularizedLog_radial_mass line 210
  15. def OAI.SharpNodal.Profiles.logKernel line 236
  16. lemma OAI.SharpNodal.Profiles.logKernel_nonneg line 238
  17. lemma OAI.SharpNodal.Profiles.logKernel_eq line 242
  18. lemma OAI.SharpNodal.Profiles.continuous_logKernel line 248
  19. lemma OAI.SharpNodal.Profiles.logKernel_uniform_away line 252
  20. lemma OAI.SharpNodal.Profiles.logKernel_mass_tendsto line 273
  21. lemma OAI.SharpNodal.Profiles.logKernel_test_tendsto line 287
  22. lemma OAI.SharpNodal.Profiles.regularizedLog_bound line 305
  23. lemma OAI.SharpNodal.Profiles.regularizedLog_tendsto line 325
  24. lemma OAI.SharpNodal.Profiles.regularizedLog_test_limit line 335
  25. lemma OAI.SharpNodal.Profiles.logarithmic_fundamental_solution line 369
  26. lemma OAI.SharpNodal.Profiles.log_translate_local line 391
  27. def OAI.SharpNodal.Profiles.aeLogPotential line 412
  28. lemma OAI.SharpNodal.Profiles.logPotential_prod_integrable line 414
  29. lemma OAI.SharpNodal.Profiles.aeLogPotential_integrableOn line 429
  30. lemma OAI.SharpNodal.Profiles.partial_translate line 433
  31. lemma OAI.SharpNodal.Profiles.laplacian_translate line 443
  32. lemma OAI.SharpNodal.Profiles.logarithmic_fundamental_solution_translate line 451
  33. lemma OAI.SharpNodal.Profiles.aeLogPotential_norm_bound line 467
  34. lemma OAI.SharpNodal.Profiles.aeLogPotential_test_swap line 482
  35. lemma OAI.SharpNodal.Profiles.aeLogPotential_distribution line 513