OAI/Analysis/FourierLLogL/Fourier/Good.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

GoodBound from the dyadic lemma

  1. lemma OAI.FourierLLogL.Period.center_sub line 12
  2. lemma OAI.FourierLLogL.Period.sumReal_integral line 15
  3. instance OAI.FourierLLogL.Period.(instance at line 56) line 56
  4. lemma OAI.FourierLLogL.Period.kernel_compare_result line 59
  5. theorem OAI.FourierLLogL.Period.AffineTreeBound.realGoodBound line 193