isPositive_linearIsometryEquiv_conj_iff

English

Positivity is preserved under a linear isometry with complex conjugation, i.e., conjugate-aligned isometry preserves IsPositive.

Русский

Положительность сохраняется при применении линейной изометрии с сопряжением комплексного поля.

LaTeX

$$$$\text{IsPositive}(f^{-*} T f) \iff \text{IsPositive}(T)$$$$

Lean4

theorem isPositive_linearIsometryEquiv_conj_iff {T : E →ₗ[𝕜] E} (f : E ≃ₗᵢ[𝕜] F) :
    IsPositive (f.toLinearMap ∘ₗ T ∘ₗ f.symm.toLinearMap) ↔ IsPositive T :=
  by
  simp_rw [IsPositive, isSymmetric_linearIsometryEquiv_conj_iff, and_congr_right_iff,
    LinearIsometryEquiv.toLinearEquiv_symm, coe_comp, LinearEquiv.coe_coe, LinearIsometryEquiv.coe_toLinearEquiv,
    LinearIsometryEquiv.coe_symm_toLinearEquiv, Function.comp_apply, LinearIsometryEquiv.inner_map_eq_flip]
  exact fun _ => ⟨fun h x => by simpa using h (f x), fun h x => h _⟩

Похожие утверждения