FiniteSeparation.lean

1 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
2 import Mathlib.LinearAlgebra.Dual.Lemmas
3 import Mathlib.LinearAlgebra.Dimension.Finite
4 import Mathlib.LinearAlgebra.Matrix.Rank
5 
6 /-! Finite separation of an arbitrary finite linearly independent family of functions.
7 The evaluation matrix is selected from the actual functions, not postulated invertible.
8 The index and sample spaces may be empty. No arithmetic density is assumed here. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperX.FiniteSeparation
12 
13 open scoped BigOperators
14 universe u v w
15 variable {K : Type u} [Field K] {I : Type v} [Fintype I] {X : Type w}
16 
17 /-- The linear measurement at a single point. -/
18 def row (f : I → X → K) (x : X) : (I → K) →ₗ[K] K :=
19   ∑ i, (f i x) • LinearMap.proj i
20 
21 theorem row_apply (f : I → X → K) (x : X) (c : I → K) :
22     row f x c = ∑ i, c i * f i x := by
23   simp [row, mul_comm]
24 
25 /-- Independent columns mean that their evaluations span the entire coefficient dual. -/
26 theorem evaluation_span (f : I → X → K) (hi : LinearIndependent K f) :
27     Submodule.span K (Set.range (row f)) = ⊤ := by
28   apply Submodule.span_eq_top_of_ne_zero
29   intro c hc
30   by_contra! h
31   have hz : ∑ i, c i • f i = 0 := by
32     funext x
33     have hx := h (row f x) (Set.mem_range_self x)
34     simpa [row_apply] using hx
35   exact hc (funext ((Fintype.linearIndependent_iff.mp hi) c hz))
36 
37 /-- Exactly as many distinct samples as columns suffice. This is a genuine existence
38 result extracted from the spanning evaluation forms, not an invertibility hypothesis. -/
39 theorem exists_square_separator (f : I → X → K) (hi : LinearIndependent K f) :
40     ∃ s : I → X, Function.Injective s ∧
41       Function.Injective (fun c : I → K => fun j => ∑ i, c i * f i (s j)) := by
42   classical
43   obtain ⟨J, a, ha, hs, hl⟩ := exists_linearIndependent' K (row f)
44   have htop : ⊤ ≤ Submodule.span K (Set.range (row f ∘ a)) := by
45     rw [hs, evaluation_span f hi]
46   let b := Module.Basis.mk hl htop
47   let e : J ≃ I := b.indexEquiv (Pi.basisFun K I).dualBasis
48   let b' := b.reindex e
49   refine ⟨a ∘ e.symm, ha.comp e.symm.injective, ?_⟩
50   intro c d hcd
51   apply (Module.evalEquiv K (I → K)).injective
52   apply b'.ext
53   intro j
54   have hj := congrFun hcd j
55   simpa [b', b, Module.Basis.reindex_apply, Module.Basis.mk_apply, row_apply,
56     Function.comp_def] using hj
57 
58 /-- Matrix form, with row orientation made explicit. -/
59 def sampleMatrix (f : I → X → K) (s : I → X) : Matrix I I K :=
60   fun j i => f i (s j)
61 
62 theorem exists_nonsingular_samples [DecidableEq I]
63     (f : I → X → K) (hi : LinearIndependent K f) :
64     ∃ s : I → X, Function.Injective s ∧ (sampleMatrix f s).det ≠ 0 := by
65   obtain ⟨s, hs, hinj⟩ := exists_square_separator f hi
66   refine ⟨s, hs, ?_⟩
67   have hmul : Function.Injective (sampleMatrix f s).mulVec := by
68     intro c d hcd
69     apply hinj
70     funext j
71     simpa [sampleMatrix, Matrix.mulVec, dotProduct, mul_comm] using congrFun hcd j
72   exact ((Matrix.isUnit_iff_isUnit_det _).mp
73     (Matrix.mulVec_injective_iff_isUnit.mp hmul)).ne_zero
74 
75 /-- A valid square separator has full column rank. -/
76 theorem separator_rank [DecidableEq I] (f : I → X → K) (s : I → X)
77     (h : (sampleMatrix f s).det ≠ 0) :
78     (sampleMatrix f s).rank = Fintype.card I := by
79   exact (Matrix.linearIndependent_rows_of_det_ne_zero h).rank_matrix
80 
81 
82 /-- The converse: one invertible evaluation matrix certifies actual functional
83 independence. Distinctness alone is not substituted for this condition. -/
84 theorem independent_of_separator [DecidableEq I] (f : I → X → K) (s : I → X)
85     (h : (sampleMatrix f s).det ≠ 0) : LinearIndependent K f := by
86   rw [Fintype.linearIndependent_iff]
87   intro c hc
88   have hz : (sampleMatrix f s).mulVec c = 0 := by
89     funext j
90     simpa [sampleMatrix, Matrix.mulVec, dotProduct, mul_comm] using congrFun hc (s j)
91   have hu : IsUnit (sampleMatrix f s) :=
92     (Matrix.isUnit_iff_isUnit_det _).2 (isUnit_iff_ne_zero.mpr h)
93   have hh : c = 0 := Matrix.mulVec_injective_iff_isUnit.mpr hu (by simpa using hz)
94   intro i
95   exact congrFun hh i
96 
97 end PaperX.FiniteSeparation

Back to source controls