The actual compact primary has exactly the source rank-one shear at zero phase throughout its history interval, including the activation time. No derivative of the finite-dimensional history is postulated.
theorem
EulerPacketPrimaryShear.zero_slice_hasFDerivAt
(A : EulerSmoothLimit.Space × ℝ → EulerSmoothLimit.Space)
(x a : EulerSmoothLimit.Space)
(hA : DifferentiableAt ℝ A (x, 0))
(hzero : ∀ (y : EulerSmoothLimit.Space), A (y, 0) = 0)
(ha : HasDerivAt (fun (θ : ℝ) => A (x, θ)) a 0)
:
theorem
EulerPacketPrimaryShear.zero_phase_graph_hasFDerivAt
(A : EulerSmoothLimit.Space × ℝ → EulerSmoothLimit.Space)
(a m : EulerSmoothLimit.Space)
(hA : DifferentiableAt ℝ A (0, 0))
(hzero : ∀ (y : EulerSmoothLimit.Space), A (y, 0) = 0)
(ha : HasDerivAt (fun (θ : ℝ) => A (0, θ)) a 0)
(c k : ℝ)
:
HasFDerivAt (fun (y : EulerSmoothLimit.Space) => c • A (y, k * inner ℝ m y))
((c * k) • ((InnerProductSpace.rankOne ℝ) a) m) 0
theorem
EulerPacketPrimaryShear.rankOne_normalized
(c : ℝ)
(v m : EulerSmoothLimit.Space)
(hv : v ≠ 0)
(hm : m ≠ 0)
:
c • ((InnerProductSpace.rankOne ℝ) v) m = (c * (‖m‖ * ‖v‖)) • ((InnerProductSpace.rankOne ℝ) (EulerPacketNormalizedPrimary.unit v)) (EulerPacketNormalizedPrimary.unit m)
noncomputable def
EulerPacketPrimaryShear.historyWave
{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 τ))
(y : EulerSmoothLimit.Space)
:
The literal leading primary on the physical phase graph in label coordinates.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketPrimaryShear.historyWave_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 τ))
:
HasFDerivAt (historyWave τ hτ hτT B δ hδ ξ hs α k t)
((α / δ) • ((InnerProductSpace.rankOne ℝ) (((B.coefficients.labelVelocity 0) ξ) t)) D.m₀) 0
theorem
EulerPacketPrimaryShear.historyWave_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 τ))
(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) => historyWave τ hτ hτT B δ hδ ξ hs α k t (Y x))
((α / δ) • ((InnerProductSpace.rankOne ℝ) (((B.coefficients.labelVelocity 0) ξ) t)) ((D.normal.field ⟨↑t, ⋯⟩) 0))
(X 0)
The physical gradient uses the actual inverse Jacobian, producing the normal F⁻ᵀm₀ rather than the initial direction m₀.
theorem
EulerPacketPrimaryShear.historyWave_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 τ))
(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) => historyWave τ hτ hτT B δ hδ ξ hs α k t (Y x)) (X 0)‖ = α / δ * (‖((B.coefficients.labelVelocity 0) ξ) t‖ * ‖(D.normal.field ⟨↑t, ⋯⟩) 0‖)