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

Proved

BookProof.WeylHamiltonian.weylHamiltonian_expectation_nonneg

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterWeylHamiltonian.

BookProof.WeylHamiltonian.weylHamiltonian_expectation_nonneg {n m : ℕ} (π : Fin n → H →L[ℂ] H) (B : Fin m → H →L[ℂ] H) (hπ : ∀ i, IsSelfAdjoint (π i)) (hB : ∀ a, IsSelfAdjoint (B a)) (x : H) : 0 ≤ RCLike.re (inner ℂ ((weylHamiltonian π B) x) x)

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

Preamble

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

View graph