Strict Positivity Of A Positive Operator Unit
ProvedFunctionalInequalities.Analysis.inner_self_pos_of_isPositive_of_isUnit_readableThis statement proves that a positive invertible operator is strictly positive.
Let E be a finite-dimensional real inner-product space, let ι be a finite index type with decidable equality, and let b be an orthonormal basis of E indexed by ι. Let T be a continuous linear endomorphism. Assume T is positive in the operator sense and is a unit. Then every nonzero v∈E satisfies
This provides the converse positivity fact needed when transferring positive-definite matrix properties to operators in orthonormal coordinates.
Formalization Note Finite dimensionality and the chosen finite orthonormal basis are explicit hypotheses of the Lean statement.
Original Lean declaration header
Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.
theorem inner_self_pos_of_isPositive_of_isUnit (b : OrthonormalBasis ι ℝ E)
(T : E →L[ℝ] E) (hpos : T.IsPositive) (hunit : IsUnit T)
{v : E} (hv : v ≠ 0) : 0 < ⟪T v, v⟫
Module navigation
Module: Analysis/Operator/Coordinates.
Source excerpt, lines 151–153 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Operator_Coordinates
open scoped RealInnerProductSpace MatrixOrder
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
variable [FiniteDimensional ℝ E] {ι : Type*} [Fintype ι] [DecidableEq ι]
theorem FunctionalInequalities.Analysis.inner_self_pos_of_isPositive_of_isUnit_readable (b : OrthonormalBasis ι ℝ E)
(T : E →L[ℝ] E) (hpos : T.IsPositive) (hunit : IsUnit T)
{v : E} (hv : v ≠ 0) : 0 < ⟪T v, v⟫ := by sorry