Finite real Galerkin systems for the weak form

The coordinates below are real coefficients of a finite orthonormal family of periodic modes. The coefficient matrix records the weak form exactly: the drift entry is the integral of (b · D eⱼ) eᵢ. In particular, no integration by parts is used to move the drift onto the test mode, and no divergence-free hypothesis occurs.

@[instance_reducible]

noncomputable def galerkinMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem galerkinMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem galerkinProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

@[reducible, inline]

abbrev AVenhance.Infra.Parabolic.FourierGalerkin.Coefficients (n : ℕ) : Type

Real coefficient vectors with their Euclidean inner product and norm.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.Coefficients n = PiLp 2 fun (x : Fin n) => ℝ

def AVenhance.Infra.Parabolic.FourierGalerkin.vecDot (u v : Fin 2 → ℝ) : ℝ

The ordinary dot product on Vec 2, written without importing PDE definitions.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.vecDot u v = ∑ k : Fin 2, u k * v k

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.weakFormMatrixEntry {n : ℕ} (b : ℝ → Torus → Fin 2 → ℝ) (κ : ℝ) (mode : Fin n → Torus → ℝ) (modeGrad : Fin n → Torus → Fin 2 → ℝ) (t : ℝ) (i j : Fin n) : ℝ

The weak-form matrix entry for trial mode j and test mode i.

The drift is kept in the source form b · D eⱼ; this definition does not rewrite it by spatial integration by parts.

Equations

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

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.modeProjectionCoefficients (n : ℕ) (mode : Fin n → Torus → ℝ) (f : Torus → ℝ) : Coefficients n

The coefficients of an L² projection onto a finite real orthonormal mode family.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.modeProjectionCoefficients n mode f = WithLp.toLp 2 fun (i : Fin n) => ∫ (x : AVenhance.Infra.Parabolic.FourierGalerkin.Torus), f x * mode i x

def AVenhance.Infra.Parabolic.FourierGalerkin.modeExpansion (n : ℕ) (mode : Fin n → Torus → ℝ) (c : Coefficients n) (x : Torus) : ℝ

The function represented by a finite real coefficient vector.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.modeExpansion n mode c x = ∑ i : Fin n, c.ofLp i * mode i x

structure AVenhance.Infra.Parabolic.FourierGalerkin.WeakFormGalerkinData (n : ℕ) (F : Type u_1) [NormedAddCommGroup F] [NormedSpace ℝ F] : Type u_1

Finite-dimensional weak-form ODE data on a finite real mode family.

coefficient is understood as the bounded measurable extension of the Galerkin matrix from the closed time interval to the line, as required by LinearODEData. matrix_spec fixes its values on the physical time interval to the weak-form entries. mode_orthonormal makes the coefficient derivative equal to the tested weak equation without a mass matrix.

• mode : Fin n → Torus → ℝ

  Real orthonormal modes spanning the finite Galerkin approximation.

• modeGrad : Fin n → Torus → Fin 2 → ℝ

  Spatial gradients of the real Galerkin modes.

• mode_orthonormal (i j : Fin n) : ∫ (x : Torus), self.mode i x * self.mode j x = if i = j then 1 else 0
• frequencyCutoff : ℕ

  Frequency cutoff fixing the finite-dimensional mode expansion.

• modeExpansion_fixed_by_projection (c : Coefficients n) (x : Torus) : realFourierProjection self.frequencyCutoff (modeExpansion n self.mode c) x = modeExpansion n self.mode c x
• initialData : Torus → ℝ

  Initial scalar function on the torus.

• drift : ℝ → Torus → Fin 2 → ℝ

  Time-dependent drift vector on the torus.

• diffusivity : ℝ

  Positive diffusion coefficient of the weak Galerkin equation.

• diffusivity_pos : 0 < self.diffusivity
• initial : Coefficients n

  Initial coefficients of the finite Galerkin approximation.

• coefficient : ℝ → Coefficients n →L[ℝ] Coefficients n

  Time-dependent continuous linear generator on the coefficient space.

• coefficientBound : ℝ

  Uniform operator-norm bound for the coefficient generator.

• coefficientBound_nonneg : 0 ≤ self.coefficientBound
• coefficient_aestronglyMeasurable : MeasureTheory.AEStronglyMeasurable self.coefficient MeasureTheory.volume
• coefficient_norm_le (t : ℝ) : ‖self.coefficient t‖ ≤ self.coefficientBound
• matrix_spec : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 1), ∀ (c : Coefficients n) (i : Fin n), ((self.coefficient t) c).ofLp i = ∑ j : Fin n, weakFormMatrixEntry self.drift self.diffusivity self.mode self.modeGrad t i j * c.ofLp j
• initial_is_projection : self.initial = modeProjectionCoefficients n self.mode self.initialData
• projection_eq_modeExpansion (x : Torus) : modeExpansion n self.mode self.initial x = realFourierProjection self.frequencyCutoff self.initialData x
• gradient : Coefficients n →L[ℝ] F

  Continuous linear gradient of a finite mode expansion.

• driftBound : ℝ

  Constant bounding the quadratic drift contribution to energy.

• driftForm : ℝ → Coefficients n → ℝ

  Quadratic drift form occurring in the weak energy identity.

• weakForm_energy : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 1), ∀ (c : Coefficients n), 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 : Coefficients n), |self.driftForm t c| ≤ self.driftBound * ‖self.gradient c‖ * ‖c‖

def AVenhance.Infra.Parabolic.FourierGalerkin.WeakFormGalerkinData.ode {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (D : WeakFormGalerkinData n F) : ODE.LinearODEData 0 1 ode._proof_1

The corresponding homogeneous measurable linear ODE on [0,1].

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakFormGalerkinData.existsUnique_solution {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (D : WeakFormGalerkinData n F) : ∃! u : C(↑(Set.Icc 0 1), Coefficients n), ODE.IsLinearIntegralSolution D.coefficient 0 D.initial 0 1 (ODE.extendCurve ode._proof_1 u) ∧ AbsolutelyContinuousOnInterval (ODE.extendCurve ode._proof_1 u) 0 1

Existence and uniqueness of the finite Galerkin coefficient path.

The path is absolutely continuous and solves the projected weak-form ODE through the integral-solution characterization supplied by Infra.ODE.Linear.