ToeplitzEmbedding.lean

1 module
2 public import Mathlib.LinearAlgebra.Matrix.Circulant
3 public import Mathlib.Algebra.BigOperators.Fin
4 public import Mathlib.Tactic
5 
6 /-!
7 Author: Komorebi P. Paper VIII 4.4.
8 Actual zero-padding and the actual circulant of length n+n. The diagonal
9 uses c[0]; r[0] is unused. No symmetry or Hermiticity is required.
10 -/
11 @[expose] public section
12 set_option autoImplicit false
13 namespace KomorebiPaperVIII
14 open Matrix
15 open scoped BigOperators
16 variable {n : ℕ} [NeZero n]
17 
18 def toeplitzMatrix (c r : Fin n → ℂ) : Matrix (Fin n) (Fin n) ℂ :=
19   fun i j => if j.val ≤ i.val then c (Fin.ofNat n (i.val-j.val))
20     else r (Fin.ofNat n (j.val-i.val))
21 
22 def toeplitzGenerator (c r : Fin n → ℂ) (k : Fin (n+n)) : ℂ :=
23   if k.val < n then c (Fin.ofNat n k.val)
24   else if k.val = n then 0 else r (Fin.ofNat n (n+n-k.val))
25 
26 def zeroPad (x : Fin n → ℂ) : Fin (n+n) → ℂ := Fin.addCases x (fun _ => 0)
27 
28 theorem toeplitz_circulant_block (c r : Fin n → ℂ) (i j : Fin n) :
29     Matrix.circulant (toeplitzGenerator c r) (Fin.castAdd n i) (Fin.castAdd n j) =
30       toeplitzMatrix c r i j := by
31   unfold Matrix.circulant toeplitzMatrix
32   simp only [Matrix.of_apply]
33   by_cases h : j.val ≤ i.val
34   · have hj : Fin.castAdd n j ≤ Fin.castAdd n i := h
35     have hd : i.val - j.val < n := lt_of_le_of_lt (Nat.sub_le _ _) i.isLt
36     simp [toeplitzGenerator, Fin.sub_val_of_le hj, hd, h]
37   · have hj : Fin.castAdd n i < Fin.castAdd n j := lt_of_not_ge h
38     have hv := Fin.coe_sub_iff_lt.mpr hj
39     have hlow : ¬ n+n+i.val-j.val < n := by omega
40     have hneq : n+n+i.val-j.val ≠ n := by omega
41     have hsub : n+n-(n+n+i.val-j.val) = j.val-i.val := by omega
42     simp [toeplitzGenerator, hv, hlow, hneq, hsub, h]
43 
44 omit [NeZero n] in
45 theorem zero_pad_left (x : Fin n → ℂ) (i : Fin n) :
46     zeroPad x (Fin.castAdd n i) = x i := by
47   simp [zeroPad]
48 
49 omit [NeZero n] in
50 theorem zero_pad_right (x : Fin n → ℂ) (i : Fin n) :
51     zeroPad x (Fin.natAdd n i) = 0 := by
52   exact Fin.addCases_right i
53 
54 theorem toeplitz_embedding_action (c r x : Fin n → ℂ) (i : Fin n) :
55     (Matrix.circulant (toeplitzGenerator c r) *ᵥ zeroPad x) (Fin.castAdd n i) =
56       (toeplitzMatrix c r *ᵥ x) i := by
57   simp only [Matrix.mulVec, dotProduct, Fin.sum_univ_add, zero_pad_left, zero_pad_right,
58     mul_zero, Finset.sum_const_zero, add_zero, toeplitz_circulant_block]
59 
60 theorem toeplitz_generator_first_half (c r : Fin n → ℂ) (i : Fin n) :
61     toeplitzGenerator c r (Fin.castAdd n i) = c i := by
62   simp [toeplitzGenerator, i.isLt, Fin.ofNat_eq_cast]
63 
64 theorem toeplitz_generator_middle (c r : Fin n → ℂ) :
65     toeplitzGenerator c r ⟨n, by have := NeZero.pos n; omega⟩ = 0 := by
66   simp [toeplitzGenerator]
67 
68 end KomorebiPaperVIII
69 
70 -- FINAL AXIOM AUDITS
71 #print axioms KomorebiPaperVIII.toeplitz_circulant_block
72 #print axioms KomorebiPaperVIII.zero_pad_left
73 #print axioms KomorebiPaperVIII.zero_pad_right
74 #print axioms KomorebiPaperVIII.toeplitz_embedding_action
75 #print axioms KomorebiPaperVIII.toeplitz_generator_first_half
76 #print axioms KomorebiPaperVIII.toeplitz_generator_middle
77 
78 #print axioms KomorebiPaperVIII.toeplitzGenerator
79 
80 #print axioms KomorebiPaperVIII.zeroPad

Back to source controls