Classical time evolution for the fixed-coordinate Dirichlet solve #
Continuous forcing gives a continuous Gram acceleration. The genuine H¹ velocity therefore has its actual derivative throughout the closed interval. The displacement keeps both zero endpoint conditions.
noncomputable def
EulerTransverseFixedEvolution.classicalAcceleration
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(f : C(↑(Set.Icc 0 T), E))
:
Classical acceleration, constructed using
EulerContinuousGramAcceleration.accelerationPath.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerTransverseFixedEvolution.displacementPath
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(f : ↥(EulerTimeLp.TimeLp T E))
:
Displacement path, given by terminalPrimitive T hT (velocityLp T hT Q Q₁ H c hc hQ hd K hK hH hsmall f).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerTransverseFixedEvolution.physicalVelocityPath
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(f : C(↑(Set.Icc 0 T), E))
:
Physical velocity path, given by multiplier Q (velocityPath T hT Q Q₁ H c hc hQ hd K hK hH hsmall (pathLp T hT f)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerTransverseFixedEvolution.physicalDerivativePath
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(f : C(↑(Set.Icc 0 T), E))
:
Physical derivative path, constructed using multiplier.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerTransverseFixedEvolution.displacementPath_initial
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(f : ↥(EulerTimeLp.TimeLp T E))
:
theorem
EulerTransverseFixedEvolution.displacementPath_terminal
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(f : ↥(EulerTimeLp.TimeLp T E))
:
theorem
EulerTransverseFixedEvolution.classicalAcceleration_equation
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(f : C(↑(Set.Icc 0 T), E))
(t : ↑(Set.Icc 0 T))
:
(EulerTransverseGramInverse.gram (Q t)) ((classicalAcceleration T hT Q Q₁ H c hc hQ hd K hK hH hsmall f) t) = (ContinuousLinearMap.adjoint (Q t))
(f t - 2 • (Q₁ t) (((velocityPath T hT Q Q₁ H c hc hQ hd K hK hH hsmall) (EulerTimeLp.pathLp T hT f)) t))
theorem
EulerTransverseFixedEvolution.classicalAcceleration_ae
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t)
(hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t)
(hTpos : 0 < T)
(f : C(↑(Set.Icc 0 T), E))
:
↑↑((accelerationLp T hT Q Q₁ H c hc hQ hd K hK hH hsmall) (EulerTimeLp.pathLp T hT f)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT (classicalAcceleration T hT Q Q₁ H c hc hQ hd K hK hH hsmall f)
theorem
EulerTransverseFixedEvolution.velocityPath_hasDerivWithinAt
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t)
(hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t)
(hTpos : 0 < T)
(f : C(↑(Set.Icc 0 T), E))
(t : ↑(Set.Icc 0 T))
:
HasDerivWithinAt
(EulerVolterraConvolution.extendPath T hT
((velocityPath T hT Q Q₁ H c hc hQ hd K hK hH hsmall) (EulerTimeLp.pathLp T hT f)))
((classicalAcceleration T hT Q Q₁ H c hc hQ hd K hK hH hsmall f) t) (Set.Icc 0 T) ↑t
The actual coordinate history has the genuine time derivative in (10), including within-interval derivatives at both endpoints.
theorem
EulerTransverseFixedEvolution.displacementPath_hasDerivWithinAt
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t)
(hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t)
(hTpos : 0 < T)
(f : C(↑(Set.Icc 0 T), E))
(t : ↑(Set.Icc 0 T))
:
HasDerivWithinAt
(EulerVolterraConvolution.extendPath T hT
(displacementPath T hT Q Q₁ H c hc hQ hd K hK hH hsmall (EulerTimeLp.pathLp T hT f)))
(((velocityPath T hT Q Q₁ H c hc hQ hd K hK hH hsmall) (EulerTimeLp.pathLp T hT f)) t) (Set.Icc 0 T) ↑t
theorem
EulerTransverseFixedEvolution.physicalVelocityPath_hasDerivWithinAt
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t)
(hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t)
(hTpos : 0 < T)
(f : C(↑(Set.Icc 0 T), E))
(t : ↑(Set.Icc 0 T))
:
HasDerivWithinAt
(EulerVolterraConvolution.extendPath T hT (physicalVelocityPath T hT Q Q₁ H c hc hQ hd K hK hH hsmall f))
((physicalDerivativePath T hT Q Q₁ H c hc hQ hd K hK hH hsmall f) t) (Set.Icc 0 T) ↑t