LeanPool.AnomalousDiffusion.AVenhance.Infra.Classical.GalerkinGenerator

The positive real Fourier coefficient derivative formula iterates to every ordered spatial derivative: finite projection commutes with each such derivative.

source

theorem AVenhance.Infra.Classical.realFourierModeFin_expansion_eq_periodicToTorus (N : ℕ) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) :

Parabolic.FourierGalerkin.modeExpansion (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) c = Torus.periodicToTorus (realFourierModeAmbientExpansion N c)

Finite real Fourier synthesis agrees with the ambient smooth periodic synthesis on the quotient torus.

source

theorem AVenhance.Infra.Classical.frozenWeakFormCoefficient_eq_projectedGenerator (N : ℕ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (κ t : ℝ) (ht : t ∈ Set.Icc 0 1) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) (hb : Continuous (b t)) :

(Parabolic.FourierGalerkin.frozenWeakFormCoefficient b κ (Parabolic.FourierGalerkin.realFourierModeFin N) (Parabolic.FourierGalerkin.realFourierModeGradFin N) t) c = Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => κ * spaceLap (realFourierModeAmbientExpansion N c) x - Homogenization.vecDot (b t x) (spaceGrad (realFourierModeAmbientExpansion N c) x))

On a finite real Fourier span, the weak matrix is precisely the orthogonal projection of κ Δu - b · ∇u. The diffusion part is identified by periodic integration by parts, while the drift part is expanded directly in the finite Fourier synthesis.

source

theorem AVenhance.Infra.Classical.realFourierProjection_product_norm_le (N : ℕ) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) (f : Homogenization.Vec 2 → ℝ) (hf : Continuous f) {B : ℝ} (_hB : 0 ≤ B) (hbound : ∀ (x : Homogenization.Vec 2), ‖f x‖ ≤ B) :

‖Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => f x * realFourierModeAmbientExpansion N c x)‖ ≤ B * ‖c‖

Multiplication by a bounded smooth periodic function followed by Fourier projection is bounded by the multiplier's uniform norm. The finite Fourier synthesis has exactly the coefficient-space L² norm.

source

noncomputable def AVenhance.Infra.Classical.realFourierProjectionCLM (N : ℕ) :

↥Parabolic.FourierGalerkin.ScalarTorusL2 →L[ℝ ] Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)

The real Fourier projection as a continuous linear map from torus L² to coefficients.

Equations

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

Instances For

source

@[simp]

theorem AVenhance.Infra.Classical.realFourierProjectionCLM_apply (N : ℕ) (f : ↥Parabolic.FourierGalerkin.ScalarTorusL2) (i : Fin (Parabolic.FourierGalerkin.RealFourierDimension N)) :

((realFourierProjectionCLM N) f).ofLp i = inner ℝ f (Parabolic.FourierGalerkin.realFourierModeL2 N i)

source

theorem AVenhance.Infra.Classical.realFourierModeProjectionCoefficients_eq_CLM (N : ℕ) {f : Parabolic.FourierGalerkin.Torus → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) :

Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) f = (realFourierProjectionCLM N) (MeasureTheory.MemLp.toLp f hf)

Integral-defined projection coefficients agree with the continuous L² projection map.

source

Real Fourier projection is additive on square-integrable inputs.

source

theorem AVenhance.Infra.Classical.realFourierModeProjectionCoefficients_smul (N : ℕ) (a : ℝ) {f : Parabolic.FourierGalerkin.Torus → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) :

Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (a • f) = a • Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) f

Real Fourier projection is homogeneous on square-integrable inputs.

source

Real Fourier projection is subtractive on square-integrable inputs.

source

theorem AVenhance.Infra.Classical.exists_uniform_bound_of_continuous_periodic (f : Homogenization.Vec 2 → ℝ) (hf : Continuous f) (hper : IsZ2Periodic f) :

∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Homogenization.Vec 2), ‖f x‖ ≤ C

A continuous integer-periodic scalar function is bounded on the whole space.

source

theorem AVenhance.Infra.Classical.memLp_periodicToTorus_real {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) (hper : IsZ2Periodic f) :

MeasureTheory.MemLp (Torus.periodicToTorus f) 2 MeasureTheory.volume

The torus representative of a continuous periodic scalar is square-integrable.

source

theorem AVenhance.Infra.Classical.realFourierProjectionCoefficients_norm_le_uniform (N : ℕ) (f : Homogenization.Vec 2 → ℝ) (hf : Continuous f) (hper : IsZ2Periodic f) {B : ℝ} (hB : 0 ≤ B) (hbound : ∀ (x : Homogenization.Vec 2), ‖f x‖ ≤ B) :

‖Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus f)‖ ≤ B

Fourier projection of a smooth periodic scalar is bounded in coefficient norm by any global uniform bound for the scalar.

source

theorem AVenhance.Infra.Classical.GalerkinGenerator.continuous_listSum (L : List (Homogenization.Vec 2 → ℝ)) (hL : ∀ f ∈ L, Continuous f) :

Continuous L.sum

source

theorem AVenhance.Infra.Classical.GalerkinGenerator.periodic_listSum (L : List (Homogenization.Vec 2 → ℝ)) (hL : ∀ f ∈ L, IsZ2Periodic f) :

IsZ2Periodic L.sum

source

theorem AVenhance.Infra.Classical.realFourierProjectionCoefficients_listSum (N : ℕ) (L : List (Homogenization.Vec 2 → ℝ)) (hcont : ∀ f ∈ L, Continuous f) (hper : ∀ f ∈ L, IsZ2Periodic f) :

Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus L.sum) = (List.map (fun (f : Homogenization.Vec 2 → ℝ) => Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus f)) L).sum

Fourier projection commutes with finite sums of continuous periodic ambient functions.

source

theorem AVenhance.Infra.Classical.realFourierProjectionCoefficients_listSum_norm_le (N : ℕ) (L : List (Homogenization.Vec 2 → ℝ)) (hcont : ∀ f ∈ L, Continuous f) (hper : ∀ f ∈ L, IsZ2Periodic f) :

‖Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus L.sum)‖ ≤ (List.map (fun (f : Homogenization.Vec 2 → ℝ) => ‖Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus f)‖) L).sum

The norm of a projected finite list sum is bounded by the sum of the projected term norms.

source

theorem AVenhance.Infra.Classical.classicalWordDerivative_finsetSum {ι : Type u_1} (s : Finset ι) (f : ι → Homogenization.Vec 2 → ℝ) (hf : ∀ i ∈ s, ContDiff ℝ (↑⊤) (f i)) (w : List (Fin 2)) :

(classicalWordDerivative w fun (x : Homogenization.Vec 2) => ∑ i ∈ s, f i x) = fun (x : Homogenization.Vec 2) => ∑ i ∈ s, classicalWordDerivative w (f i) x

Ordered spatial derivatives distribute over a finite sum of smooth scalar functions.

source

theorem AVenhance.Infra.Classical.classicalWordDerivative_sub (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) :

(classicalWordDerivative w fun (x : Homogenization.Vec 2) => f x - g x) = fun (x : Homogenization.Vec 2) => classicalWordDerivative w f x - classicalWordDerivative w g x

Ordered spatial derivatives commute with subtraction.

source

theorem AVenhance.Infra.Classical.classicalWordDerivative_const_mul (w : List (Fin 2)) (a : ℝ) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) :

(classicalWordDerivative w fun (x : Homogenization.Vec 2) => a * f x) = fun (x : Homogenization.Vec 2) => a * classicalWordDerivative w f x

Ordered spatial derivatives commute with multiplication by a real constant.

source

theorem AVenhance.Infra.Classical.classicalWordDerivative_spaceLap (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) :

(classicalWordDerivative w fun (x : Homogenization.Vec 2) => spaceLap f x) = fun (x : Homogenization.Vec 2) => spaceLap (classicalWordDerivative w f) x

Spatial derivatives commute with the Laplacian on smooth functions.