Theorems · Theorem · harmonic analysis

isBigO_norm_Icc_restrict_atBot

∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : C(ℝ, E)} {b : ℝ},
  0 < b →
    (⇑f =O[Filter.atBot] fun x => |x| ^ (-b)) →
      ∀ (R S : ℝ), (fun x => ‖ContinuousMap.restrict (Set.Icc (x + R) (x + S)) f‖) =O[Filter.atBot] fun x => |x| ^ (-b)

Defined in

Mathlib.Analysis.Fourier.PoissonSummation

Cited by

1 results in Mathlib

Foundations

Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroup