The actual source packet is Euler in the physical parent coordinates. The normalized frame and inverse identities are supplied by the parent construction, and the final physical scaling is explicit.

Euler's spatial/amplitude rescaling, proved for the actual first derivatives and scalar pressure. Time is unchanged.

noncomputable def EulerSpatialRescaling.coordinates {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ell : ℝ) : ℝ × E →L[ℝ] ℝ × E

Coordinates, given by (fst ℝ ℝ E).prod ((ell⁻¹ • ContinuousLinearMap.id ℝ E).comp (snd ℝ ℝ E)).

Equations

• EulerSpatialRescaling.coordinates ell = (ContinuousLinearMap.fst ℝ ℝ E).prod ((ell⁻¹ • ContinuousLinearMap.id ℝ E) ∘SL ContinuousLinearMap.snd ℝ ℝ E)

@[simp]

theorem EulerSpatialRescaling.coordinates_apply {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ell : ℝ) (q : ℝ × E) : (coordinates ell) q = (q.1, ell⁻¹ • q.2)

noncomputable def EulerSpatialRescaling.velocity {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ell : ℝ) (u : ℝ × E → E) (q : ℝ × E) : E

Velocity, given by ell • u (coordinates ell q).

Equations

• EulerSpatialRescaling.velocity ell u q = ell • u ((EulerSpatialRescaling.coordinates ell) q)

noncomputable def EulerSpatialRescaling.pressure {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ell : ℝ) (p : ℝ × E → ℝ) (q : ℝ × E) : ℝ

Pressure, given by ell^2*p (coordinates ell q).

Equations

• EulerSpatialRescaling.pressure ell p q = ell ^ 2 * p ((EulerSpatialRescaling.coordinates ell) q)

theorem EulerSpatialRescaling.velocity_hasFDerivAt {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ell : ℝ) (u : ℝ × E → E) (q : ℝ × E) (hu : DifferentiableAt ℝ u ((coordinates ell) q)) : HasFDerivAt (velocity ell u) (ell • fderiv ℝ u ((coordinates ell) q) ∘SL coordinates ell) q

theorem EulerSpatialRescaling.pressure_gradient {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (ell : ℝ) (hell : ell ≠ 0) (p : ℝ × E → ℝ) (q : ℝ × E) (hp : DifferentiableAt ℝ (fun (y : E) => p (q.1, y)) (ell⁻¹ • q.2)) : gradient (fun (y : E) => pressure ell p (q.1, y)) q.2 = ell • gradient (fun (y : E) => p (q.1, y)) (ell⁻¹ • q.2)

theorem EulerSpatialRescaling.momentumResidual_eq {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (ell : ℝ) (hell : ell ≠ 0) (u : ℝ × E → E) (p : ℝ × E → ℝ) (q : ℝ × E) (hu : DifferentiableAt ℝ u ((coordinates ell) q)) (hp : DifferentiableAt ℝ (fun (y : E) => p (q.1, y)) (ell⁻¹ • q.2)) : EulerLagrangian.momentumResidual (velocity ell u) (pressure ell p) q = ell • EulerLagrangian.momentumResidual u p ((coordinates ell) q)

theorem EulerSpatialRescaling.momentumResidual_zero {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (ell : ℝ) (hell : ell ≠ 0) (u : ℝ × E → E) (p : ℝ × E → ℝ) (q : ℝ × E) (hu : DifferentiableAt ℝ u ((coordinates ell) q)) (hp : DifferentiableAt ℝ (fun (y : E) => p (q.1, y)) (ell⁻¹ • q.2)) (hEuler : EulerLagrangian.momentumResidual u p ((coordinates ell) q) = 0) : EulerLagrangian.momentumResidual (velocity ell u) (pressure ell p) q = 0

theorem EulerSpatialRescaling.spatial_derivative {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ell : ℝ) (hell : ell ≠ 0) (u : ℝ × E → E) (t : ℝ) (x : E) (hu : DifferentiableAt ℝ (fun (y : E) => u (t, y)) (ell⁻¹ • x)) : fderiv ℝ (fun (y : E) => velocity ell u (t, y)) x = fderiv ℝ (fun (y : E) => u (t, y)) (ell⁻¹ • x)

Normalizing the actual parent Euler velocity and pressure preserves Euler and supplies the true time law of the normalized particle map.

noncomputable def EulerParentPacketFrames.Parent.normalizedVelocity (A : Parent) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space

Normalized velocity, given by EulerSpatialRescaling.velocity A.ell⁻¹ u.

Equations

• A.normalizedVelocity u = EulerSpatialRescaling.velocity A.ell⁻¹ u

noncomputable def EulerParentPacketFrames.Parent.normalizedPressure (A : Parent) (p : ℝ × EulerSmoothLimit.Space → ℝ) : ℝ × EulerSmoothLimit.Space → ℝ

Normalized pressure, given by EulerSpatialRescaling.pressure A.ell⁻¹ p.

Equations

• A.normalizedPressure p = EulerSpatialRescaling.pressure A.ell⁻¹ p

@[simp]

theorem EulerParentPacketFrames.Parent.normalizedVelocity_apply (A : Parent) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (q : ℝ × EulerSmoothLimit.Space) : A.normalizedVelocity u q = A.ell⁻¹ • u (q.1, A.ell • q.2)

@[simp]

theorem EulerParentPacketFrames.Parent.normalizedPressure_apply (A : Parent) (p : ℝ × EulerSmoothLimit.Space → ℝ) (q : ℝ × EulerSmoothLimit.Space) : A.normalizedPressure p q = A.ell⁻¹ ^ 2 * p (q.1, A.ell • q.2)

theorem EulerParentPacketFrames.Parent.normalizedVelocity_differentiableAt (A : Parent) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (t : ℝ) (x : EulerSmoothLimit.Space) (hu : DifferentiableAt ℝ u (t, A.ell • x)) : DifferentiableAt ℝ (A.normalizedVelocity u) (t, x)

theorem EulerParentPacketFrames.Parent.normalizedPressure_differentiableAt (A : Parent) (p : ℝ × EulerSmoothLimit.Space → ℝ) (t : ℝ) (x : EulerSmoothLimit.Space) (hp : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => p (t, y)) (A.ell • x)) : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => A.normalizedPressure p (t, y)) x

theorem EulerParentPacketFrames.Parent.normalizedMomentum_zero (A : Parent) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (p : ℝ × EulerSmoothLimit.Space → ℝ) (t : ℝ) (x : EulerSmoothLimit.Space) (hu : DifferentiableAt ℝ u (t, A.ell • x)) (hp : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => p (t, y)) (A.ell • x)) (he : EulerLagrangian.momentumResidual u p (t, A.ell • x) = 0) : EulerLagrangian.momentumResidual (A.normalizedVelocity u) (A.normalizedPressure p) (t, x) = 0

theorem EulerParentPacketFrames.Parent.packetPosition_velocity_eventually (A : Parent) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hvelocity : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), (A.velocity.field t) x = u (↑t, A.position t x)) (t : ℝ) (ht : t ∈ Set.Ioo 0 A.T) (x : EulerSmoothLimit.Space) : (fun (q : ℝ × EulerSmoothLimit.Space) => (fderiv ℝ A.packetPosition q) (1, 0)) =ᶠ[nhds (t, x)] fun (q : ℝ × EulerSmoothLimit.Space) => A.normalizedVelocity u (q.1, A.packetPosition q)

theorem EulerParentPacketFrames.Parent.normalizedVelocity_restore (A : Parent) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (q : ℝ × EulerSmoothLimit.Space) : EulerSpatialRescaling.velocity A.ell (A.normalizedVelocity u) q = u q

theorem EulerParentPacketFrames.Parent.normalizedVelocity_add_restore (A : Parent) (u w : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (q : ℝ × EulerSmoothLimit.Space) : EulerSpatialRescaling.velocity A.ell (fun (r : ℝ × EulerSmoothLimit.Space) => A.normalizedVelocity u r + w r) q = u q + A.ell • w (q.1, A.ell⁻¹ • q.2)

noncomputable def EulerParentPacketFrames.Parent.packetFrame (A : Parent) (q : ℝ × EulerSmoothLimit.Space) : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Packet frame, given by A.frame.realField A.T A.T_pos.le q.1 q.2.

Equations

• A.packetFrame q = SmoothTimeField.realField A.T ⋯ A.frame q.1 q.2

theorem EulerParentPacketFrames.Parent.packetInverseCoordinates_differentiableAt (A : Parent) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hXY : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), A.position t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (t : ℝ) (ht : t ∈ Set.Ioo 0 A.T) (x : EulerSmoothLimit.Space) : DifferentiableAt ℝ (EulerPacketPhysicalTransform.inverseCoordinates (A.packetInverse Y)) (t, x)

theorem EulerParentPacketFrames.Parent.packetInverse_time_continuous (A : Parent) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hY : Continuous (Function.uncurry Y)) : Continuous fun (q : ↑(Set.Icc 0 A.T) × EulerSmoothLimit.Space) => A.packetInverse Y (↑q.1, q.2)

theorem EulerParentPacketFrames.Parent.packetFrame_match (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : A.packetFrame (↑t, x) = ((A.transverseData m hm J support hSupport).F.field t) x

noncomputable def EulerParentPacketFrames.Parent.normalizedExactVelocity (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (q : ℝ × EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Normalized exact velocity, constructed using A.normalizedVelocity.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerParentPacketFrames.Parent.normalizedExactPressure (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (p : ℝ × EulerSmoothLimit.Space → ℝ) (q : ℝ × EulerSmoothLimit.Space) : ℝ

Normalized exact pressure, given by A.normalizedPressure p q + physicalPressure (((exactPacketOfResidual P B residual)).rawGraphPotential k) (A.packetInverse Y) q.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerParentPacketFrames.Parent.exactPacketVelocity (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space

Exact packet velocity, given by EulerSpatialRescaling.velocity A.ell (A.normalizedExactVelocity m hm J support hSupport B residual k Y u).

Equations

• A.exactPacketVelocity m hm J support hSupport B residual k Y u = EulerSpatialRescaling.velocity A.ell (A.normalizedExactVelocity m hm J support hSupport B residual k Y u)

noncomputable def EulerParentPacketFrames.Parent.exactPacketPressure (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (p : ℝ × EulerSmoothLimit.Space → ℝ) : ℝ × EulerSmoothLimit.Space → ℝ

Exact packet pressure, given by EulerSpatialRescaling.pressure A.ell (A.normalizedExactPressure m hm J support hSupport B residual k Y p).

Equations

• A.exactPacketPressure m hm J support hSupport B residual k Y p = EulerSpatialRescaling.pressure A.ell (A.normalizedExactPressure m hm J support hSupport B residual k Y p)

theorem EulerParentPacketFrames.Parent.normalizedExactVelocity_differentiableAt (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hYX : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), Y t (A.position t x) = x) (hXY : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), A.position t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ∀ t ∈ Set.Ioo 0 A.T, ∀ (x : EulerSmoothLimit.Space), DifferentiableAt ℝ u (t, x)) (t : ℝ) (ht : t ∈ Set.Ioo 0 A.T) (x : EulerSmoothLimit.Space) : DifferentiableAt ℝ (A.normalizedExactVelocity m hm J support hSupport B residual k Y u) (t, x)

theorem EulerParentPacketFrames.Parent.normalizedExactPressure_differentiableAt (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (hk : k * κ = 1) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hXY : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), A.position t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (p : ℝ × EulerSmoothLimit.Space → ℝ) (hp : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => p (↑t, y)) x) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => A.normalizedExactPressure m hm J support hSupport B residual k Y p (↑t, y)) x

theorem EulerParentPacketFrames.Parent.normalizedExact_momentum (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (hk : k * κ = 1) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hYX : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), Y t (A.position t x) = x) (hXY : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), A.position t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (p : ℝ × EulerSmoothLimit.Space → ℝ) (hvelocity : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), (A.velocity.field t) x = u (↑t, A.position t x)) (hu : ∀ t ∈ Set.Ioo 0 A.T, ∀ (x : EulerSmoothLimit.Space), DifferentiableAt ℝ u (t, x)) (hp : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => p (↑t, y)) x) (heuler : ∀ t ∈ Set.Ioo 0 A.T, ∀ (x : EulerSmoothLimit.Space), EulerLagrangian.momentumResidual u p (t, x) = 0) (t : ℝ) (ht : t ∈ Set.Ioo 0 A.T) (x : EulerSmoothLimit.Space) : EulerLagrangian.momentumResidual (A.normalizedExactVelocity m hm J support hSupport B residual k Y u) (A.normalizedExactPressure m hm J support hSupport B residual k Y p) (t, x) = 0

theorem EulerParentPacketFrames.Parent.exactPacketVelocity_differentiableAt (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hYX : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), Y t (A.position t x) = x) (hXY : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), A.position t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ∀ t ∈ Set.Ioo 0 A.T, ∀ (x : EulerSmoothLimit.Space), DifferentiableAt ℝ u (t, x)) (t : ℝ) (ht : t ∈ Set.Ioo 0 A.T) (x : EulerSmoothLimit.Space) : DifferentiableAt ℝ (A.exactPacketVelocity m hm J support hSupport B residual k Y u) (t, x)

theorem EulerParentPacketFrames.Parent.exactPacket_momentum (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (hk : k * κ = 1) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hYX : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), Y t (A.position t x) = x) (hXY : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), A.position t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (p : ℝ × EulerSmoothLimit.Space → ℝ) (hvelocity : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), (A.velocity.field t) x = u (↑t, A.position t x)) (hu : ∀ t ∈ Set.Ioo 0 A.T, ∀ (x : EulerSmoothLimit.Space), DifferentiableAt ℝ u (t, x)) (hp : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => p (↑t, y)) x) (heuler : ∀ t ∈ Set.Ioo 0 A.T, ∀ (x : EulerSmoothLimit.Space), EulerLagrangian.momentumResidual u p (t, x) = 0) (t : ℝ) (ht : t ∈ Set.Ioo 0 A.T) (x : EulerSmoothLimit.Space) : EulerLagrangian.momentumResidual (A.exactPacketVelocity m hm J support hSupport B residual k Y u) (A.exactPacketPressure m hm J support hSupport B residual k Y p) (t, x) = 0

theorem EulerParentPacketFrames.Parent.exactPacketVelocity_eq_corrected (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (Y : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : A.exactPacketVelocity m hm J support hSupport B residual k Y u (↑t, x) = A.correctedPacketVelocity B k Y (fun (s : ↑(Set.Icc 0 A.T)) (y : EulerSmoothLimit.Space) => u (↑s, y)) t x