Energy data for finite Galerkin ODEs with an integrable forcing.

structure AVenhance.Infra.Classical.EnergyWeakFormData (E : Type u_1) (G : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup G] [NormedSpace ℝ G] : Type (max u_1 u_2)

A finite weak-form Galerkin system together with a coefficient-side forcing.

• coefficient : ℝ → E →L[ℝ] E

  Time-dependent linear operator in the Galerkin evolution equation.

• coefficientBound : ℝ

  Uniform operator-norm bound for the Galerkin coefficient.

• coefficientBound_nonneg : 0 ≤ self.coefficientBound
• coefficient_aestronglyMeasurable : MeasureTheory.AEStronglyMeasurable self.coefficient MeasureTheory.volume
• coefficient_norm_le (t : ℝ) : ‖self.coefficient t‖ ≤ self.coefficientBound
• diffusivity : ℝ

  Positive diffusion coefficient in the energy identity.

• diffusivity_pos : 0 < self.diffusivity
• gradient : E →L[ℝ] G

  Continuous linear gradient operator on the Galerkin state space.

• driftBound : ℝ

  Constant controlling the drift contribution to the energy estimate.

• driftForm : ℝ → E → ℝ

  Quadratic drift contribution appearing in the energy identity.

• weakForm_energy : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 1), ∀ (c : E), 2 * inner ℝ c ((self.coefficient t) c) = -2 * self.driftForm t c - 2 * self.diffusivity * ‖self.gradient c‖ ^ 2
• drift_bound : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 1), ∀ (c : E), |self.driftForm t c| ≤ self.driftBound * ‖self.gradient c‖ * ‖c‖

noncomputable def AVenhance.Infra.Classical.WeakFormGalerkinData.toEnergyWeakForm {n : ℕ} {G : Type u_1} [NormedAddCommGroup G] [NormedSpace ℝ G] (W : Parabolic.FourierGalerkin.WeakFormGalerkinData n G) : EnergyWeakFormData (Parabolic.FourierGalerkin.Coefficients n) G

The energy fields extracted from a weak-form Fourier Galerkin system.

Equations

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

structure AVenhance.Infra.Classical.ForcedGalerkinData (E : Type u_1) (G : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup G] [NormedSpace ℝ G] : Type (max u_1 u_2)

An energy-controlled finite-dimensional linear ODE with an integrable forcing.

• weak : EnergyWeakFormData E G

  Coefficient, gradient, and energy identity for the unforced equation.

• initial : E

  Initial Galerkin state at time zero.

• forcing : ℝ → E

  Integrable time-dependent forcing in the Galerkin state space.

• forcing_integrable : IntervalIntegrable self.forcing MeasureTheory.volume 0 1

def AVenhance.Infra.Classical.ForcedGalerkinData.ode {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup G] [NormedSpace ℝ G] (D : ForcedGalerkinData E G) : ODE.LinearODEData 0 1 ode._proof_1

The inhomogeneous finite-dimensional linear ODE.

Equations

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

theorem AVenhance.Infra.Classical.ForcedGalerkinData.existsUnique_solution {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), ODE.IsLinearIntegralSolution D.weak.coefficient D.forcing D.initial 0 1 (ODE.extendCurve ode._proof_1 u) ∧ AbsolutelyContinuousOnInterval (ODE.extendCurve ode._proof_1 u) 0 1

Existence and uniqueness of the forced coefficient path.

theorem AVenhance.Infra.Classical.ForcedGalerkinData.uniformEnergyEstimateOfLinearGrowth {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) {A G✝ : ℝ} (hAcoef : 0 ≤ A) (_hG : 0 ≤ G✝) (hforce : ∀ t ∈ Set.Icc 0 1, ‖D.forcing t‖ ≤ A * ‖ODE.extendCurve ode._proof_1 u t‖ + G✝) (t : ℝ) : t ∈ Set.Icc 0 1 → ‖ODE.extendCurve ode._proof_1 u t‖ ^ 2 ≤ (‖D.initial‖ ^ 2 + G✝ ^ 2) * Real.exp ((max D.weak.driftBound 0 ^ 2 / D.weak.diffusivity + 2 * A + 1) * t) ∧ ‖ODE.extendCurve ode._proof_1 u t‖ ^ 2 + D.weak.diffusivity * ∫ (s : ℝ) in 0..t, ‖D.weak.gradient (ODE.extendCurve ode._proof_1 u s)‖ ^ 2 ≤ ‖D.initial‖ ^ 2 + G✝ ^ 2 + (max D.weak.driftBound 0 ^ 2 / D.weak.diffusivity + 2 * A + 1) * (t * ((‖D.initial‖ ^ 2 + G✝ ^ 2) * Real.exp ((max D.weak.driftBound 0 ^ 2 / D.weak.diffusivity + 2 * A + 1) * t)))

Cutoff-independent scalar and integrated-gradient estimates for a forced Galerkin path.

The forcing bound is measured in coefficient-space L². The constants depend on the drift bound, diffusivity, initial datum, and forcing bound, but not on the mode dimension.