`BookProof.ChapterF4.hermitian_flow_preserves_normSq` {n : ℕ} (H : Matrix (Fin n) (Fin n) ℂ) (hH : H.IsHermitian) (t : ℝ) (c : Fin n → ℂ) : star ((NormedSpace.exp ((-Complex.I * (t

Proved

BookProof.ChapterF4.hermitian_flow_preserves_normSq

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterF4.

BookProof.ChapterF4.hermitian_flow_preserves_normSq {n : ℕ} (H : Matrix (Fin n) (Fin n) ℂ) (hH : H.IsHermitian) (t : ℝ) (c : Fin n → ℂ) : star ((NormedSpace.exp ((-Complex.I * (t : ℂ)) • H)).mulVec c) ⬝ᵥ (NormedSpace.exp ((-Complex.I * (t : ℂ)) • H)).mulVec c = star c ⬝ᵥ c

Formalization note: Lean 4 identifier BookProof.ChapterF4.hermitian_flow_preserves_normSq.

Preamble

-- Generated from ChapterF4.lean — theorem BookProof.ChapterF4.hermitian_flow_preserves_normSq
import Mathlib
import Definitions.Def_ChapterF4
open BookProof.ChapterF4


open scoped BigOperators Matrix

variable {d k : ℕ}
variable {A : Type*} [NormedRing A] [NormedAlgebra ℂ A] [StarRing A] [ContinuousStar A]
  [CompleteSpace A] [StarModule ℂ A]
variable {α κ Ω : Type*} [Fintype α] [DecidableEq α] [Fintype κ] [DecidableEq κ]
  {mΩ : MeasurableSpace Ω}

Formal statement

theorem BookProof.ChapterF4.hermitian_flow_preserves_normSq {n : ℕ} (H : Matrix (Fin n) (Fin n) ℂ)
    (hH : H.IsHermitian) (t : ℝ) (c : Fin n → ℂ) :
    star ((NormedSpace.exp ((-Complex.I * (t : ℂ)) • H)).mulVec c)
          ⬝ᵥ (NormedSpace.exp ((-Complex.I * (t : ℂ)) • H)).mulVec c
      = star c ⬝ᵥ c := by sorry

View graph