OAI/Analysis/PlanarEndpoint/Heat.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. lemma OAI.PlanarEndpoint.gaussianWeight_superlevel line 14
  2. lemma OAI.PlanarEndpoint.gaussianWeight_superlevel_empty line 23
  3. lemma OAI.PlanarEndpoint.lintegral_gaussianWeight_le_of_ball line 29
  4. def OAI.PlanarEndpoint.heatKernel line 50
  5. lemma OAI.PlanarEndpoint.heatKernel_nonneg line 53
  6. lemma OAI.PlanarEndpoint.integral_gaussianWeight line 57
  7. lemma OAI.PlanarEndpoint.integral_heatKernel line 62
  8. lemma OAI.PlanarEndpoint.integrable_gaussianWeight line 67
  9. lemma OAI.PlanarEndpoint.continuous_heatKernel line 73
  10. lemma OAI.PlanarEndpoint.integrable_heatKernel line 77
  11. lemma OAI.PlanarEndpoint.lintegral_heatKernel line 82
  12. lemma OAI.PlanarEndpoint.lintegral_heatKernel_le_of_ball line 88
  13. lemma OAI.PlanarEndpoint.heat_mul_le_of_ball line 108
  14. lemma OAI.PlanarEndpoint.cutoff_ball_mass line 142
  15. lemma OAI.PlanarEndpoint.heat_mul_cutoff_le line 171
  16. def OAI.PlanarEndpoint.heatTailCoefficient line 183
  17. lemma OAI.PlanarEndpoint.heatTailCoefficient_nonneg line 186
  18. lemma OAI.PlanarEndpoint.heatKernel_le_tail line 191
  19. lemma OAI.PlanarEndpoint.heatTailCoefficient_tendsto line 210
  20. lemma OAI.PlanarEndpoint.heat_mul_tail_bound line 227
  21. lemma OAI.PlanarEndpoint.tendsto_heat_mul_tail line 258
  22. lemma OAI.PlanarEndpoint.heat_mul_cutoff_eq line 276
  23. lemma OAI.PlanarEndpoint.tendsto_heat_mul_zero_of_small_balls line 282
  24. lemma OAI.PlanarEndpoint.small_ball_mass_of_tendsto_average line 318
  25. lemma OAI.PlanarEndpoint.tendsto_heat_mul_zero_of_lebesgue line 349
  26. lemma OAI.PlanarEndpoint.gaussianWeight_lower_on_unit_ball line 359
  27. lemma OAI.PlanarEndpoint.gaussianWeight_lintegral_unit_ball_lower line 376
  28. lemma OAI.PlanarEndpoint.lintegral_gaussian_mul_lt_top_of_unit_ball_mass line 391
  29. lemma OAI.PlanarEndpoint.integrable_gaussian_mul_of_unit_ball_mass line 442
  30. lemma OAI.PlanarEndpoint.reflect_preimage_ball line 458
  31. lemma OAI.PlanarEndpoint.locallyIntegrable_reflect line 465
  32. lemma OAI.PlanarEndpoint.integral_reflect_ball line 477
  33. lemma OAI.PlanarEndpoint.integrable_heat_mul_of_unit_ball_mass line 484
  34. lemma OAI.PlanarEndpoint.heat_envelope line 492