FrobeniusSeparation.lean

1 import PaperXII.ReuseFiniteSeparation
2 
3 /-! Paper XII 10.9. Samples lie in the actual domain of the supplied functions.
4 The existence proof is reused from Paper X; the inverse formula and natural
5 multiplicity recovery are proved here. Natural multiplicities require characteristic zero. -/
6 namespace PaperXII.FrobeniusSeparation
7 
8 open scoped BigOperators
9 open PaperX.FiniteSeparation
10 
11 variable {K I Ω : Type*} [Field K] [Fintype I] [DecidableEq I]
12 
13 /-- The trace function of a carrier with coefficients c. -/
14 def combination (t : I → Ω → K) (c : I → K) : Ω → K :=
15   fun v ↦ ∑ i, c i * t i v
16 
17 /-- Values at the selected points, in row order. -/
18 def samples (t : I → Ω → K) (s : I → Ω) (c : I → K) : I → K :=
19   fun j ↦ combination t c (s j)
20 
21 omit [DecidableEq I] in
22 /-- The measurement map is multiplication by the actual evaluation matrix. -/
23 theorem samples_eq_mulVec (t : I → Ω → K) (s : I → Ω) (c : I → K) :
24     samples t s c = (sampleMatrix t s).mulVec c := by
25   funext j
26   simp only [samples, combination, sampleMatrix, Matrix.mulVec, dotProduct, mul_comm]
27 
28 /-- Recover coefficients using the inverse evaluation matrix. -/
29 noncomputable def recover (t : I → Ω → K) (s : I → Ω) (values : I → K) : I → K :=
30   (sampleMatrix t s)⁻¹.mulVec values
31 
32 /-- The inverse formula recovers every coefficient vector from its measured values. -/
33 theorem recover_samples (t : I → Ω → K) (s : I → Ω)
34     (h : (sampleMatrix t s).det ≠ 0) (c : I → K) :
35     recover t s (samples t s c) = c := by
36   rw [recover, samples_eq_mulVec, Matrix.mulVec_mulVec,
37     Matrix.nonsing_inv_mul _ (isUnit_iff_ne_zero.mpr h), Matrix.one_mulVec]
38 
39 /-- Nonsingular samples determine coefficients uniquely. -/
40 theorem samples_injective (t : I → Ω → K) (s : I → Ω)
41     (h : (sampleMatrix t s).det ≠ 0) : Function.Injective (samples t s) := by
42   intro c d hcd
43   have heq := congrArg (recover t s) hcd
44   simpa only [recover_samples t s h] using heq
45 
46 /-- Claim 10.9, including the actual inverse formula for recovery. -/
47 theorem exists_separator_and_recovery (t : I → Ω → K) (hi : LinearIndependent K t) :
48     ∃ s : I → Ω, Function.Injective s ∧ (sampleMatrix t s).det ≠ 0 ∧
49       (∀ c, recover t s (samples t s c) = c) ∧ Function.Injective (samples t s) := by
50   obtain ⟨s, hs, hdet⟩ := exists_nonsingular_samples t hi
51   exact ⟨s, hs, hdet, recover_samples t s hdet, samples_injective t s hdet⟩
52 
53 /-- The selected measurements recover natural multiplicities in characteristic zero. -/
54 theorem natural_multiplicities_unique [CharZero K] (t : I → Ω → K) (s : I → Ω)
55     (h : (sampleMatrix t s).det ≠ 0) (m n : I → ℕ)
56     (heq : samples t s (fun i ↦ (m i : K)) = samples t s (fun i ↦ (n i : K))) : m = n := by
57   have hc := samples_injective t s h heq
58   funext i
59   exact Nat.cast_injective (congrFun hc i)
60 
61 /-- The multiplicity separator exists; invertibility is derived from functional independence. -/
62 theorem exists_multiplicity_separator [CharZero K] (t : I → Ω → K)
63     (hi : LinearIndependent K t) :
64     ∃ s : I → Ω, Function.Injective s ∧ (sampleMatrix t s).det ≠ 0 ∧
65       ∀ m n : I → ℕ,
66         samples t s (fun i ↦ (m i : K)) = samples t s (fun i ↦ (n i : K)) → m = n := by
67   obtain ⟨s, hs, hdet⟩ := exists_nonsingular_samples t hi
68   exact ⟨s, hs, hdet, natural_multiplicities_unique t s hdet⟩
69 
70 /-- Without functional independence, no square evaluation matrix can be invertible. -/
71 theorem dependent_has_no_separator (t : I → Ω → K) (h : ¬ LinearIndependent K t)
72     (s : I → Ω) : (sampleMatrix t s).det = 0 := by
73   by_contra hdet
74   exact h (independent_of_separator t s hdet)
75 
76 end PaperXII.FrobeniusSeparation

Back to source controls