Large spectrum of a function

noncomputable def largeSpec {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] (f : G → ℂ) (η : ℝ) : Finset (AddChar G ℂ)

The η-large spectrum of a function.

Equations

• largeSpec f η = {ψ : AddChar G ℂ | η * ‖f‖_[1] ≤ ‖dft f ψ‖}

@[simp]

theorem mem_largeSpec {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] {f : G → ℂ} {η : ℝ} {ψ : AddChar G ℂ} : ψ ∈ largeSpec f η ↔ η * ‖f‖_[1] ≤ ‖dft f ψ‖

theorem largeSpec_anti {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] (f : G → ℂ) : Antitone (largeSpec f)

@[simp]

theorem largeSpec_zero_left {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] (η : ℝ) : largeSpec 0 η = Finset.univ

@[simp]

theorem largeSpec_zero_right {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] (f : G → ℂ) : largeSpec f 0 = Finset.univ