Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Classical.GalerkinDerivative

Commutator forcing bounds for differentiated finite Fourier paths.

@[instance_reducible]

noncomputable def classicalDerivativeMeasureSpaceUnitAddCircle :

MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

Instances For

theorem classicalDerivativeMeasureIsAddHaarUnitAddCircle :

MeasureTheory.volume.IsAddHaarMeasure

theorem classicalDerivativeProbabilityUnitAddCircle :

MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem classicalDerivativeProbabilityTorus :

MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

noncomputable def AVenhance.Infra.Classical.classicalWordCommutatorTerms (w : List (Fin 2)) (b u : Homogenization.Vec 2 → ℝ) (j : Fin 2) :

List (Homogenization.Vec 2 → ℝ)

The finite list of scalar products in one component of the transport commutator.

Equations

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

Instances For

theorem AVenhance.Infra.Classical.GalerkinDerivative.classicalWordDerivative_periodic (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hper : IsZ2Periodic f) :

IsZ2Periodic (classicalWordDerivative w f)

theorem AVenhance.Infra.Classical.GalerkinDerivative.classicalPeriodic_mul {f g : Homogenization.Vec 2 → ℝ} (hf : IsZ2Periodic f) (hg : IsZ2Periodic g) :

IsZ2Periodic fun (x : Homogenization.Vec 2) => f x * g x

theorem AVenhance.Infra.Classical.GalerkinDerivative.listMapSum_mono {α : Type} (L : List α) (f g : α → ℝ) (h : ∀ a ∈ L, f a ≤ g a) :

(List.map f L).sum ≤ (List.map g L).sum

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

Continuous L.sum

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

IsZ2Periodic L.sum

theorem AVenhance.Infra.Classical.GalerkinDerivative.classicalSpaceLap_contDiff (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) :

ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => spaceLap f x

theorem AVenhance.Infra.Classical.GalerkinDerivative.classicalSpaceLap_periodic {f : Homogenization.Vec 2 → ℝ} (hper : IsZ2Periodic f) :

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

theorem AVenhance.Infra.Classical.GalerkinDerivative.classicalTransport_contDiff (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) (hb : ContDiff ℝ (↑⊤) b) (hu : ContDiff ℝ (↑⊤) u) :

ContDiff ℝ (↑⊤) (classicalTransport b u)

theorem AVenhance.Infra.Classical.GalerkinDerivative.classicalTransport_periodic (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) (hbp : IsZ2Periodic b) (hup : IsZ2Periodic u) :

IsZ2Periodic (classicalTransport b u)

The coefficient derivative map commutes with Fourier projection of a smooth periodic field.

theorem AVenhance.Infra.Classical.GalerkinDerivative.classicalWordCommutatorTerms_continuous (w : List (Fin 2)) (b u : Homogenization.Vec 2 → ℝ) (hb : ContDiff ℝ (↑⊤) b) (hu : ContDiff ℝ (↑⊤) u) (j : Fin 2) (f : Homogenization.Vec 2 → ℝ) :

f ∈ classicalWordCommutatorTerms w b u j → Continuous f

theorem AVenhance.Infra.Classical.GalerkinDerivative.classicalWordCommutatorTerms_periodic (w : List (Fin 2)) (b u : Homogenization.Vec 2 → ℝ) (hbp : IsZ2Periodic b) (hup : IsZ2Periodic u) (j : Fin 2) (f : Homogenization.Vec 2 → ℝ) :

f ∈ classicalWordCommutatorTerms w b u j → IsZ2Periodic f

theorem AVenhance.Infra.Classical.classicalWordCommutatorExpansion_projection_norm_le (N : ℕ) (w : List (Fin 2)) (b : Homogenization.Vec 2 → ℝ) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) (j : Fin 2) {B : ℝ} (hB : 0 ≤ B) (hb : ContDiff ℝ (↑⊤) b) (hbp : IsZ2Periodic b) (hDb : ∀ p ∈ classicalWordCommutatorSplits w, ∀ (x : Homogenization.Vec 2), |classicalWordDerivative p.1 b x| ≤ B) :

‖Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus (classicalWordCommutatorExpansion w b fun (x : Homogenization.Vec 2) => spaceGrad (realFourierModeAmbientExpansion N c) x j))‖ ≤ (List.map (fun (p : List (Fin 2) × List (Fin 2)) => B * ‖(realFourierWordDerivativeMap N (j :: p.2)) c‖) (classicalWordCommutatorSplits w)).sum

A component commutator projection is bounded by the uniform drift derivative bound times the sum of the coefficient norms of the solution derivatives appearing in Leibniz's rule.

noncomputable def AVenhance.Infra.Classical.classicalWordTransportCommutatorExpansion (w : List (Fin 2)) (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) :

Homogenization.Vec 2 → ℝ

The full transport commutator is the sum over the two drift components.

Equations

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

Instances For

theorem AVenhance.Infra.Classical.classicalWordTransportCommutatorExpansion_projection_norm_le (N : ℕ) (w : List (Fin 2)) (b : Homogenization.Vec 2 → Homogenization.Vec 2) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) {B : ℝ} (hB : 0 ≤ B) (hb : ContDiff ℝ (↑⊤) b) (hbp : IsZ2Periodic b) (hDb : ∀ (j : Fin 2), ∀ p ∈ classicalWordCommutatorSplits w, ∀ (x : Homogenization.Vec 2), |classicalWordDerivative p.1 (fun (y : Homogenization.Vec 2) => b y j) x| ≤ B) :

‖Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus (classicalWordTransportCommutatorExpansion w b (realFourierModeAmbientExpansion N c)))‖ ≤ ∑ j : Fin 2, (List.map (fun (p : List (Fin 2) × List (Fin 2)) => B * ‖(realFourierWordDerivativeMap N (j :: p.2)) c‖) (classicalWordCommutatorSplits w)).sum

Projection of the full transport commutator is bounded by the drift derivative bound times the finite sum of all coefficient derivative norms in Leibniz's expansion.

theorem AVenhance.Infra.Classical.ForcedGalerkinData.transformedForcing_eq_wordResidual {N : ℕ} {G : Type u_1} [NormedAddCommGroup G] [NormedSpace ℝ G] (D : ForcedGalerkinData (Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) G) (w : List (Fin 2)) (t κ : ℝ) (b : Homogenization.Vec 2 → Homogenization.Vec 2) (F : Homogenization.Vec 2 → ℝ) (hb : ContDiff ℝ (↑⊤) b) (hbp : IsZ2Periodic b) (hF : ContDiff ℝ (↑⊤) F) (hFper : IsZ2Periodic F) (hweak : ∀ (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)), (D.weak.coefficient 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 - classicalTransport b (realFourierModeAmbientExpansion N c) x)) (hforce : D.forcing t = Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus F)) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) :

D.transformedForcing (realFourierWordDerivativeMap N w) (fun (x : ℝ) => c) t = Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => classicalWordDerivative w F x - classicalWordTransportCommutatorExpansion w b (realFourierModeAmbientExpansion N c) x)

A transformed forced Galerkin source is the projection of the differentiated forcing minus the exact transport commutator.