therefore
Sign up
Open navigation
All proofs
Project-declaredLean 4.32.0 · mathlib@81a5d257c8e4

Fourier Coeff eq fourier Coeff of aeeq

fourierCoeff_eq_fourierCoeff_of_aeeq

harmonic analysisFourier analysismeasure theorybasic

Plain-language statement

Two almost-everywhere strongly measurable functions on the circle that agree almost everywhere have the same Fourier coefficient at every fixed integer frequency nn.

Exact Lean statement

theorem fourierCoeff_eq_fourierCoeff_of_aeeq {T : ℝ} [hT : Fact (0 < T)] {n : ℤ} {f g : AddCircle T → ℂ}
    (hf : AEStronglyMeasurable f haarAddCircle) (hg : AEStronglyMeasurable g haarAddCircle)
    (h : f =ᵐ[haarAddCircle] g) : fourierCoeff f n = fourierCoeff g n

Formal artifact

Lean source

Canonical source
Full Lean sourceLean 4
theorem fourierCoeff_eq_fourierCoeff_of_aeeq {T : ℝ} [hT : Fact (0 < T)] {n : ℤ} {f g : AddCircle T → ℂ}    (hf : AEStronglyMeasurable f haarAddCircle) (hg : AEStronglyMeasurable g haarAddCircle)    (h : f =ᵐ[haarAddCircle] g) : fourierCoeff f n = fourierCoeff g n := by  unfold fourierCoeff  apply integral_congr_ae  change @DFunLike.coe C(AddCircle T, ℂ) (AddCircle T) (fun x ↦ ℂ) ContinuousMap.instFunLike (fourier (-n)) * f =ᶠ[ae haarAddCircle] @DFunLike.coe C(AddCircle T, ℂ) (AddCircle T) (fun x ↦ ℂ) ContinuousMap.instFunLike (fourier (-n)) * g  have fourier_measurable : AEStronglyMeasurable (⇑(@fourier T (-n))) haarAddCircle := (ContinuousMap.measurable _).aestronglyMeasurable  rw [← AEEqFun.mk_eq_mk (hf := fourier_measurable.mul hf) (hg := fourier_measurable.mul hg),      ← AEEqFun.mk_mul_mk _ _ fourier_measurable hf, ← AEEqFun.mk_mul_mk _ _ fourier_measurable hg]  congr 1  rwa [AEEqFun.mk_eq_mk]
Project
Carleson formalization
License
Apache-2.0
Commit
74ef907d6bdb
Source
Carleson/Classical/Basic.lean:17-27

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.32.0

Ae tendsto zero of distribution le

ae_tendsto_zero_of_distribution_le

Plain-language statement

Suppose that, for every error threshold δ>0\delta>0 and every measure tolerance ε>0\varepsilon>0, one can choose N0N_0 so that the set where sup⁡N>N0∥f(x)−FN(x)∥\sup_{N>N_0}\lVert f(x)-F_N(x)\rVert exceeds δ\delta has measure at most ε\varepsilon. Then FN(x)F_N(x) converges to f(x)f(x) for almost every xx.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Antichain operator

antichain_operator

Plain-language statement

For an antichain A\mathfrak{A} of pairwise incomparable tiles, and measurable functions ff and gg bounded by the indicators of FF and GG, the pairing of gg with the Carleson sum over A\mathfrak{A} is controlled by the L2L^2 norms of ff and gg and by positive powers of the two tile-density parameters. Concretely, the bound is

C(a,q) dens1(A)(q−1)/(8a4) dens2(A)1/q−1/2 ∥f∥2∥g∥2.C(a,q)\,\mathrm{dens}_1(\mathfrak{A})^{(q-1)/(8a^4)}\,\mathrm{dens}_2(\mathfrak{A})^{1/q-1/2}\,\lVert f\rVert_2\lVert g\rVert_2.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record