Quantitative Fourier approximation on finite-dimensional tori

This file was automatically generated by Codex.

This module proves integration-by-parts bounds for Fourier coefficients, coordinate derivative estimates on finite-dimensional tori, lattice-shell counting, absolute convergence and explicit uniform Fourier truncation bounds. The derivative order exceeds the dimension; every dimension and derivative factor in the tail estimate is explicit. All statements and supporting definitions use only Mathlib and this module.

Source: blueprint/formalization_blueprint.tex, lem:fourier-foundation, lines 130-146. Verified library references are Mathlib.Analysis.Fourier.AddCircle and Mathlib.Analysis.Fourier.AddCircleMulti (characters, coefficients and Fourier completeness), and Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas. The integration-by-parts attribution to ../lean-dfr is retained below.

For lem:weyl (line 1333) the module also contains the first-moment Lipschitz bound for Fourier integrals, Fourier propagation along return progressions, Plancherel's theorem on L¹ ∩ L² (adapted with attribution from ../lean-dfr/DFR/Auto/IntegralPlancherel.lean; Stein–Weiss, Chapter I, Theorem 2.3), a square-mass bound on separated balls, and the resulting smallness of the progression step. For lem:chartfourier it proves that smooth ℤⁿ-periodic functions on ℝⁿ have absolutely convergent Fourier series with derivative-controlled coefficients (periodic_fourier_expansion). For lem:separation (line 1409) it proves that a bilinear convolution form ∫∫ F(u) G(v) K(v-u) is bounded by sup |𝓕 K| times the L² norms of F, G (norm_integral_convolution_form_le, with the correlation form norm_integral_correlation_le), via Parseval on L¹ ∩ L², the convolution structure of translates and Cauchy–Schwarz (Plancherel as in Stein–Weiss, Chapter I, Theorem 2.3).

Fourier coefficient estimates

The following one-dimensional integration-by-parts proofs are adapted from ../lean-dfr/DFR/Auto/Twisted/ConeDecompositionMultiplierTheorem/, ConeDecompositionMultiplierTheorem.lean, copyright 2026 Joris Roos, Apache 2.0. They implement the coordinate estimate in blueprint Lemma lem:fourier-foundation, lines 130–146.

theorem TrilinearHT.Auto.fourierCoeffOn_of_hasDerivAt_zeroBoundary {a b : ℝ} (hab : a < b) {f f' : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0) (hf : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) (hf' : IntervalIntegrable f' MeasureTheory.volume a b) (hboundary : f b = f a) : fourierCoeffOn hab f n = -(1 / (-2 * ↑Real.pi * Complex.I * ↑n)) * ((↑b - ↑a) * fourierCoeffOn hab f' n)

theorem TrilinearHT.Auto.norm_fourierCoeffOn_of_hasDerivAt_zeroBoundary {a b : ℝ} (hab : a < b) {f f' : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0) (hf : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) (hf' : IntervalIntegrable f' MeasureTheory.volume a b) (hboundary : f b = f a) : ‖fourierCoeffOn hab f n‖ = ‖1 / (-2 * ↑Real.pi * Complex.I * ↑n)‖ * |b - a| * ‖fourierCoeffOn hab f' n‖

theorem TrilinearHT.Auto.norm_fourierCoeffOn_le_of_norm_le {a b C : ℝ} (hab : a < b) {f : ℝ → ℂ} (n : ℤ) (hf : ∀ x ∈ Set.uIoc a b, ‖f x‖ ≤ C) : ‖fourierCoeffOn hab f n‖ ≤ C

theorem TrilinearHT.Auto.norm_fourier_antideriv_factor (n : ℤ) : ‖1 / (-2 * ↑Real.pi * Complex.I * ↑n)‖ = (2 * Real.pi * |↑n|)⁻¹

theorem TrilinearHT.Auto.norm_fourierCoeffOn_le_of_iteratedDeriv_bound {a b C : ℝ} (hab : a < b) {f : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0) (N : ℕ) (hf : ContDiff ℝ (↑N) f) (hboundary : ∀ r < N, iteratedDeriv r f b = iteratedDeriv r f a) (hbound : ∀ x ∈ Set.uIoc a b, ‖iteratedDeriv N f x‖ ≤ C) : ‖fourierCoeffOn hab f n‖ ≤ ((2 * Real.pi * |↑n|)⁻¹ * |b - a|) ^ N * C

theorem TrilinearHT.Auto.periodic_iteratedDeriv {f : ℝ → ℂ} {T : ℝ} (hf : Function.Periodic f T) (m : ℕ) : Function.Periodic (iteratedDeriv m f) T

Derivatives preserve the period, including the endpoint identities needed for repeated integration by parts.

theorem TrilinearHT.Auto.norm_fourierCoeff_le_of_periodic_derivative_bound (F : UnitAddCircle → ℂ) {n : ℤ} (hn : n ≠ 0) (m : ℕ) {A : ℝ} (hf : ContDiff ℝ ↑m fun (x : ℝ) => F ↑x) (hbound : ∀ (x : ℝ), ‖iteratedDeriv m (fun (t : ℝ) => F ↑t) x‖ ≤ A) : ‖fourierCoeff F n‖ ≤ (2 * Real.pi * |↑n|)⁻¹ ^ m * A

Blueprint Lemma lem:fourier-foundation, lines 130–146, in one coordinate of the unit torus. The coefficient is Mathlib's Haar coefficient.

@[instance_reducible]

noncomputable def TrilinearHT.Auto.unitAddCircleFourierMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

Normalized Haar measure used for the torus Fourier integral.

Equations

• TrilinearHT.Auto.unitAddCircleFourierMeasureSpace = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem TrilinearHT.Auto.instIsProbabilityMeasureUnitAddCircleVolume_leanPool : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem TrilinearHT.Auto.mFourierCoeff_eq_coordinate_integral {d : ℕ} (F : UnitAddTorus (Fin (d + 1)) → ℂ) (hF : Continuous F) (n : Fin (d + 1) → ℤ) (i : Fin (d + 1)) : UnitAddTorus.mFourierCoeff F n = ∫ (y : UnitAddTorus (Fin d)), (∏ j : Fin d, (fourier (-n (i.succAbove j))) (y j)) * fourierCoeff (fun (t : AddCircle 1) => F (i.insertNth t y)) (n i)

Splitting off an arbitrary torus coordinate in the Fourier integral.

theorem TrilinearHT.Auto.norm_mFourierCoeff_le_coordinate {d : ℕ} (F : UnitAddTorus (Fin (d + 1)) → ℂ) (hF : Continuous F) (n : Fin (d + 1) → ℤ) (i : Fin (d + 1)) (hi : n i ≠ 0) (m : ℕ) {A : ℝ} (hsmooth : ∀ (y : UnitAddTorus (Fin d)), ContDiff ℝ ↑m fun (t : ℝ) => F (i.insertNth (↑t) y)) (hbound : ∀ (y : UnitAddTorus (Fin d)) (x : ℝ), ‖iteratedDeriv m (fun (t : ℝ) => F (i.insertNth (↑t) y)) x‖ ≤ A) : ‖UnitAddTorus.mFourierCoeff F n‖ ≤ (2 * Real.pi * |↑(n i)|)⁻¹ ^ m * A

The multivariate coefficient inherits the one-dimensional derivative bound in each nonzero frequency coordinate.

noncomputable def TrilinearHT.Auto.frequencyLength {d : ℕ} (n : Fin d → ℤ) : ℝ

Euclidean length of an integer frequency, as in the blueprint's torus estimates.

Equations

• TrilinearHT.Auto.frequencyLength n = √(∑ j : Fin d, ↑(n j) ^ 2)

theorem TrilinearHT.Auto.frequencyLength_nonneg {d : ℕ} (n : Fin d → ℤ) : 0 ≤ frequencyLength n

theorem TrilinearHT.Auto.frequencyLength_pos {d : ℕ} {n : Fin d → ℤ} (hn : n ≠ 0) : 0 < frequencyLength n

theorem TrilinearHT.Auto.exists_dominant_frequency {d : ℕ} (n : Fin (d + 1) → ℤ) : ∃ (i : Fin (d + 1)), frequencyLength n ≤ √(↑d + 1) * |↑(n i)|

A largest coordinate controls the Euclidean frequency length.

theorem TrilinearHT.Auto.norm_mFourierCoeff_le_derivative_bound {d : ℕ} (F : UnitAddTorus (Fin (d + 1)) → ℂ) (hF : Continuous F) (n : Fin (d + 1) → ℤ) (hn : n ≠ 0) (m : ℕ) {A : ℝ} (hsmooth : ∀ (i : Fin (d + 1)) (y : UnitAddTorus (Fin d)), ContDiff ℝ ↑m fun (t : ℝ) => F (i.insertNth (↑t) y)) (hbound : ∀ (i : Fin (d + 1)) (y : UnitAddTorus (Fin d)) (x : ℝ), ‖iteratedDeriv m (fun (t : ℝ) => F (i.insertNth (↑t) y)) x‖ ≤ A) : ‖UnitAddTorus.mFourierCoeff F n‖ ≤ A * (√(↑d + 1) / (2 * Real.pi * frequencyLength n)) ^ m

Blueprint Lemma lem:fourier-foundation, lines 130–133: the exact Euclidean-frequency decay estimate. Coordinate derivatives are taken on real lifts of torus slices, so their periodic boundary conditions follow automatically.

theorem TrilinearHT.Auto.abs_frequency_coordinate_le {d : ℕ} (n : Fin d → ℤ) (i : Fin d) : |↑(n i)| ≤ frequencyLength n

theorem TrilinearHT.Auto.one_le_frequencyLength {d : ℕ} {n : Fin d → ℤ} (hn : n ≠ 0) : 1 ≤ frequencyLength n

def TrilinearHT.Auto.frequencyBox (d N : ℕ) : Finset (Fin d → ℤ)

A finite box containing all frequencies in a bounded Euclidean ball.

Equations

• TrilinearHT.Auto.frequencyBox d N = Fintype.piFinset fun (x : Fin d) => Finset.Icc (-↑N) ↑N

theorem TrilinearHT.Auto.card_frequencyBox (d N : ℕ) : (frequencyBox d N).card = (2 * N + 1) ^ d

theorem TrilinearHT.Auto.mem_frequencyBox_of_length_le {d N : ℕ} {n : Fin d → ℤ} (h : frequencyLength n ≤ ↑N) : n ∈ frequencyBox d N

noncomputable def TrilinearHT.Auto.frequencyShell (d : ℕ) (T : ℝ) : Finset (Fin d → ℤ)

The nonzero portion of a dyadic shell. The zero mode is deliberately separate: see automation/ErrorReport.md for the printed first-shell omission.

Equations

• TrilinearHT.Auto.frequencyShell d T = {n ∈ TrilinearHT.Auto.frequencyBox d ⌈2 * T⌉₊ | n ≠ 0 ∧ T ≤ 1 + TrilinearHT.Auto.frequencyLength n ∧ 1 + TrilinearHT.Auto.frequencyLength n < 2 * T}

theorem TrilinearHT.Auto.mem_frequencyShell {d : ℕ} {T : ℝ} {n : Fin d → ℤ} : n ∈ frequencyShell d T ↔ n ≠ 0 ∧ T ≤ 1 + frequencyLength n ∧ 1 + frequencyLength n < 2 * T

theorem TrilinearHT.Auto.card_frequencyShell_le {d : ℕ} {T : ℝ} (hT : 1 ≤ T) : ↑(frequencyShell d T).card ≤ (7 * T) ^ d

theorem TrilinearHT.Auto.sum_frequencyShell_le {d m : ℕ} {A T : ℝ} (hA : 0 ≤ A) (hT : 1 ≤ T) (c : (Fin d → ℤ) → ℂ) (hc : ∀ (n : Fin d → ℤ), n ≠ 0 → ‖c n‖ ≤ A * (√↑d / (2 * Real.pi * frequencyLength n)) ^ m) : ∑ n ∈ frequencyShell d T, ‖c n‖ ≤ 7 ^ d * A * √↑d ^ m * T ^ (↑d - ↑m)

Absolute shell mass from the blueprint's coefficient estimate. The explicit constant 7 ^ d is independent of the derivative order m. The expression (sqrt d) ^ m is the factor d ^ (m/2) in the source.

theorem TrilinearHT.Auto.exists_mem_dyadic_frequencyShell {d : ℕ} {n : Fin d → ℤ} (hn : n ≠ 0) : ∃ (k : ℕ), n ∈ frequencyShell d (2 ^ k)

Nonzero integer frequencies are covered by the dyadic shells.

theorem TrilinearHT.Auto.summable_dyadic_frequencyShell {d m : ℕ} {A : ℝ} (hA : 0 ≤ A) (hm : d < m) (c : (Fin d → ℤ) → ℂ) (hc : ∀ (n : Fin d → ℤ), n ≠ 0 → ‖c n‖ ≤ A * (√↑d / (2 * Real.pi * frequencyLength n)) ^ m) : Summable fun (k : ℕ) => ∑ n ∈ frequencyShell d (2 ^ k), ‖c n‖

The shell estimates form a convergent geometric series once the derivative order exceeds the dimension.

theorem TrilinearHT.Auto.summable_norm_of_finite_shells {β : Type u_1} (c : β → ℂ) (z : β) (s : ℕ → Finset β) (hcover : ∀ (b : β), b ≠ z → ∃ (k : ℕ), b ∈ s k) (hmass : Summable fun (k : ℕ) => ∑ b ∈ s k, ‖c b‖) : Summable fun (b : β) => ‖c b‖

A countable collection of finite shells with summable masses controls the entire series, with one separately handled exceptional index.

theorem TrilinearHT.Auto.summable_norm_of_frequency_decay {d m : ℕ} {A : ℝ} (hA : 0 ≤ A) (hm : d < m) (c : (Fin d → ℤ) → ℂ) (hc : ∀ (n : Fin d → ℤ), n ≠ 0 → ‖c n‖ ≤ A * (√↑d / (2 * Real.pi * frequencyLength n)) ^ m) : Summable fun (n : Fin d → ℤ) => ‖c n‖

Absolute convergence of a coefficient sequence with decay order above dimension.

theorem TrilinearHT.Auto.summable_norm_mFourierCoeff {d m : ℕ} {A : ℝ} (hm : d + 1 < m) (F : UnitAddTorus (Fin (d + 1)) → ℂ) (hF : Continuous F) (hsmooth : ∀ (i : Fin (d + 1)) (y : UnitAddTorus (Fin d)), ContDiff ℝ ↑m fun (t : ℝ) => F (i.insertNth (↑t) y)) (hbound : ∀ (i : Fin (d + 1)) (y : UnitAddTorus (Fin d)) (x : ℝ), ‖iteratedDeriv m (fun (t : ℝ) => F (i.insertNth (↑t) y)) x‖ ≤ A) : Summable fun (n : Fin (d + 1) → ℤ) => ‖UnitAddTorus.mFourierCoeff F n‖

Blueprint Lemma lem:fourier-foundation: choosing a derivative order above the dimension gives absolute convergence of the torus Fourier coefficients.

theorem TrilinearHT.Auto.hasSum_mFourier_of_derivative_bound {d m : ℕ} {A : ℝ} (hm : d + 1 < m) (F : C(UnitAddTorus (Fin (d + 1)), ℂ)) (hsmooth : ∀ (i : Fin (d + 1)) (y : UnitAddTorus (Fin d)), ContDiff ℝ ↑m fun (t : ℝ) => F (i.insertNth (↑t) y)) (hbound : ∀ (i : Fin (d + 1)) (y : UnitAddTorus (Fin d)) (x : ℝ), ‖iteratedDeriv m (fun (t : ℝ) => F (i.insertNth (↑t) y)) x‖ ≤ A) : HasSum (fun (n : Fin (d + 1) → ℤ) => UnitAddTorus.mFourierCoeff (⇑F) n • UnitAddTorus.mFourier n) F

Blueprint Lemma lem:fourier-foundation: the Fourier series converges in the uniform norm of continuous functions on the torus.

theorem TrilinearHT.Auto.tsum_norm_le_shell_masses {β : Type u_1} (c : β → ℂ) (s : ℕ → Finset β) (hcover : ∀ (b : β), c b ≠ 0 → ∃ (k : ℕ), b ∈ s k) (hmass : Summable fun (k : ℕ) => ∑ b ∈ s k, ‖c b‖) : (Summable fun (b : β) => ‖c b‖) ∧ ∑' (b : β), ‖c b‖ ≤ ∑' (k : ℕ), ∑ b ∈ s k, ‖c b‖

Summable shell masses bound the total absolute mass whenever the shells cover the support. Overlap of shells is harmless for this upper bound.

theorem TrilinearHT.Auto.exists_mem_late_frequencyShell {d : ℕ} {n : Fin d → ℤ} (hn : n ≠ 0) (K : ℕ) (hK : 2 ^ K ≤ 1 + frequencyLength n) : ∃ (k : ℕ), n ∈ frequencyShell d (2 ^ (K + k))

Frequencies past a dyadic cutoff are covered by the later shells.

theorem TrilinearHT.Auto.frequency_tail_bound {d m : ℕ} {A : ℝ} (hA : 0 ≤ A) (hm : d < m) (c : (Fin d → ℤ) → ℂ) (hc : ∀ (n : Fin d → ℤ), n ≠ 0 → ‖c n‖ ≤ A * (√↑d / (2 * Real.pi * frequencyLength n)) ^ m) (K : ℕ) : (∑' (n : Fin d → ℤ), if n ≠ 0 ∧ 2 ^ K ≤ 1 + frequencyLength n then ‖c n‖ else 0) ≤ 7 ^ d * A * √↑d ^ m * (2 ^ K) ^ (↑d - ↑m) / (1 - 2 ^ (↑d - ↑m))

Quantitative absolute Fourier tail. Taking m greater than the dimension plus a requested tail power gives that power of decay, with explicit constants.

noncomputable def TrilinearHT.Auto.frequencyTruncationSet (d K : ℕ) : Finset (Fin d → ℤ)

Frequencies retained by a dyadic Fourier truncation, including the constant mode.

Equations

• TrilinearHT.Auto.frequencyTruncationSet d K = {n ∈ TrilinearHT.Auto.frequencyBox d ⌈2 ^ K⌉₊ | n = 0 ∨ 1 + TrilinearHT.Auto.frequencyLength n < 2 ^ K}

theorem TrilinearHT.Auto.mem_frequencyTruncationSet {d K : ℕ} {n : Fin d → ℤ} : n ∈ frequencyTruncationSet d K ↔ n = 0 ∨ 1 + frequencyLength n < 2 ^ K

theorem TrilinearHT.Auto.fourier_modulation_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : E → ℂ) (c : ℝ) (ω ξ : E) : FourierTransform.fourier (fun (x : E) => ↑(Real.fourierChar (c + inner ℝ x ω)) * f x) ξ = ↑(Real.fourierChar c) * FourierTransform.fourier f (ξ - ω)

Multiplication by a linear phase translates the Fourier transform exactly.

theorem TrilinearHT.Auto.fourier_progression_lower {E : Type u_1} [AddCommGroup E] (f : E → ℂ) (ω : E) (ε : ℝ) (hstep : ∀ (ξ : E), ‖f ξ‖ - ε ≤ ‖f (ξ - ω)‖) (ξ : E) (j : ℕ) : ‖f ξ‖ - ↑j * ε ≤ ‖f (ξ - j • ω)‖

Iterating a uniform one-step loss along an arithmetic progression.

Plancherel's theorem on L¹ ∩ L²

The identification of Mathlib's abstract L² Fourier transform with the integral transform on L¹ ∩ L², and the resulting Plancherel identity, are adapted with attribution from ../lean-dfr/DFR/Auto/IntegralPlancherel.lean (revision 28d3daff672dd670e2c4bd29130dab9668c9c1e2, Joris Roos, author Claude, Apache-2.0). References: Stein–Weiss, Introduction to Fourier Analysis on Euclidean Spaces, Chapter I, Theorem 2.3; Grafakos, Classical Fourier Analysis, 3rd ed., Theorem 2.2.14. Used in lem:weyl, line 1333.

theorem TrilinearHT.Auto.integral_fourier_smul_eq_of_integrable {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (g : SchwartzMap V ℂ) {f : V → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) : ∫ (x : V), FourierTransform.fourier (⇑g) x • f x = ∫ (ξ : V), g ξ • FourierTransform.fourier f ξ

The multiplication formula ∫ (𝓕 g) f = ∫ g (𝓕 f) for Schwartz g and integrable f.

theorem TrilinearHT.Auto.continuous_fourier_of_integrable {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {f : V → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) : Continuous (FourierTransform.fourier f)

The integral Fourier transform of an integrable function is continuous.

theorem TrilinearHT.Auto.fourierLp_ae_eq_fourier {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {f : V → ℂ} (hf1 : MeasureTheory.Integrable f MeasureTheory.volume) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ↑↑(FourierTransform.fourier (MeasureTheory.MemLp.toLp f hf2)) =ᵐ[MeasureTheory.volume] FourierTransform.fourier f

On L¹ ∩ L² the abstract L² Fourier transform agrees almost everywhere with the integral transform.

theorem TrilinearHT.Auto.memLp_two_fourier {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {f : V → ℂ} (hf1 : MeasureTheory.Integrable f MeasureTheory.volume) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.MemLp (FourierTransform.fourier f) 2 MeasureTheory.volume

The integral Fourier transform of f ∈ L¹ ∩ L² is square integrable.

theorem TrilinearHT.Auto.integral_conj_mul_fourier {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {f g : V → ℂ} (hf1 : MeasureTheory.Integrable f MeasureTheory.volume) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg1 : MeasureTheory.Integrable g MeasureTheory.volume) (hg2 : MeasureTheory.MemLp g 2 MeasureTheory.volume) : ∫ (ξ : V), (starRingEnd ℂ) (FourierTransform.fourier f ξ) * FourierTransform.fourier g ξ = ∫ (x : V), (starRingEnd ℂ) (f x) * g x

The pairing identity ∫ conj (𝓕 f) (𝓕 g) = ∫ conj f g on L¹ ∩ L².

theorem TrilinearHT.Auto.integral_norm_sq_fourier {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {f : V → ℂ} (hf1 : MeasureTheory.Integrable f MeasureTheory.volume) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ∫ (ξ : V), ‖FourierTransform.fourier f ξ‖ ^ 2 = ∫ (x : V), ‖f x‖ ^ 2

Plancherel's theorem: ∫ ‖𝓕 f‖² = ∫ ‖f‖² for f ∈ L¹ ∩ L².

theorem TrilinearHT.Auto.integral_norm_mul_le_sqrt {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℂ} (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) : ∫ (x : α), ‖f x‖ * ‖g x‖ ∂μ ≤ √(∫ (x : α), ‖f x‖ ^ 2 ∂μ) * √(∫ (x : α), ‖g x‖ ^ 2 ∂μ)

Cauchy–Schwarz for the absolute pairing of two square-integrable functions.

theorem TrilinearHT.Auto.fourier_comp_add_right_apply (G : ℝ → ℂ) (s ξ : ℝ) : FourierTransform.fourier (fun (u : ℝ) => G (u + s)) ξ = ↑(Real.fourierChar (s * ξ)) * FourierTransform.fourier G ξ

The Fourier transform of a right translate.

theorem TrilinearHT.Auto.norm_integral_correlation_le {F G K : ℝ → ℂ} (hF1 : MeasureTheory.Integrable F MeasureTheory.volume) (hF2 : MeasureTheory.MemLp F 2 MeasureTheory.volume) (hG1 : MeasureTheory.Integrable G MeasureTheory.volume) (hG2 : MeasureTheory.MemLp G 2 MeasureTheory.volume) (hK : MeasureTheory.Integrable K MeasureTheory.volume) {M : ℝ} (hM : ∀ (ξ : ℝ), ‖FourierTransform.fourier K ξ‖ ≤ M) : ‖∫ (s : ℝ), K s * ∫ (u : ℝ), F u * G (u + s)‖ ≤ M * √(∫ (x : ℝ), ‖F x‖ ^ 2) * √(∫ (x : ℝ), ‖G x‖ ^ 2)

Blueprint lem:separation, line 1409: a correlation form ∫ K(s) ∫ F(u) G(u+s) du ds is bounded by the supremum of the Fourier transform of K times the L² norms (Plancherel).

theorem TrilinearHT.Auto.norm_integral_convolution_form_le {F G K : ℝ → ℂ} (hF1 : MeasureTheory.Integrable F MeasureTheory.volume) (hF2 : MeasureTheory.MemLp F 2 MeasureTheory.volume) (hG1 : MeasureTheory.Integrable G MeasureTheory.volume) (hG2 : MeasureTheory.MemLp G 2 MeasureTheory.volume) (hK : MeasureTheory.Integrable K MeasureTheory.volume) {M : ℝ} (hM : ∀ (ξ : ℝ), ‖FourierTransform.fourier K ξ‖ ≤ M) : ‖∫ (p : ℝ × ℝ), F p.1 * G p.2 * K (p.2 - p.1)‖ ≤ M * √(∫ (x : ℝ), ‖F x‖ ^ 2) * √(∫ (x : ℝ), ‖G x‖ ^ 2)

Blueprint lem:separation, line 1409: a bilinear convolution form is bounded by the supremum of the Fourier transform of its kernel times the L² norms (Plancherel).

Fourier series of smooth periodic functions on ℝⁿ

The torus results above are transported to ℤⁿ-periodic functions on ℝⁿ. Used in lem:chartfourier, lines 1361–1377.

@[instance_reducible]

noncomputable def TrilinearHT.Auto.unitAddCirclePeriodicMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

Normalized Haar measure used to transfer periodic functions to the torus.

Equations

• TrilinearHT.Auto.unitAddCirclePeriodicMeasureSpace = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem TrilinearHT.Auto.instIsProbabilityMeasureUnitAddCircleVolume_leanPool_1 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

noncomputable def TrilinearHT.Auto.torusProjection (n : ℕ) : (Fin n → ℝ) → UnitAddTorus (Fin n)

The coordinatewise quotient map ℝⁿ → (ℝ/ℤ)ⁿ.

Equations

• TrilinearHT.Auto.torusProjection n x i = ↑(x i)

theorem TrilinearHT.Auto.torusProjection_isOpenQuotientMap (n : ℕ) : IsOpenQuotientMap (torusProjection n)

theorem TrilinearHT.Auto.torusProjection_surjective (n : ℕ) : Function.Surjective (torusProjection n)

theorem TrilinearHT.Auto.torusProjection_eq_iff {n : ℕ} {x y : Fin n → ℝ} : torusProjection n x = torusProjection n y ↔ ∃ (j : Fin n → ℤ), x = y + fun (i : Fin n) => ↑(j i)

theorem TrilinearHT.Auto.mFourier_torusProjection {n : ℕ} (v : Fin n → ℤ) (x : Fin n → ℝ) : (UnitAddTorus.mFourier v) (torusProjection n x) = ↑(Real.fourierChar (∑ i : Fin n, ↑(v i) * x i))

The Fourier monomial at a projected point is the usual real character.

noncomputable def TrilinearHT.Auto.periodicDescent {n : ℕ} (f : (Fin n → ℝ) → ℂ) : UnitAddTorus (Fin n) → ℂ

The function on the torus induced by a ℤⁿ-periodic function.

Equations

• TrilinearHT.Auto.periodicDescent f y = f (Function.surjInv ⋯ y)

theorem TrilinearHT.Auto.periodicDescent_apply {n : ℕ} {f : (Fin n → ℝ) → ℂ} (hper : ∀ (x : Fin n → ℝ) (j : Fin n → ℤ), f (x + fun (i : Fin n) => ↑(j i)) = f x) (x : Fin n → ℝ) : periodicDescent f (torusProjection n x) = f x

theorem TrilinearHT.Auto.periodicDescent_continuous {n : ℕ} {f : (Fin n → ℝ) → ℂ} (hf : Continuous f) (hper : ∀ (x : Fin n → ℝ) (j : Fin n → ℤ), f (x + fun (i : Fin n) => ↑(j i)) = f x) : Continuous (periodicDescent f)

noncomputable def TrilinearHT.Auto.periodicFourierCoeff {n : ℕ} (f : (Fin n → ℝ) → ℂ) (v : Fin n → ℤ) : ℂ

The Fourier coefficients of a ℤⁿ-periodic function on ℝⁿ, defined through its descent to the torus.

Equations

• TrilinearHT.Auto.periodicFourierCoeff f v = UnitAddTorus.mFourierCoeff (TrilinearHT.Auto.periodicDescent f) v

theorem TrilinearHT.Auto.torusProjection_insertNth {d : ℕ} (i : Fin (d + 1)) (t : ℝ) (x : Fin d → ℝ) : torusProjection (d + 1) (i.insertNth t x) = i.insertNth (↑t) (torusProjection d x)

theorem TrilinearHT.Auto.periodic_fourier_expansion {d m : ℕ} {A B : ℝ} (hm : d + 1 < m) (f : (Fin (d + 1) → ℝ) → ℂ) (hf : Continuous f) (hper : ∀ (x : Fin (d + 1) → ℝ) (j : Fin (d + 1) → ℤ), f (x + fun (i : Fin (d + 1)) => ↑(j i)) = f x) (hsmooth : ∀ (i : Fin (d + 1)) (x : Fin d → ℝ), ContDiff ℝ ↑m fun (t : ℝ) => f (i.insertNth t x)) (hbound : ∀ (i : Fin (d + 1)) (x : Fin d → ℝ) (t : ℝ), ‖iteratedDeriv m (fun (t : ℝ) => f (i.insertNth t x)) t‖ ≤ A) (hB : ∀ (x : Fin (d + 1) → ℝ), ‖f x‖ ≤ B) : (∀ (x : Fin (d + 1) → ℝ), HasSum (fun (v : Fin (d + 1) → ℤ) => periodicFourierCoeff f v * ↑(Real.fourierChar (∑ i : Fin (d + 1), ↑(v i) * x i))) (f x)) ∧ (Summable fun (v : Fin (d + 1) → ℤ) => ‖periodicFourierCoeff f v‖) ∧ (∀ (v : Fin (d + 1) → ℤ), v ≠ 0 → ‖periodicFourierCoeff f v‖ ≤ A * (√(↑d + 1) / (2 * Real.pi * frequencyLength v)) ^ m) ∧ ∀ (v : Fin (d + 1) → ℤ), ‖periodicFourierCoeff f v‖ ≤ B

Fourier series of smooth periodic functions. A continuous ℤⁿ-periodic function whose coordinate slices have m-th derivatives bounded by A, with m > n, is the sum of its absolutely convergent Fourier series at every point. Its nonzero coefficients obey |c_v| ≤ A (√n / (2π|v|))^m, and every coefficient is bounded by the supremum of |f|. Used in lem:chartfourier, lines 1361–1377.

theorem TrilinearHT.Auto.norm_iteratedDeriv_line_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (hf : ContDiff ℝ (↑⊤) f) (x v : E) (m : ℕ) (t : ℝ) : ‖iteratedDeriv m (fun (s : ℝ) => f (s • v + x)) t‖ ≤ ‖iteratedFDeriv ℝ m f (t • v + x)‖ * ‖v‖ ^ m

A line through x in direction v loses at most ‖v‖ᵐ in the m-th derivative.

theorem TrilinearHT.Auto.periodic_fourier_expansion_of_fderiv {n m : ℕ} (hn : 1 ≤ n) (hm : n < m) {A B : ℝ} (f : (Fin n → ℝ) → ℂ) (hf : ContDiff ℝ (↑⊤) f) (hper : ∀ (x : Fin n → ℝ) (j : Fin n → ℤ), f (x + fun (i : Fin n) => ↑(j i)) = f x) (hA : ∀ (x : Fin n → ℝ), ‖iteratedFDeriv ℝ m f x‖ ≤ A) (hB : ∀ (x : Fin n → ℝ), ‖f x‖ ≤ B) : (∀ (x : Fin n → ℝ), HasSum (fun (v : Fin n → ℤ) => periodicFourierCoeff f v * ↑(Real.fourierChar (∑ i : Fin n, ↑(v i) * x i))) (f x)) ∧ (Summable fun (v : Fin n → ℤ) => ‖periodicFourierCoeff f v‖) ∧ (∀ (v : Fin n → ℤ), v ≠ 0 → ‖periodicFourierCoeff f v‖ ≤ A * (√↑n / (2 * Real.pi * frequencyLength v)) ^ m) ∧ ∀ (v : Fin n → ℤ), ‖periodicFourierCoeff f v‖ ≤ B

Fourier series of smooth periodic functions on ℝⁿ, operator-norm form. A smooth ℤⁿ-periodic function, n ≥ 1, whose m-th derivative (m > n) is bounded by A in operator norm is the sum of its absolutely convergent Fourier series, with |c_v| ≤ A (√n/(2π|v|))^m for v ≠ 0 and |c_v| ≤ sup |f|.