TraceBoundaries.lean

1 import PaperX.TraceExamples
2 import Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
3 
4 /-! Boundaries of finite trace information: distinctness is weaker than linear
5 independence; a multiplicity vector does not choose an embedded subspace. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.TraceBoundaries
9 
10 open scoped BigOperators Matrix
11 open PaperX.FiniteSeparation
12 
13 /-- Three distinct functions, but the third is the sum of the first two. -/
14 def dependentFunctions : Fin 3 → ℚ → ℚ := ![fun _ => 1, fun x => x, fun x => 1+x]
15 
16 theorem functions_distinct : Function.Injective dependentFunctions := by
17   intro i j h
18   fin_cases i <;> fin_cases j <;> try rfl
19   all_goals solve
20     | (have h0 := congrFun h 0; norm_num [dependentFunctions] at h0)
21     | (have h1 := congrFun h 1; norm_num [dependentFunctions] at h1)
22 
23 theorem no_three_sample_separator (s : Fin 3 → ℚ) :
24     (sampleMatrix dependentFunctions s).det = 0 := by
25   apply Matrix.exists_mulVec_eq_zero_iff.mp
26   refine ⟨![1,1,-1], ?_, ?_⟩
27   · intro h
28     have h0 := congrFun h 0
29     norm_num at h0
30   · ext j
31     simp [sampleMatrix, dependentFunctions, Matrix.mulVec, dotProduct, Fin.sum_univ_succ]
32 
33 /-- Two different embedded one-dimensional summands of the same trivial carrier. -/
34 def leftProjector : Matrix (Fin 2) (Fin 2) ℚ := !![1,0; 0,0]
35 def rightProjector : Matrix (Fin 2) (Fin 2) ℚ := !![0,0; 0,1]
36 
37 theorem left_idempotent : leftProjector * leftProjector = leftProjector := by decide +kernel
38 
39 theorem right_idempotent : rightProjector * rightProjector = rightProjector := by decide +kernel
40 
41 theorem projectors_distinct : leftProjector ≠ rightProjector := by decide +kernel
42 
43 theorem equal_projector_traces : leftProjector.trace = 1 ∧ rightProjector.trace = 1 := by
44   decide +kernel
45 
46 /-- Both projectors commute with every scalar action, hence in particular with a
47 trivial group representation. Their equal traces do not identify them. -/
48 theorem projectors_commute_scalar (a : ℚ) :
49     leftProjector * (a • 1) = (a • 1) * leftProjector ∧
50     rightProjector * (a • 1) = (a • 1) * rightProjector := by
51   simp
52 
53 end PaperX.TraceBoundaries

Back to source controls