Actual inviscid corrections agree across compatible Sobolev levels.

Actual inviscid corrections agree across compatible Sobolev levels.

theorem EulerInviscidCorrectionRestriction.inviscid_equation_restrict (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)))) (hu : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT u r)) (EulerCylinderSobolevSpace.value period ((EulerCorrectionOperators.CorrectionData.coefficients period D ⋯).apply ⟨t, ⋯⟩ (u ⟨t, ⋯⟩))) t) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.truncateOperator period (q + 1))) u) r)) (EulerCylinderSobolevSpace.value period ((EulerCorrectionOperators.CorrectionData.coefficients period (EulerCorrectionLowerData.lowerData period D KG KL KQ hG hL hQ) hq).apply ⟨t, ⋯⟩ ((EulerCylinderSobolevSpace.truncateOperator period (q + 1)) (u ⟨t, ⋯⟩)))) t

The literal inviscid equation is preserved by lowering the actual Sobolev order.

theorem EulerInviscidCorrectionCompatibility.inviscid_corrections_compatible (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)))) (hu : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT u r)) (EulerCylinderSobolevSpace.value period ((EulerCorrectionOperators.CorrectionData.coefficients period D ⋯).apply ⟨t, ⋯⟩ (u ⟨t, ⋯⟩))) t) (B : EulerCorrectionStabilityBudget.StabilityBudget period hT (EulerCorrectionLowerData.lowerData period D KG KL KQ hG hL hQ)) (v : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hv : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT v r)) (EulerCylinderSobolevSpace.value period ((EulerCorrectionOperators.CorrectionData.coefficients period (EulerCorrectionLowerData.lowerData period D KG KL KQ hG hL hQ) hq).apply ⟨t, ⋯⟩ (v ⟨t, ⋯⟩))) t) (hi : (EulerCylinderSobolevSpace.truncateOperator period (q + 1)) (u ⟨0, ⋯⟩) = v ⟨0, ⋯⟩) (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) : (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.truncateOperator period (q + 1))) u = v

Actual inviscid corrections constructed at neighboring Sobolev orders coincide after restriction.