Block14Examples.lean

1 import KomorebiLSM.FiniteTableP32
2 import KomorebiLSM.Block13Examples
3 
4 set_option autoImplicit false
5 namespace Komorebi.LSM.Block14Examples
6 open Komorebi.LSM.Spectral Komorebi.LSM.BasisCoordinates
7 
8 /-- The sole singular value of scalar multiplication by two is at index zero. -/
9 theorem double_first_singular :
10     ((2:ℝ) • (LinearMap.id : ℝ →ₗ[ℝ] ℝ)).singularValues 0 = 2 := by
11   have hr : Module.finrank ℝ (((2:ℝ) • (LinearMap.id : ℝ →ₗ[ℝ] ℝ)).range) = 1 := by
12     have hsur : Function.Surjective ((2:ℝ) • (LinearMap.id : ℝ →ₗ[ℝ] ℝ)) := by
13       intro y
14       refine ⟨y/2, ?_⟩
15       change (2:ℝ)*(y/2) = y
16       ring
17     rw [LinearMap.range_eq_top.mpr hsur]
18     simp
19   have h := Block13Examples.double_leastPositive
20   simpa [leastPositive, hr] using h
21 
22 theorem discard_all_scalar_modes :
23     ‖(leadingLeft (((2:ℝ) • ContinuousLinearMap.id ℝ ℝ).toLinearMap) 0 (by simp))ᗮ.starProjection.comp
24       ((2:ℝ) • ContinuousLinearMap.id ℝ ℝ)‖ = 2 := by
25   rw [leadingLeft_tail_norm]
26   exact double_first_singular
27 
28 theorem retain_all_scalar_modes :
29     ‖(leadingLeft (((2:ℝ) • ContinuousLinearMap.id ℝ ℝ).toLinearMap) 1 (by simp))ᗮ.starProjection.comp
30       ((2:ℝ) • ContinuousLinearMap.id ℝ ℝ)‖ = 0 := by
31   rw [leadingLeft_tail_norm]
32   exact singularValue_zero_at_max_rank _ 1 (by simp)
33 
34 /-- A wide rank-one table has a zero second singular value. -/
35 theorem rectangular_maximum_rank_tail_zero : Block13Examples.firstCoordinate.singularValues 1 = 0 :=
36   singularValue_zero_at_max_rank _ 1 (by simp)
37 
38 /-- The universal perturbation constant one is attained by scalar two versus zero. -/
39 theorem scalar_perturbation_sharp :
40     |((2:ℝ) • (LinearMap.id : ℝ →ₗ[ℝ] ℝ)).singularValues 0 -
41       (0 : ℝ →ₗ[ℝ] ℝ).singularValues 0| =
42       ‖((2:ℝ) • ContinuousLinearMap.id ℝ ℝ) - 0‖ := by
43   rw [double_first_singular]
44   simp [norm_smul, ContinuousLinearMap.norm_id]
45 
46 theorem same_basis_cross_identity {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
47     [FiniteDimensional ℝ E] (P : Submodule ℝ E) (r : ℕ)
48     (U : OrthonormalBasis (Fin r) ℝ P) : cross U U = 1 := by
49   ext i j
50   rw [cross_entry, Matrix.one_apply]
51   exact U.inner_eq_ite i j
52 
53 theorem zero_rank_tail_is_zero :
54     ‖(leadingLeft (0 : ℝ →ₗ[ℝ] ℝ) 0 (by simp))ᗮ.starProjection.comp
55       (0 : ℝ →L[ℝ] ℝ)‖ = 0 := by simp
56 
57 end Komorebi.LSM.Block14Examples

Back to source controls