OAI/Geometry/Cannon/Conformal/CutoffBump.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonMetricQC.cutoffBump line 28
  2. def OAI.CannonMetricQC.smoothCutoff line 34
  3. lemma OAI.CannonMetricQC.smoothCutoff_smooth line 36
  4. lemma OAI.CannonMetricQC.smoothCutoff_support line 39
  5. lemma OAI.CannonMetricQC.smoothCutoff_lipschitz line 42
  6. lemma OAI.CannonMetricQC.smoothCutoff_bound line 46
  7. lemma OAI.CannonMetricQC.smoothCutoff_zero line 50
  8. lemma OAI.CannonMetricQC.smoothCutoff_one line 54
  9. lemma OAI.CannonMetricQC.exists_smooth_cutoff line 63
  10. lemma OAI.CannonMetricQC.cutoff_fderiv_eq line 72
  11. theorem OAI.CannonMetricQC.weakQS_local_weakW12 line 82
  12. lemma OAI.CannonMetricQC.norm_integral_sq_le line 124
  13. theorem OAI.CannonMetricQC.kernel_energy_pointwise line 131
  14. lemma OAI.CannonMetricQC.translated_ball_energy_le line 167
  15. theorem OAI.CannonMetricQC.kernel_energy_local line 186
  16. lemma OAI.CannonMetricQC.convolution_directional line 223
  17. lemma OAI.CannonMetricQC.fderiv_reflect line 238
  18. theorem OAI.CannonMetricQC.weak_derivative_convolution line 245
  19. def OAI.CannonMetricQC.mollifier line 270
  20. def OAI.CannonMetricQC.mollify line 276
  21. lemma OAI.CannonMetricQC.mollify_smooth line 279
  22. lemma OAI.CannonMetricQC.mollify_eq_complex_convolution line 284
  23. lemma OAI.CannonMetricQC.mollifier_radius_tendsto line 292
  24. lemma OAI.CannonMetricQC.mollify_locally_uniform line 296
  25. lemma OAI.CannonMetricQC.plane_opNorm_le line 309
  26. lemma OAI.CannonMetricQC.plane_opNorm_sq line 323
  27. lemma OAI.CannonMetricQC.mollify_directional line 328
  28. lemma OAI.CannonMetricQC.mollify_energy_local line 337
  29. theorem OAI.CannonMetricQC.mollify_opNorm_energy line 350