OAI/Analysis/IntegralMeans/SmoothMeans.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Brennan.logDisk line 10
  2. lemma OAI.Brennan.logDisk_norm line 12
  3. lemma OAI.Brennan.logDisk_mem_disk line 15
  4. lemma OAI.Brennan.logDisk_analytic line 19
  5. lemma OAI.Brennan.logDisk_injOn line 22
  6. lemma OAI.Brennan.logDisk_realProd line 31
  7. lemma OAI.Brennan.logDisk_periodic line 38
  8. lemma OAI.Brennan.logStrip_smooth_periodic_side line 41
  9. lemma OAI.Brennan.exp_boundary_lower line 60
  10. lemma OAI.Brennan.logStrip_height_bound line 73
  11. def OAI.Brennan.bracketSq line 120
  12. def OAI.Brennan.smoothPower line 122
  13. lemma OAI.Brennan.bracketSq_eq line 124
  14. lemma OAI.Brennan.bracketSq_pos line 128
  15. lemma OAI.Brennan.bracketSq_contDiff line 130
  16. lemma OAI.Brennan.smoothPower_contDiff line 133
  17. def OAI.Brennan.bracketSqDeriv line 136
  18. lemma OAI.Brennan.bracketSq_hasFDerivAt line 139
  19. lemma OAI.Brennan.smoothPower_hasFDerivAt line 145
  20. lemma OAI.Brennan.bracketSqDeriv_hasFDerivAt line 149
  21. lemma OAI.Brennan.smoothPower_secondReal line 159
  22. lemma OAI.Brennan.laplacian_smoothPower line 172
  23. lemma OAI.Brennan.laplacian_smoothPower_bounds line 182
  24. lemma OAI.Brennan.bracketSq_decay_integrable line 196
  25. lemma OAI.Brennan.schlicht_smooth_trace line 215
  26. lemma OAI.Brennan.continuous_circle_smoothPower line 255
  27. lemma OAI.Brennan.schlicht_smooth_means line 262