Gaussian elimination: multi-row forward sweep (refinement)

GaussPivotStep.lean treats a single forward-elimination pivot step and proves it preserves the solution set of A · x = b. This file iterates that step across a list of target rows — the forward sweep that eliminates one fixed pivot column from each of a batch of rows — and proves the whole sweep preserves the solution set, by induction over the row list using the single-step lemma.

A sweep is parameterized by a fixed pivot row p and a list targets of (row, coefficient) pairs: it folds the single pivot step pivotStepMat … r c across the list, in order. The matrix transform is gaussSweepMat and the target-vector transform is gaussSweepRhs. As long as every target row in the list is distinct from the pivot row p (hp : ∀ rc ∈ targets, p ≠ rc.1), the single-step invariance composes:

gaussSweep_preserves_solution : (gaussSweepMat A p targets).mulVec x = gaussSweepRhs b p targets ↔ A.mulVec x = b

This is the forward-elimination-preserves-solutions result. The remaining Gaussian-elimination tail — pivot selection (search for a nonzero pivot, row swaps), back-substitution, and the termination argument — is the suite's frontier.

API

• gaussSweepMat — coefficient matrix after sweeping the pivot step across targets.
• gaussSweepRhs — target vector after the same sweep.
• gaussSweep_preserves_solution — x solves the swept system iff it solves the original one (solution-set invariance of the whole forward sweep).

def Transfer.Examples.CoqEAL.GaussSweep.gaussSweepMat {n : Type u_1} [DecidableEq n] {R : Type u_2} [CommRing R] (A : Matrix n n R) (p : n) : List (n × R) → Matrix n n R

The coefficient matrix after a forward sweep: fold the single pivot step (against the fixed pivot row p) across the list targets of (target row, coefficient) pairs, in order.

Equations

• One or more equations did not get rendered due to their size.
• Transfer.Examples.CoqEAL.GaussSweep.gaussSweepMat A p [] = A

def Transfer.Examples.CoqEAL.GaussSweep.gaussSweepRhs {n : Type u_1} [DecidableEq n] {R : Type u_2} [CommRing R] (b : n → R) (p : n) : List (n × R) → n → R

The target vector after the same forward sweep.

Equations

• One or more equations did not get rendered due to their size.
• Transfer.Examples.CoqEAL.GaussSweep.gaussSweepRhs b p [] = b

@[simp]

theorem Transfer.Examples.CoqEAL.GaussSweep.gaussSweepMat_nil {n : Type u_1} [DecidableEq n] {R : Type u_2} [CommRing R] (A : Matrix n n R) (p : n) : gaussSweepMat A p [] = A

@[simp]

theorem Transfer.Examples.CoqEAL.GaussSweep.gaussSweepMat_cons {n : Type u_1} [DecidableEq n] {R : Type u_2} [CommRing R] (A : Matrix n n R) (p : n) (rc : n × R) (rest : List (n × R)) : gaussSweepMat A p (rc :: rest) = gaussSweepMat (GaussPivotStep.pivotStepMat A p rc.1 rc.2) p rest

@[simp]

theorem Transfer.Examples.CoqEAL.GaussSweep.gaussSweepRhs_nil {n : Type u_1} [DecidableEq n] {R : Type u_2} [CommRing R] (b : n → R) (p : n) : gaussSweepRhs b p [] = b

@[simp]

theorem Transfer.Examples.CoqEAL.GaussSweep.gaussSweepRhs_cons {n : Type u_1} [DecidableEq n] {R : Type u_2} [CommRing R] (b : n → R) (p : n) (rc : n × R) (rest : List (n × R)) : gaussSweepRhs b p (rc :: rest) = gaussSweepRhs (GaussPivotStep.pivotStepRhs b p rc.1 rc.2) p rest

theorem Transfer.Examples.CoqEAL.GaussSweep.gaussSweep_preserves_solution {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (p : n) (x : n → R) (targets : List (n × R)) (A : Matrix n n R) (b : n → R) : (∀ rc ∈ targets, p ≠ rc.1) → ((gaussSweepMat A p targets).mulVec x = gaussSweepRhs b p targets ↔ A.mulVec x = b)

The forward sweep preserves the solution set. A vector x satisfies the swept system gaussSweepMat A p targets · x = gaussSweepRhs b p targets iff it satisfies the original system A · x = b, provided every target row in the sweep is distinct from the pivot row p. Proof: induction over the row list, peeling one pivot step at a time via pivotStep_preserves_solution.