Continuous acceleration from the genuine Gram inverse

A continuous velocity and continuous forcing give an actual continuous acceleration path through the previously constructed positive Gram inverse. Its norm and its identification with the strong L² acceleration are proved directly, for arbitrary complete real Hilbert coefficient spaces.

noncomputable def EulerContinuousGramAcceleration.accelerationPath {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (v : C(↑(Set.Icc 0 T), U)) (f : C(↑(Set.Icc 0 T), E)) : C(↑(Set.Icc 0 T), U)

The actual continuous acceleration recovered from velocity and forcing.

Equations

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

@[simp]

theorem EulerContinuousGramAcceleration.accelerationPath_apply {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (v : C(↑(Set.Icc 0 T), U)) (f : C(↑(Set.Icc 0 T), E)) (t : ↑(Set.Icc 0 T)) : (accelerationPath T Q Q₁ c hc hQ v f) t = (EulerTransverseGramInverse.gramInverse (Q t) c hc ⋯) ((ContinuousLinearMap.adjoint (Q t)) (f t - 2 • (Q₁ t) (v t)))

theorem EulerContinuousGramAcceleration.accelerationPath_equation {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (v : C(↑(Set.Icc 0 T), U)) (f : C(↑(Set.Icc 0 T), E)) (t : ↑(Set.Icc 0 T)) : (EulerTransverseGramInverse.gram (Q t)) ((accelerationPath T Q Q₁ c hc hQ v f) t) = (ContinuousLinearMap.adjoint (Q t)) (f t - 2 • (Q₁ t) (v t))

The strong projected equation holds at every time for this path.

theorem EulerContinuousGramAcceleration.accelerationPath_norm {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (v : C(↑(Set.Icc 0 T), U)) (f : C(↑(Set.Icc 0 T), E)) : ‖accelerationPath T Q Q₁ c hc hQ v f‖ ≤ c⁻¹ * ‖Q‖ * (‖f‖ + 2 * ‖Q₁‖ * ‖v‖)

The continuous acceleration has the same explicit coefficient bound as the L² inverse.

theorem EulerContinuousGramAcceleration.accelerationPath_ae {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (hT : 0 ≤ T) (v a : ↥(EulerTimeLp.TimeLp T U)) (f : ↥(EulerTimeLp.TimeLp T E)) (vC : C(↑(Set.Icc 0 T), U)) (fC : C(↑(Set.Icc 0 T), E)) (hv : ↑↑v =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT vC) (hf : ↑↑f =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT fC) (heq : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, (EulerTransverseGramInverse.gram (EulerVolterraConvolution.extendPath T hT Q t)) (↑↑a t) = (ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T hT Q t)) (↑↑f t - 2 • (EulerVolterraConvolution.extendPath T hT Q₁ t) (↑↑v t))) : ↑↑a =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT (accelerationPath T Q Q₁ c hc hQ vC fC)

Every genuine L² strong acceleration with the given continuous data is almost everywhere this constructed continuous path.