Commit 2022-07-23 22:32 0179605f

View on Github →

feat(analysis/inner_product_space/positive): definition and basic facts about positive operators (#15470)

Estimated changes

Modified src/analysis/inner_product_space/adjoint.lean

added theorem continuous_linear_map.is_self_adjoint_iff_adjoint_eq

added theorem inner_product_space.is_self_adjoint.add

added theorem inner_product_space.is_self_adjoint.adjoint_conj

added theorem inner_product_space.is_self_adjoint.adjoint_eq

added theorem inner_product_space.is_self_adjoint.conj_adjoint

added theorem inner_product_space.is_self_adjoint.conj_orthogonal_projection

added theorem inner_product_space.is_self_adjoint_id

added theorem inner_product_space.is_self_adjoint_zero

added theorem inner_product_space.orthogonal_projection_is_self_adjoint

added theorem submodule.adjoint_orthogonal_projection

added theorem submodule.adjoint_subtypeL

Created src/analysis/inner_product_space/positive.lean

added theorem continuous_linear_map.is_positive.add

added theorem continuous_linear_map.is_positive.adjoint_conj

added theorem continuous_linear_map.is_positive.conj_adjoint

added theorem continuous_linear_map.is_positive.conj_orthogonal_projection

added theorem continuous_linear_map.is_positive.inner_nonneg_left

added theorem continuous_linear_map.is_positive.inner_nonneg_right

added theorem continuous_linear_map.is_positive.is_self_adjoint

added theorem continuous_linear_map.is_positive.orthogonal_projection_comp

added def continuous_linear_map.is_positive

added theorem continuous_linear_map.is_positive_id

added theorem continuous_linear_map.is_positive_iff_complex

added theorem continuous_linear_map.is_positive_zero