The amplitude in the literal terminal datum gives exactly the amplitude multiplying the physical primary wave.

Exact rank-one primary shear throughout the joined history and forward interval, obtained from the proved factorization of the actual primary.

noncomputable def EulerPacketPrimaryShear.fullWave {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α k : ℝ) (t : ↑(Set.Icc 0 D.T)) (y : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Full wave, given by (α/k) • vector τ hτ hτT B (initialData D δ hδ ξ hs) (t,(y,k*⟪D.m₀,y⟫_ℝ)).

Equations

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

theorem EulerPacketPrimaryShear.fullWave_hasFDerivAt {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α k : ℝ) (hk : k ≠ 0) (t : ↑(Set.Icc 0 D.T)) : HasFDerivAt (fullWave τ hτ hτT B δ hδ ξ hs α k t) ((α / δ) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.envelopedVelocity τ hτ hτT B δ hδ ξ hs (↑t) 0)) D.m₀) 0

theorem EulerPacketPrimaryShear.fullWave_physical_hasFDerivAt {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α k : ℝ) (hk : k ≠ 0) (t : ↑(Set.Icc 0 D.T)) (X Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : HasFDerivAt X ((D.F.field t) 0) 0) (hY : DifferentiableAt ℝ Y (X 0)) (hleft : ∀ (y : EulerSmoothLimit.Space), Y (X y) = y) : HasFDerivAt (fun (x : EulerSmoothLimit.Space) => fullWave τ hτ hτT B δ hδ ξ hs α k t (Y x)) ((α / δ) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.envelopedVelocity τ hτ hτT B δ hδ ξ hs (↑t) 0)) ((D.normal.field t) 0)) (X 0)

theorem EulerPacketPrimaryShear.fullWave_physical_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α k : ℝ) (hα : 0 ≤ α) (hk : k ≠ 0) (t : ↑(Set.Icc 0 D.T)) (X Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : HasFDerivAt X ((D.F.field t) 0) 0) (hY : DifferentiableAt ℝ Y (X 0)) (hleft : ∀ (y : EulerSmoothLimit.Space), Y (X y) = y) : ‖fderiv ℝ (fun (x : EulerSmoothLimit.Space) => fullWave τ hτ hτT B δ hδ ξ hs α k t (Y x)) (X 0)‖ = α / δ * (‖(D.normal.field t) 0‖ * ‖EulerPacketPrimaryFactorization.envelopedVelocity τ hτ hτT B δ hδ ξ hs (↑t) 0‖)

theorem EulerPacketPrimaryShear.fullWave_physical_normalized_gradient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α k : ℝ) (hk : k ≠ 0) (t : ↑(Set.Icc 0 D.T)) (X Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : HasFDerivAt X ((D.F.field t) 0) 0) (hY : DifferentiableAt ℝ Y (X 0)) (hleft : ∀ (y : EulerSmoothLimit.Space), Y (X y) = y) (hv : EulerPacketPrimaryFactorization.envelopedVelocity τ hτ hτT B δ hδ ξ hs (↑t) 0 ≠ 0) : fderiv ℝ (fun (x : EulerSmoothLimit.Space) => fullWave τ hτ hτT B δ hδ ξ hs α k t (Y x)) (X 0) = (α / δ * (‖(D.normal.field t) 0‖ * ‖EulerPacketPrimaryFactorization.envelopedVelocity τ hτ hτT B δ hδ ξ hs (↑t) 0‖)) • ((InnerProductSpace.rankOne ℝ) (EulerPacketNormalizedPrimary.unit (EulerPacketPrimaryFactorization.envelopedVelocity τ hτ hτT B δ hδ ξ hs (↑t) 0))) (EulerPacketNormalizedPrimary.unit ((D.normal.field t) 0))

The normalized rank-one expression is exactly the one in the source geometry record, with c=α/δ and the actual primary velocity.

theorem EulerPacketPrimaryShear.fullWave_physical_canonical_gradient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α k : ℝ) (hk : k ≠ 0) (t : ↑(Set.Icc 0 D.T)) (X Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : HasFDerivAt X ((D.F.field t) 0) 0) (hY : DifferentiableAt ℝ Y (X 0)) (hleft : ∀ (y : EulerSmoothLimit.Space), Y (X y) = y) : fderiv ℝ (fun (x : EulerSmoothLimit.Space) => fullWave τ hτ hτT B δ hδ ξ hs α k t (Y x)) (X 0) = (α / δ) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT B ξ hs (↑t) 0)) ((D.normal.field t) 0)

theorem EulerPacketPrimaryShear.fullWave_physical_canonical_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α k : ℝ) (hα : 0 ≤ α) (hk : k ≠ 0) (t : ↑(Set.Icc 0 D.T)) (X Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : HasFDerivAt X ((D.F.field t) 0) 0) (hY : DifferentiableAt ℝ Y (X 0)) (hleft : ∀ (y : EulerSmoothLimit.Space), Y (X y) = y) : ‖fderiv ℝ (fun (x : EulerSmoothLimit.Space) => fullWave τ hτ hτT B δ hδ ξ hs α k t (Y x)) (X 0)‖ = α / δ * (‖(D.normal.field t) 0‖ * ‖EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT B ξ hs (↑t) 0‖)

theorem EulerPacketPrimaryShear.fullWave_target_shear {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (h k : ℝ) (hh : 0 ≤ h) (hk : k ≠ 0) (t : ↑(Set.Icc 0 D.T)) (X Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : HasFDerivAt X ((D.F.field t) 0) 0) (hY : DifferentiableAt ℝ Y (X 0)) (hleft : ∀ (y : EulerSmoothLimit.Space), Y (X y) = y) (hv : EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT B ξ hs (↑t) 0 ≠ 0) : ‖fderiv ℝ (fun (x : EulerSmoothLimit.Space) => fullWave τ hτ hτT B δ hδ ξ hs (δ * h / (‖(D.normal.field t) 0‖ * ‖EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT B ξ hs (↑t) 0‖)) k t (Y x)) (X 0)‖ = h

The source amplitude choice gives exactly the requested center shear for the genuine primary, at any chosen target time. The size in this choice uses the velocity independent of the narrow profile δ.

theorem EulerPacketTerminalDatum.terminal_smul {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (δ : ℝ) (hδ : 0 < δ) (ξ : U) (a : ℝ) : terminal δ hδ (a • ξ) = a • terminal δ hδ ξ

theorem EulerPacketTerminalDatum.initialData_value_smul {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a : ℝ) : (initialData D δ hδ (a • ξ) hs).value = a • (initialData D δ hδ ξ hs).value

theorem EulerPacketPrimaryShear.vector_terminal_smul {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a : ℝ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerTransversePacketPrimary.vector τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, x, θ) = a • EulerTransversePacketPrimary.vector τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ ξ hs) (↑t, x, θ)

theorem EulerPacketPrimaryShear.scaled_terminal_wave_eq {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a k : ℝ) (t : ↑(Set.Icc 0 D.T)) : (fun (x : EulerSmoothLimit.Space) => k⁻¹ • EulerTransversePacketPrimary.vector τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, x, k * inner ℝ D.m₀ x)) = fullWave τ hτ hτT B δ hδ ξ hs a k t

theorem EulerPacketPrimaryShear.scaled_terminal_physical_gradient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a k : ℝ) (hk : k ≠ 0) (t : ↑(Set.Icc 0 D.T)) (X Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : HasFDerivAt X ((D.F.field t) 0) 0) (hY : DifferentiableAt ℝ Y (X 0)) (hleft : ∀ (y : EulerSmoothLimit.Space), Y (X y) = y) : fderiv ℝ (fun (x : EulerSmoothLimit.Space) => k⁻¹ • EulerTransversePacketPrimary.vector τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, Y x, k * inner ℝ D.m₀ (Y x))) (X 0) = (a / δ) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT B ξ hs (↑t) 0)) ((D.normal.field t) 0)

This derivative belongs to the literal primary used by the initialized packet, where the amplitude is inserted in its terminal datum.