Modes

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.pairFrequency_injective {p q : ℤ × ℤ} (h : pairFrequency p = pairFrequency q) : p = q

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.integral_mFourier (k : Fin 2 → ℤ) : ∫ (x : Torus), (UnitAddTorus.mFourier k) x = if k = 0 then 1 else 0

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.mFourierCoeff_mFourier (k l : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (⇑(UnitAddTorus.mFourier l)) k = if k = l then 1 else 0

theorem AVenhance.Infra.Parabolic.FourierGalerkin.complexFourierPartialSumComplex_mFourier {N : ℕ} (k : Fin 2 → ℤ) (hk : frequencyPair k ∈ symmetricFrequencyBox N) (x : Torus) : complexFourierPartialSumComplex N (⇑(UnitAddTorus.mFourier k)) x = (UnitAddTorus.mFourier k) x

A Fourier character in the cutoff box is exactly fixed by the finite Fourier sum.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.integrable_mFourier_mul_of_continuous {f : Torus → ℂ} (hf : Continuous f) (k : Fin 2 → ℤ) : MeasureTheory.Integrable (fun (x : Torus) => (UnitAddTorus.mFourier (-k)) x * f x) MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.mFourierCoeff_add_of_continuous {f g : Torus → ℂ} (hf : Continuous f) (hg : Continuous g) (k : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => f x + g x) k = UnitAddTorus.mFourierCoeff f k + UnitAddTorus.mFourierCoeff g k

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.mFourierCoeff_const_mul {f : Torus → ℂ} (c : ℂ) (k : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => c * f x) k = c * UnitAddTorus.mFourierCoeff f k

theorem AVenhance.Infra.Parabolic.FourierGalerkin.complexFourierPartialSumComplex_add {N : ℕ} {f g : Torus → ℂ} (hf : Continuous f) (hg : Continuous g) (x : Torus) : complexFourierPartialSumComplex N (fun (y : Torus) => f y + g y) x = complexFourierPartialSumComplex N f x + complexFourierPartialSumComplex N g x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.complexFourierPartialSumComplex_const_mul {N : ℕ} {f : Torus → ℂ} (c : ℂ) (x : Torus) : complexFourierPartialSumComplex N (fun (y : Torus) => c * f y) x = c * complexFourierPartialSumComplex N f x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.ofReal_sqrtTwo_mul_re (z : ℂ) : ↑(√2 * z.re) = ↑(√2 / 2) * (z + star z)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.ofReal_sqrtTwo_mul_im (z : ℂ) : ↑(√2 * z.im) = ↑(√2 / 2) * -Complex.I * (z - star z)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.mFourier_star_at (k : Fin 2 → ℤ) (x : Torus) : star ((UnitAddTorus.mFourier k) x) = (UnitAddTorus.mFourier (-k)) x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.integrable_mFourier (k : Fin 2 → ℤ) : MeasureTheory.Integrable (fun (x : Torus) => (UnitAddTorus.mFourier k) x) MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.integral_re_mFourier (k : Fin 2 → ℤ) : ∫ (x : Torus), ((UnitAddTorus.mFourier k) x).re = if k = 0 then 1 else 0

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.integral_im_mFourier (k : Fin 2 → ℤ) : ∫ (x : Torus), ((UnitAddTorus.mFourier k) x).im = 0

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.integrable_re_mFourier (k : Fin 2 → ℤ) : MeasureTheory.Integrable (fun (x : Torus) => ((UnitAddTorus.mFourier k) x).re) MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.integrable_im_mFourier (k : Fin 2 → ℤ) : MeasureTheory.Integrable (fun (x : Torus) => ((UnitAddTorus.mFourier k) x).im) MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.integral_re_fourierProduct (k l : Fin 2 → ℤ) : ∫ (x : Torus), ((UnitAddTorus.mFourier k) x * (UnitAddTorus.mFourier l) x).re = if k = -l then 1 else 0

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.integral_im_fourierProduct (k l : Fin 2 → ℤ) : ∫ (x : Torus), ((UnitAddTorus.mFourier k) x * (UnitAddTorus.mFourier l) x).im = 0

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.two_re_mul_re (z w : ℂ) : 2 * z.re * w.re = (z * w).re + (z * star w).re

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.two_im_mul_im (z w : ℂ) : 2 * z.im * w.im = (z * star w).re - (z * w).re

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.two_re_mul_im (z w : ℂ) : 2 * z.re * w.im = (z * w).im - (z * star w).im

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.two_im_mul_re (z w : ℂ) : 2 * z.im * w.re = (z * w).im + (z * star w).im

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.mFourier_add_at (k l : Fin 2 → ℤ) (x : Torus) : (UnitAddTorus.mFourier (k + l)) x = (UnitAddTorus.mFourier k) x * (UnitAddTorus.mFourier l) x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.mFourier_sub_at (k l : Fin 2 → ℤ) (x : Torus) : (UnitAddTorus.mFourier (k - l)) x = (UnitAddTorus.mFourier k) x * star ((UnitAddTorus.mFourier l) x)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.integral_re_mul_re (k l : Fin 2 → ℤ) : ∫ (x : Torus), ((UnitAddTorus.mFourier k) x).re * ((UnitAddTorus.mFourier l) x).re = (if k = -l then 1 / 2 else 0) + if k = l then 1 / 2 else 0

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.integral_im_mul_im (k l : Fin 2 → ℤ) : ∫ (x : Torus), ((UnitAddTorus.mFourier k) x).im * ((UnitAddTorus.mFourier l) x).im = (if k = l then 1 / 2 else 0) - if k = -l then 1 / 2 else 0

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.integral_re_mul_im (k l : Fin 2 → ℤ) : ∫ (x : Torus), ((UnitAddTorus.mFourier k) x).re * ((UnitAddTorus.mFourier l) x).im = 0

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.integral_im_mul_re (k l : Fin 2 → ℤ) : ∫ (x : Torus), ((UnitAddTorus.mFourier k) x).im * ((UnitAddTorus.mFourier l) x).re = 0

def AVenhance.Infra.Parabolic.FourierGalerkin.representativeFrequency {N : ℕ} (p : ↥(positiveFrequencyRepresentatives N)) : Fin 2 → ℤ

The ordered integer frequency of a positive representative.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.representativeFrequency p = AVenhance.Infra.Parabolic.FourierGalerkin.pairFrequency ↑p

theorem AVenhance.Infra.Parabolic.FourierGalerkin.representativeFrequency_mem_box {N : ℕ} (p : ↥(positiveFrequencyRepresentatives N)) : frequencyPair (representativeFrequency p) ∈ symmetricFrequencyBox N

theorem AVenhance.Infra.Parabolic.FourierGalerkin.representativeFrequency_injective {N : ℕ} {p q : ↥(positiveFrequencyRepresentatives N)} (h : representativeFrequency p = representativeFrequency q) : p = q

theorem AVenhance.Infra.Parabolic.FourierGalerkin.representativeFrequency_ne_neg {N : ℕ} (p q : ↥(positiveFrequencyRepresentatives N)) : representativeFrequency p ≠ -representativeFrequency q

@[reducible, inline]

abbrev AVenhance.Infra.Parabolic.FourierGalerkin.RealFourierIndex (N : ℕ) : Type

The finite real Fourier index: one constant mode and a cosine/sine pair for each representative. Bool.false selects cosine and Bool.true selects sine.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.RealFourierIndex N = Option (↥(AVenhance.Infra.Parabolic.FourierGalerkin.positiveFrequencyRepresentatives N) × Bool)

@[instance_reducible]

noncomputable instance AVenhance.Infra.Parabolic.FourierGalerkin.realFourierIndexFintype (N : ℕ) : Fintype (RealFourierIndex N)

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.realFourierIndexFintype N = id inferInstance

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierMode (N : ℕ) (a : RealFourierIndex N) (x : Torus) : ℝ

Real trigonometric modes on the unit torus, normalized so nonconstant modes have norm one.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Parabolic.FourierGalerkin.realFourierMode N none x = 1

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierMode_cos_complexExpansion (N : ℕ) (p : ↥(positiveFrequencyRepresentatives N)) (x : Torus) : ↑(realFourierMode N (some (p, false)) x) = ↑(√2 / 2) * ((UnitAddTorus.mFourier (representativeFrequency p)) x + (UnitAddTorus.mFourier (-representativeFrequency p)) x)

Complexification of a cosine mode as the two characters at opposite frequencies.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierMode_sin_complexExpansion (N : ℕ) (p : ↥(positiveFrequencyRepresentatives N)) (x : Torus) : ↑(realFourierMode N (some (p, true)) x) = ↑(√2 / 2) * -Complex.I * ((UnitAddTorus.mFourier (representativeFrequency p)) x - (UnitAddTorus.mFourier (-representativeFrequency p)) x)

Complexification of a sine mode as the two characters at opposite frequencies.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierMode_continuous (N : ℕ) (a : RealFourierIndex N) : Continuous (realFourierMode N a)

Each real trigonometric mode is continuous on the quotient torus.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeAmbient (N : ℕ) (a : RealFourierIndex N) (x : Homogenization.Vec 2) : ℝ

The corresponding smooth periodic function on Euclidean representatives.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeAmbient N none x = 1

theorem AVenhance.Infra.Parabolic.FourierGalerkin.representativeFrequency_ne_zero {N : ℕ} (p : ↥(positiveFrequencyRepresentatives N)) : representativeFrequency p ≠ 0

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.representativeFrequency_eq_iff {N : ℕ} (p q : ↥(positiveFrequencyRepresentatives N)) : representativeFrequency p = representativeFrequency q ↔ p = q

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierMode_orthonormal (N : ℕ) (a b : RealFourierIndex N) : ∫ (x : Torus), realFourierMode N a x * realFourierMode N b x = if a = b then 1 else 0

The real modes on a symmetric frequency box form an orthonormal family.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierMode_eq_periodicToTorus (N : ℕ) (a : RealFourierIndex N) : realFourierMode N a = Torus.periodicToTorus (realFourierModeAmbient N a)

The ambient representative transfers back to the mode on the quotient torus.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeAmbient_contDiff (N : ℕ) (a : RealFourierIndex N) : ContDiff ℝ ⊤ (realFourierModeAmbient N a)

The Euclidean real modes are smooth, including every derivative order.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeAmbient_periodic (N : ℕ) (a : RealFourierIndex N) : IsZ2Periodic (realFourierModeAmbient N a)

The Euclidean real modes are periodic in the lattice convention.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Modes.spaceGrad_periodic_of_smooth {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hper : IsZ2Periodic f) : IsZ2Periodic (spaceGrad f)

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeAmbientGrad (N : ℕ) (a : RealFourierIndex N) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The Euclidean gradient field attached to a real Fourier mode.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeAmbientGrad N a x = AVenhance.spaceGrad (AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeAmbient N a) x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeAmbientGrad_continuous (N : ℕ) (a : RealFourierIndex N) : Continuous (realFourierModeAmbientGrad N a)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeAmbientGrad_periodic (N : ℕ) (a : RealFourierIndex N) : IsZ2Periodic (realFourierModeAmbientGrad N a)

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeGrad (N : ℕ) (a : RealFourierIndex N) (x : Torus) : Homogenization.Vec 2

The periodic gradient mode on the quotient torus.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeGrad N a x = AVenhance.Infra.Torus.periodicToTorus (AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeAmbientGrad N a) x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierMode_cos_fourierCoeff (N : ℕ) (p : ↥(positiveFrequencyRepresentatives N)) (l : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (fun (y : UnitAddTorus (Fin 2)) => ↑(realFourierMode N (some (p, false)) y)) l = (↑(√2 / 2) * if l = representativeFrequency p then 1 else 0) + ↑(√2 / 2) * if l = -representativeFrequency p then 1 else 0

Complex Fourier coefficients of a real cosine mode are supported on its two opposite characters.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierMode_sin_fourierCoeff (N : ℕ) (p : ↥(positiveFrequencyRepresentatives N)) (l : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (fun (y : UnitAddTorus (Fin 2)) => ↑(realFourierMode N (some (p, true)) y)) l = (↑(√2 / 2) * -Complex.I * if l = representativeFrequency p then 1 else 0) - ↑(√2 / 2) * -Complex.I * if l = -representativeFrequency p then 1 else 0

Complex Fourier coefficients of a real sine mode are supported on its two opposite characters, with the imaginary signs fixed by the Fourier convention.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierMode_const_fourierCoeff (N : ℕ) (l : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (fun (y : UnitAddTorus (Fin 2)) => ↑(realFourierMode N none y)) l = if l = 0 then 1 else 0

The constant real mode has only its zero Fourier coefficient.