Linear coefficient transforms of forced finite-dimensional Galerkin paths.

def AVenhance.Infra.Classical.ForcedGalerkinData.transformedForcing {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup G] [NormedSpace ℝ G] (D : ForcedGalerkinData E G) (L : E →L[ℝ] E) (y : ℝ → E) : ℝ → E

The forcing generated when a fixed linear map is applied to a forced Galerkin path.

Equations

• D.transformedForcing L y t = L (D.forcing t) + L ((D.weak.coefficient t) (y t)) - (D.weak.coefficient t) (L (y t))

def AVenhance.Infra.Classical.ForcedGalerkinData.linearTransform {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup G] [NormedSpace ℝ G] (D : ForcedGalerkinData E G) (L : E →L[ℝ] E) (y : ℝ → E) (hforcing : IntervalIntegrable (D.transformedForcing L y) MeasureTheory.volume 0 1) : ForcedGalerkinData E G

Reuse the same weak operator and assign the transformed path its correct initial state and commutator forcing.

Equations

• D.linearTransform L y hforcing = { weak := D.weak, initial := L D.initial, forcing := D.transformedForcing L y, forcing_integrable := hforcing }

def AVenhance.Infra.Classical.ForcedGalerkinData.mapPath {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : E →L[ℝ] E) (u : C(↑(Set.Icc 0 1), E)) : C(↑(Set.Icc 0 1), E)

Apply a continuous linear map to a coefficient path.

Equations

• AVenhance.Infra.Classical.ForcedGalerkinData.mapPath L u = { toFun := fun (t : ↑(Set.Icc 0 1)) => L (u t), continuous_toFun := ⋯ }

@[simp]

theorem AVenhance.Infra.Classical.ForcedGalerkinData.extendCurve_mapPath {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : E →L[ℝ] E) (u : C(↑(Set.Icc 0 1), E)) : ODE.extendCurve extendCurve_mapPath._proof_1 (mapPath L u) = fun (t : ℝ) => L (ODE.extendCurve extendCurve_mapPath._proof_1 u t)

theorem AVenhance.Infra.Classical.ForcedGalerkinData.mapPath_isSolution {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup G] [NormedSpace ℝ G] (D : ForcedGalerkinData E G) (u : C(↑(Set.Icc 0 1), E)) (hu : D.ode.IsSolution u) (L : E →L[ℝ] E) (hforcing : IntervalIntegrable (D.transformedForcing L (ODE.extendCurve extendCurve_mapPath._proof_1 u)) MeasureTheory.volume 0 1) : (D.linearTransform L (ODE.extendCurve extendCurve_mapPath._proof_1 u) hforcing).ode.IsSolution (mapPath L u)

A continuous linear transform of a forced Galerkin solution again solves the same weak operator equation, with its commutator included in the forcing.

theorem AVenhance.Infra.Classical.ForcedGalerkinData.transformedForcing_intervalIntegrable {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup G] [NormedSpace ℝ G] (D : ForcedGalerkinData E G) (u : C(↑(Set.Icc 0 1), E)) (L : E →L[ℝ] E) : IntervalIntegrable (D.transformedForcing L (ODE.extendCurve extendCurve_mapPath._proof_1 u)) MeasureTheory.volume 0 1

The commutator forcing produced by a continuous linear transform of a finite Galerkin path is interval integrable.

noncomputable def AVenhance.Infra.Classical.ForcedGalerkinData.wordDerivativeTransform {N : ℕ} {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] (D : ForcedGalerkinData (Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) G) (u : C(↑(Set.Icc 0 1), Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N))) (w : List (Fin 2)) : ForcedGalerkinData (Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) G

The forced Galerkin data and path obtained by differentiating every retained Fourier mode along one ordered spatial derivative word.

Equations

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

theorem AVenhance.Infra.Classical.ForcedGalerkinData.wordDerivativeTransform_isSolution {N : ℕ} {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] (D : ForcedGalerkinData (Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) G) (u : C(↑(Set.Icc 0 1), Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N))) (hu : D.ode.IsSolution u) (w : List (Fin 2)) : (D.wordDerivativeTransform u w).ode.IsSolution (mapPath (realFourierWordDerivativeMap N w) u)

The coefficient path obtained by differentiating a Galerkin path solves the transformed forced system with the commutator included in its forcing.