Positive Square Root Norm Estimate
ProvedFunctionalInequalities.KLS.LogConcave.Suspension.norm_sub_one_le_of_isPositive_mul_self_readableThis is a technical estimate for positive continuous linear operators.
Let be a complete real inner-product normed space, and let be continuous linear maps. Assume that is positive and that , where multiplication denotes composition. Then
The result records that a positive square root is no farther from the identity, in operator norm, than its square. It is used in covariance-whitening and approximation arguments.
Original Lean declaration header
Within namespace FunctionalInequalities.KLS.LogConcave.Suspension. Shown in its original module context. Proof omitted.
theorem norm_sub_one_le_of_isPositive_mul_self
[CompleteSpace E]
{S Q : E →L[ℝ] E} (hS : S.IsPositive)
(hQ : S * S = Q) : ‖S - 1‖ ≤ ‖Q - 1‖
Module navigation
Module: KLS/BKL/CompactReduction.
Previous: cumulantBoundCompact_two_of_letwinCompact · Next: opNorm_le_of_inner_eq.
Source excerpt, lines 115–118 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_CompactReduction
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
theorem FunctionalInequalities.KLS.LogConcave.Suspension.norm_sub_one_le_of_isPositive_mul_self_readable
[CompleteSpace E]
{S Q : E →L[ℝ] E} (hS : S.IsPositive)
(hQ : S * S = Q) : ‖S - 1‖ ≤ ‖Q - 1‖ := by sorry