Coordinate derivatives of the real Fourier modes used by the Galerkin system.

@[instance_reducible]

noncomputable def classicalGalerkinMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

Use normalized Haar measure on the unit circle for periodic integrals.

Equations

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

theorem AVenhance.Infra.Classical.LinearIntegralSolution.continuousLinearMap_transform {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {A : ℝ → E →L[ℝ] E} {f y : ℝ → E} {y₀ : E} {a b : ℝ} (hab : a ≤ b) (hy : ODE.IsLinearIntegralSolution A f y₀ a b y) (hRhs : IntervalIntegrable (ODE.linearRhs A f y) MeasureTheory.volume a b) (L : E →L[ℝ] E) : ODE.IsLinearIntegralSolution A (fun (t : ℝ) => L (f t) + L ((A t) (y t)) - (A t) (L (y t))) (L y₀) a b fun (t : ℝ) => L (y t)

Applying a fixed continuous linear map to a finite-dimensional linear ODE solution adds the commutator of that map with the ODE operator to the transformed forcing.

theorem AVenhance.Infra.Classical.GalerkinModeCalculus.torusCharacter_line_eq {n : ℕ} (i : Fin (n + 1)) (k : Fin (n + 1) → ℤ) (z : Homogenization.Vec n) (t : ℝ) : Torus.torusCharacter k (i.insertNth t z) = (fourier (-k i)) ↑t * ∏ j : Fin n, (fourier (-k (i.succAbove j))) ↑(z j)

theorem AVenhance.Infra.Classical.GalerkinModeCalculus.torusCharacter_line_hasDerivAt {n : ℕ} (i : Fin (n + 1)) (k : Fin (n + 1) → ℤ) (z : Homogenization.Vec n) (t : ℝ) : HasDerivAt (fun (s : ℝ) => Torus.torusCharacter k (i.insertNth s z)) (-2 * ↑Real.pi * Complex.I * ↑(k i) * Torus.torusCharacter k (i.insertNth t z)) t

theorem AVenhance.Infra.Classical.GalerkinModeCalculus.coordDeriv_torusCharacter {n : ℕ} (i : Fin (n + 1)) (k : Fin (n + 1) → ℤ) (x : Homogenization.Vec (n + 1)) : Torus.coordDeriv i (Torus.torusCharacter k) x = -2 * ↑Real.pi * Complex.I * ↑(k i) * Torus.torusCharacter k x

theorem AVenhance.Infra.Classical.coordDeriv_re {f : Homogenization.Vec 2 → ℂ} (hf : ContDiff ℝ 1 f) (i : Fin 2) (x : Homogenization.Vec 2) : Torus.coordDeriv i (fun (y : Homogenization.Vec 2) => ↑(f y).re) x = ↑(Torus.coordDeriv i f x).re

theorem AVenhance.Infra.Classical.coordDeriv_im {f : Homogenization.Vec 2 → ℂ} (hf : ContDiff ℝ 1 f) (i : Fin 2) (x : Homogenization.Vec 2) : Torus.coordDeriv i (fun (y : Homogenization.Vec 2) => ↑(f y).im) x = ↑(Torus.coordDeriv i f x).im

theorem AVenhance.Infra.Classical.GalerkinModeCalculus.spaceGrad_re_eq_coordDeriv {f : Homogenization.Vec 2 → ℂ} (hf : ContDiff ℝ 1 f) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => (f y).re) x i = (Torus.coordDeriv i f x).re

theorem AVenhance.Infra.Classical.GalerkinModeCalculus.spaceGrad_im_eq_coordDeriv {f : Homogenization.Vec 2 → ℂ} (hf : ContDiff ℝ 1 f) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => (f y).im) x i = (Torus.coordDeriv i f x).im

theorem AVenhance.Infra.Classical.GalerkinModeCalculus.spaceGrad_const_smul {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (c : ℝ) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => c * f y) x i = c * spaceGrad f x i

def AVenhance.Infra.Classical.realFourierModeIndexSwap {N : ℕ} : Parabolic.FourierGalerkin.RealFourierIndex N → Parabolic.FourierGalerkin.RealFourierIndex N

Exchange the sine and cosine modes at each frequency, fixing the constant mode.

Equations

• AVenhance.Infra.Classical.realFourierModeIndexSwap none = none
• AVenhance.Infra.Classical.realFourierModeIndexSwap (some (p, false)) = some (p, true)
• AVenhance.Infra.Classical.realFourierModeIndexSwap (some (p, true)) = some (p, false)

theorem AVenhance.Infra.Classical.realFourierModeIndexSwap_involutive {N : ℕ} (a : Parabolic.FourierGalerkin.RealFourierIndex N) : realFourierModeIndexSwap (realFourierModeIndexSwap a) = a

noncomputable def AVenhance.Infra.Classical.realFourierModeDerivativeScale {N : ℕ} (a : Parabolic.FourierGalerkin.RealFourierIndex N) (i : Fin 2) : ℝ

The signed frequency multiplier in the coordinate derivative of a real mode.

Equations

• AVenhance.Infra.Classical.realFourierModeDerivativeScale none i = 0
• AVenhance.Infra.Classical.realFourierModeDerivativeScale (some (p, false)) i = -(2 * Real.pi * ↑(AVenhance.Infra.Parabolic.FourierGalerkin.representativeFrequency p i))
• AVenhance.Infra.Classical.realFourierModeDerivativeScale (some (p, true)) i = 2 * Real.pi * ↑(AVenhance.Infra.Parabolic.FourierGalerkin.representativeFrequency p i)

theorem AVenhance.Infra.Classical.representativeFrequency_coordinate_abs_le (N : ℕ) (p : ↥(Parabolic.FourierGalerkin.positiveFrequencyRepresentatives N)) (i : Fin 2) : |Parabolic.FourierGalerkin.representativeFrequency p i| ≤ ↑N

theorem AVenhance.Infra.Classical.realFourierModeDerivativeScale_abs_le (N : ℕ) (a : Parabolic.FourierGalerkin.RealFourierIndex N) (i : Fin 2) : |realFourierModeDerivativeScale a i| ≤ 2 * Real.pi * ↑N

theorem AVenhance.Infra.Classical.realFourierModeDerivativeScale_swap (N : ℕ) (a : Parabolic.FourierGalerkin.RealFourierIndex N) (i : Fin 2) : realFourierModeDerivativeScale (realFourierModeIndexSwap a) i = -realFourierModeDerivativeScale a i

theorem AVenhance.Infra.Classical.spaceGrad_realFourierModeAmbient (N : ℕ) (a : Parabolic.FourierGalerkin.RealFourierIndex N) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (Parabolic.FourierGalerkin.realFourierModeAmbient N a) x i = match a with | none => 0 | some (p, false) => -(2 * Real.pi * ↑(Parabolic.FourierGalerkin.representativeFrequency p i)) * Parabolic.FourierGalerkin.realFourierModeAmbient N (realFourierModeIndexSwap a) x | some (p, true) => 2 * Real.pi * ↑(Parabolic.FourierGalerkin.representativeFrequency p i) * Parabolic.FourierGalerkin.realFourierModeAmbient N (realFourierModeIndexSwap a) x

A coordinate derivative of a real Fourier mode is the frequency factor times its paired sine or cosine mode.

noncomputable def AVenhance.Infra.Classical.realFourierModeAmbientExpansion (N : ℕ) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) : Homogenization.Vec 2 → ℝ

A finite real Fourier expansion written on Euclidean representatives.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Classical.GalerkinModeCalculus.contDiff_finset_sum {ι : Type u_1} (s : Finset ι) (f : ι → Homogenization.Vec 2 → ℝ) (hf : ∀ i ∈ s, ContDiff ℝ ⊤ (f i)) : ContDiff ℝ ⊤ fun (x : Homogenization.Vec 2) => ∑ i ∈ s, f i x

theorem AVenhance.Infra.Classical.GalerkinModeCalculus.spaceGrad_finset_sum {ι : Type u_1} (s : Finset ι) (f : ι → Homogenization.Vec 2 → ℝ) (hf : ∀ i ∈ s, ContDiff ℝ ⊤ (f i)) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => ∑ j ∈ s, f j y) x i = ∑ j ∈ s, spaceGrad (f j) x i

theorem AVenhance.Infra.Classical.GalerkinModeCalculus.spaceGrad_realConstant_mul {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (c : ℝ) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => c * f y) x i = c * spaceGrad f x i

theorem AVenhance.Infra.Classical.realFourierModeAmbientExpansion_contDiff (N : ℕ) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) : ContDiff ℝ ⊤ (realFourierModeAmbientExpansion N c)

theorem AVenhance.Infra.Classical.spaceGrad_realFourierModeAmbientExpansion (N : ℕ) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (realFourierModeAmbientExpansion N c) x i = ∑ j : Fin (Parabolic.FourierGalerkin.RealFourierDimension N), c.ofLp j * realFourierModeDerivativeScale ((Parabolic.FourierGalerkin.realFourierIndexEquivFin N).symm j) i * Parabolic.FourierGalerkin.realFourierModeAmbient N (realFourierModeIndexSwap ((Parabolic.FourierGalerkin.realFourierIndexEquivFin N).symm j)) x

Differentiating a finite Fourier expansion multiplies each coefficient by its frequency and replaces its cosine or sine mode with the paired mode. The result therefore stays in the same cutoff space.

noncomputable def AVenhance.Infra.Classical.GalerkinModeCalculus.realFourierModeIndexSwapFinEquiv (N : ℕ) : Fin (Parabolic.FourierGalerkin.RealFourierDimension N) ≃ Fin (Parabolic.FourierGalerkin.RealFourierDimension N)

Sine-cosine exchange transported to the finite Galerkin index set.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Classical.realFourierModeDerivativeCoefficients (N : ℕ) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) (i : Fin 2) : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)

Coefficients of the coordinate derivative of a finite Fourier expansion.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Classical.spaceGrad_realFourierModeAmbientExpansion_eq_derivativeExpansion (N : ℕ) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) (i : Fin 2) : (fun (x : Homogenization.Vec 2) => spaceGrad (realFourierModeAmbientExpansion N c) x i) = realFourierModeAmbientExpansion N (realFourierModeDerivativeCoefficients N c i)

Coordinate derivatives of a finite real Fourier expansion are represented by the explicit coefficient derivative map, without leaving the cutoff space.

theorem AVenhance.Infra.Classical.GalerkinModeCalculus.coefficient_norm_sq_eq_sum_sq {n : ℕ} (c : Parabolic.FourierGalerkin.Coefficients n) : ‖c‖ ^ 2 = ∑ j : Fin n, c.ofLp j ^ 2

theorem AVenhance.Infra.Classical.realFourierModeDerivativeCoefficients_norm_le (N : ℕ) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) (i : Fin 2) : ‖realFourierModeDerivativeCoefficients N c i‖ ≤ 2 * Real.pi * ↑N * ‖c‖

The coordinate derivative map has the expected cutoff-dependent Fourier multiplier bound. The differentiated-energy estimates below will remove this frequency factor by measuring one more spatial derivative.

noncomputable def AVenhance.Infra.Classical.GalerkinModeCalculus.realFourierModeDerivativeLinearMap (N : ℕ) (i : Fin 2) : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N) →ₗ[ℝ] Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)

Coordinate differentiation of Fourier coefficients as a linear map.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Classical.realFourierModeDerivativeMap (N : ℕ) (i : Fin 2) : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N) →L[ℝ] Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)

The coordinate derivative on the finite Fourier coefficient space as a continuous linear map. Its operator norm is bounded by the largest retained frequency.

Equations

• AVenhance.Infra.Classical.realFourierModeDerivativeMap N i = (AVenhance.Infra.Classical.GalerkinModeCalculus.realFourierModeDerivativeLinearMap N i).mkContinuous (2 * Real.pi * ↑N) ⋯

@[simp]

theorem AVenhance.Infra.Classical.realFourierModeDerivativeMap_apply (N : ℕ) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) (i : Fin 2) : (realFourierModeDerivativeMap N i) c = realFourierModeDerivativeCoefficients N c i

def AVenhance.Infra.Classical.realFourierWordDerivativeCoefficients (N : ℕ) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) : List (Fin 2) → Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)

The coefficient transform for an ordered word of coordinate derivatives.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Classical.realFourierWordDerivativeCoefficients N c [] = c

def AVenhance.Infra.Classical.realFourierWordDerivativeMap (N : ℕ) : List (Fin 2) → Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N) →L[ℝ] Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)

The bounded linear map on Fourier coefficients associated with a derivative word.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Classical.realFourierWordDerivativeMap N (i :: w) = AVenhance.Infra.Classical.realFourierModeDerivativeMap N i ∘SL AVenhance.Infra.Classical.realFourierWordDerivativeMap N w

@[simp]

theorem AVenhance.Infra.Classical.realFourierWordDerivativeMap_apply (N : ℕ) (w : List (Fin 2)) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) : (realFourierWordDerivativeMap N w) c = realFourierWordDerivativeCoefficients N c w

theorem AVenhance.Infra.Classical.classicalWordDerivative_realFourierModeAmbientExpansion (N : ℕ) (w : List (Fin 2)) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) : classicalWordDerivative w (realFourierModeAmbientExpansion N c) = realFourierModeAmbientExpansion N (realFourierWordDerivativeCoefficients N c w)

Every ordered spatial derivative of a finite Fourier expansion remains in its original cutoff, with coefficients given by the corresponding word derivative map.

noncomputable def AVenhance.Infra.Classical.GalerkinModeCalculus.standardUnitTorusVolume : MeasureTheory.Measure Parabolic.FourierGalerkin.Torus

Product of the normalized Haar measures on the two circle factors.

Equations

• AVenhance.Infra.Classical.GalerkinModeCalculus.standardUnitTorusVolume = MeasureTheory.Measure.pi fun (x : Fin 2) => AddCircle.haarAddCircle

theorem AVenhance.Infra.Classical.GalerkinModeCalculus.galerkinTorusVolume_eq_standard : MeasureTheory.volume = standardUnitTorusVolume

theorem AVenhance.Infra.Classical.GalerkinModeCalculus.integral_periodicToTorus_mul_eq_unitCell {f g : Homogenization.Vec 2 → ℝ} : ∫ (x : Parabolic.FourierGalerkin.Torus), Torus.periodicToTorus f x * Torus.periodicToTorus g x = ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, f x * g x

theorem AVenhance.Infra.Classical.realFourierModeDerivativeCoefficients_projection (N : ℕ) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hper : IsZ2Periodic f) (i : Fin 2) : realFourierModeDerivativeCoefficients N (Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus f)) i = Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => spaceGrad f x i)

Fourier projection commutes with a coordinate derivative. The weak gradient identity follows from periodic integration by parts and the fact that differentiating a retained mode stays in the same cutoff.