Positivity Of A Right Inverse

This statement shows that a right inverse of a strictly positive operator is strictly positive.

Let E be a real inner-product normed additive group, and let T and B be continuous linear endomorphisms of E. Assume

1. for every nonzero v, $\langle Tv,v\rangle>0$;
2. $T\circ B=\operatorname{id}_E$.

Then for every nonzero v,

The result is a generic operator-positivity lemma applicable to right inverses, without a finite-dimensional assumption.

Formalization Note The inner products are real-valued and the conclusion is strict positivity for every vector explicitly assumed nonzero.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem inner_self_pos_of_comp_eq_id (T B : E →L[ℝ] E)
    (hpos : ∀ v : E, v ≠ 0 → 0 < ⟪T v, v⟫)
    (hTB : T.comp B = ContinuousLinearMap.id ℝ E) {v : E} (hv : v ≠ 0) :
    0 < ⟪B v, v⟫

Module navigation

Module: Analysis/Operator/Positive.

Source excerpt, lines 62–65 · Frozen source 408915f.