`BookProof.WeylHamiltonian.weylHamiltonian_isPositive` {n m : ℕ} (π : Fin n → H →L[ℂ] H) (B : Fin m → H →L[ℂ] H) (hπ : ∀ i, IsSelfAdjoint (π i)) (hB : ∀ a, IsSelfAdjoint (B...

Proved

BookProof.WeylHamiltonian.weylHamiltonian_isPositive

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterWeylHamiltonian.

BookProof.WeylHamiltonian.weylHamiltonian_isPositive {n m : ℕ} (π : Fin n → H →L[ℂ] H) (B : Fin m → H →L[ℂ] H) (hπ : ∀ i, IsSelfAdjoint (π i)) (hB : ∀ a, IsSelfAdjoint (B a)) : (weylHamiltonian π B).IsPositive

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

Preamble

-- Generated from ChapterWeylHamiltonian.lean — theorem BookProof.WeylHamiltonian.weylHamiltonian_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.weylHamiltonian_isPositive {n m : ℕ}
    (π : Fin n → H →L[ℂ] H) (B : Fin m → H →L[ℂ] H)
    (hπ : ∀ i, IsSelfAdjoint (π i)) (hB : ∀ a, IsSelfAdjoint (B a)) :
    (weylHamiltonian π B).IsPositive := by sorry

View graph