FinitePrefix.lean

1 import Mathlib.LinearAlgebra.FiniteDimensional.Basic
2 import Mathlib.Tactic
3 
4 /-! P17: explicit rational finite-dimensional nilpotent systems for every horizon. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.Delay
7 
8 def shift (n : ℕ) : (Fin n → ℚ) →ₗ[ℚ] (Fin n → ℚ) where
9   toFun x i := if h : i.val + 1 < n then x ⟨i.val + 1, h⟩ else 0
10   map_add' x y := by funext i; dsimp; split <;> simp
11   map_smul' a x := by funext i; dsimp; split <;> simp
12 
13 theorem shift_power (n k : ℕ) (x : Fin n → ℚ) (i : Fin n) :
14     (shift n ^ k) x i = if h : i.val + k < n then x ⟨i.val + k, h⟩ else 0 := by
15   induction k generalizing i with
16   | zero => simp
17   | succ k ih =>
18     rw [pow_succ', Module.End.mul_apply]
19     change (if h : i.val + 1 < n then (shift n ^ k) x ⟨i.val+1,h⟩ else 0) = _
20     split_ifs with h h'
21     · rw [ih]
22       simp only
23       split_ifs with h''
24       · congr 1; apply Fin.ext; change i.val + 1 + k = i.val + (k + 1); omega
25       · omega
26     · rw [ih]
27       simp only
28       split_ifs with h''
29       · omega
30       · rfl
31     · omega
32     · rfl
33 
34 theorem shift_nilpotent (n : ℕ) : shift n ^ n = 0 := by
35   apply LinearMap.ext
36   intro x
37   funext i
38   rw [shift_power]
39   simp only [LinearMap.zero_apply, Pi.zero_apply]
40   split_ifs with h
41   · omega
42   · rfl
43 
44 def delayedInitial (T : ℕ) : Fin (T+2) → ℚ :=
45   fun i => if i.val = T+1 then 1 else 0
46 
47 def output (T : ℕ) : (Fin (T+2) → ℚ) →ₗ[ℚ] ℚ := LinearMap.proj ⟨0,by omega⟩
48 
49 theorem delayed_output (T t : ℕ) :
50     output T ((shift (T+2) ^ t) (delayedInitial T)) = if t = T+1 then 1 else 0 := by
51   change (shift (T+2) ^ t) (delayedInitial T) ⟨0,by omega⟩ = _
52   rw [shift_power]
53   simp only [Nat.zero_add]
54   split_ifs with h h'
55   · simp [delayedInitial, h']
56   · simp [delayedInitial, h']
57   · omega
58   · rfl
59 
60 theorem finite_prefix_indistinguishability (T : ℕ) :
61     ∃ (L₀ L₁ : (Fin (T+2) → ℚ) →ₗ[ℚ] (Fin (T+2) → ℚ))
62       (C : (Fin (T+2) → ℚ) →ₗ[ℚ] ℚ) (x₀ x₁ : Fin (T+2) → ℚ),
63       L₀^(T+2) = 0 ∧ L₁^(T+2) = 0 ∧
64       (∀ t ≤ T, C ((L₀^t) x₀) = C ((L₁^t) x₁)) ∧
65       C ((L₀^(T+1)) x₀) ≠ C ((L₁^(T+1)) x₁) := by
66   refine ⟨0, shift (T+2), output T, 0, delayedInitial T, ?_, shift_nilpotent _, ?_, ?_⟩
67   · simp
68   · intro t ht
69     rw [map_zero, map_zero, delayed_output]
70     simp [show t ≠ T+1 by omega]
71   · rw [map_zero, map_zero, delayed_output]
72     simp
73 end Komorebi.LSM.Delay

Back to source controls