Fourier decay for finite products of periodized covariance factors

This file closes the analytic bridge between the coordinate-line periodization estimates and eight-fold periodic Fourier integration by parts. The derivative allocation is kept in symmetric-power form until the multinomial sum is evaluated. Consequently the only combinatorial loss is the eighth power of the number of factors, and compact support does not introduce a lattice-cardinality factor.

noncomputable def Anderson4D.SmoothCutoff.etaPeriodizationCoordLineFactor (ρ : SmoothCutoff) (ε : ℝ) (x : R4) (i : Fin dim) (a t : ℝ) : ℝ

A true covariance-periodization factor restricted to a translated coordinate line.

Equations

• ρ.etaPeriodizationCoordLineFactor ε x i a t = ρ.etaPeriodizationR4 ε (Function.update x i (a + t))

theorem Anderson4D.SmoothCutoff.contDiff_etaPeriodizationCoordLineFactor_eight (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : R4) (i : Fin dim) (a : ℝ) : ContDiff ℝ 8 (ρ.etaPeriodizationCoordLineFactor ε x i a)

A translated coordinate line of the true periodization is C⁸.

theorem Anderson4D.SmoothCutoff.iteratedDeriv_etaPeriodizationCoordLineFactor (ρ : SmoothCutoff) (ε : ℝ) (x : R4) (i : Fin dim) (a t : ℝ) (r : ℕ) : iteratedDeriv r (ρ.etaPeriodizationCoordLineFactor ε x i a) t = iteratedDeriv r (fun (s : ℝ) => ρ.etaPeriodizationR4 ε (Function.update x i s)) (a + t)

Translation commutes with every iterated derivative of a coordinate line factor.

theorem Anderson4D.SmoothCutoff.abs_iteratedDeriv_etaPeriodizationCoordLineFactor_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : R4) (i : Fin dim) (a t : ℝ) {r : ℕ} (hr : r ≤ 8) : |iteratedDeriv r (ρ.etaPeriodizationCoordLineFactor ε x i a) t| ≤ ρ.etaDerivativeMajorantConstant * ε⁻¹ ^ r * ρ.auxiliaryCutoff.etaPeriodizationR4 ε (Function.update x i (a + t))

Global derivative majorant for a translated coordinate-line factor. There is no lattice-cardinality loss.

noncomputable def Anderson4D.SmoothCutoff.etaPeriodizationCoordLineProduct {ι : Type u_1} (ρ : SmoothCutoff) (u : Finset ι) (ε : ℝ) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) (t : ℝ) : ℝ

A finite product of true covariance-periodization coordinate lines. The index finset consists of slots, so equal factor data remain distinct.

Equations

• ρ.etaPeriodizationCoordLineProduct u ε x i a t = ∏ j ∈ u, ρ.etaPeriodizationCoordLineFactor ε (x j) (i j) (a j) t

theorem Anderson4D.SmoothCutoff.contDiff_etaPeriodizationCoordLineProduct_eight {ι : Type u_1} (ρ : SmoothCutoff) (u : Finset ι) {ε : ℝ} (hε : 0 < ε) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) : ContDiff ℝ 8 (ρ.etaPeriodizationCoordLineProduct u ε x i a)

The product of finitely many true coordinate-line factors is C⁸.

noncomputable def Anderson4D.SmoothCutoff.etaAuxiliaryCoordLineProduct {ι : Type u_1} (ρ : SmoothCutoff) (u : Finset ι) (ε : ℝ) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) (t : ℝ) : ℝ

The product of the auxiliary periodizations which majorizes all derivative allocations of the true product.

Equations

• ρ.etaAuxiliaryCoordLineProduct u ε x i a t = ∏ j ∈ u, ρ.auxiliaryCutoff.etaPeriodizationR4 ε (Function.update (x j) (i j) (a j + t))

theorem Anderson4D.SmoothCutoff.contDiff_etaAuxiliaryCoordLineProduct_eight {ι : Type u_1} (ρ : SmoothCutoff) (u : Finset ι) {ε : ℝ} (hε : 0 < ε) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) : ContDiff ℝ 8 (ρ.etaAuxiliaryCoordLineProduct u ε x i a)

The auxiliary product is continuous (indeed C⁸).

theorem Anderson4D.SmoothCutoff.etaPeriodizationR4_nonneg (ρ : SmoothCutoff) (ε : ℝ) (y : R4) : 0 ≤ ρ.etaPeriodizationR4 ε y

The arbitrary-representative periodization is nonnegative.

theorem Anderson4D.SmoothCutoff.etaAuxiliaryCoordLineProduct_nonneg {ι : Type u_1} (ρ : SmoothCutoff) (u : Finset ι) (ε : ℝ) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) (t : ℝ) : 0 ≤ ρ.etaAuxiliaryCoordLineProduct u ε x i a t

Pointwise nonnegativity of the auxiliary product.

theorem Anderson4D.SmoothCutoff.sym_count_le_order {ι : Type u_1} [DecidableEq ι] {r : ℕ} (p : Sym ι r) (j : ι) : Multiset.count j ↑p ≤ r

Every component count of an order-r symmetric allocation is at most r.

theorem Anderson4D.SmoothCutoff.sum_countPerms_sym_eq_card_pow {ι : Type u_1} [DecidableEq ι] (u : Finset ι) (r : ℕ) : ∑ p ∈ u.sym r, ↑(↑p).countPerms = ↑u.card ^ r

The total multiplicity of all weak allocations of r derivative slots is exactly the r-th power of the number of product slots.

theorem Anderson4D.SmoothCutoff.prod_derivativeMajorant_eq {ι : Type u_1} [DecidableEq ι] (ρ : SmoothCutoff) (u : Finset ι) (ε : ℝ) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) (t : ℝ) {r : ℕ} {p : Sym ι r} (hp : p ∈ u.sym r) : ∏ j ∈ u, ρ.etaDerivativeMajorantConstant * ε⁻¹ ^ Multiset.count j ↑p * ρ.auxiliaryCutoff.etaPeriodizationR4 ε (Function.update (x j) (i j) (a j + t)) = ρ.etaDerivativeMajorantConstant ^ u.card * ε⁻¹ ^ r * ρ.etaAuxiliaryCoordLineProduct u ε x i a t

Exact algebraic collapse of one derivative allocation. The total power of ε⁻¹ is the derivative order, not the number of factors times that order.

theorem Anderson4D.SmoothCutoff.abs_iteratedDeriv_etaPeriodizationCoordLineProduct_le {ι : Type u_1} [DecidableEq ι] (ρ : SmoothCutoff) (u : Finset ι) {ε : ℝ} (hε : 0 < ε) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) (t : ℝ) {r : ℕ} (hr : r ≤ 8) : |iteratedDeriv r (ρ.etaPeriodizationCoordLineProduct u ε x i a) t| ≤ ↑u.card ^ r * (ρ.etaDerivativeMajorantConstant ^ u.card * ε⁻¹ ^ r * ρ.etaAuxiliaryCoordLineProduct u ε x i a t)

Derivative majorant for every order through eight. The symmetric allocation sum costs exactly card(u)^r; in particular the order-eight cost is card(u)^8.

theorem Anderson4D.SmoothCutoff.abs_iteratedDeriv_eight_etaPeriodizationCoordLineProduct_le {ι : Type u_1} [DecidableEq ι] (ρ : SmoothCutoff) (u : Finset ι) {ε : ℝ} (hε : 0 < ε) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) (t : ℝ) : |iteratedDeriv 8 (ρ.etaPeriodizationCoordLineProduct u ε x i a) t| ≤ ↑u.card ^ 8 * (ρ.etaDerivativeMajorantConstant ^ u.card * ε⁻¹ ^ 8 * ρ.etaAuxiliaryCoordLineProduct u ε x i a t)

The order-eight specialization used in periodic Fourier decay.

theorem Anderson4D.SmoothCutoff.etaPeriodizationCoordLineFactor_add_two_pi (ρ : SmoothCutoff) (ε : ℝ) (x : R4) (i : Fin dim) (a t : ℝ) : ρ.etaPeriodizationCoordLineFactor ε x i a (t + 2 * Real.pi) = ρ.etaPeriodizationCoordLineFactor ε x i a t

Each translated coordinate-line factor has period 2π.

theorem Anderson4D.SmoothCutoff.periodic_etaPeriodizationCoordLineProduct {ι : Type u_1} (ρ : SmoothCutoff) (u : Finset ι) (ε : ℝ) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) : Function.Periodic (ρ.etaPeriodizationCoordLineProduct u ε x i a) (2 * Real.pi)

The finite product has period 2π.

noncomputable def Anderson4D.SmoothCutoff.etaPeriodizationCoordLineProductC {ι : Type u_1} (ρ : SmoothCutoff) (u : Finset ι) (ε : ℝ) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) (t : ℝ) : ℂ

Complexification of the real covariance product.

Equations

• ρ.etaPeriodizationCoordLineProductC u ε x i a t = ↑(ρ.etaPeriodizationCoordLineProduct u ε x i a t)

theorem Anderson4D.SmoothCutoff.contDiff_etaPeriodizationCoordLineProductC_eight {ι : Type u_1} (ρ : SmoothCutoff) (u : Finset ι) {ε : ℝ} (hε : 0 < ε) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) : ContDiff ℝ 8 (ρ.etaPeriodizationCoordLineProductC u ε x i a)

The complexified product is C⁸ over ℝ.

theorem Anderson4D.SmoothCutoff.norm_iteratedDeriv_etaPeriodizationCoordLineProductC_le_abs {ι : Type u_1} (ρ : SmoothCutoff) (u : Finset ι) {ε : ℝ} (hε : 0 < ε) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) (t : ℝ) {r : ℕ} (hr : r ≤ 8) : ‖iteratedDeriv r (ρ.etaPeriodizationCoordLineProductC u ε x i a) t‖ ≤ |iteratedDeriv r (ρ.etaPeriodizationCoordLineProduct u ε x i a) t|

Complexification preserves the derivative norm up to the (unit) operator norm of ofRealCLM.

theorem Anderson4D.SmoothCutoff.norm_iteratedDeriv_etaPeriodizationCoordLineProductC_le {ι : Type u_1} [DecidableEq ι] (ρ : SmoothCutoff) (u : Finset ι) {ε : ℝ} (hε : 0 < ε) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) (t : ℝ) {r : ℕ} (hr : r ≤ 8) : ‖iteratedDeriv r (ρ.etaPeriodizationCoordLineProductC u ε x i a) t‖ ≤ ↑u.card ^ r * (ρ.etaDerivativeMajorantConstant ^ u.card * ε⁻¹ ^ r * ρ.etaAuxiliaryCoordLineProduct u ε x i a t)

Pointwise complex derivative majorant for every order through eight.

theorem Anderson4D.SmoothCutoff.periodic_etaPeriodizationCoordLineProductC {ι : Type u_1} (ρ : SmoothCutoff) (u : Finset ι) (ε : ℝ) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) : Function.Periodic (ρ.etaPeriodizationCoordLineProductC u ε x i a) (2 * Real.pi)

The complexified product has period 2π.

theorem Anderson4D.SmoothCutoff.negPiPiPeriodicJets_etaPeriodizationCoordLineProductC {ι : Type u_1} (ρ : SmoothCutoff) (u : Finset ι) (ε : ℝ) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) : NegPiPiPeriodicJets (ρ.etaPeriodizationCoordLineProductC u ε x i a) 8

The complex covariance product supplies all endpoint jets required for eight integrations by parts.

theorem Anderson4D.SmoothCutoff.norm_fourierCoeffOn_etaPeriodizationCoordLineProductC_le_auxIntegral {ι : Type u_1} [DecidableEq ι] (ρ : SmoothCutoff) (u : Finset ι) {ε : ℝ} (hε : 0 < ε) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) {n : ℤ} (hn : n ≠ 0) : ‖fourierCoeffOn ⋯ (ρ.etaPeriodizationCoordLineProductC u ε x i a) n‖ ≤ |↑n|⁻¹ ^ 8 * (2 * Real.pi)⁻¹ * ∫ (t : ℝ) in -Real.pi..Real.pi, ↑u.card ^ 8 * (ρ.etaDerivativeMajorantConstant ^ u.card * ε⁻¹ ^ 8 * ρ.etaAuxiliaryCoordLineProduct u ε x i a t)

Eight-fold periodic integration by parts with the derivative integral replaced by the honest auxiliary-periodization majorant.

theorem Anderson4D.SmoothCutoff.norm_fourierCoeffOn_etaPeriodizationCoordLineProductC_le {ι : Type u_1} [DecidableEq ι] (ρ : SmoothCutoff) (u : Finset ι) {ε : ℝ} (hε : 0 < ε) (x : ι → R4) (i : ι → Fin dim) (a : ι → ℝ) {n : ℤ} (hn : n ≠ 0) : ‖fourierCoeffOn ⋯ (ρ.etaPeriodizationCoordLineProductC u ε x i a) n‖ ≤ |↑n|⁻¹ ^ 8 * (2 * Real.pi)⁻¹ * (↑u.card ^ 8 * ρ.etaDerivativeMajorantConstant ^ u.card * ε⁻¹ ^ 8) * ∫ (t : ℝ) in -Real.pi..Real.pi, ρ.etaAuxiliaryCoordLineProduct u ε x i a t

Pulled-constant form of the preceding estimate. This is the reusable |n|⁻⁸ Fourier-decay statement; the remaining integral contains only true auxiliary-cutoff periodizations.