Exact coordinate normalization of the actual packet residual. The linear, metric, and derivative-free quadratic coefficients are precisely those constructed in PacketSourceCorrectionCoefficients.

Genuine time and spatial derivatives of z = k F⁻¹ W. The inverse derivative is derived from the prescribed deformation, including at the endpoints of the actual time interval.

@[instance_reducible]

noncomputable def EulerPacketCoordinates.instPacketCoordinateJets1 : NormedAddCommGroup EulerSmoothLimit.Space

Cache the standard NormedAddCommGroup Space instance to shorten typeclass synthesis.

Equations

• EulerPacketCoordinates.instPacketCoordinateJets1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCoordinates.instPacketCoordinateJets2 : NormedSpace ℝ EulerSmoothLimit.Space

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

Equations

• EulerPacketCoordinates.instPacketCoordinateJets2 = inferInstance

noncomputable def EulerPacketCoordinates.coordinate {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (W : EulerPacketProfileRecursion.VectorField) : EulerPacketProfileRecursion.VectorField

Coordinate, defined pointwise by k • rawInverse D z (W z).

Equations

• EulerPacketCoordinates.coordinate D k W z = k • (EulerPacketCorrectionCoefficients.rawInverse D z) (W z)

noncomputable def EulerPacketCoordinates.inverseTime {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (z : EulerPacketPointJets.Domain) : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Inverse time, given by D.inverseDerivative (D.clamp z.1) z.2.1.

Equations

• EulerPacketCoordinates.inverseTime D z = (D.inverseDerivative (D.clamp z.1)) z.2.1

noncomputable def EulerPacketCoordinates.inverseTimeCoefficient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) : EulerPacketCylinderField.MatrixCoefficient D.T (inverseTime D)

Inverse time coefficient, bundling path, orbit, raw_eq.

Equations

• EulerPacketCoordinates.inverseTimeCoefficient D = { path := D.inverseDerivative, orbit := ⋯, raw_eq := ⋯ }

noncomputable def EulerPacketCoordinates.coordinateTime {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (W Wt : EulerPacketProfileRecursion.VectorField) : EulerPacketProfileRecursion.VectorField

Coordinate time, defined pointwise by k • (inverseTime D z (W z) + rawInverse D z (Wt z)).

Equations

• EulerPacketCoordinates.coordinateTime D k W Wt z = k • ((EulerPacketCoordinates.inverseTime D z) (W z) + (EulerPacketCorrectionCoefficients.rawInverse D z) (Wt z))

theorem EulerPacketCoordinates.coordinateTime_formula {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (W Wt : EulerPacketProfileRecursion.VectorField) (z : EulerPacketPointJets.Domain) : coordinateTime D k W Wt z = k • ((EulerPacketCorrectionCoefficients.rawInverse D z) (Wt z) - (EulerPacketCorrectionCoefficients.rawInverse D z) ((D.strain z) (W z)))

theorem EulerPacketCoordinates.frame_coordinate {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (W : EulerPacketProfileRecursion.VectorField) (z : EulerPacketPointJets.Domain) : (EulerPacketCorrectionCoefficients.rawFrame D z) (coordinate D k W z) = k • W z

theorem EulerPacketCoordinates.reconstruct {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (hk : k ≠ 0) (W : EulerPacketProfileRecursion.VectorField) (z : EulerPacketPointJets.Domain) : W z = k⁻¹ • (EulerPacketCorrectionCoefficients.rawFrame D z) (coordinate D k W z)

theorem EulerPacketCoordinates.normal_coordinate {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (W : EulerPacketProfileRecursion.VectorField) (z : EulerPacketPointJets.Domain) : inner ℝ D.m₀ (coordinate D k W z) = k * inner ℝ (D.normalField z) (W z)

theorem EulerPacketCoordinates.coordinate_hasDerivWithinAt {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (W Wt : EulerPacketProfileRecursion.VectorField) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) (hW : HasDerivWithinAt (fun (r : ℝ) => W (r, x, θ)) (Wt (↑t, x, θ)) (Set.Icc 0 D.T) ↑t) : HasDerivWithinAt (fun (r : ℝ) => coordinate D k W (r, x, θ)) (coordinateTime D k W Wt (↑t, x, θ)) (Set.Icc 0 D.T) ↑t

theorem EulerPacketCoordinates.coordinate_derivWithin {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (W Wt : EulerPacketProfileRecursion.VectorField) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) (hW : HasDerivWithinAt (fun (r : ℝ) => W (r, x, θ)) (Wt (↑t, x, θ)) (Set.Icc 0 D.T) ↑t) : derivWithin (fun (r : ℝ) => coordinate D k W (r, x, θ)) (Set.Icc 0 D.T) ↑t = coordinateTime D k W Wt (↑t, x, θ)

noncomputable def EulerPacketCoordinates.coordinateField {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] {W : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P D.T W) (k : ℝ) : EulerPacketCylinderField.Field P D.T (coordinate D k W)

Coordinate field, given by ((inverseCoefficient D).multiply G).smul k.

Equations

• EulerPacketCoordinates.coordinateField D G k = ((EulerPacketCorrectionCoefficients.inverseCoefficient D).multiply G).smul k

noncomputable def EulerPacketCoordinates.coordinateTimeField {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] {W Wt : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P D.T W) (Gt : EulerPacketCylinderField.Field P D.T Wt) (k : ℝ) : EulerPacketCylinderField.Field P D.T (coordinateTime D k W Wt)

Coordinate time field, given by (((inverseTimeCoefficient D).multiply G).add ((inverseCoefficient D).multiply Gt)).smul k.

Equations

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

theorem EulerPacketCoordinates.coordinateField_time {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] {W Wt : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P D.T W) (Gt : EulerPacketCylinderField.Field P D.T Wt) (k : ℝ) (hW : EulerPacketCylinderField.TimeDerivative ⋯ G Gt) : EulerPacketCylinderField.TimeDerivative ⋯ (coordinateField D G k) (coordinateTimeField D G Gt k)

theorem EulerPacketCoordinates.coordinate_smooth {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] {W : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P D.T W) (k : ℝ) (t : ↑(Set.Icc 0 D.T)) : ContDiff ℝ ↑⊤ fun (y : EulerPacketPointJets.SpatialDomain) => coordinate D k W (↑t, y)

theorem EulerPacketCoordinates.normalized_spatial_derivative {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] {W : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P D.T W) (k : ℝ) (hk : k ≠ 0) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) (v : EulerPacketPointJets.SpatialDomain) : k • (EulerPacketCorrectionCoefficients.rawInverse D (↑t, x, θ)) ((fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => W (↑t, y)) (x, θ)) v) = (EulerPacketCorrectionCoefficients.rawInverse D (↑t, x, θ)) (((fderiv ℝ (⇑(D.F.field t)) x) v.1) (coordinate D k W (↑t, x, θ))) + (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => coordinate D k W (↑t, y)) (x, θ)) v

@[instance_reducible]

noncomputable def EulerPacketCoordinates.instPacketCoordinateResidual1 : NormedAddCommGroup EulerSmoothLimit.Space

Cache the standard NormedAddCommGroup Space instance to shorten typeclass synthesis.

Equations

• EulerPacketCoordinates.instPacketCoordinateResidual1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCoordinates.instPacketCoordinateResidual2 : NormedSpace ℝ EulerSmoothLimit.Space

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

Equations

• EulerPacketCoordinates.instPacketCoordinateResidual2 = inferInstance

noncomputable def EulerPacketCoordinates.transport {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (κ : ℝ) (Z : EulerPacketProfileRecursion.VectorField) (z : EulerPacketPointJets.Domain) : EulerSmoothLimit.Space

Transport, given by fderiv ℝ (fun y => Z (z.1,y)) z.2 (κ • Z z,⟪D.m₀,Z z⟫_ℝ).

Equations

• EulerPacketCoordinates.transport D κ Z z = (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => Z (z.1, y)) z.2) (κ • Z z, inner ℝ D.m₀ (Z z))

noncomputable def EulerPacketCoordinates.algebraic {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (κ : ℝ) (Z : EulerPacketProfileRecursion.VectorField) (z : EulerPacketPointJets.Domain) : EulerSmoothLimit.Space

Algebraic, given by ∑ i : Fin 3, (Z z) i • rawQuadratic D κ i z (Z z).

Equations

• EulerPacketCoordinates.algebraic D κ Z z = ∑ i : Fin 3, (Z z).ofLp i • (EulerPacketCorrectionCoefficients.rawQuadratic D κ i z) (Z z)

noncomputable def EulerPacketCoordinates.coordinatePressure {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (p : EulerPacketProfileRecursion.ScalarField) (z : EulerPacketPointJets.Domain) : EulerSmoothLimit.Space

Coordinate pressure, given by k • pressureGradient p z + k^2 • ((pressureJet p z).2 angleDirection • D.m₀).

Equations

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

noncomputable def EulerPacketCoordinates.liftedPressure {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (κ : ℝ) (p : EulerPacketProfileRecursion.ScalarField) (z : EulerPacketPointJets.Domain) : EulerSmoothLimit.Space

Lifted pressure, given by κ • pressureGradient p z + (pressureJet p z).2 angleDirection • D.m₀.

Equations

• EulerPacketCoordinates.liftedPressure D κ p z = κ • EulerPacketCylinderField.pressureGradient p z + (EulerPacketPointJets.pressureJet p z).2 EulerPacketPointJets.angleDirection • D.m₀

theorem EulerPacketCoordinates.transport_formula {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (κ : ℝ) (Z : EulerPacketProfileRecursion.VectorField) (z : EulerPacketPointJets.Domain) : transport D κ Z z = κ • (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => Z (z.1, y)) z.2) (Z z, 0) + inner ℝ D.m₀ (Z z) • (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => Z (z.1, y)) z.2) (0, 1)

theorem EulerPacketCoordinates.algebraic_formula {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (κ : ℝ) (Z : EulerPacketProfileRecursion.VectorField) (z : EulerPacketPointJets.Domain) : algebraic D κ Z z = κ • (EulerPacketCorrectionCoefficients.rawInverse D z) (((fderiv ℝ (fun (x : EulerSmoothLimit.Space) => EulerPacketCorrectionCoefficients.rawFrame D (z.1, x, z.2.2)) z.2.1) (Z z)) (Z z))

theorem EulerPacketCoordinates.normalized_pressure {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (p : EulerPacketProfileRecursion.ScalarField) (z : EulerPacketPointJets.Domain) : k • (EulerPacketCorrectionCoefficients.rawInverse D z) ((EulerPacketPointJets.slowPressure (EulerPacketCorrectionCoefficients.rawInverse D z)) (EulerPacketPointJets.pressureJet p z) + k • (EulerPacketPointJets.fastPressure (D.normalField z)) (EulerPacketPointJets.pressureJet p z)) = (EulerPacketCorrectionCoefficients.rawMetric D z) (coordinatePressure D k p z)

theorem EulerPacketCoordinates.coordinatePressure_eq_lifted {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (hk : k ≠ 0) (p : EulerPacketProfileRecursion.ScalarField) (z : EulerPacketPointJets.Domain) (hp : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => p (z.1, y)) z.2) : coordinatePressure D k p z = liftedPressure D k⁻¹ (k ^ 2 • p) z

theorem EulerPacketCoordinates.normalized_linear {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] {W Wt : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P D.T W) (Gt : EulerPacketCylinderField.Field P D.T Wt) (k : ℝ) (hW : EulerPacketCylinderField.TimeDerivative ⋯ G Gt) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : k • (EulerPacketCorrectionCoefficients.rawInverse D (↑t, x, θ)) ((EulerPacketPointJets.linearPart (D.strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) W (↑t, x, θ))) = coordinateTime D k W Wt (↑t, x, θ) + (EulerPacketCorrectionCoefficients.rawLinear D (↑t, x, θ)) (coordinate D k W (↑t, x, θ))

theorem EulerPacketCoordinates.normalized_nonlinear {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] {W : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P D.T W) (k : ℝ) (hk : k ≠ 0) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : k • (EulerPacketCorrectionCoefficients.rawInverse D (↑t, x, θ)) (((EulerPacketPointJets.slowAdvection (EulerPacketCorrectionCoefficients.rawInverse D (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) W (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) W (↑t, x, θ)) + k • ((EulerPacketPointJets.fastAdvection (D.normalField (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) W (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) W (↑t, x, θ))) = transport D k⁻¹ (coordinate D k W) (↑t, x, θ) + algebraic D k⁻¹ (coordinate D k W) (↑t, x, θ)

theorem EulerPacketCoordinates.normalized_residual {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] {W Wt : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P D.T W) (Gt : EulerPacketCylinderField.Field P D.T Wt) (k : ℝ) (hk : k ≠ 0) (hW : EulerPacketCylinderField.TimeDerivative ⋯ G Gt) (p : EulerPacketProfileRecursion.ScalarField) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : k • (EulerPacketCorrectionCoefficients.rawInverse D (↑t, x, θ)) (EulerPacketPointJets.slicedMomentumResidual (Set.Icc 0 D.T) k⁻¹ (EulerPacketCorrectionCoefficients.rawInverse D (↑t, x, θ)) (D.strain (↑t, x, θ)) (D.normalField (↑t, x, θ)) W p (↑t, x, θ)) = coordinateTime D k W Wt (↑t, x, θ) + (EulerPacketCorrectionCoefficients.rawLinear D (↑t, x, θ)) (coordinate D k W (↑t, x, θ)) + transport D k⁻¹ (coordinate D k W) (↑t, x, θ) + algebraic D k⁻¹ (coordinate D k W) (↑t, x, θ) + (EulerPacketCorrectionCoefficients.rawMetric D (↑t, x, θ)) (coordinatePressure D k p (↑t, x, θ))