Genuine Cauchy convergence of uniformly bounded nonlinear viscous corrections in continuous cylinder L².

Genuine finite-interval Lipschitz comparison of actual correction solutions at different viscosities.

@[instance_reducible]

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

The existing Sobolev normed-group instance for the actual viscosity comparison.

Equations

• EulerCorrectionViscosityStability.comparisonSobolevGroup period q = inferInstance

@[instance_reducible]

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

The existing real Sobolev module instance for the actual viscosity comparison.

Equations

• EulerCorrectionViscosityStability.comparisonSobolevSpace period q = inferInstance

theorem EulerCorrectionViscosityStability.correction_viscosity_pointwise (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (T : ℝ) (hT : 0 ≤ T) (D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T)) (B : EulerCorrectionStabilityBudget.StabilityBudget period hT D) (ν μ : ℝ) (hν : 0 < ν) (hμ : 0 < μ) (hν1 : ν ≤ 1) (u v : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (R : ℝ) (huR : ‖u‖ ≤ R) (hvR : ‖v‖ ≤ R) (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) (hz : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (D.approximation t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) (hud : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (u t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) (hvd : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (v t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) (t : ↑(Set.Icc 0 T)) : ‖EulerCylinderSobolevSpace.value period (u t) - EulerCylinderSobolevSpace.value period (v t)‖ ≤ EulerCorrectionStabilityBudget.StabilityBudget.comparisonConstant period B R * |ν - μ|

Two actual zero-initial correction mild solutions obey a pointwise L² Lipschitz estimate in viscosity. The differential energy inequality is derived from their literal equations and the actual spatial cancellations.

theorem EulerViscosityCauchy.cauchySeq_of_norm_le {X : Type u_1} [NormedAddCommGroup X] (u : ℕ → X) (a : ℕ → ℝ) (C : ℝ) (hC : 0 ≤ C) (ha : CauchySeq a) (hbound : ∀ (m n : ℕ), ‖u m - u n‖ ≤ C * |a m - a n|) : CauchySeq u

An actual Lipschitz comparison transfers Cauchy convergence between normed-valued sequences.

noncomputable def EulerViscosityCauchy.valuePath (period : ℝ) [Fact (0 < period)] {q : ℕ} (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period))

The genuine continuous L² path underlying a finite-Sobolev correction path.

Equations

• EulerViscosityCauchy.valuePath period T u = (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period q)) u

theorem EulerViscosityCauchy.correction_viscosity_norm (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (T : ℝ) (hT : 0 ≤ T) (D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T)) (B : EulerCorrectionStabilityBudget.StabilityBudget period hT D) (ν μ : ℝ) (hν : 0 < ν) (hμ : 0 < μ) (hν1 : ν ≤ 1) (u v : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (R : ℝ) (huR : ‖u‖ ≤ R) (hvR : ‖v‖ ≤ R) (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) (hz : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (D.approximation t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) (hud : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (u t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) (hvd : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (v t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) : ‖valuePath period T u - valuePath period T v‖ ≤ EulerCorrectionStabilityBudget.StabilityBudget.comparisonConstant period B R * |ν - μ|

The actual pointwise comparison controls the full continuous L² path norm.

theorem EulerViscosityCauchy.correction_family_cauchy (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (T : ℝ) (hT : 0 ≤ T) (D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T)) (B : EulerCorrectionStabilityBudget.StabilityBudget period hT D) (ν : ℕ → ℝ) (hν : ∀ (n : ℕ), 0 < ν n) (hν1 : ∀ (n : ℕ), ν n ≤ 1) (hνc : CauchySeq ν) (u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (R : ℝ) (huR : ∀ (n : ℕ), ‖u n‖ ≤ R) (hu : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), (u n) t = EulerQuadraticSource.quadraticDuhamel period (ν n) ⋯ hT ⋯ (EulerCorrectionOperators.CorrectionData.coefficients period D hq) 0 (u n) t) (hz : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (D.approximation t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) (hud : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period ((u n) t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) : CauchySeq fun (n : ℕ) => valuePath period T (u n)

Every actual uniformly Sobolev-bounded correction family with Cauchy viscosities is Cauchy in continuous cylinder L². Both the nonlinear difference equation and its metric estimate are proved internally.