The genuine transverse Gram inverse

The inverse of Q*Q, for Q = F R⊥, is constructed from the lower frame bound. Its inverse identities and derivative follow from the already proved coercive operator inverse, not from an assumed matrix inverse.

noncomputable def EulerTransverseGramInverse.realAdjoint {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : (U →L[ℝ] E) →L[ℝ] E →L[ℝ] U

Taking an adjoint is an actual bounded real-linear map.

Equations

• EulerTransverseGramInverse.realAdjoint = { toFun := fun (Q : U →L[ℝ] E) => ContinuousLinearMap.adjoint Q, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

noncomputable def EulerTransverseGramInverse.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) : U →L[ℝ] U

The transverse Gram matrix as a genuine bounded operator.

Equations

• EulerTransverseGramInverse.gram Q = ContinuousLinearMap.adjoint Q ∘SL Q

theorem EulerTransverseGramInverse.gram_inner {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : U →L[ℝ] E) (x : U) : inner ℝ ((gram Q) x) x = ‖Q x‖ ^ 2

The Gram quadratic form is precisely the squared physical-frame norm.

theorem EulerTransverseGramInverse.gram_coercive {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 : ℝ) (hQ : ∀ (x : U), c * ‖x‖ ^ 2 ≤ ‖Q x‖ ^ 2) (x : U) : c * ‖x‖ ^ 2 ≤ inner ℝ ((gram Q) x) x

A lower frame bound is a coercivity bound for the actual Gram matrix.

noncomputable def EulerTransverseGramInverse.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 : ∀ (x : U), c * ‖x‖ ^ 2 ≤ ‖Q x‖ ^ 2) : U →L[ℝ] U

The Gram inverse is constructed by the actual coercive solver.

Equations

• EulerTransverseGramInverse.gramInverse Q c hc hQ = EulerCoerciveProjection.coerciveInverse (EulerTransverseGramInverse.gram Q) c hc ⋯

theorem EulerTransverseGramInverse.gram_inverse_apply {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 : ∀ (x : U), c * ‖x‖ ^ 2 ≤ ‖Q x‖ ^ 2) (x : U) : (gram Q) ((gramInverse Q c hc hQ) x) = x

The constructed Gram inverse is a right inverse.

theorem EulerTransverseGramInverse.inverse_gram_apply {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 : ∀ (x : U), c * ‖x‖ ^ 2 ≤ ‖Q x‖ ^ 2) (x : U) : (gramInverse Q c hc hQ) ((gram Q) x) = x

The constructed Gram inverse is a left inverse.

theorem EulerTransverseGramInverse.gramInverse_norm {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 : ∀ (x : U), c * ‖x‖ ^ 2 ≤ ‖Q x‖ ^ 2) : ‖gramInverse Q c hc hQ‖ ≤ c⁻¹

The inverse norm retains the quantitative lower frame bound.

noncomputable def EulerTransverseGramInverse.frameLeftInverse {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 : ∀ (x : U), c * ‖x‖ ^ 2 ≤ ‖Q x‖ ^ 2) : E →L[ℝ] U

A canonical bounded left inverse for the physical transverse frame.

Equations

• EulerTransverseGramInverse.frameLeftInverse Q c hc hQ = EulerTransverseGramInverse.gramInverse Q c hc hQ ∘SL ContinuousLinearMap.adjoint Q

theorem EulerTransverseGramInverse.frameLeftInverse_apply {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 : ∀ (x : U), c * ‖x‖ ^ 2 ≤ ‖Q x‖ ^ 2) (x : U) : (frameLeftInverse Q c hc hQ) (Q x) = x

The canonical left inverse recovers every transverse coordinate.

theorem EulerTransverseGramInverse.hasDerivAt_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) (t : ℝ) (hQ : HasDerivAt Q Q₁ t) : HasDerivAt (fun (s : ℝ) => ContinuousLinearMap.adjoint (Q s)) (ContinuousLinearMap.adjoint Q₁) t

Differentiating the actual adjoint commutes with the real derivative.

theorem EulerTransverseGramInverse.hasDerivAt_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) (t : ℝ) (hQ : HasDerivAt Q Q₁ t) : HasDerivAt (fun (s : ℝ) => gram (Q s)) (ContinuousLinearMap.adjoint Q₁ ∘SL Q t + ContinuousLinearMap.adjoint (Q t) ∘SL Q₁) t

The Gram derivative is the literal product rule.

theorem EulerTransverseGramInverse.hasDerivAt_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 : ∀ (s : ℝ) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q s) x‖ ^ 2) (Q₁ : U →L[ℝ] E) (t : ℝ) (hd : HasDerivAt Q Q₁ t) : HasDerivAt (fun (s : ℝ) => gramInverse (Q s) c hc ⋯) (-gramInverse (Q t) c hc ⋯ ∘SL (ContinuousLinearMap.adjoint Q₁ ∘SL Q t + ContinuousLinearMap.adjoint (Q t) ∘SL Q₁) ∘SL gramInverse (Q t) c hc ⋯) t

The constructed Gram inverse has the actual inverse derivative.

noncomputable def EulerTransverseGramInverse.adjointPath {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), E →L[ℝ] U)

The adjoint of a continuous coefficient path is a continuous coefficient path.

Equations

• EulerTransverseGramInverse.adjointPath T Q = { toFun := fun (t : ↑(Set.Icc 0 T)) => ContinuousLinearMap.adjoint (Q t), continuous_toFun := ⋯ }

theorem EulerTransverseGramInverse.timeMultiplier_adjoint {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 : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : ContinuousLinearMap.adjoint (EulerTimeLp.timeMultiplier T hT Q) = EulerTimeLp.timeMultiplier T hT (adjointPath T Q)

The actual Bochner multiplier adjoint is pointwise transposition of the coefficient.