`BookProof.BrstLeakage.norm_unitary_apply` {U : E →L[ℂ] E} (hU : U ∈ unitary (E →L[ℂ] E)) (x : E) : ‖U x‖ = ‖x‖
ProvedBookProof.BrstLeakage.norm_unitary_applytheoremstimepiece
Prove the following Lean 4 theorem from ChapterBrstTruncationLeakage.
BookProof.BrstLeakage.norm_unitary_apply {U : E →L[ℂ] E} (hU : U ∈ unitary (E →L[ℂ] E)) (x : E) : ‖U x‖ = ‖x‖
Formalization note: Lean 4 identifier BookProof.BrstLeakage.norm_unitary_apply.
Preamble
-- Generated from ChapterBrstTruncationLeakage.lean — theorem BookProof.BrstLeakage.norm_unitary_apply
import Mathlib
import Definitions.Def_ChapterBrstTruncationLeakage
open BookProof.BrstLeakage
open NormedSpace
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]Formal statement
theorem BookProof.BrstLeakage.norm_unitary_apply {U : E →L[ℂ] E} (hU : U ∈ unitary (E →L[ℂ] E)) (x : E) :
‖U x‖ = ‖x‖ := by sorry