Tangency, the physical tangent ODE, and nonvanishing of the actual canonical primary. Nonvanishing follows from the prescribed nonzero terminal displacement, rather than from an assumption on the solved velocity.
theorem
EulerLinearDuhamel.Evolution.homogeneous_zero_at
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{T : ℝ}
{hT : 0 ≤ T}
{G : C(↑(Set.Icc 0 T), E →L[ℝ] E)}
(U : Evolution T hT G)
(f : ℝ → E)
(hf : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt f ((G t) (f ↑t)) (Set.Icc 0 T) ↑t)
(s t : ↑(Set.Icc 0 T))
(hs : f ↑s = 0)
:
A zero of a genuine homogeneous solution propagates in either time direction.
theorem
EulerCylinderDirichlet.Coefficients.labelVelocity_exists_ne_zero
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(x : EulerSmoothLimit.Space)
(ξ : U)
(hξ : ξ ≠ 0)
:
∃ (t : ↑(Set.Icc 0 T)), ((D.labelVelocity x) ξ) t ≠ 0
A nonzero terminal coordinate forces the actual physical history velocity to be nonzero at some time.
theorem
EulerPacketPrimaryFactorization.canonicalNormal_equation
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
theorem
EulerPacketPrimaryFactorization.canonicalVelocity_tangent
{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τ ⋯))
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
theorem
EulerPacketPrimaryFactorization.canonicalVelocity_equation
{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τ ⋯))
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
HasDerivWithinAt (fun (s : ℝ) => canonicalVelocity τ hτ hτT B ξ hs s x)
(-((D.M.field t) x) (canonicalVelocity τ hτ hτT B ξ hs (↑t) x) + (2 * inner ℝ ((D.normal.field t) x) (((D.M.field t) x) (canonicalVelocity τ hτ hτT B ξ hs (↑t) x)) / ‖(D.normal.field t) x‖ ^ 2) • (D.normal.field t) x)
(Set.Icc 0 D.T) ↑t
theorem
EulerPacketPrimaryFactorization.canonicalVelocity_ne_zero
{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τ ⋯))
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(hξ : ξ ≠ 0)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(hx : EulerSpatialCutoffs.innerCutoff x ≠ 0)
:
theorem
EulerPacketPrimaryFactorization.canonicalVelocity_center_ne_zero
{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τ ⋯))
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(hξ : ξ ≠ 0)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerPacketPrimaryFactorization.canonical_size_pos
{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τ ⋯))
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(hξ : ξ ≠ 0)
(t : ↑(Set.Icc 0 D.T))
:
noncomputable def
EulerPacketPrimaryFactorization.canonicalVelocityPath
{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τ ⋯))
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(x : EulerSmoothLimit.Space)
:
Canonical velocity path, bundling toFun, continuous_toFun.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketPrimaryFactorization.canonical_amplitude_pos
{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τ ⋯))
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(hξ : ξ ≠ 0)
(t : ↑(Set.Icc 0 D.T))
(δ h : ℝ)
(hδ : 0 < δ)
(hh : 0 < h)
:
theorem
EulerPacketPrimaryFactorization.scaled_terminal_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τ ⋯))
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(hξ : ξ ≠ 0)
(δ : ℝ)
(hδ : 0 < δ)
(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)
:
The actual scaled terminal datum achieves the requested primary gradient norm; nonvanishing is proved from its nonzero terminal direction.