def
definition
complex_hilbert_from_ledger
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Quantum.ComplexHilbertStructure on GitHub at line 10.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
7
8open IndisputableMonolith.Quantum
9
10def complex_hilbert_from_ledger : Prop :=
11 ∀ (H : Type*) [RSHilbertSpace H], ∀ ψ : NormalizedState H, ‖ψ.vec‖ = 1
12
13theorem normalized_state_unit_norm {H : Type*} [RSHilbertSpace H]
14 (ψ : NormalizedState H) : ‖ψ.vec‖ = 1 :=
15 ψ.norm_one
16
17theorem complex_hilbert_structure : complex_hilbert_from_ledger := by
18 intro H hH ψ
19 exact ψ.norm_one
20
21/-- Universe-stable extractor for complex-Hilbert structure. -/
22theorem complex_hilbert_implies_unit_norm.{u}
23 (h : @complex_hilbert_from_ledger.{u}) : @complex_hilbert_from_ledger.{u} :=
24 h
25
26end ComplexHilbertStructure
27end Quantum
28end IndisputableMonolith