OAI/Analysis/NodalLength/LogGradients.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpNodal.Profiles.logGradient line 167
  2. lemma OAI.SharpNodal.Profiles.norm_logGradient line 169
  3. lemma OAI.SharpNodal.Profiles.measurable_logGradient line 176
  4. lemma OAI.SharpNodal.Profiles.inv_norm_integrableOn_ball line 179
  5. lemma OAI.SharpNodal.Profiles.inverse_translate_local line 187
  6. lemma OAI.SharpNodal.Profiles.inversePotential_prod_integrable line 208
  7. lemma OAI.SharpNodal.Profiles.logGradientPotential_prod_integrable line 224
  8. def OAI.SharpNodal.Profiles.aeLogGradient line 232
  9. lemma OAI.SharpNodal.Profiles.aeLogGradient_integrableOn line 234
  10. lemma OAI.SharpNodal.Profiles.ae_inverse_kernel_integrable line 238
  11. lemma OAI.SharpNodal.Profiles.truncated_gradient_dominating line 254
  12. lemma OAI.SharpNodal.Profiles.tendsto_truncated_kernels line 292
  13. theorem OAI.SharpNodal.Profiles.truncated_potential_limits line 317
  14. lemma OAI.SharpNodal.Profiles.partial_regularizedLog_bound line 347
  15. lemma OAI.SharpNodal.Profiles.partial_regularizedLog_tendsto line 359
  16. lemma OAI.SharpNodal.Profiles.partial_regularizedLog_test_limit line 372
  17. lemma OAI.SharpNodal.Profiles.logarithmic_gradient_distribution line 404
  18. lemma OAI.SharpNodal.Profiles.logarithmic_gradient_distribution_translate line 423
  19. lemma OAI.SharpNodal.Profiles.aeLogGradient_component_test_swap line 433
  20. lemma OAI.SharpNodal.Profiles.aeLogPotential_gradient_distribution line 470
  21. def OAI.SharpNodal.Profiles.WeakGradientZeroOn line 486
  22. lemma OAI.SharpNodal.Profiles.weakGradient_rconv_partial line 490
  23. lemma OAI.SharpNodal.Profiles.weakGradient_rconv_constant line 519
  24. def OAI.SharpNodal.Profiles.gradientBump line 534
  25. lemma OAI.SharpNodal.Profiles.gradientBump_tendsto line 539
  26. lemma OAI.SharpNodal.Profiles.rconv_normed_eq line 542
  27. lemma OAI.SharpNodal.Profiles.ae_gradientBump_converges line 550
  28. theorem OAI.SharpNodal.Profiles.weakGradient_constant_ae line 562
  29. lemma OAI.SharpNodal.Profiles.aeLogPotential_locallyIntegrable line 589
  30. lemma OAI.SharpNodal.Profiles.aeLogGradient_locallyIntegrable line 595
  31. lemma OAI.SharpNodal.Profiles.potential_sum_gradient_distribution line 601
  32. lemma OAI.SharpNodal.Profiles.potential_zeroGradient_weak line 619
  33. lemma OAI.SharpNodal.Profiles.profile_eq_constant_of_ae line 647
  34. theorem OAI.SharpNodal.Profiles.profile_nonzero_gradient line 665