EuclideanTransfer.lean

1 module
2 public import Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
3 public import Mathlib.Analysis.Matrix.PosDef
4 public import Mathlib.Analysis.Normed.Algebra.MatrixExponential
5 public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
6 public import Mathlib.Tactic
7 /-! Author: Komorebi P. Paper VII, checked third block.
8 This module is independently compilable using the pinned portable Lean kit. -/
9 public section
10 set_option autoImplicit false
11 set_option backward.isDefEq.respectTransparency false
12 set_option backward.isDefEq.respectTransparency.types false
13 set_option linter.unusedSectionVars false
14 namespace KomorebiPaperVII.EuclideanTransfer
15 open Matrix NormedSpace
16 open scoped Matrix.Norms.Operator ComplexOrder
17 variable {n : Type*} [Fintype n] [DecidableEq n]
18 
19 /-- The power-series exponential, not a separately postulated transfer family. -/
20 noncomputable def transfer (H : Matrix n n ℂ) (e t : ℝ) : Matrix n n ℂ :=
21   exp ((-t) • (H - e • (1 : Matrix n n ℂ)))
22 
23 theorem shifted_hermitian (H : Matrix n n ℂ) (hH : H.IsHermitian) (e t : ℝ) :
24     ((-t) • (H - e • (1 : Matrix n n ℂ))).IsHermitian := by
25   exact (hH.sub (isHermitian_one.smul (IsSelfAdjoint.all e))).smul (IsSelfAdjoint.all (-t))
26 
27 theorem transfer_hermitian (H : Matrix n n ℂ) (hH : H.IsHermitian) (e t : ℝ) :
28     (transfer H e t).IsHermitian := (shifted_hermitian H hH e t).exp
29 
30 theorem transfer_zero (H : Matrix n n ℂ) (e : ℝ) : transfer H e 0 = 1 := by
31   simp [transfer]
32 
33 theorem transfer_add (H : Matrix n n ℂ) (e t s : ℝ) :
34     transfer H e (t+s) = transfer H e t * transfer H e s := by
35   unfold transfer
36   rw [neg_add, add_smul]
37   exact Matrix.exp_add_of_commute _ _ (((Commute.refl _).smul_left (-t)).smul_right (-s))
38 
39 theorem transfer_cfc (H : Matrix n n ℂ) (hH : H.IsHermitian) (e t : ℝ) :
40     transfer H e t = cfc (fun x : ℝ => Real.exp ((-t)*(x-e))) H := by
41   rw [cfc_comp' Real.exp (fun x : ℝ => (-t)*(x-e)) H]
42   have hlin : cfc (fun x : ℝ => (-t)*(x-e)) H = (-t) • (H - e • (1 : Matrix n n ℂ)) := by
43     rw [cfc_const_mul (-t) (fun x : ℝ => x-e) H,
44       cfc_sub (fun x : ℝ => x) (fun _ : ℝ => e) H, cfc_id' ℝ H hH.isSelfAdjoint, cfc_const e H hH.isSelfAdjoint]
45     simp only [Algebra.algebraMap_eq_smul_one]
46   rw [hlin, CFC.real_exp_eq_normedSpace_exp (shifted_hermitian H hH e t).isSelfAdjoint]
47   rfl
48 
49 theorem transfer_spectrum (H : Matrix n n ℂ) (hH : H.IsHermitian) (e t : ℝ) :
50     spectrum ℝ (transfer H e t) =
51       (fun x : ℝ => Real.exp ((-t)*(x-e))) '' spectrum ℝ H := by
52   rw [transfer_cfc H hH, cfc_map_spectrum (f := fun x : ℝ => Real.exp ((-t)*(x-e))) (a := H) hH.isSelfAdjoint]
53 
54 theorem transfer_posDef (H : Matrix n n ℂ) (hH : H.IsHermitian) (e t : ℝ) :
55     (transfer H e t).PosDef := by
56   let ht := transfer_hermitian H hH e t
57   rw [ht.posDef_iff_eigenvalues_pos]
58   intro i
59   have hi := ht.eigenvalues_mem_spectrum_real i
60   rw [transfer_spectrum H hH] at hi
61   obtain ⟨x, _, hx⟩ := hi
62   rw [← hx]
63   exact Real.exp_pos _
64 
65 theorem transfer_spectrum_interval (H : Matrix n n ℂ) (hH : H.IsHermitian)
66     (e t : ℝ) (ht : 0 ≤ t) (he : ∀ x ∈ spectrum ℝ H, e ≤ x) :
67     spectrum ℝ (transfer H e t) ⊆ Set.Ioc 0 1 := by
68   rw [transfer_spectrum H hH]
69   rintro _ ⟨x, hx, rfl⟩
70   exact ⟨Real.exp_pos _, Real.exp_le_one_iff.mpr (mul_nonpos_of_nonpos_of_nonneg
71     (neg_nonpos.mpr ht) (sub_nonneg.mpr (he x hx)))⟩
72 
73 /-- A minimum is defined only for a nonempty state space. -/
74 noncomputable def groundEnergy [Nonempty n] {H : Matrix n n ℂ} (hH : H.IsHermitian) : ℝ :=
75   (Finset.univ.image hH.eigenvalues).min' (Finset.univ_nonempty.image _)
76 
77 theorem ground_energy_le [Nonempty n] {H : Matrix n n ℂ} (hH : H.IsHermitian)
78     (x : ℝ) (hx : x ∈ spectrum ℝ H) : groundEnergy hH ≤ x := by
79   rw [hH.spectrum_real_eq_range_eigenvalues] at hx
80   obtain ⟨i, rfl⟩ := hx
81   exact Finset.min'_le _ _ (Finset.mem_image.mpr ⟨i, Finset.mem_univ _, rfl⟩)
82 
83 theorem ground_energy_mem [Nonempty n] {H : Matrix n n ℂ} (hH : H.IsHermitian) :
84     groundEnergy hH ∈ spectrum ℝ H := by
85   rw [hH.spectrum_real_eq_range_eigenvalues]
86   obtain ⟨i, _, hi⟩ := Finset.mem_image.mp (Finset.min'_mem _ (Finset.univ_nonempty.image hH.eigenvalues))
87   exact ⟨i, hi⟩
88 
89 theorem finite_euclidean_transfer [Nonempty n] (H : Matrix n n ℂ)
90     (hH : H.IsHermitian) (t s : ℝ) (ht : 0 ≤ t) :
91     (transfer H (groundEnergy hH) t).PosDef ∧
92     transfer H (groundEnergy hH) (t+s) =
93       transfer H (groundEnergy hH) t * transfer H (groundEnergy hH) s ∧
94     spectrum ℝ (transfer H (groundEnergy hH) t) ⊆ Set.Ioc 0 1 := by
95   exact ⟨transfer_posDef H hH _ _, transfer_add H _ _ _,
96     transfer_spectrum_interval H hH _ _ ht (ground_energy_le hH)⟩
97 
98 /-- Explicitly covers the complex spectrum as well as its real Hermitian coordinates. -/
99 theorem transfer_complex_spectrum [Nonempty n] (H : Matrix n n ℂ)
100     (hH : H.IsHermitian) (t : ℝ) (ht : 0 ≤ t) :
101     spectrum ℂ (transfer H (groundEnergy hH) t) ⊆
102       Complex.ofReal '' Set.Ioc (0 : ℝ) 1 := by
103   let hT := transfer_hermitian H hH (groundEnergy hH) t
104   rw [hT.spectrum_eq_image_range]
105   rintro _ ⟨x, hx, rfl⟩
106   refine ⟨x, ?_, rfl⟩
107   apply transfer_spectrum_interval H hH _ _ ht (ground_energy_le hH)
108   rw [hT.spectrum_real_eq_range_eigenvalues]
109   exact hx
110 end KomorebiPaperVII.EuclideanTransfer
111 
112 /-! Complete declaration-level trust audit. -/
113 #print axioms KomorebiPaperVII.EuclideanTransfer.shifted_hermitian
114 #print axioms KomorebiPaperVII.EuclideanTransfer.transfer_hermitian
115 #print axioms KomorebiPaperVII.EuclideanTransfer.transfer_zero
116 #print axioms KomorebiPaperVII.EuclideanTransfer.transfer_add
117 #print axioms KomorebiPaperVII.EuclideanTransfer.transfer_cfc
118 #print axioms KomorebiPaperVII.EuclideanTransfer.transfer_spectrum
119 #print axioms KomorebiPaperVII.EuclideanTransfer.transfer_posDef
120 #print axioms KomorebiPaperVII.EuclideanTransfer.transfer_spectrum_interval
121 #print axioms KomorebiPaperVII.EuclideanTransfer.ground_energy_le
122 #print axioms KomorebiPaperVII.EuclideanTransfer.ground_energy_mem
123 #print axioms KomorebiPaperVII.EuclideanTransfer.finite_euclidean_transfer
124 #print axioms KomorebiPaperVII.EuclideanTransfer.transfer_complex_spectrum

Back to source controls