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.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.