Related estimates used together by the same construction modules.

Exact repeated restriction of coherent prescribed coefficient and field data.

theorem EulerAllOrderCorrectionData.Data.lower_twice (period : ℝ) [Fact (0 < period)] {T : ℝ} (A : Data period T) (q : ℕ) : EulerCorrectionLowerData.lowerData period (EulerCorrectionLowerData.lowerData period (atOrder period A (q + 1 + 1)) (A.metric.jet (q + 1)) (A.linear.jet (q + 1)) (fun (i : Fin 3) => (A.quadratic i).jet (q + 1)) ⋯ ⋯ ⋯) (A.metric.jet q) (A.linear.jet q) (fun (i : Fin 3) => (A.quadratic i).jet q) ⋯ ⋯ ⋯ = atOrder period A q

Two genuine lower-data operations return precisely the prescribed lower-order data, including the approximation and residual paths.

The literal inviscid correction equation follows from the actual strongly convergent viscous family.

@[instance_reducible]

noncomputable def EulerCorrectionLimitEquation.limitEquationGroup (period : ℝ) [Fact (0 < period)] (s : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period s)

The inherited normed group on each actual Sobolev value space.

Equations

• EulerCorrectionLimitEquation.limitEquationGroup period s = inferInstance

@[instance_reducible]

noncomputable def EulerCorrectionLimitEquation.limitEquationSpace (period : ℝ) [Fact (0 < period)] (s : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period s)

The inherited real normed space on each actual Sobolev value space.

Equations

• EulerCorrectionLimitEquation.limitEquationSpace period s = inferInstance

theorem EulerCorrectionLimitEquation.correction_limit_equation (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (T : ℝ) (hT : 0 ≤ T) (D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)) (KG : (t : ↑(Set.Icc 0 T)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (D.metric.coefficient t)) (KL : (t : ↑(Set.Icc 0 T)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (D.linear.coefficient t)) (KQ : (i : Fin 3) → (t : ↑(Set.Icc 0 T)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q ((D.quadratic i).coefficient t)) (hG : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KG t)) (hL : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KL t)) (hQ : ∀ (i : Fin 3), Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KQ i t)) (u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1)))) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (M : ℝ) (huM : ∀ (n : ℕ), ‖u n‖ ≤ M) (hconv : Filter.Tendsto (fun (n : ℕ) => (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.truncateOperator period (q + 1))) (u n)) Filter.atTop (nhds e)) (hsol : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), (u n) t = EulerQuadraticSource.quadraticDuhamel period (EulerViscosityDefect.viscositySequence n) ⋯ hT ⋯ (EulerCorrectionOperators.CorrectionData.coefficients period D ⋯) 0 (u n) t) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT e r)) (EulerCylinderSobolevSpace.value period ((EulerCorrectionOperators.CorrectionData.coefficients period (EulerCorrectionLowerData.lowerData period D KG KL KQ hG hL hQ) hq).apply ⟨t, ⋯⟩ (e ⟨t, ⋯⟩))) t

A genuine bounded viscous family converging one Sobolev order lower solves the actual inviscid correction equation at the limit. The nonlinear source restriction and convergence, the vanishing viscosity term, and the integral passage are proved internally.