Support vector machines

as in s4cs

def separable {k : ℕ} (A B : Set (Fin k → ℝ)) : Prop

Equations

• separable A B = ∃ (b : ℝ) (w : Fin k → ℝ), (∀ x ∈ A, w ⬝ᵥ x - b ≤ -1) ∧ ∀ x ∈ B, w ⬝ᵥ x - b ≥ 1

theorem tooHardForChatGPT (x y : ℝ) (h₀ : 2 ≤ x + y) : 2 ≤ x ^ 2 + y ^ 2

theorem tooHardForChatGPT₁ {x y : ℝ} (h₀ : 2 < x + y) : 2 < x ^ 2 + y ^ 2

theorem uniqueClaim₂ (x y : ℝ) (h₀ : 2 ≤ x + y) (h₁ : x ^ 2 + y ^ 2 ≤ 2) : (x, y) = (1, 1)

def A₀ : Set (Fin 2 → ℝ)

Equations

• A₀ = {![0, 0], ![1, 1]}

def A₁ : Set (Fin 2 → ℝ)

Equations

• A₁ = {![0, 1], ![1, 0]}

def φ : (Fin 2 → ℝ) → Fin 3 → ℝ

Equations

• φ x = ![x 0, x 1, (x 0 + x 1 - 1) ^ 2]

def φ₀ : (Fin 2 → ℝ) → Fin 1 → ℝ

The "kernel trick" means we forget about the data just map "without the computational burden of explicitly performing the transformation"

Equations

• φ₀ x = ![(x 0 + x 1 - 1) ^ 2]