OAI/Analysis/FourierLLogL/Dyadic/Span.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Signed combination spans and Fourier support

  1. def OAI.FourierLLogL.Dyadic.enclosed line 13
  2. lemma OAI.FourierLLogL.Dyadic.enclosed_zero line 16
  3. lemma OAI.FourierLLogL.Dyadic.enclosed_mem line 19
  4. lemma OAI.FourierLLogL.Dyadic.enclosed_neg line 24
  5. lemma OAI.FourierLLogL.Dyadic.enclosed_add line 31
  6. lemma OAI.FourierLLogL.Dyadic.enclosed_insert line 40
  7. lemma OAI.FourierLLogL.Dyadic.enclosed_sum line 54
  8. def OAI.FourierLLogL.Dyadic.palace line 67
  9. lemma OAI.FourierLLogL.Dyadic.palace_size line 69
  10. def OAI.FourierLLogL.Dyadic.spanned line 87

    Source documentation

    The Fourier coefficients are supported within a bandwidth of the signed span. This form (arbitrary thickening of our unthickened case) will also be used for broad capture.

    def spanned (s : Finset (Grid M)) (f : Grid M → ℂ) : Prop :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Grid

  11. lemma OAI.FourierLLogL.Dyadic.spanned_one line 90
  12. lemma OAI.FourierLLogL.Dyadic.fc_real_step line 96
  13. lemma OAI.FourierLLogL.Dyadic.expand_one_step line 107
  14. lemma OAI.FourierLLogL.Dyadic.span_augment line 113