Energy estimate for a finite Galerkin system

The finite weak-form matrix splits into transport and diffusion forms. The transport contribution is bounded by B ‖D u‖ ‖u‖; Young's inequality absorbs one diffusion term and leaves a scalar Grönwall coefficient B² / κ. The result below takes those two finite-dimensional form facts as its interface, so the spatial mode calculus can establish them independently.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.drift_absorption {κ B g u q : ℝ} (hκ : 0 < κ) (hq : |q| ≤ B * g * u) : -2 * q - 2 * κ * g ^ 2 ≤ B ^ 2 / κ * u ^ 2 - κ * g ^ 2

Young's inequality in the form used to absorb the drift into diffusion.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.galerkin_energy_estimate {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : ODE.LinearODEData 0 1 galerkin_energy_estimate._proof_1} (u : C(↑(Set.Icc 0 1), E)) (hu : D.IsSolution u) (hforcing : D.f = 0) (gradient : E →L[ℝ] F) (κ B : ℝ) (hκ : 0 < κ) (driftForm : ℝ → E → ℝ) (hform : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 1), ∀ (v : E), 2 * inner ℝ v ((D.A t) v) = -2 * driftForm t v - 2 * κ * ‖gradient v‖ ^ 2) (hdrift : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 1), ∀ (v : E), |driftForm t v| ≤ B * ‖gradient v‖ * ‖v‖) (t : ℝ) : t ∈ Set.Icc 0 1 → ‖ODE.extendCurve galerkin_energy_estimate._proof_1 u t‖ ^ 2 ≤ ‖D.y₀‖ ^ 2 * Real.exp (B ^ 2 / κ * t) ∧ ‖ODE.extendCurve galerkin_energy_estimate._proof_1 u t‖ ^ 2 + κ * ∫ (s : ℝ) in 0..t, ‖gradient (ODE.extendCurve galerkin_energy_estimate._proof_1 u s)‖ ^ 2 ≤ ‖D.y₀‖ ^ 2 + B ^ 2 / κ * (t * ‖D.y₀‖ ^ 2 * Real.exp (B ^ 2 / κ * t))

Grönwall control of a homogeneous finite-dimensional ODE with a dissipative weak form.

gradient is the finite-mode spatial gradient map and driftForm is the tested ∫ (b · D u) u term. hform is the coefficient-space identity obtained by testing the projected weak equation against the current Galerkin state. hdrift is the Cauchy-Schwarz estimate using the essential bound on b; no divergence-free condition is used.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakFormGalerkinData.IsSolution.energyEstimate {n : ℕ} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (D : WeakFormGalerkinData n F) (u : C(↑(Set.Icc 0 1), Coefficients n)) (hu : D.ode.IsSolution u) (t : ℝ) : t ∈ Set.Icc 0 1 → ‖ODE.extendCurve galerkin_energy_estimate._proof_1 u t‖ ^ 2 ≤ ‖D.initial‖ ^ 2 * Real.exp (D.driftBound ^ 2 / D.diffusivity * t) ∧ ‖ODE.extendCurve galerkin_energy_estimate._proof_1 u t‖ ^ 2 + D.diffusivity * ∫ (s : ℝ) in 0..t, ‖D.gradient (ODE.extendCurve galerkin_energy_estimate._proof_1 u s)‖ ^ 2 ≤ ‖D.initial‖ ^ 2 + D.driftBound ^ 2 / D.diffusivity * (t * ‖D.initial‖ ^ 2 * Real.exp (D.driftBound ^ 2 / D.diffusivity * t))

The energy estimate specialized to a finite real weak-form Galerkin system.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakFormGalerkinData.IsSolution.unique {n : ℕ} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (D : WeakFormGalerkinData n F) {u v : C(↑(Set.Icc 0 1), Coefficients n)} (hu : D.ode.IsSolution u) (hv : D.ode.IsSolution v) : u = v

Uniqueness of the absolutely-continuous coefficient path for fixed Galerkin data.