Linear regression

over ℝ or ℂ

noncomputable def K₁ {n : ℕ} {R : Type u_1} [RCLike R] (x : Fin n → R) : Submodule R (EuclideanSpace R (Fin n))

Equations

• K₁ x = Submodule.span R {WithLp.toLp 2 x, WithLp.toLp 2 fun (x : Fin n) => 1}

theorem hxK₁ {n : ℕ} {R : Type u_1} [RCLike R] (x : Fin n → R) : WithLp.toLp 2 x ∈ K₁ x

theorem h1K₁ {n : ℕ} {R : Type u_1} [RCLike R] (x : Fin n → R) : (WithLp.toLp 2 fun (x : Fin n) => 1) ∈ K₁ x

theorem topsub₁ {n : ℕ} {R : Type u_1} [RCLike R] (x : Fin n → R) : ⊤ ≤ Submodule.span R (Set.range ![⟨WithLp.toLp 2 x, ⋯⟩, ⟨WithLp.toLp 2 fun (x : Fin n) => 1, ⋯⟩])

def Kvec₁ {n : ℕ} {R : Type u_1} [RCLike R] (x : Fin n → R) : Fin (Nat.succ 0).succ → ↥(K₁ x)

Equations

• Kvec₁ x = ![⟨WithLp.toLp 2 x, ⋯⟩, ⟨WithLp.toLp 2 fun (x : Fin n) => 1, ⋯⟩]

noncomputable def regression_coordinates₁ {n : ℕ} {R : Type u_1} [RCLike R] (x y : Fin n → R) (lin_indep : LinearIndependent R (Kvec₁ x)) : Fin 2 → R

Given points (x i, y i), obtain the coordinates [c, d] such that y = c x + d is the best fit regression line.

Equations

• regression_coordinates₁ x y lin_indep i = ((Module.Basis.mk lin_indep ⋯).repr ⟨(K₁ x).starProjection (WithLp.toLp 2 y), ⋯⟩) i

def A {m : ℕ} {R : Type u_1} [RCLike R] (x : Fin m → R) : Matrix (Fin m) (Fin 2) R

Equations

• A x = Matrix.transpose ![x, fun (x : Fin m) => 1]

noncomputable def getCoeffs {m : ℕ} {R : Type u_1} [RCLike R] (x y : Fin m → R) : Matrix (Fin 2) (Fin 1) R

Equations

• getCoeffs x y = (((A x).transpose.mulᵣ (A x))⁻¹.mulᵣ (A x).transpose).mulᵣ fun (i : Fin m) (x : Fin 1) => y i

def theDistance {m : ℕ} {R : Type u_1} [RCLike R] (x y : Fin m → R) (M : Matrix (Fin 2) (Fin 1) R) : R

getCoeffs is supposed to mimize this

Equations

• theDistance x y M = ∑ i : Fin m, (y i - (M 0 0 + M 1 0 * x i)) ^ 2

theorem getCoeffs_minimizes_theDistance {m : ℕ} {R : Type u_1} [RCLike R] [LE R] (x y : Fin m → R) (M : Matrix (Fin 2) (Fin 1) R) (a b : R) : theDistance x y (getCoeffs x y) ≤ theDistance x y M

getCoeffs minimizes theDistance.

theorem matrix_smul {m : ℕ} {R : Type u_1} [RCLike R] (b : Matrix (Fin m) (Fin 1) R) (v : Matrix (Fin 2) (Fin 2) R) (c : R) (o : Matrix (Fin m) (Fin 2) R) (i : Matrix (Fin 2) (Fin m) R) : o * (c • v * i * b) = c • (o * (v * i * b))

theorem getx {m : ℕ} {R : Type u_1} [RCLike R] (x : Fin m → R) (c : R) (e : Matrix (Fin 2) (Fin 1) R) : ((c • e) 0 0 • x + (c • e) 1 0 • fun (x : Fin m) => 1) = fun (i : Fin m) => (c • (A x).mulᵣ e) i 0

theorem getDet {n : ℕ} {R : Type u_1} [RCLike R] (x : Fin n → R) : !![∑ i : Fin n, x i ^ 2, ∑ i : Fin n, x i; ∑ i : Fin n, x i, ↑n]⁻¹ = ((∑ i : Fin n, x i ^ 2) * ↑n - (∑ i : Fin n, x i) ^ 2)⁻¹ • !![↑n, -∑ i : Fin n, x i; -∑ i : Fin n, x i, ∑ i : Fin n, x i ^ 2]

theorem matmulcase {m : ℕ} {R : Type u_1} [RCLike R] (x : Fin m → R) : Matrix.mulᵣ ![x, fun (x : Fin m) => 1] (Matrix.transpose ![x, fun (x : Fin m) => 1]) = !![∑ i : Fin m, x i ^ 2, ∑ i : Fin m, x i; ∑ i : Fin m, x i, ↑m]

theorem matrix_proj_in_subspace {m : ℕ} {R : Type u_1} [RCLike R] (x : Fin m → R) (Y : Matrix (Fin m) (Fin 1) R) : (WithLp.toLp 2 fun (i : Fin m) => (A x).mulᵣ ((((A x).transpose.mulᵣ (A x))⁻¹.mulᵣ (A x).transpose).mulᵣ Y) i 0) ∈ K₁ x

theorem matrix_algebra {n t o w : ℕ} {R : Type u_1} [RCLike R] (B : Matrix (Fin n) (Fin t) R) (hB : IsUnit (B.transpose * B).det) (m : Fin t → Fin o → R) (P : Matrix (Fin n) (Fin w) R) : Matrix.transpose m * B.transpose * P = Matrix.transpose m * B.transpose * (B * ((B.transpose * B)⁻¹ * B.transpose * P))

theorem star_projection_is_matrix_product {m : ℕ} {R : Type u_1} [RCLike R] [TrivialStar R] {x : Fin m → R} (y : Fin m → R) (hB : IsUnit ((A x).transpose * A x).det) : (fun (i : Fin m) => (A x).mulᵣ ((((A x).transpose.mulᵣ (A x))⁻¹.mulᵣ (A x).transpose).mulᵣ fun (j : Fin m) (x : Fin 1) => y j) i 0) = ((K₁ x).starProjection (WithLp.toLp 2 y)).ofLp

This does not hold over ℂ.

theorem getCoeffs_eq_regression_coordinates₁ {m : ℕ} (x y : Fin m → ℝ) (i : Fin 2) (hl : LinearIndependent ℝ (Kvec₁ x)) (hB : IsUnit ((A x).transpose * A x).det) : getCoeffs x y i 0 = regression_coordinates₁ x y hl i

noncomputable def hat {m : ℕ} (x y : Fin m → ℝ) (h : LinearIndependent ℝ (Kvec₁ x)) : Fin m → ℝ

The coordinates "y hat" or y^.

Equations

• hat x y h i = regression_coordinates₁ x y h 0 * x i + regression_coordinates₁ x y h 1

noncomputable def bar {m : ℕ} (y : Fin m → ℝ) : ℝ

The value "y bar".

Equations

• bar y = 1 / ↑m * ∑ i : Fin m, y i

def nonconstant {m : ℕ} (x : Fin m → ℝ) : Prop

Equations

• nonconstant x = ∃ (i : Fin m) (j : Fin m), x i ≠ x j

theorem indep_of_nonconstant {m : ℕ} {x : Fin m → ℝ} (h : nonconstant x) : LinearIndependent ℝ (Kvec₁ x)

theorem isunit_of_nonconstant {m : ℕ} (x : Fin m → ℝ) (hx : (∑ i : Fin m, x i ^ 2) * ↑m - (∑ i : Fin m, x i) ^ 2 ≠ 0) : IsUnit ((A x).transpose * A x).det

theorem sum_of_constant' {m : ℕ} (x : Fin m → ℝ) (h : nonconstant x) : ∑ f : Fin 2 → Fin m with f 0 ≠ f 1, (x (f 0) - x (f 1)) ^ 2 ≠ 0

theorem Finset.sum_iUnion {k : ℕ} {T : Type u_1} [Fintype T] (A : Fin k → Finset T) (X : T → ℝ) (h : univ.toSet.PairwiseDisjoint A) : ∑ i : T with i ∈ ⋃ (j : Fin k), ↑(A j), X i = ∑ j : Fin k, ∑ i : T with i ∈ A j, X i

A "missing lemma" in Mathlib?

theorem decompose_pair_sum {n : ℕ} (f : Fin n → ℝ) : ∑ x : Fin 2 → Fin n, f (x 0) = ∑ i : Fin n, ∑ g : Fin 2 → Fin n with g 0 = i, f (g 0)

theorem diagonalSq {m : ℕ} (x : Fin m → ℝ) (x_1 : Fin m) : ∑ x_2 : Fin 2 → Fin m with x_2 1 = x_1, x (x_2 0) ^ 2 = ∑ i : Fin m, x i ^ 2

theorem sum_ij_xi2 {m : ℕ} (x : Fin m → ℝ) : ∑ σ : Fin 2 → Fin m, x (σ 0) ^ 2 = ↑m * ∑ σ : Fin 2 → Fin m with σ 0 = σ 1, x (σ 0) * x (σ 1)

theorem offDiagonalSq {m : ℕ} (x : Fin m → ℝ) : ∑ f : Fin 2 → Fin m with f 0 ≠ f 1, x (f 1) ^ 2 = (↑m - 1) * ∑ i : Fin m, x i ^ 2

theorem determinant_value_nonzero_of_nonconstant {m : ℕ} (x : Fin m → ℝ) (h : nonconstant x) : (∑ i : Fin m, x i ^ 2) * ↑m - (∑ i : Fin m, x i) ^ 2 ≠ 0

theorem average_predicted_value {m : ℕ} (x y : Fin m → ℝ) (h : nonconstant x) : ∑ i : Fin m, y i = ∑ i : Fin m, hat x y ⋯ i

def A₃ (x : Fin 3 → ℝ) : Matrix (Fin 3) (Fin 2) ℝ

Equations

• A₃ x = !![x 0, 1; x 1, 1; x 2, 1]

noncomputable def getCoeffs₃ (x y : Fin 3 → ℝ) : Matrix (Fin 2) (Fin 1) ℝ

Equations

• getCoeffs₃ x y = (((A₃ x).transpose.mulᵣ (A₃ x))⁻¹.mulᵣ (A₃ x).transpose).mulᵣ !![y 0; y 1; y 2]

theorem getx₃ (x : Fin 3 → ℝ) (c : ℝ) (e : Matrix (Fin 2) (Fin 1) ℝ) : ((c • e) 0 0 • x + (c • e) 1 0 • fun (x : Fin 3) => 1) = fun (i : Fin 3) => (c • (!![x 0, 1; x 1, 1; x 2, 1] * e)) i 0

theorem getDet₃ (x₀ x₁ x₂ : ℝ) : !![x₀ ^ 2 + x₁ ^ 2 + x₂ ^ 2, x₀ + x₁ + x₂; x₀ + x₁ + x₂, 3]⁻¹ = (2 * (x₀ ^ 2 + x₁ ^ 2 + x₂ ^ 2 - x₀ * x₁ - x₀ * x₂ - x₁ * x₂))⁻¹ • !![3, -(x₀ + x₁ + x₂); -(x₀ + x₁ + x₂), x₀ ^ 2 + x₁ ^ 2 + x₂ ^ 2]

theorem matrix_proj_in_subspace₃ (x : Fin 3 → ℝ) (Y : Matrix (Fin 3) (Fin 1) ℝ) : (WithLp.toLp 2 fun (i : Fin 3) => (A₃ x).mulᵣ ((((A₃ x).transpose.mulᵣ (A₃ x))⁻¹.mulᵣ (A₃ x).transpose).mulᵣ Y) i 0) ∈ K₁ x

theorem star_projection_is_matrix_product₃ {x : Fin 3 → ℝ} (y : Fin 3 → ℝ) (hB : IsUnit (!![x 0, 1; x 1, 1; x 2, 1].transpose * !![x 0, 1; x 1, 1; x 2, 1]).det) : (fun (i : Fin 3) => (A₃ x).mulᵣ ((((A₃ x).transpose.mulᵣ (A₃ x))⁻¹.mulᵣ (A₃ x).transpose).mulᵣ !![y 0; y 1; y 2]) i 0) = ((K₁ x).starProjection (WithLp.toLp 2 y)).ofLp

theorem getCoeffs₃_eq_regression_coordinates₁ (x y : Fin 3 → ℝ) (i : Fin 2) (hl : LinearIndependent ℝ (Kvec₁ x)) (hB : IsUnit (!![x 0, 1; x 1, 1; x 2, 1].transpose * !![x 0, 1; x 1, 1; x 2, 1]).det) : getCoeffs₃ x y i 0 = regression_coordinates₁ x y hl i

noncomputable def K₂ {n : ℕ} (x₀ x₁ : Fin n → ℝ) : Submodule ℝ (EuclideanSpace ℝ (Fin n))

Multivariate regression.

Equations

• K₂ x₀ x₁ = Submodule.span ℝ {WithLp.toLp 2 x₀, WithLp.toLp 2 x₁, WithLp.toLp 2 fun (x : Fin n) => 1}

theorem hxK₂₀ {n : ℕ} (x₀ x₁ : Fin n → ℝ) : WithLp.toLp 2 x₀ ∈ K₂ x₀ x₁

theorem hxK₂₁ {n : ℕ} (x₀ x₁ : Fin n → ℝ) : WithLp.toLp 2 x₁ ∈ K₂ x₀ x₁

theorem h1K₂ {n : ℕ} (x₀ x₁ : Fin n → ℝ) : (WithLp.toLp 2 fun (x : Fin n) => 1) ∈ K₂ x₀ x₁

theorem topsub₂ {n : ℕ} (x₀ x₁ : Fin n → ℝ) : ⊤ ≤ Submodule.span ℝ (Set.range ![⟨WithLp.toLp 2 x₀, ⋯⟩, ⟨WithLp.toLp 2 x₁, ⋯⟩, ⟨WithLp.toLp 2 fun (x : Fin n) => 1, ⋯⟩])

def Kvec₂ {n : ℕ} (x₀ x₁ : Fin n → ℝ) : Fin (Nat.succ 0).succ.succ → ↥(K₂ x₀ x₁)

Equations

• Kvec₂ x₀ x₁ = ![⟨WithLp.toLp 2 x₀, ⋯⟩, ⟨WithLp.toLp 2 x₁, ⋯⟩, ⟨WithLp.toLp 2 fun (x : Fin n) => 1, ⋯⟩]

noncomputable def regression_coordinates₂ {n : ℕ} (x₀ x₁ y : Fin n → ℝ) (lin_indep : LinearIndependent ℝ (Kvec₂ x₀ x₁)) : Fin 3 → ℝ

Equations

• regression_coordinates₂ x₀ x₁ y lin_indep i = ((Module.Basis.mk lin_indep ⋯).repr ⟨(K₂ x₀ x₁).starProjection (WithLp.toLp 2 y), ⋯⟩) i

theorem indep₀₁₂ : LinearIndependent ℝ (Kvec₁ ![0, 1, 2])

theorem hvo₀₁₁ (w : EuclideanSpace ℝ (Fin 3)) (hw : w ∈ K₁ ![0, 1, 2]) : inner ℝ (!₂[0, 1, 1] - !₂[1 / 6, 4 / 6, 7 / 6]) w = 0