OAI/Analysis/FourierLLogL/Fourier/Translate.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Translation averaging

  1. def OAI.FourierLLogL.Period.window line 12
  2. def OAI.FourierLLogL.Period.origins line 13
  3. lemma OAI.FourierLLogL.Period.flip_dilate line 15
  4. lemma OAI.FourierLLogL.Period.jump_average_all line 23

    Source documentation

    Translation average over origins for a single length.

    lemma jump_average_all (F : ℝ → ℂ) (hf : Measurable F) (B : ℝ) (hb : ∀ x, ‖F x‖ ≤ B)
    (x r b : ℝ) (hr : 0 < r) (hr' : r ≤ 1) :
    (∫ a : ℝ, jump F (a+b) r x) =
      ∫ t in window, kappa (t/r) • F (x-t) := by
…

    Mentions: OAI.FourierLLogL.Period.jump, OAI.FourierLLogL.Period.window, OAI.FourierLLogL.Period.kappa

  5. lemma OAI.FourierLLogL.Period.jump_average line 100
  6. lemma OAI.FourierLLogL.Period.haarLayer_average line 115