Coercive operator transport between Hilbert models

This elementary operator lemma applies equally to mean and transverse displacement spaces, including forms with nonlocal initial-trace terms.

noncomputable def EulerHilbertCoerciveTransport.transportedOperator {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] (D : V →L[ℝ] W) (A : W →L[ℝ] W) : V →L[ℝ] V

Pull a genuine bounded operator back along a bounded linear coordinate map.

Equations

• EulerHilbertCoerciveTransport.transportedOperator D A = ContinuousLinearMap.adjoint D ∘SL A ∘SL D

theorem EulerHilbertCoerciveTransport.transportedOperator_inner {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] (D : V →L[ℝ] W) (A : W →L[ℝ] W) (u v : V) : inner ℝ ((transportedOperator D A) u) v = inner ℝ (A (D u)) (D v)

The transported bilinear form is exactly the original form on the image.

theorem EulerHilbertCoerciveTransport.transportedOperator_coercive {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] (D : V →L[ℝ] W) (A : W →L[ℝ] W) (a d : ℝ) (ha : 0 ≤ a) (hA : ∀ (w : W), a * ‖w‖ ^ 2 ≤ inner ℝ (A w) w) (hD : ∀ (v : V), d * ‖v‖ ^ 2 ≤ ‖D v‖ ^ 2) (v : V) : a * d * ‖v‖ ^ 2 ≤ inner ℝ ((transportedOperator D A) v) v

Coercivity transports using only a proved lower bound for the coordinate map.

theorem EulerHilbertCoerciveTransport.transported_forcing_inner {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] (D : V →L[ℝ] W) (f : W) (v : V) : inner ℝ ((ContinuousLinearMap.adjoint D) f) v = inner ℝ f (D v)

The transported forcing is the actual adjoint pullback.