The same exact packet that constructs the next particle map supplies its physical Euler evolution. All new flow and Euler laws are proved from the old evolution and the actual correction solver.

The actual scalar pressure of the corrected source packet has the constructed continuous physical pressure force, at every time.

@[instance_reducible]

noncomputable def EulerParentPacketFrames.Parent.instParentPacketExactPressure1 : NormedAddCommGroup EulerSmoothLimit.Space

Cache the standard NormedAddCommGroup Space instance to shorten typeclass synthesis.

Equations

• EulerParentPacketFrames.Parent.instParentPacketExactPressure1 = inferInstance

@[instance_reducible]

noncomputable def EulerParentPacketFrames.Parent.instParentPacketExactPressure2 : NormedSpace ℝ EulerSmoothLimit.Space

Cache the standard NormedSpace ℝ Space instance to shorten typeclass synthesis.

Equations

• EulerParentPacketFrames.Parent.instParentPacketExactPressure2 = inferInstance

@[instance_reducible]

noncomputable def EulerParentPacketFrames.Parent.instParentPacketExactPressure3 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerParentPacketFrames.Parent.instParentPacketExactPressure3 = inferInstance

@[instance_reducible]

noncomputable def EulerParentPacketFrames.Parent.instParentPacketExactPressure4 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerParentPacketFrames.Parent.instParentPacketExactPressure4 = inferInstance

theorem EulerParentPacketFrames.Parent.transformedForce_continuous (A : Parent) (Y force g : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hY : Continuous (Function.uncurry Y)) (hforce : Continuous (Function.uncurry force)) (hg : Continuous (Function.uncurry g)) : Continuous fun (q : ↑(Set.Icc 0 A.T) × EulerSmoothLimit.Space) => force q.1 q.2 + A.ell • (ContinuousLinearMap.adjoint ((A.inverse.field q.1) (A.ell⁻¹ • Y q.1 q.2))) (g q.1 (A.ell⁻¹ • Y q.1 q.2))

noncomputable def EulerParentPacketFrames.Parent.exactPacketForce (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 force : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Exact packet force, constructed using force.

Equations

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

theorem EulerParentPacketFrames.Parent.exactPacketForce_continuous (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 force : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hY : Continuous (Function.uncurry Y)) (hforce : Continuous (Function.uncurry force)) : Continuous (Function.uncurry (A.exactPacketForce m hm J support hSupport B residual k Y force))

theorem EulerParentPacketFrames.Parent.normalizedExactPressure_gradient (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 → ℝ) (force : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hp : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => p (↑t, y)) x) (hgradient : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), gradient (fun (y : EulerSmoothLimit.Space) => p (↑t, y)) x = force t x) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : gradient (fun (y : EulerSmoothLimit.Space) => A.normalizedExactPressure m hm J support hSupport B residual k Y p (↑t, y)) x = A.ell⁻¹ • force t (A.ell • x) + (ContinuousLinearMap.adjoint ((A.inverse.field t) (A.packetInverse Y (↑t, x)))) ((EulerAllOrderDriftCorrection.exactPacketOfResidual P B residual).graphPressure k t (A.packetInverse Y (↑t, x)))

theorem EulerParentPacketFrames.Parent.exactPacketPressure_gradient (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 → ℝ) (force : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hp : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => p (↑t, y)) x) (hgradient : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), gradient (fun (y : EulerSmoothLimit.Space) => p (↑t, y)) x = force t x) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : gradient (fun (y : EulerSmoothLimit.Space) => A.exactPacketPressure m hm J support hSupport B residual k Y p (↑t, y)) x = A.exactPacketForce m hm J support hSupport B residual k Y force t x

Incompressibility of the actual corrected parent velocity. The normalized packet uses the parent's genuine determinant-one Jacobian, and the final physical rescaling preserves divergence exactly.

theorem EulerSpatialRescaling.divergence_eq (ell : ℝ) (hell : ell ≠ 0) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (t : ℝ) (x : EulerSmoothLimit.Space) (hu : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => u (t, y)) (ell⁻¹ • x)) : EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => velocity ell u (t, y)) x = EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => u (t, y)) (ell⁻¹ • x)

theorem EulerParentPacketFrames.Parent.normalizedVelocity_divergence (A : Parent) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (t : ℝ) (x : EulerSmoothLimit.Space) (hu : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => u (t, y)) (A.ell • x)) : EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => A.normalizedVelocity u (t, y)) x = EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => u (t, y)) (A.ell • x)

theorem EulerParentPacketFrames.Parent.packetPosition_spatial_frame (A : Parent) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : fderiv ℝ (fun (y : EulerSmoothLimit.Space) => A.packetPosition (↑t, y)) x = A.packetFrame (↑t, x)

theorem EulerParentPacketFrames.Parent.packetFrame_det (A : Parent) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : Matrix.det (EulerPacketPiola.operatorMatrix (A.packetFrame (↑t, x))) = 1

theorem EulerParentPacketFrames.Parent.normalizedExact_euler (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) (hdiv : ∀ t ∈ Set.Ioo 0 A.T, ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => u (t, y)) 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 ∧ EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => A.normalizedExactVelocity m hm J support hSupport B residual k Y u (t, y)) x = 0

theorem EulerParentPacketFrames.Parent.exactPacket_euler (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) (hdiv : ∀ t ∈ Set.Ioo 0 A.T, ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => u (t, y)) 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 ∧ EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => A.exactPacketVelocity m hm J support hSupport B residual k Y u (t, y)) x = 0

The new parent is the particle map of the actual corrected Euler velocity, and its acceleration is minus the actual constructed pressure force. Both matches are derived from the existing parent law and Euler.

theorem EulerParentPacketFrames.Parent.child_velocity_exact (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)) {raw : EulerPacketProfileRecursion.VectorField} (V : EulerPacketCylinderField.Field P A.T raw) (hV : Z = V.toFieldTower) (G : EulerPhysicalGraphFlowBounds.Data P A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient P B V) (k : ℝ) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (q : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) q) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 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) (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 : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : ((A.child G k m hgraph nextEll hnext hnext1).velocity.field t) x = A.exactPacketVelocity m hm J support hSupport B residual k Y u (↑t, (A.child G k m hgraph nextEll hnext hnext1).position t x)

theorem EulerParentPacketFrames.Parent.child_acceleration_exact (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)) {raw : EulerPacketProfileRecursion.VectorField} (V : EulerPacketCylinderField.Field P A.T raw) (hV : Z = V.toFieldTower) (G : EulerPhysicalGraphFlowBounds.Data P A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient P B V) (k : ℝ) (hk : k * κ = 1) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (q : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) q) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 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 → ℝ) (force : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hforce : Continuous (Function.uncurry force)) (hgradient : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), gradient (fun (y : EulerSmoothLimit.Space) => p (↑t, y)) x = force t x) (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 : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : ((A.child G k m hgraph nextEll hnext hnext1).acceleration.field t) x = -A.exactPacketForce m hm J support hSupport B residual k Y force t ((A.child G k m hgraph nextEll hnext hnext1).position t x)

noncomputable def EulerParentPacketFrames.Evolution.child {A : Parent} (E : Evolution A) {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)) {raw : EulerPacketProfileRecursion.VectorField} (V : EulerPacketCylinderField.Field P A.T raw) (hV : Z = V.toFieldTower) (G : EulerPhysicalGraphFlowBounds.Data P A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient P B V) (k : ℝ) (hk : k * κ = 1) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (q : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) q) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) : Evolution (A.child G k m hgraph nextEll hnext hnext1)

Child, bundling inverse, velocity, pressure, force and the required compatibility proofs.

Equations

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

@[simp]

theorem EulerParentPacketFrames.Evolution.child_velocity {A : Parent} (E : Evolution A) {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)) {raw : EulerPacketProfileRecursion.VectorField} (V : EulerPacketCylinderField.Field P A.T raw) (hV : Z = V.toFieldTower) (G : EulerPhysicalGraphFlowBounds.Data P A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient P B V) (k : ℝ) (hk : k * κ = 1) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (q : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) q) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) : (E.child m hm J support hSupport B residual V hV G hG k hk hgraph nextEll hnext hnext1).velocity = A.exactPacketVelocity m hm J support hSupport B residual k E.inverse.field E.velocity

@[simp]

theorem EulerParentPacketFrames.Evolution.child_pressure {A : Parent} (E : Evolution A) {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)) {raw : EulerPacketProfileRecursion.VectorField} (V : EulerPacketCylinderField.Field P A.T raw) (hV : Z = V.toFieldTower) (G : EulerPhysicalGraphFlowBounds.Data P A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient P B V) (k : ℝ) (hk : k * κ = 1) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (q : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) q) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) : (E.child m hm J support hSupport B residual V hV G hG k hk hgraph nextEll hnext hnext1).pressure = A.exactPacketPressure m hm J support hSupport B residual k E.inverse.field E.pressure

@[simp]

theorem EulerParentPacketFrames.Evolution.child_force {A : Parent} (E : Evolution A) {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)) {raw : EulerPacketProfileRecursion.VectorField} (V : EulerPacketCylinderField.Field P A.T raw) (hV : Z = V.toFieldTower) (G : EulerPhysicalGraphFlowBounds.Data P A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient P B V) (k : ℝ) (hk : k * κ = 1) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (q : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) q) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) : (E.child m hm J support hSupport B residual V hV G hG k hk hgraph nextEll hnext hnext1).force = A.exactPacketForce m hm J support hSupport B residual k E.inverse.field E.force