Block11Examples.lean

1 import KomorebiLSM.CoreStability
2 import KomorebiLSM.FilteringStability
3 
4 set_option autoImplicit false
5 namespace Komorebi.LSM.Block11Examples
6 open Filtering Identification
7 
8 theorem strict_margin_preserves_mass :
9     (0:ℝ) < (ContinuousLinearMap.id ℝ ℝ) (3/4) := by norm_num
10 
11 theorem boundary_margin_can_zero_mass :
12     let lam := ContinuousLinearMap.id ℝ ℝ
13     lam (1:ℝ) = 1 ∧ ‖(0:ℝ)-1‖ = 1 ∧ lam 0 = 0 := by norm_num
14 
15 theorem insufficient_margin_can_negative_mass :
16     let lam := ContinuousLinearMap.id ℝ ℝ
17     lam (1:ℝ) = 1 ∧ lam (-1) < 0 := by norm_num
18 
19 /-- Arbitrarily small absolute error can still change a normalized state by one. -/
20 theorem rare_branch_amplification (η : ℝ) (hη : 0 < η) :
21     let lam : (ℝ × ℝ) →L[ℝ] ℝ := ContinuousLinearMap.fst ℝ ℝ ℝ
22     ‖((η,η):ℝ × ℝ)-(η,0)‖ = η ∧
23     ‖Filtering.normalize lam (η,η)-Filtering.normalize lam (η,0)‖ = 1 := by
24   have hn : η ≠ 0 := ne_of_gt hη
25   simp [Filtering.normalize, Prod.norm_def, abs_of_pos hη, hn, hη.le]
26 
27 theorem zero_noise_exact {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
28     [FiniteDimensional ℝ E] (H B : E →L[ℝ] E) (hH : 0 < rowGain H) :
29     coreFit H 0 0 B = B := by
30   have h := core_error_identity H 0 0 B (by simpa using hH)
31   apply sub_eq_zero.mp
32   simpa using h
33 
34 theorem zero_noise_filter_exact {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
35     (lam : E →L[ℝ] ℝ) (B : E →L[ℝ] E) (z : E) :
36     Filtering.normalize lam (B z)-Filtering.normalize lam (B z) = 0 := sub_self _
37 
38 theorem core_gap_boundary_is_singular : (1:ℝ)+(-1)=0 := by norm_num
39 
40 theorem fitted_bound_can_be_sharper :
41     ((0:ℝ) + (2/3)*(1/2))/1 < ((0:ℝ)+1*(1/2))/(1-1/2) := by norm_num
42 
43 end Komorebi.LSM.Block11Examples

Back to source controls