Continuous acceleration and classical time derivatives for the mean inverse #
With a continuous representative of the prescribed forcing, the actual strong equation constructs continuous coordinate acceleration and physical time derivative. The original AC paths have these derivatives at every interior time, and within the interval at both endpoints.
@[instance_reducible]
Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass
synthesis.
Instances For
@[instance_reducible]
Cache the standard InnerProductSpace ℝ solenoidalSpace instance to shorten typeclass
synthesis.
Instances For
@[instance_reducible]
Cache the standard NormedAddCommGroup (solenoidalSpace →L[ℝ] L2) instance to shorten
typeclass synthesis.
Instances For
def
EulerMeanVariationalInverse.StrongMeanEvolution.coordinateVelocityPath
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
:
The original coordinate velocity is continuous on the closed time interval.
Equations
Instances For
@[simp]
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.coordinateVelocityPath_apply
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(t : ↑(Set.Icc 0 T))
:
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.coordinateVelocityPath_ae
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
:
This is a continuous representative of the actual L² coordinate velocity.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.coordinateVelocityPath_norm
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(hTpos : 0 < T)
:
The coordinate path has the actual H¹ trace bound.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.gram_equation_ae
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
:
∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, (EulerTransverseGramInverse.gram (EulerVolterraConvolution.extendPath T hT (solenoidalFrame T F) t))
(↑↑s.acceleration t) = (ContinuousLinearMap.adjoint ((solenoidalFrame T F) (Set.projIcc 0 T hT t)))
(↑↑f t - 2 • ((solenoidalFrame T F₁) (Set.projIcc 0 T hT t)) (↑↑s.velocityLp t))
The already proved projected equation is the ordinary solenoidal Gram equation.
noncomputable def
EulerMeanVariationalInverse.StrongMeanEvolution.classicalAcceleration
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
:
Continuous coordinate acceleration constructed by the actual Gram inverse.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.classicalAcceleration_norm
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
:
Its norm is the source's ordinary inverse-Gram estimate for time suprema.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.classicalAcceleration_ae
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
(hf : ↑↑f =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT fC)
:
↑↑s.acceleration =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT (s.classicalAcceleration c hc hLower fC)
The L² acceleration is genuinely represented by this continuous path.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.velocity_hasDerivWithinAt
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
(hf : ↑↑f =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT fC)
(t : ↑(Set.Icc 0 T))
:
HasDerivWithinAt s.velocity ((s.classicalAcceleration c hc hLower fC) t) (Set.Icc 0 T) ↑t
Coordinate velocity has the classical acceleration at every time within the interval.
noncomputable def
EulerMeanVariationalInverse.StrongMeanEvolution.classicalPhysicalDerivative
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
:
The physical derivative path is the actual continuous product-rule expression.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.classicalPhysicalDerivative_ae
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
(hf : ↑↑f =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT fC)
:
↑↑s.velocityDerivative =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT (s.classicalPhysicalDerivative c hc hLower fC)
This continuous path is the already constructed physical derivative B_t.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.physical_hasDerivWithinAt
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
(hf : ↑↑f =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT fC)
(hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F₁ t) (Set.Icc 0 T) ↑t)
(t : ↑(Set.Icc 0 T))
:
HasDerivWithinAt s.physicalPath ((s.classicalPhysicalDerivative c hc hLower fC) t) (Set.Icc 0 T) ↑t
The original physical mean velocity now has a classical time derivative at every time, including the endpoint derivatives within the interval.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.classicalPhysicalDerivative_norm
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
:
The physical time-derivative supremum pays only the two coefficient factors.