OAI/Analysis/Fourier/HeightLayers.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FourierLLogL.Torus line 14
  2. instance OAI.FourierLLogL.circlePeriod_pos line 16

    Also declared: ComparatorChallenges/FourierLLogL.lean:8 (same declaration text).

  3. def OAI.FourierLLogL.circleMeasure line 20
  4. def OAI.FourierLLogL.MemLLogL line 24
  5. def OAI.FourierLLogL.symmetricPartialSum line 30
  6. instance OAI.FourierLLogL.(instance at line 37) line 37
  7. theorem OAI.FourierLLogL.circleMeasure_univ line 41
  8. theorem OAI.FourierLLogL.fourier_of_real line 45
  9. theorem OAI.FourierLLogL.fourierCoeff_eq_integral line 53
  10. theorem OAI.FourierLLogL.fourierCoeff_eq_normalized_intervalIntegral line 59
  11. theorem OAI.FourierLLogL.orliczDensity_nonneg line 73
  12. theorem OAI.FourierLLogL.MemLLogL.integrable line 80
  13. theorem OAI.FourierLLogL.MemLLogL.congr_ae line 91
  14. theorem OAI.FourierLLogL.continuous_symmetricPartialSum line 99
  15. theorem OAI.FourierLLogL.measurable_symmetricPartialSum line 105
  16. theorem OAI.FourierLLogL.symmetricPartialSum_congr_ae line 110
  17. theorem OAI.FourierLLogL.symmetricPartialSum_zero line 116
  18. theorem OAI.FourierLLogL.symmetricPartialSum_cutoff_zero line 121
  19. theorem OAI.FourierLLogL.symmetricPartialSum_add line 125
  20. theorem OAI.FourierLLogL.symmetricPartialSum_const_mul line 133
  21. theorem OAI.FourierLLogL.norm_fourierCoeff_le line 139
  22. theorem OAI.FourierLLogL.norm_symmetricPartialSum_le line 151
  23. theorem OAI.FourierLLogL.exists_measurable_null_of_ae line 172
  24. theorem OAI.FourierLLogL.ae_convergence_iff_exists_measurable_null line 183
  25. theorem OAI.FourierLLogL.tendsto_symmetricPartialSum_of_summable line 198
  26. theorem OAI.FourierLLogL.fourierCoeff_tsum line 207
  27. theorem OAI.FourierLLogL.symmetricPartialSum_tsum line 220
  28. theorem OAI.FourierLLogL.tendsto_symmetricPartialSum_tsum line 233
  29. theorem OAI.FourierLLogL.mass_logMinus_le line 249
  30. theorem OAI.FourierLLogL.summable_mass_logMinus line 265
  31. theorem OAI.FourierLLogL.summable_layerCost line 280
  32. def OAI.FourierLLogL.heightLayerSet line 291
  33. def OAI.FourierLLogL.heightLayer line 296
  34. def OAI.FourierLLogL.heightLayerMass line 300
  35. theorem OAI.FourierLLogL.heightLayerSet_nullMeasurable line 303
  36. theorem OAI.FourierLLogL.heightLayerSet_pairwise_disjoint line 308
  37. theorem OAI.FourierLLogL.MemLLogL.heightLayer_integrable line 319
  38. theorem OAI.FourierLLogL.heightLayerMass_nonneg line 323
  39. theorem OAI.FourierLLogL.heightLayerMass_eq_integral_norm line 327
  40. theorem OAI.FourierLLogL.MemLLogL.summable_weighted_heightLayerMass line 334
  41. theorem OAI.FourierLLogL.MemLLogL.summable_heightLayer_norm line 355
  42. theorem OAI.FourierLLogL.MemLLogL.summable_heightLayerCost line 366
  43. def OAI.FourierLLogL.boundedPart line 381
  44. theorem OAI.FourierLLogL.MemLLogL.boundedPart_integrable line 384
  45. theorem OAI.FourierLLogL.norm_boundedPart_le line 388
  46. theorem OAI.FourierLLogL.norm_heightLayer_le line 394
  47. theorem OAI.FourierLLogL.mem_boundedPart_or_heightLayerSet line 402
  48. theorem OAI.FourierLLogL.boundedPart_add_tsum_heightLayer line 426
  49. theorem OAI.FourierLLogL.MemLLogL.symmetricPartialSum_heightDecomposition line 454