Commit 2023-06-01 14:53 c34b1e7b

View on Github →

feat: port Analysis.InnerProductSpace.Positive (#4553)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/InnerProductSpace/Positive.lean

added theorem ContinuousLinearMap.IsPositive.add

added theorem ContinuousLinearMap.IsPositive.adjoint_conj

added theorem ContinuousLinearMap.IsPositive.conj_adjoint

added theorem ContinuousLinearMap.IsPositive.conj_orthogonalProjection

added theorem ContinuousLinearMap.IsPositive.inner_nonneg_left

added theorem ContinuousLinearMap.IsPositive.inner_nonneg_right

added theorem ContinuousLinearMap.IsPositive.isSelfAdjoint

added theorem ContinuousLinearMap.IsPositive.orthogonalProjection_comp

added def ContinuousLinearMap.IsPositive

added theorem ContinuousLinearMap.isPositive_iff_complex

added theorem ContinuousLinearMap.isPositive_one

added theorem ContinuousLinearMap.isPositive_zero