def IsTriangular (n : ℤ) : Prop

Equations

• IsTriangular n = ∃ (k : ℤ), k * (k + 1) = 2 * n

def IsnPolygonal (s : ℤ) : s ≥ 3 → (n : ℕ) → Prop

Equations

• IsnPolygonal s x✝ n = (n = 0 ∨ ∃ (k : ℕ), (↑s - 2) / 2 * (↑k * (↑k - 1)) + ↑k = ↑n)

def IsnPolygonal' (s : ℤ) : s ≥ 3 → (n : ℕ) → Prop

Equations

• IsnPolygonal' s x✝ n = (n = 0 ∨ ∃ (k : ℕ), (↑s - 2) / 2 * (↑k ^ 2 - ↑k) + ↑k = ↑n)

def IsnPolygonal'' (s : ℤ) : s ≥ 3 → (n : ℕ) → Prop

Equations

• IsnPolygonal'' s x✝ n = (n = 0 ∨ ∃ (k : ℕ), ((↑s - 2) * ↑k ^ 2 - (↑s - 4) * ↑k) / 2 = ↑n)

def IsnPolygonal₀ (s : ℤ) : s ≥ 3 → (n : ℕ) → Prop

Equations

• IsnPolygonal₀ s x✝ n = (n = 0 ∨ IsSquare (8 * (s - 2) * ↑n + (s - 4) ^ 2) ∧ (Int.sqrt (8 * (s - 2) * ↑n + (s - 4) ^ 2) + (s - 4)) % (2 * (s - 2)) = 0)

def Triangular : Type

Equations

• Triangular = { n : ℕ // IsTriangular ↑n }

def Polygonal (s : ℤ) (hs : s ≥ 3) : Type

Equations

• Polygonal s hs = { n : ℕ // IsnPolygonal s hs n }

def foldrfun (s : ℤ) (hs : s ≥ 3) (x1 : Polygonal s hs) (x2 : ℤ) : ℤ

Equations

• foldrfun s hs x1 x2 = ↑↑x1 + x2

instance instLeftCommutativePolygonalIntFoldrfun {n : ℤ} {hs : n ≥ 3} : LeftCommutative (foldrfun n hs)

def sumPolyToInt (s : ℤ) (hs : s ≥ 3) (S : List (Polygonal s hs)) : ℤ

Equations

• sumPolyToInt s hs S = List.foldr (foldrfun s hs) 0 S

theorem kfactq (k : ℚ) : k * (k - 1) = k ^ 2 - k

Both conditions IsnPolygonal and IsnPolygonal' are equivalent.

theorem PolyEquiv : IsnPolygonal = IsnPolygonal'

theorem PolyEquiv' : IsnPolygonal = IsnPolygonal''

theorem PolyEquiv₀ : IsnPolygonal = IsnPolygonal₀

instance instBEqPolygonal {s : ℤ} {hs : s ≥ 3} : BEq (Polygonal s hs)

Equations

• instBEqPolygonal = { beq := fun (a b : Polygonal s hs) => if (↑a == ↑b) = true then true else false }

instance instLawfulBEqPolygonal {s : ℤ} {hs : s ≥ 3} : LawfulBEq (Polygonal s hs)

instance instDecidableEqPolygonal {s : ℤ} {hs : s ≥ 3} : DecidableEq (Polygonal s hs)

Equations

• instDecidableEqPolygonal a b = if h : ↑a = ↑b then isTrue ⋯ else isFalse ⋯

instance instLEPolygonal {s : ℤ} {hs : s ≥ 3} : LE (Polygonal s hs)

Equations

• instLEPolygonal = { le := fun (a b : Polygonal s hs) => ↑a ≤ ↑b }

theorem Polyrw (s : ℤ) (hs : s ≥ 3) (n : ℕ) : IsnPolygonal s hs n ↔ IsnPolygonal' s hs n

theorem one_is_poly (s : ℤ) (hs : s ≥ 3) : IsnPolygonal s hs 1

theorem zero_is_poly (s : ℤ) (hs : s ≥ 3) : IsnPolygonal s hs 0

def PolyOne (s : ℤ) (hs : s ≥ 3) : Polygonal s hs

Equations

• PolyOne s hs = ⟨1, ⋯⟩

def PolyZero (s : ℤ) (hs : s ≥ 3) : Polygonal s hs

Equations

• PolyZero s hs = ⟨0, ⋯⟩

instance instDecidableIsnPolygonal₀ {m : ℤ} {n : m ≥ 3} {h : ℕ} : Decidable (IsnPolygonal₀ m n h)

Equations

• instDecidableIsnPolygonal₀ = id instDecidableOr

instance instDecidableIsnPolygonal {m : ℤ} {n : m ≥ 3} {h : ℕ} : Decidable (IsnPolygonal m n h)

Equations

• instDecidableIsnPolygonal = decidable_of_iff (IsnPolygonal₀ m n h) ⋯

theorem polyform (m : ℤ) (r : ℕ) (hm2geq3 : m + 2 ≥ 3) : ↑m / 2 * (↑r ^ 2 - ↑r) + ↑r = ↑|⌈↑m / 2 * (↑r ^ 2 - ↑r) + ↑r⌉|

theorem polyformval (m : ℤ) (r : ℕ) (hm2geq3 : m + 2 ≥ 3) : IsnPolygonal (m + 2) hm2geq3 ⌈↑m / 2 * (↑r ^ 2 - ↑r) + ↑r⌉.natAbs

def getnthpoly (s : ℤ) (hs : s ≥ 3) (n : ℕ) : Polygonal s hs

Equations

• getnthpoly s hs n = ⟨⌈(↑s - 2) / 2 * (↑n ^ 2 - ↑n) + ↑n⌉.natAbs, ⋯⟩

theorem getnthpoly_monotone (s : ℤ) (hs : s ≥ 3) (n : ℕ) : ↑(getnthpoly s hs n) ≤ ↑(getnthpoly s hs (n + 1))

theorem getnthpoly_polyone (s : ℤ) (hs : s ≥ 3) : getnthpoly s hs 1 = PolyOne s hs

theorem getnthpoly_intone (s : ℤ) (hs : s ≥ 3) : ↑(getnthpoly s hs 1) = 1

theorem getnthpoly_geq (s : ℤ) (hs : s ≥ 3) (n : ℕ) : ↑(getnthpoly s hs n) ≥ n

theorem poly_set (s : ℤ) (hs : s ≥ 3) : {x : ℕ | IsnPolygonal s hs x} = {x : ℕ | ∃ (n : ℕ), ↑(getnthpoly s hs n) = x}

def getnthpolyfun (s : ℤ) (hs : s ≥ 3) (a : ℕ) : Polygonal s hs

Equations

• getnthpolyfun s hs a = getnthpoly s hs a

def getlepoly₀ (s : ℤ) (hs : s ≥ 3) (b : ℕ) : Finset (Polygonal s hs)

Equations

• getlepoly₀ s hs b = Finset.filter (fun (x : Polygonal s hs) => ↑x ≤ b) (getnthpolyfun s hs '' ↑(Finset.range (b + 1))).toFinset

def finCaseDec (p : ℕ → Prop) (n : ℕ) [DecidablePred p] : Decidable (∃ a < n + 1, p a)

Equations

• finCaseDec p n = ⋯.mp (List.decidableBEx p (List.range (n + 1)))

theorem getlepoly₀Correct (s : ℤ) (hs : s ≥ 3) (n : ℕ) : ↑(getlepoly₀ s hs n) = {a : Polygonal s hs | ↑a ≤ n}

def IsNKPolygonal (s : ℤ) (hs : s ≥ 3) (k n : ℕ) : Prop

Equations

• IsNKPolygonal s hs k n = ∃ (S : List ℕ), (S.all fun (b : ℕ) => decide (IsnPolygonal s hs b)) = true ∧ S.length = k ∧ S.sum = n

instance instDecidablePredNatIsNKPolygonalOfNat (m : ℤ) (hm : m ≥ 3) : DecidablePred (IsNKPolygonal m hm 0)

Equations

• instDecidablePredNatIsNKPolygonalOfNat m hm 0 = id (let_fun this := ⋯; isTrue this)
• instDecidablePredNatIsNKPolygonalOfNat m hm k.succ = id (let_fun this := ⋯; isFalse this)

instance instDecidablePredNatIsNKPolygonal (s : ℤ) (hs : s ≥ 3) (k : ℕ) : DecidablePred (IsNKPolygonal s hs k)

Equations

• One or more equations did not get rendered due to their size.