The constructed local viscous Euler correction satisfies the actual differential equation and pressure constraint.

@[instance_reducible]

noncomputable def EulerCorrectionOperators.equationSobolevGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedAddCommGroup (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerCorrectionOperators.equationSobolevGroup period q = inferInstance

@[instance_reducible]

noncomputable def EulerCorrectionOperators.equationSobolevSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedSpace ℝ (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerCorrectionOperators.equationSobolevSpace period q = inferInstance

noncomputable def EulerCorrectionOperators.CorrectionData.rawSource (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : Type u_1} [TopologicalSpace T] (D : CorrectionData period q T) (hq : 6 ≤ q) (t : T) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The actual non-pressure residual and nonlinear increment in equation (17).

Equations

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

noncomputable def EulerCorrectionOperators.CorrectionData.pressure (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : Type u_1} [TopologicalSpace T] (D : CorrectionData period q T) (hq : 6 ≤ q) (t : T) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The correction pressure is the actual unique coercive gradient solution with the sign of equation (17).

Equations

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

theorem EulerCorrectionOperators.CorrectionData.pressure_mem_gradient (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : Type u_1} [TopologicalSpace T] (D : CorrectionData period q T) (hq : 6 ≤ q) (t : T) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : EulerCylinderSobolevSpace.value period (pressure period D hq t e) ∈ EulerLiftedGradientSpace.gradientSpace period D.κ D.direction

The actual pressure belongs to the closed lifted gradient space.

theorem EulerCorrectionOperators.CorrectionData.source_value (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : Type u_1} [TopologicalSpace T] (D : CorrectionData period q T) (hq : 6 ≤ q) (t : T) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : EulerCylinderSobolevSpace.value period ((coefficients period D hq).apply t e) = -EulerCylinderSobolevSpace.value period (rawSource period D hq t e) - (D.metric.coefficient t).operator (EulerCylinderSobolevSpace.value period (pressure period D hq t e))

The projected source equals the literal non-pressure source plus the actual coefficient-weighted pressure.

theorem EulerCorrectionOperators.exists_local_euler_correction_PDE (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (ν : ℝ) (hν : 0 < ν) (S : ℝ) (hS : 0 < S) (D : CorrectionData period q ↑(Set.Icc 0 S)) : ∃ (T : ℝ) (hT : 0 < T) (hTS : T ≤ S) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))), ‖e‖ ≤ 1 ∧ e ⟨0, ⋯⟩ = 0 ∧ (∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (e t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) ∧ ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T ⋯ e r)) (ν • (EulerSobolevHeatGenerator.laplacianEvaluation period (q + 1) ⋯) (e ⟨t, ⋯⟩) - EulerCylinderSobolevSpace.value period (CorrectionData.rawSource period D hq ((EulerQuadraticSource.timeInclusion hTS) ⟨t, ⋯⟩) (e ⟨t, ⋯⟩)) - (D.metric.coefficient ((EulerQuadraticSource.timeInclusion hTS) ⟨t, ⋯⟩)).operator (EulerCylinderSobolevSpace.value period (CorrectionData.pressure period D hq ((EulerQuadraticSource.timeInclusion hTS) ⟨t, ⋯⟩) (e ⟨t, ⋯⟩)))) t

The constructed actual local Euler correction has zero initial error, zero lifted divergence, and satisfies equation (17) in L² at every interior time.