Smooth sample paths of the mollified noise

The torus is represented in the project as a product of quotient groups, for which mathlib does not currently expose a smooth-manifold structure. We therefore use the standard equivalent definition: a torus function is smooth when its periodic pullback to ℝ⁴ is smooth. This file proves that property almost surely for every fixed positive mollification scale.

noncomputable def Anderson4D.torusQuotient (x : R4) : T4

The quotient map from the universal cover ℝ⁴ to the torus.

Equations

• Anderson4D.torusQuotient x i = ↑(x i)

def Anderson4D.frequencyPhase (k : Z4) : R4 →L[ℝ] ℝ

The real phase k · x, as a continuous linear functional.

Equations

• Anderson4D.frequencyPhase k = ∑ i : Fin Anderson4D.dim, ↑(k i) • ContinuousLinearMap.proj i

@[simp]

theorem Anderson4D.frequencyPhase_apply (k : Z4) (x : R4) : (frequencyPhase k) x = ∑ i : Fin dim, ↑(k i) * x i

noncomputable def Anderson4D.realPlaneWave (t : ℝ) : ℂ

The one-dimensional unit-modulus plane wave.

Equations

• Anderson4D.realPlaneWave t = Complex.exp (Complex.I * ↑t)

theorem Anderson4D.contDiff_realPlaneWave (n : ℕ∞) : ContDiff ℝ (↑n) realPlaneWave

theorem Anderson4D.iteratedDeriv_realPlaneWave (n : ℕ) : iteratedDeriv n realPlaneWave = fun (t : ℝ) => Complex.I ^ n * realPlaneWave t

theorem Anderson4D.norm_iteratedFDeriv_realPlaneWave (n : ℕ) (t : ℝ) : ‖iteratedFDeriv ℝ n realPlaneWave t‖ = 1

noncomputable def Anderson4D.liftedChar (k : Z4) : R4 → ℂ

A Fourier character pulled back to the universal cover.

Equations

• Anderson4D.liftedChar k = Anderson4D.realPlaneWave ∘ ⇑(Anderson4D.frequencyPhase k)

theorem Anderson4D.contDiff_liftedChar (k : Z4) (n : ℕ∞) : ContDiff ℝ (↑n) (liftedChar k)

theorem Anderson4D.liftedChar_eq_charT4_torusQuotient (k : Z4) (x : R4) : liftedChar k x = charT4 k (torusQuotient x)

Pulling a project character back along the quotient map gives the usual Euclidean plane wave.

theorem Anderson4D.norm_frequencyPhase_le (k : Z4) : ‖frequencyPhase k‖ ≤ latticePolynomialWeight 1 k

The phase functional is bounded by the project's degree-one lattice weight.

theorem Anderson4D.norm_iteratedFDeriv_liftedChar_le (n : ℕ) (k : Z4) (x : R4) : ‖iteratedFDeriv ℝ n (liftedChar k) x‖ ≤ latticePolynomialWeight n k

Uniform derivative bound for a lifted Fourier character. It is tailored to the weighted summability theorem in NoiseRegularity.

noncomputable def Anderson4D.NoiseModel.smoothMollifiedTerm (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (k : Z4) (x : R4) : ℂ

One Fourier summand of the mollified field, pulled back to ℝ⁴ and including the Lebesgue white-noise normalization.

Equations

• M.smoothMollifiedTerm ρ ε ω k x = ↑Anderson4D.NoiseModel.whiteNoiseFourierScale * M.mollifiedRandomCoeff ρ ε k ω * Anderson4D.liftedChar k x

theorem Anderson4D.NoiseModel.contDiff_smoothMollifiedTerm (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (k : Z4) (n : ℕ∞) : ContDiff ℝ (↑n) (M.smoothMollifiedTerm ρ ε ω k)

theorem Anderson4D.NoiseModel.norm_iteratedFDeriv_smoothMollifiedTerm_le (M : NoiseModel) (r : ℕ) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (k : Z4) (x : R4) : ‖iteratedFDeriv ℝ r (M.smoothMollifiedTerm ρ ε ω k) x‖ ≤ ‖whiteNoiseFourierScale‖ * ‖M.weightedMollifiedRandomCoeff r ρ ε k ω‖

The derivative of a Fourier summand is controlled by the corresponding polynomially weighted random coefficient.

noncomputable def Anderson4D.NoiseModel.xiEpsLiftC (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (x : R4) : ℂ

Complex pullback of the mollified Fourier series to the universal cover.

Equations

• M.xiEpsLiftC ρ ε ω x = ∑' (k : Anderson4D.Z4), M.smoothMollifiedTerm ρ ε ω k x

theorem Anderson4D.NoiseModel.contDiff_xiEpsLiftC_of_weightedSummable (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (hω : ∀ (r : ℕ), Summable fun (k : Z4) => ‖M.weightedMollifiedRandomCoeff r ρ ε k ω‖) : ContDiff ℝ (↑⊤) (M.xiEpsLiftC ρ ε ω)

Summability at every polynomial weight implies smoothness of the complex periodic pullback.

noncomputable def Anderson4D.NoiseModel.xiEpsLift (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (x : R4) : ℝ

Real-valued smooth pullback of the mollified noise.

Equations

• M.xiEpsLift ρ ε ω x = (M.xiEpsLiftC ρ ε ω x).re

theorem Anderson4D.NoiseModel.xiEpsLift_eq_xiEps_torusQuotient (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (x : R4) : M.xiEpsLift ρ ε ω x = M.xiEps ρ ε ω (torusQuotient x)

The smooth Euclidean pullback is exactly the project field evaluated after quotienting to the torus.

theorem Anderson4D.NoiseModel.contDiff_xiEpsLift_of_weightedSummable (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (hω : ∀ (r : ℕ), Summable fun (k : Z4) => ‖M.weightedMollifiedRandomCoeff r ρ ε k ω‖) : ContDiff ℝ (↑⊤) (M.xiEpsLift ρ ε ω)

theorem Anderson4D.NoiseModel.ae_contDiff_xiEpsLift (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : ∀ᵐ (ω : M.Ω), ContDiff ℝ (↑⊤) (M.xiEpsLift ρ ε ω)

For every fixed positive scale, the mollified field has a smooth periodic pullback almost surely.

theorem Anderson4D.NoiseModel.ae_forall_nat_scale_contDiff_xiEpsLift (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) : ∀ᵐ (ω : M.Ω), ∀ (n : ℕ), ContDiff ℝ (↑⊤) (M.xiEpsLift ρ (ε n) ω)

A single probability-one event works simultaneously for every member of an arbitrary countable positive scale family. This is the form used for a prescribed sequence εₙ → 0.