Pointwise decomposition of the actual corrected velocity and pressure. The identities concern the constructed exact packet, not an arbitrary pair satisfying an energy bound.

theorem EulerAllOrderDriftCorrection.Budget.correctedFieldTower_eq (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) : correctedFieldTower P B = A.approximation.add (fieldTower P B)

theorem EulerAllOrderDriftCorrection.Budget.correctedPressureTower_eq (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (R : ApproximationResidual P hT A) : correctedPressureTower P B R = R.pressure.add (pressureTower P B)

theorem EulerAllOrderDriftCorrection.Budget.correctedFieldTower_pointField (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P) : (correctedFieldTower P B).pointField t x = A.approximation.pointField t x + pointField P B t x

theorem EulerAllOrderDriftCorrection.Budget.correctedPressureTower_pointField (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (R : ApproximationResidual P hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P) : (correctedPressureTower P B R).pointField t x = R.pressure.pointField t x + pointPressure P B t x

theorem EulerAllOrderDriftCorrection.exactPacketOfResidual_velocity_pointField (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (R : ApproximationResidual P hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P) : (exactPacketOfResidual P B R).velocity.pointField t x = A.approximation.pointField t x + Budget.pointField P B t x

theorem EulerAllOrderDriftCorrection.exactPacketOfResidual_pressure_pointField (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (R : ApproximationResidual P hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P) : (exactPacketOfResidual P B R).pressure.pointField t x = R.pressure.pointField t x + Budget.pointPressure P B t x