Block9Examples.lean

1 import KomorebiLSM.FinitePrefix
2 import KomorebiLSM.LearnedRealization
3 
4 set_option autoImplicit false
5 namespace Komorebi.LSM.Block9Examples
6 open Identification Delay
7 
8 theorem no_observed_prefix_identifies_all_futures (T : ℕ) :
9     (∀ t ≤ T, output T ((shift (T+2)^t) (delayedInitial T)) = 0) ∧
10     output T ((shift (T+2)^(T+1)) (delayedInitial T)) = 1 := by
11   constructor
12   · intro t ht; rw [delayed_output]; simp [show t ≠ T+1 by omega]
13   · rw [delayed_output]; simp
14 
15 theorem warmup_zero_boundary :
16     observation (LinearMap.id : ℚ →ₗ[ℚ] ℚ) LinearMap.id 0 = 0 ∧
17     observation (LinearMap.id : ℚ →ₗ[ℚ] ℚ) LinearMap.id 1 1 ⟨0,by decide⟩ = 1 := by
18   constructor
19   · apply LinearMap.ext; intro x; funext i; exact Fin.elim0 i
20   · rfl
21 
22 def inputPlane : ℚ →ₗ[ℚ] (ℚ × ℚ) := LinearMap.inl ℚ ℚ ℚ
23 
24 def firstFit : (ℚ × ℚ) →ₗ[ℚ] (ℚ × ℚ) := LinearMap.id
25 
26 def secondFit : (ℚ × ℚ) →ₗ[ℚ] (ℚ × ℚ) :=
27   LinearMap.prod (LinearMap.fst ℚ ℚ ℚ) (2 • LinearMap.snd ℚ ℚ ℚ)
28 
29 theorem empirical_closed_span_not_coverage :
30     firstFit.comp inputPlane = inputPlane ∧ secondFit.comp inputPlane = inputPlane ∧
31     firstFit (0,1) ≠ secondFit (0,1) := by
32   constructor
33   · rfl
34   constructor
35   · apply LinearMap.ext; intro x; ext <;> simp [secondFit,inputPlane]
36   · norm_num [firstFit,secondFit]
37 
38 theorem inconsistent_zero_input :
39     ¬ ∃ B : ℚ →ₗ[ℚ] ℚ, B.comp (0 : ℚ →ₗ[ℚ] ℚ) = LinearMap.id := by
40   rintro ⟨B,hB⟩
41   have he := congrArg (fun F : ℚ →ₗ[ℚ] ℚ => F 1) hB
42   norm_num at he
43 
44 theorem pinv_identity : pinv (LinearMap.id : ℝ →ₗ[ℝ] ℝ) = LinearMap.id := by
45   apply LinearMap.ext
46   intro x
47   have he := apply_retained (LinearMap.id : ℝ →ₗ[ℝ] ℝ) x
48   simpa using (pinv_apply_image (LinearMap.id : ℝ →ₗ[ℝ] ℝ) x).trans he
49 
50 theorem learned_scalar_exact :
51     learned (LinearMap.id : ℝ →ₗ[ℝ] ℝ) (3 • LinearMap.id) = 3 • LinearMap.id := by
52   apply learned_eq_true
53   · exact Function.surjective_id
54   · simp
55 
56 /-- With true B=1, input=1, input perturbation=-1/2 and no output error,
57 the fitted scalar is 2 and the denominator bound is attained. -/
58 theorem scalar_perturbation_sharp :
59     |(1 : ℝ)/(1-1/2)-1| = (1*(1/2))/(1-1/2) := by norm_num
60 
61 theorem perturbation_boundary_collapses_rank : (1 : ℝ) + (-1) = 0 ∧ |(-1 : ℝ)| = 1 := by norm_num
62 
63 theorem unstable_rollout_amplifies (t : ℕ) : (2 : ℚ)^(t+1) = 2*2^t := by ring
64 
65 end Komorebi.LSM.Block9Examples

Back to source controls