Theory Linear_System

section ‹Homogeneous linear systems with more unknowns than equations›

theory Linear_System
  imports Subfield
begin

text ‹A homogeneous linear system with strictly more unknowns than equations has a nontrivial
  solution.  This is the pigeonhole principle of linear algebra, and it is what powers ∗‹Artin's
  theorem› on the fixed field of a finite group of automorphisms: there one produces a nonzero
  solution of the system @{text "∑j σ(xj) cj = 0"}, one equation per automorphism @{text σ}, from
  an assumed excess of independent elements @{text "xj"}.

  We index equations by a finite set @{term I} and unknowns by a finite set @{term J}, rather than by
  initial segments @{term "{..<m}"} and @{term "{..<n}"}.  This matters: the proof eliminates one
  unknown at each step, and with index ∗‹sets› that is just @{term "J - {k}"}, whereas with initial
  segments every step would need a reindexing bijection.

  Everything happens inside a subfield @{term K}: the coefficients lie in @{term K} and so does the
  solution, since Gaussian elimination only ever adds, multiplies and divides.›

context Subfield
begin

text ‹The proof is Gaussian elimination, by induction on the set of equations.

  With no equations at all, any nonzero vector will do --- and there is an unknown to put it in,
  since @{term "card {} < card J"} forces @{term J} nonempty.

  For the inductive step, single out one equation.  If all its coefficients vanish it is no
  constraint, and the induction hypothesis applied to the remaining equations already gives a
  solution.  Otherwise some coefficient @{term "A i0 k"} is nonzero, and we use that equation to
  ∗‹eliminate› the unknown @{term k}: subtracting a suitable multiple of equation @{term i0} from
  each remaining equation produces a smaller system in the unknowns @{term "J - {k}"}, to which the
  induction hypothesis applies because @{term "card I < card J - 1"}.  Solving that and then choosing
  @{term "c k"} to satisfy equation @{term i0} solves the whole system.  Nontriviality survives
  because the recursively obtained solution is already nonzero ∗‹somewhere in› @{term "J - {k}"},
  and we do not touch those entries.›
theorem underdetermined_solution:
  fixes A :: "'i ⇒ 'j ⇒ 'a"
  assumes "finite I" and "finite J" and "card I < card J"
    and "⋀i j. ⟦ i ∈ I; j ∈ J ⟧ ⟹ A i j ∈ K"
  shows "∃c. (∀j. c j ∈ K) ∧ (∃j ∈ J. c j ≠ 0) ∧ (∀i ∈ I. (∑j ∈ J. A i j * c j) = 0)"
  using assms
proof (induction I arbitrary: J A rule: finite_induct)
  case empty
  ― ‹No equations: put a @{term 1} in any single unknown.›
  then obtain j0 where j0: "j0 ∈ J" by (metis card.empty gr_implies_not_zero card_gt_0_iff equals0I)
  ― ‹The constant-one vector: every entry lies in @{term K}, and it is nonzero at @{term j0}.
    (A one-hot vector would do as well, but the ‹if› makes the nontriviality step fiddly.)  The
    witness is supplied explicitly by @{text "exI[of _ c]"} rather than left to an automatic
    method, so that nothing has to be guessed for the function @{term c}.›
  define c :: "'j ⇒ 'a" where "c = (λ_. 1)"
  show ?case
  proof (intro exI[of _ c] conjI)
    show "∀j. c j ∈ K" by (simp add: c_def)
    show "∃j ∈ J. c j ≠ 0" using j0 by (intro bexI[of _ j0]) (simp_all add: c_def)
    show "∀i ∈ {}. (∑j ∈ J. A i j * c j) = 0" by simp
  qed
next
  case (insert i0 I)
  then have fJ: "finite J" and card: "card (insert i0 I) < card J"
    and ent: "⋀i j. ⟦ i ∈ insert i0 I; j ∈ J ⟧ ⟹ A i j ∈ K"
    by auto
  have cardI: "card I < card J" using card insert.hyps by (simp add: card_insert_if)
  show ?case
  proof (cases "∀j ∈ J. A i0 j = 0")
    case True
    ― ‹The singled-out equation is vacuous, so the rest of the system already decides the matter.

      The induction generalises over @{term A}, so the hypothesis must be told ∗‹which› matrix to
      use: @{text "where A = A"}.  Without it, unifying the closure premise leaves the matrix
      arguments as unknowns --- the hypothesis comes back mentioning @{text "A (?i i j) (?j i j)"}
      --- and any automatic method then searches for those two index functions instead of simply
      stripping the existential.  That search does not terminate.›
    have entI: "⋀i j. ⟦ i ∈ I; j ∈ J ⟧ ⟹ A i j ∈ K" using ent by auto
    obtain c where c: "∀j. c j ∈ K" "∃j ∈ J. c j ≠ 0"
      "∀i ∈ I. (∑j ∈ J. A i j * c j) = 0"
      using insert.IH[where A = A, OF fJ cardI entI] by blast
    have "(∑j ∈ J. A i0 j * c j) = 0" using True by simp
    with c show ?thesis by (intro exI[of _ c] conjI) blast+
  next
    case False
    then obtain k where k: "k ∈ J" and a: "A i0 k ≠ 0" by blast
    define a where "a = A i0 k"
    have aK: "a ∈ K" and anz: "a ≠ 0" using ent k a by (auto simp: a_def)
    ― ‹Eliminate the unknown @{term k} from every remaining equation.›
    define B where "B = (λi j. A i j - A i k * A i0 j / a)"
    have BK: "⋀i j. ⟦ i ∈ I; j ∈ J - {k} ⟧ ⟹ B i j ∈ K"
      unfolding B_def using ent k aK by (auto intro!: diff_closed mult_closed divide_closed)
    have cardJk: "card I < card (J - {k})"
      using card k fJ insert.hyps by (simp add: card_insert_if card_Diff_singleton)
    obtain c' where c'K: "∀j. c' j ∈ K"
      and c'nz: "∃j ∈ J - {k}. c' j ≠ 0"
      and c'eq: "∀i ∈ I. (∑j ∈ J - {k}. B i j * c' j) = 0"
      ― ‹Same instantiation caveat as in the vacuous case: pin both the matrix and the index set.›
      using insert.IH[where A = B and J = "J - {k}", OF finite_Diff[OF fJ] cardJk BK] by blast
    ― ‹Now choose the eliminated unknown so as to satisfy the singled-out equation.›
    define S where "S = (∑j ∈ J - {k}. A i0 j * c' j)"
    define c where "c = (λj. if j = k then - S / a else c' j)"
    have SK: "S ∈ K" unfolding S_def using ent c'K by (auto intro!: sum_closed mult_closed)
    have cK: "⋀j. c j ∈ K"
      unfolding c_def using SK aK c'K by (auto intro!: divide_closed uminus_closed)
    have ck: "c k = - S / a" by (simp add: c_def)
    have cj: "⋀j. j ∈ J - {k} ⟹ c j = c' j" by (simp add: c_def)
    ― ‹Split every sum over @{term J} at the eliminated unknown.›
    have split: "(∑j ∈ J. f j * c j) = f k * c k + (∑j ∈ J - {k}. f j * c' j)" for f
    proof -
      have "(∑j ∈ J. f j * c j) = f k * c k + (∑j ∈ J - {k}. f j * c j)"
        using k fJ by (simp add: sum.remove)
      also have "(∑j ∈ J - {k}. f j * c j) = (∑j ∈ J - {k}. f j * c' j)"
        by (rule sum.cong) (auto simp: cj)
      finally show ?thesis .
    qed
    have eq0: "(∑j ∈ J. A i0 j * c j) = 0"
      using split[of "A i0"] anz by (simp add: ck a_def[symmetric] S_def[symmetric])
    have eqI: "(∑j ∈ J. A i j * c j) = 0" if i: "i ∈ I" for i
    proof -
      ― ‹The eliminated equation says exactly that the tail sum equals @{term "A i k / a * S"}.›
      have "(∑j ∈ J - {k}. A i j * c' j) - A i k / a * S = 0"
        using c'eq i unfolding B_def S_def
        by (simp add: sum_subtractf field_simps sum_distrib_left flip: sum_divide_distrib)
      then have tail: "(∑j ∈ J - {k}. A i j * c' j) = A i k / a * S" by simp
      have "(∑j ∈ J. A i j * c j) = A i k * (- S / a) + A i k / a * S"
        using split[of "A i"] by (simp add: ck tail)
      also have "… = 0" by (simp add: field_simps)
      finally show ?thesis .
    qed
    show ?thesis
    proof (intro exI conjI)
      show "∀j. c j ∈ K" using cK by blast
      show "∃j ∈ J. c j ≠ 0" using c'nz cj by force
      show "∀i ∈ insert i0 I. (∑j ∈ J. A i j * c j) = 0" using eq0 eqI by blast
    qed
  qed
qed

end (* subfield *)

end