`BookProof.WeylHamiltonian.smul_nonneg_isPositive` (T : H →L[ℂ] H) (h : T.IsPositive) {c : ℝ} (hc : 0 ≤ c) : ((c : ℂ) • T).IsPositive

Proved

BookProof.WeylHamiltonian.smul_nonneg_isPositive

by leonardopedro · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterWeylHamiltonian.

BookProof.WeylHamiltonian.smul_nonneg_isPositive (T : H →L[ℂ] H) (h : T.IsPositive) {c : ℝ} (hc : 0 ≤ c) : ((c : ℂ) • T).IsPositive

Formalization note: Lean 4 identifier BookProof.WeylHamiltonian.smul_nonneg_isPositive.

Preamble

-- Generated from ChapterWeylHamiltonian.lean — theorem BookProof.WeylHamiltonian.smul_nonneg_isPositive
import Mathlib
import Definitions.Def_ChapterWeylHamiltonian
open BookProof.WeylHamiltonian



open ContinuousLinearMap
open scoped BigOperators

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]

Formal statement

theorem BookProof.WeylHamiltonian.smul_nonneg_isPositive (T : H →L[ℂ] H) (h : T.IsPositive)
    {c : ℝ} (hc : 0 ≤ c) : ((c : ℂ) • T).IsPositive := by sorry

View graph