The actual nonlinear correction source is identical across compatible Sobolev levels.

theorem EulerCorrectionSourceRestriction.truncate_transport (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))) : (EulerCylinderSobolevSpace.truncateOperator period q) (((EulerSobolevTransport.transportBilinear period ⋯ L hL) u) v) = ((EulerSobolevTransport.transportBilinear period hq L hL) ((EulerCylinderSobolevSpace.truncateOperator period (q + 1)) u)) ((EulerCylinderSobolevSpace.truncateOperator period (q + 1)) v)

The actual quadratic transport field restricts to the same lower-order transport.

theorem EulerCorrectionSourceRestriction.truncate_rawSource (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) {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)) (t : ↑(Set.Icc 0 T)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))) : (EulerCylinderSobolevSpace.truncateOperator period q) (EulerCorrectionOperators.CorrectionData.rawSource period D ⋯ t u) = EulerCorrectionOperators.CorrectionData.rawSource period (EulerCorrectionLowerData.lowerData period D KG KL KQ hG hL hQ) hq t ((EulerCylinderSobolevSpace.truncateOperator period (q + 1)) u)

Restricting the literal nonlinear raw source gives the raw source of the actual lower data.

theorem EulerCorrectionSourceRestriction.restrictOperator_succ_eq_truncate (period : ℝ) [Fact (0 < period)] {q : ℕ} (h : q ≤ q + 1) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : (EulerCylinderSobolevSpace.restrictOperator period h) u = (EulerCylinderSobolevSpace.truncateOperator period q) u

theorem EulerCorrectionSourceRestriction.coefficients_apply_eq (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : Type u_1} [TopologicalSpace T] (D : EulerCorrectionOperators.CorrectionData period q T) (hq : 6 ≤ q) (t : T) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : (EulerCorrectionOperators.CorrectionData.coefficients period D hq).apply t u = -(EulerSobolevCoefficientPressure.projectedSourceOperator period (D.metric.jet t) D.κ D.direction D.coercivity ⋯ ⋯) (EulerCorrectionOperators.CorrectionData.rawSource period D hq t u)

theorem EulerCorrectionSourceRestriction.truncate_source (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) {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)) (t : ↑(Set.Icc 0 T)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))) : (EulerCylinderSobolevSpace.truncateOperator period q) ((EulerCorrectionOperators.CorrectionData.coefficients period D ⋯).apply t u) = (EulerCorrectionOperators.CorrectionData.coefficients period (EulerCorrectionLowerData.lowerData period D KG KL KQ hG hL hQ) hq).apply t ((EulerCylinderSobolevSpace.truncateOperator period (q + 1)) u)

The actual projected nonlinear mild source commutes exactly with Sobolev restriction.