Block13Examples.lean

1 import KomorebiLSM.SpectralSharpness
2 
3 set_option autoImplicit false
4 namespace Komorebi.LSM.Block13Examples
5 open Komorebi.LSM.Spectral Komorebi.LSM.Identification
6 
7 /-- The scalar factor two has the actual singular value two. -/
8 theorem double_leastPositive : leastPositive ((2:ℝ) • (LinearMap.id : ℝ →ₗ[ℝ] ℝ)) = 2 := by
9   let A : ℝ →ₗ[ℝ] ℝ := (2:ℝ) • LinearMap.id
10   have hsur : Function.Surjective A := by
11     intro y
12     refine ⟨y/2, ?_⟩
13     change (2:ℝ)*(y/2) = y
14     ring
15   have hr : 0 < Module.finrank ℝ A.range := by
16     rw [LinearMap.range_eq_top.mpr hsur]
17     simp
18   obtain ⟨v,_,hn,ha⟩ := exists_unit_minimizer A hr
19   change ‖(2:ℝ)*v‖ = leastPositive A at ha
20   rw [norm_mul, Real.norm_of_nonneg (by norm_num : (0:ℝ) ≤ 2), hn, mul_one] at ha
21   exact ha.symm
22 
23 theorem double_inverse_norm :
24     ‖pinvL ((2:ℝ) • ContinuousLinearMap.id ℝ ℝ)‖ = (1/2:ℝ) := by
25   let A : ℝ →L[ℝ] ℝ := (2:ℝ) • ContinuousLinearMap.id ℝ ℝ
26   have hsur : Function.Surjective A.toLinearMap := by
27     intro y
28     refine ⟨y/2, ?_⟩
29     change (2:ℝ)*(y/2) = y
30     ring
31   have hr : 0 < Module.finrank ℝ A.toLinearMap.range := by
32     rw [LinearMap.range_eq_top.mpr hsur]
33     simp
34   have h := pinv_operator_norm_eq A hr
35   have hs : leastPositive A.toLinearMap = 2 := double_leastPositive
36   rw [hs] at h
37   simpa only [A, inv_eq_one_div] using h
38 
39 theorem zero_has_no_positive_singular_value : leastPositive (0 : ℝ →ₗ[ℝ] ℝ) = 0 := by
40   simp [leastPositive]
41 
42 noncomputable def firstCoordinate : EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] ℝ :=
43   (LinearMap.proj (0:Fin 2)).comp (WithLp.linearEquiv 2 ℝ (Fin 2 → ℝ)).toLinearMap
44 
45 /-- A rank-one table cannot have a positive lower bound on its whole domain. -/
46 theorem global_lower_fails_for_projection :
47     ∃ v : EuclideanSpace ℝ (Fin 2),
48       ‖firstCoordinate v‖ < leastPositive firstCoordinate * ‖v‖ := by
49   have hsur : Function.Surjective firstCoordinate := by
50     intro y
51     exact ⟨WithLp.toLp 2 (fun _ => y), rfl⟩
52   have hr : 0 < Module.finrank ℝ firstCoordinate.range := by
53     rw [LinearMap.range_eq_top.mpr hsur]
54     simp
55   let v : EuclideanSpace ℝ (Fin 2) := WithLp.toLp 2 ![0,1]
56   have hv : v ≠ 0 := by
57     intro h
58     have h' := congrArg (fun w : EuclideanSpace ℝ (Fin 2) => w 1) h
59     norm_num [v] at h'
60   have hz : firstCoordinate v = 0 := by rfl
61   refine ⟨v, ?_⟩
62   rw [hz, norm_zero]
63   exact mul_pos (leastPositive_pos firstCoordinate hr) (norm_pos_iff.mpr hv)
64 
65 end Komorebi.LSM.Block13Examples

Back to source controls