Theorems · Definition · harmonic analysis

fourierLp

{T : ℝ} → [hT : Fact (0 < T)] → (p : ENNReal) → [Fact (1 ≤ p)] → ℤ → ↥(MeasureTheory.Lp ℂ p AddCircle.haarAddCircle)

The family of monomials fourier n, parametrized by n : ℤ and considered as elements of the Lp space of functions AddCircle T → ℂ.

Defined in

Mathlib.Analysis.Fourier.AddCircle

Cited by

9 results in Mathlib

Foundations

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

Assumes

FactFact