The exact viscosity-difference equation of two genuine nonlinear mild corrections.

Every actual continued mild correction obeys the literal viscous PDE with its genuine coercive pressure.

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

The literal PDE follows at every interior time from any actual correction mild solution.

@[instance_reducible]

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

The existing Sobolev normed-group instance, fixed explicitly for difference-equation elaboration.

Equations

• EulerCorrectionDifferencePDE.differenceSobolevGroup period q = inferInstance

@[instance_reducible]

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

The existing real Sobolev module instance, fixed explicitly for difference-equation elaboration.

Equations

• EulerCorrectionDifferencePDE.differenceSobolevSpace period q = inferInstance

noncomputable def EulerCorrectionDifferencePDE.differenceRhs (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : Type u_1} [TopologicalSpace T] (D : EulerCorrectionOperators.CorrectionData period q T) (hq : 6 ≤ q) (ν μ : ℝ) (t : T) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The literal right side of the viscosity-difference equation, including its genuine pressure difference.

Equations

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

theorem EulerCorrectionDifferencePDE.vector_difference_identity {H : Type u_1} [AddCommGroup H] [Module ℝ H] (ν μ : ℝ) (a b ru rv top rem pu pv : H) (hraw : ru - rv = top + rem) : ν • (a - b) + (ν - μ) • b - top - rem - (pu - pv) = ν • a - ru - pu - (μ • b - rv - pv)

Exact vector subtraction for a bilinear evolution with two viscosities.

theorem EulerCorrectionDifferencePDE.differenceRhs_eq_sub (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : Type u_1} [TopologicalSpace T] (D : EulerCorrectionOperators.CorrectionData period q T) (hq : 6 ≤ q) (ν μ : ℝ) (t : T) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : differenceRhs period D hq ν μ t u v = ν • (EulerSobolevHeatGenerator.laplacianEvaluation period (q + 1) ⋯) u - EulerCylinderSobolevSpace.value period (EulerCorrectionOperators.CorrectionData.rawSource period D hq t u) - (D.metric.coefficient t).operator (EulerCylinderSobolevSpace.value period (EulerCorrectionOperators.CorrectionData.pressure period D hq t u)) - (μ • (EulerSobolevHeatGenerator.laplacianEvaluation period (q + 1) ⋯) v - EulerCylinderSobolevSpace.value period (EulerCorrectionOperators.CorrectionData.rawSource period D hq t v) - (D.metric.coefficient t).operator (EulerCylinderSobolevSpace.value period (EulerCorrectionOperators.CorrectionData.pressure period D hq t v)))

The exposed difference equation is exactly the subtraction of the two actual PDE right sides.

theorem EulerCorrectionDifferencePDE.correction_difference_hasDerivAt (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (ν μ : ℝ) (hν : 0 < ν) (hμ : 0 < μ) (T : ℝ) (hT : 0 ≤ T) (D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T)) (u v : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hu : ∀ (t : ↑(Set.Icc 0 T)), u t = EulerQuadraticSource.quadraticDuhamel period ν hν hT ⋯ (EulerCorrectionOperators.CorrectionData.coefficients period D hq) 0 u t) (hv : ∀ (t : ↑(Set.Icc 0 T)), v t = EulerQuadraticSource.quadraticDuhamel period μ hμ hT ⋯ (EulerCorrectionOperators.CorrectionData.coefficients period D hq) 0 v t) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (s : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT u s) - EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT v s)) (differenceRhs period D hq ν μ ⟨t, ⋯⟩ (u ⟨t, ⋯⟩) (v ⟨t, ⋯⟩)) t

Subtracting two actual mild correction equations gives the literal transport-pressure-heat difference equation.