HeisenbergDimension.lean

1 import PaperXI.HeisenbergCardinality
2 import Mathlib.Basic.Complex.Basic
3 import Mathlib.Data.Nat.Sqrt
4 
5 /-! Dimension and square-root cardinality in the finite Schrödinger model. -/
6 
7 set_option autoImplicit false
8 
9 namespace PaperXI.HeisenbergDimension
10 
11 open Module
12 
13 variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]
14 variable [FiniteDimensional K X]
15 
16 theorem natCard_dual : Nat.card (Module.Dual K X) = Nat.card X := by
17   rw [Module.natCard_eq_pow_finrank (K := K) (V := Module.Dual K X),
18     Subspace.dual_finrank_eq,
19     Module.natCard_eq_pow_finrank (K := K) (V := X)]
20 
21 theorem natCard_symplectic : Nat.card (X × Module.Dual K X) = (Nat.card X) ^ 2 := by
22   rw [Nat.card_prod, natCard_dual, pow_two]
23 
24 theorem sqrt_natCard_symplectic :
25     Nat.sqrt (Nat.card (X × Module.Dual K X)) = Nat.card X := by
26   rw [natCard_symplectic, Nat.sqrt_eq']
27 
28 variable [Fintype X]
29 
30 omit [AddCommGroup X] in
31 theorem finrank_function : finrank ℂ (X → ℂ) = Nat.card X := by
32   rw [Module.finrank_fintype_fun_eq_card, Nat.card_eq_fintype_card]
33 
34 theorem finrank_function_pow : finrank ℂ (X → ℂ) = Nat.card K ^ finrank K X := by
35   rw [finrank_function, Module.natCard_eq_pow_finrank (K := K) (V := X)]
36 
37 theorem finrank_function_sqrt :
38     finrank ℂ (X → ℂ) = Nat.sqrt (Nat.card (X × Module.Dual K X)) := by
39   rw [finrank_function, sqrt_natCard_symplectic]
40 
41 end PaperXI.HeisenbergDimension

Back to source controls