Theorems · Theorem · harmonic analysis

isBigO_norm_restrict_cocompact

∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : C(ℝ, E)) {b : ℝ},
  0 < b →
    (⇑f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)) →
      ∀ (K : TopologicalSpace.Compacts ℝ),
        (fun x => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[Filter.cocompact ℝ] fun x =>
          |x| ^ (-b)

Defined in: Mathlib.Analysis.Fourier.PoissonSummation
Cited by: 1 results in Mathlib
Foundations: Depth 201 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites38

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
Realstatement and proof · cited by 25,697
NormedAddCommGroupstatement and proof · cited by 15,752
SetLike.coestatement and proof · cited by 8,199
Set.Elemstatement and proof · cited by 7,166
Norm.normstatement and proof · cited by 5,413
LE.le.transproof · cited by 3,151
ContinuousMapstatement and proof · cited by 2,491
Filter.atTopproof · cited by 2,405
zero_addproof · cited by 2,366
Nat.cast_zeroproof · cited by 1,870

Cited by1

Results whose statement or proof uses this declaration.

Real.tsum_eq_tsum_fourier_of_rpow_decay_of_summableproof · cited by 1