Time-dependent inverse of a coercive transverse Gram matrix

The coefficient inverse and its derivative are constructed from the frame and its quantitative lower bound. These are coefficient theorems, independent of any chosen variational solution.

theorem EulerTransverseGramPath.hasDerivWithinAt_adjoint {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : ℝ → U →L[ℝ] E) (Q₁ : U →L[ℝ] E) (s : Set ℝ) (t : ℝ) (hQ : HasDerivWithinAt Q Q₁ s t) : HasDerivWithinAt (fun (r : ℝ) => ContinuousLinearMap.adjoint (Q r)) (ContinuousLinearMap.adjoint Q₁) s t

The within-set derivative of an actual adjoint.

theorem EulerTransverseGramPath.hasDerivWithinAt_gram {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : ℝ → U →L[ℝ] E) (Q₁ : U →L[ℝ] E) (s : Set ℝ) (t : ℝ) (hQ : HasDerivWithinAt Q Q₁ s t) : HasDerivWithinAt (fun (r : ℝ) => EulerTransverseGramInverse.gram (Q r)) (ContinuousLinearMap.adjoint Q₁ ∘SL Q t + ContinuousLinearMap.adjoint (Q t) ∘SL Q₁) s t

The within-set derivative of an actual Gram matrix.

theorem EulerTransverseGramPath.hasDerivWithinAt_gramInverse {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : ℝ → U →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hQ : ∀ (r : ℝ) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q r) x‖ ^ 2) (Q₁ : U →L[ℝ] E) (s : Set ℝ) (t : ℝ) (hd : HasDerivWithinAt Q Q₁ s t) : HasDerivWithinAt (fun (r : ℝ) => EulerTransverseGramInverse.gramInverse (Q r) c hc ⋯) (-EulerTransverseGramInverse.gramInverse (Q t) c hc ⋯ ∘SL (ContinuousLinearMap.adjoint Q₁ ∘SL Q t + ContinuousLinearMap.adjoint (Q t) ∘SL Q₁) ∘SL EulerTransverseGramInverse.gramInverse (Q t) c hc ⋯) s t

Actual inverse differentiation is valid within the time interval, including endpoints.

noncomputable def EulerTransverseGramPath.gramPath {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : C(↑(Set.Icc 0 T), U →L[ℝ] U)

Continuous Gram coefficient, constructed by the actual adjoint and composition.

Equations

• EulerTransverseGramPath.gramPath T Q = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerTransverseGramInverse.gram (Q t), continuous_toFun := ⋯ }

noncomputable def EulerTransverseGramPath.gramDerivativePath {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(↑(Set.Icc 0 T), U →L[ℝ] U)

Continuous derivative coefficient of the Gram matrix.

Equations

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

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

The genuinely constructed Gram inverse varies continuously on the interval.

Equations

• EulerTransverseGramPath.gramInversePath T Q c hc hQ = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerTransverseGramInverse.gramInverse (Q t) c hc ⋯, continuous_toFun := ⋯ }

noncomputable def EulerTransverseGramPath.gramInverseDerivativePath {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)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) : C(↑(Set.Icc 0 T), U →L[ℝ] U)

Explicit continuous coefficient of the inverse derivative -K⁻¹ K' K⁻¹.

Equations

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

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

The canonical left-inverse coefficient is continuous.

Equations

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

noncomputable def EulerTransverseGramPath.frameLeftInverseDerivativePath {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)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) : C(↑(Set.Icc 0 T), E →L[ℝ] U)

The continuous coefficient of the derivative of the frame left inverse.

Equations

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

theorem EulerTransverseGramPath.gramInversePath_hasDerivWithinAt {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)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (hT : 0 ≤ T) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (gramInversePath T Q c hc hQ)) ((gramInverseDerivativePath T Q Q₁ c hc hQ) t) (Set.Icc 0 T) ↑t

The constructed inverse coefficient has its claimed within-interval derivative.

theorem EulerTransverseGramPath.frameLeftInversePath_hasDerivWithinAt {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)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (hT : 0 ≤ T) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (frameLeftInversePath T Q c hc hQ)) ((frameLeftInverseDerivativePath T Q Q₁ c hc hQ) t) (Set.Icc 0 T) ↑t

The constructed frame left inverse has its claimed within-interval derivative.