The actual compact-wave primary starting at time zero. It is the genuine homogeneous forward evolution, has the prescribed initial field, and supplies the literal homogeneous equation and all primary regularity/parity inputs.

@[reducible, inline]

noncomputable abbrev EulerPacketForwardPrimary.forcing {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) : EulerTransversePacketProvider.Forcing P D 0

Forcing: an abbreviation for homogeneousForcing D.

Equations

• EulerPacketForwardPrimary.forcing D = EulerPacketCylinderField.homogeneousForcing D

@[reducible, inline]

noncomputable abbrev EulerPacketForwardPrimary.vector {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (Y : EulerTransversePacketProvider.InitialData P D) : EulerPacketProfileRecursion.VectorField

Vector: an abbreviation for (forcing D).vector Y.

Equations

• EulerPacketForwardPrimary.vector D Y = (EulerPacketForwardPrimary.forcing D).vector Y

@[reducible, inline]

noncomputable abbrev EulerPacketForwardPrimary.scalar {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (Y : EulerTransversePacketProvider.InitialData P D) : EulerPacketProfileRecursion.ScalarField

Scalar: an abbreviation for (forcing D).scalar Y.

Equations

• EulerPacketForwardPrimary.scalar D Y = (EulerPacketForwardPrimary.forcing D).scalar Y

@[reducible, inline]

noncomputable abbrev EulerPacketForwardPrimary.derivative {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (Y : EulerTransversePacketProvider.InitialData P D) : EulerPacketProfileRecursion.VectorField

Derivative: an abbreviation for (forcing D).vectorDerivative Y.

Equations

• EulerPacketForwardPrimary.derivative D Y = (EulerPacketForwardPrimary.forcing D).vectorDerivative Y

theorem EulerPacketForwardPrimary.forcing_path_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) : (forcing D).path = 0

noncomputable def EulerPacketForwardPrimary.profile {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (Y : EulerTransversePacketProvider.InitialData P D) (O : EulerPacketProfileRecursion.Operators) : EulerPacketProfileRecursion.Profile

Profile, given by homogeneousPrimary D Y O.

Equations

• EulerPacketForwardPrimary.profile D Y O = EulerPacketCylinderField.homogeneousPrimary D Y O

noncomputable def EulerPacketForwardPrimary.regularity {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (Y : EulerTransversePacketProvider.InitialData P D) (O : EulerPacketProfileRecursion.Operators) (hcorrector : O.curlCorrector = D.curlCorrector P) : EulerPacketCylinderField.ProfileRegularity P D.T ⋯ D.support (profile D Y O)

Regularity, given by homogeneousPrimaryRegularity D Y O hcorrector.

Equations

• EulerPacketForwardPrimary.regularity D Y O hcorrector = EulerPacketCylinderField.homogeneousPrimaryRegularity D Y O hcorrector

theorem EulerPacketForwardPrimary.equation {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (Y : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.linearPart (D.strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) (vector D Y) (↑t, x, θ)) + (EulerPacketPointJets.fastPressure (D.normalField (↑t, x, θ))) (EulerPacketPointJets.pressureJet (scalar D Y) (↑t, x, θ)) = 0

theorem EulerPacketForwardPrimary.tangent {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (Y : EulerTransversePacketProvider.InitialData P D) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) : inner ℝ (D.normalField (t, x, θ)) (vector D Y (t, x, θ)) = 0

theorem EulerPacketForwardPrimary.mean_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (Y : EulerTransversePacketProvider.InitialData P D) (t : ℝ) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, vector D Y (t, x, θ) = 0

theorem EulerPacketForwardPrimary.pressure_smooth {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (Y : EulerTransversePacketProvider.InitialData P D) (t : ℝ) : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => scalar D Y (t, y)

theorem EulerPacketForwardPrimary.parity {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (Y : EulerTransversePacketProvider.InitialData P D) (O : EulerPacketProfileRecursion.Operators) (hcorrector : O.curlCorrector = D.curlCorrector P) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) (hY : (EulerCylinderFieldReflection.reflection P) ↑Y.value = -↑Y.value) : EulerPacketCylinderField.ProfileParity D.T (profile D Y O)

noncomputable def EulerPacketTerminalDatum.forwardPrimary {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (O : EulerPacketProfileRecursion.Operators) : EulerPacketProfileRecursion.Profile

Forward primary, given by EulerPacketForwardPrimary.profile D (initialData D δ hδ ξ hs) O.

Equations

• EulerPacketTerminalDatum.forwardPrimary D δ hδ ξ hs O = EulerPacketForwardPrimary.profile D (EulerPacketTerminalDatum.initialData D δ hδ ξ hs) O

noncomputable def EulerPacketTerminalDatum.forwardPrimaryRegularity {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (O : EulerPacketProfileRecursion.Operators) (hcorrector : O.curlCorrector = D.curlCorrector period) : EulerPacketCylinderField.ProfileRegularity period D.T ⋯ D.support (forwardPrimary D δ hδ ξ hs O)

Forward primary regularity, given by EulerPacketForwardPrimary.regularity D (initialData D δ hδ ξ hs) O hcorrector.

Equations

• EulerPacketTerminalDatum.forwardPrimaryRegularity D δ hδ ξ hs O hcorrector = EulerPacketForwardPrimary.regularity D (EulerPacketTerminalDatum.initialData D δ hδ ξ hs) O hcorrector

theorem EulerPacketTerminalDatum.forwardPrimary_equation {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (O : EulerPacketProfileRecursion.Operators) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.linearPart (D.strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) (forwardPrimary D δ hδ ξ hs O).high (↑t, x, θ)) + (EulerPacketPointJets.fastPressure (D.normalField (↑t, x, θ))) (EulerPacketPointJets.pressureJet (forwardPrimary D δ hδ ξ hs O).highPressure (↑t, x, θ)) = 0

theorem EulerPacketTerminalDatum.forwardPrimary_tangent {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (O : EulerPacketProfileRecursion.Operators) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) : inner ℝ (D.normalField (t, x, θ)) ((forwardPrimary D δ hδ ξ hs O).high (t, x, θ)) = 0

theorem EulerPacketTerminalDatum.forwardPrimary_mean_zero {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (O : EulerPacketProfileRecursion.Operators) (t : ℝ) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..period, (forwardPrimary D δ hδ ξ hs O).high (t, x, θ) = 0

theorem EulerPacketTerminalDatum.forwardPrimary_parity {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (O : EulerPacketProfileRecursion.Operators) (hcorrector : O.curlCorrector = D.curlCorrector period) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) : EulerPacketCylinderField.ProfileParity D.T (forwardPrimary D δ hδ ξ hs O)

theorem EulerPacketTerminalDatum.forwardPrimary_initial {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (O : EulerPacketProfileRecursion.Operators) (x : EulerSmoothLimit.Space) (θ : ℝ) : (forwardPrimary D δ hδ ξ hs O).high (0, x, θ) = (EulerSpatialCutoffs.innerCutoff x * EulerPeriodicProfile.profile δ θ) • ((D.frame.field ⟨0, ⋯⟩) x) ξ

theorem EulerPacketTerminalDatum.forwardPrimary_initial_angular {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (O : EulerPacketProfileRecursion.Operators) (x : EulerSmoothLimit.Space) : HasDerivAt (fun (θ : ℝ) => (forwardPrimary D δ hδ ξ hs O).high (0, x, θ)) ((EulerSpatialCutoffs.innerCutoff x * δ⁻¹) • ((D.frame.field ⟨0, ⋯⟩) x) ξ) 0

theorem EulerPacketTerminalDatum.forwardPrimary_initial_angular_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (O : EulerPacketProfileRecursion.Operators) : ‖deriv (fun (θ : ℝ) => (forwardPrimary D δ hδ ξ hs O).high (0, 0, θ)) 0‖ = δ⁻¹ * ‖((D.frame.field ⟨0, ⋯⟩) 0) ξ‖