HaarHilbert.lean

1 import KomorebiPaperV.HilbertPackets
2 import Mathlib.Analysis.Real.Sqrt
3 
4 /-! Author: Komorebi P. Normalized Haar on entire complex l2 channels. -/
5 
6 namespace KomorebiPaperV.HaarHilbert
7 open KomorebiPaperV.HilbertPackets
8 
9 noncomputable def low (x y : Signal ℤ) : Signal ℤ :=
10   (Real.sqrt 2)⁻¹ • (x + y)
11 
12 noncomputable def high (x y : Signal ℤ) : Signal ℤ :=
13   (Real.sqrt 2)⁻¹ • (x - y)
14 
15 theorem inverse_low (x y : Signal ℤ) : low (low x y) (high x y) = x := by
16   have hs : (Real.sqrt 2)⁻¹ * (Real.sqrt 2)⁻¹ * 2 = 1 := by
17     rw [← mul_inv, Real.mul_self_sqrt (by norm_num)]
18     norm_num
19   unfold low high
20   rw [← smul_add]
21   have hab : x + y + (x - y) = (2 : ℝ) • x := by module
22   rw [hab, smul_smul, smul_smul, hs, one_smul]
23 
24 theorem inverse_high (x y : Signal ℤ) : high (low x y) (high x y) = y := by
25   have hs : (Real.sqrt 2)⁻¹ * (Real.sqrt 2)⁻¹ * 2 = 1 := by
26     rw [← mul_inv, Real.mul_self_sqrt (by norm_num)]
27     norm_num
28   unfold low high
29   rw [← smul_sub]
30   have hab : x + y - (x - y) = (2 : ℝ) • y := by module
31   rw [hab, smul_smul, smul_smul, hs, one_smul]
32 
33 theorem energy (x y : Signal ℤ) :
34     ‖low x y‖ ^ 2 + ‖high x y‖ ^ 2 = ‖x‖ ^ 2 + ‖y‖ ^ 2 := by
35   have hs : ‖(Real.sqrt 2)⁻¹‖ ^ 2 = (1 / 2 : ℝ) := by
36     rw [Real.norm_eq_abs, sq_abs, inv_pow, Real.sq_sqrt (by norm_num)]
37     norm_num
38   dsimp [low, high]
39   rw [norm_smul, norm_smul, mul_pow, mul_pow, hs]
40   nlinarith [parallelogram_law_with_norm ℂ x y]
41 
42 theorem low_apply (x y : Signal ℤ) (n : ℤ) :
43     low x y n = ((Real.sqrt 2 : ℝ) : ℂ)⁻¹ * (x n + y n) := by
44   change (Real.sqrt 2)⁻¹ • (x n + y n) = _
45   rw [Complex.real_smul, Complex.ofReal_inv]
46 
47 theorem high_apply (x y : Signal ℤ) (n : ℤ) :
48     high x y n = ((Real.sqrt 2 : ℝ) : ℂ)⁻¹ * (x n - y n) := by
49   change (Real.sqrt 2)⁻¹ • (x n - y n) = _
50   rw [Complex.real_smul, Complex.ofReal_inv]
51 
52 end KomorebiPaperV.HaarHilbert

Back to source controls