def IsTriangular (n : ℤ) : Prop

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Triangular : Type

Equations

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

def Polygonal (m : ℤ) (hm : m ≥ 3) : Type

Equations

• Polygonal m hm = { n : ℕ // IsnPolygonal m hm n }

def foldrfun (m : ℤ) (hm : m ≥ 3) (x1 : Polygonal m hm) (x2 : ℤ) : ℤ

Equations

• foldrfun m hm x1 x2 = ↑↑x1 + x2

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

def sumPolyToInt (m : ℤ) (hm : m ≥ 3) (S : List (Polygonal m hm)) : ℤ

Equations

• sumPolyToInt m hm S = List.foldr (foldrfun m hm) 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 {m : ℤ} {hm : m ≥ 3} : BEq (Polygonal m hm)

Equations

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

instance instLawfulBEqPolygonal {m : ℤ} {hm : m ≥ 3} : LawfulBEq (Polygonal m hm)

instance instDecidableEqPolygonal {n : ℤ} {hm : n ≥ 3} : DecidableEq (Polygonal n hm)

Equations

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

instance instLEPolygonal {m : ℤ} {hm : m ≥ 3} : LE (Polygonal m hm)

Equations

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

theorem Polyrw (m : ℤ) (n : ℕ) (hm : m ≥ 3) : IsnPolygonal m hm n ↔ IsnPolygonal' m hm n

theorem one_is_poly (m : ℤ) (hm : m ≥ 3) : IsnPolygonal m hm 1

theorem zero_is_poly (m : ℤ) (hm : m ≥ 3) : IsnPolygonal m hm 0

def PolyOne (m : ℤ) (hm : m ≥ 3) : Polygonal m hm

Equations

• PolyOne m hm = ⟨1, ⋯⟩

def PolyZero (m : ℤ) (hm : m ≥ 3) : Polygonal m hm

Equations

• PolyZero m hm = ⟨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 (m : ℤ) (hm : m ≥ 3) (n : ℕ) : Polygonal m hm

Equations

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

theorem getnthpoly_monotone (m : ℤ) (hm : m ≥ 3) (n : ℕ) : ↑(getnthpoly m hm n) ≤ ↑(getnthpoly m hm (n + 1))

theorem getnthpoly_polyone (m : ℤ) (hm : m ≥ 3) : getnthpoly m hm 1 = PolyOne m hm

theorem getnthpoly_intone (m : ℤ) (hm : m ≥ 3) : ↑(getnthpoly m hm 1) = 1

theorem getnthpoly_geq (m : ℤ) (n : ℕ) (hm : m ≥ 3) : ↑(getnthpoly m hm n) ≥ n

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

def getnthpolyfun (m : ℤ) (hm : m ≥ 3) (x : ℕ) : Polygonal m hm

Equations

• getnthpolyfun m hm x = getnthpoly m hm x

def getlepoly₀ (m : ℤ) (hm : m ≥ 3) (b : ℕ) : Finset (Polygonal m hm)

Equations

• getlepoly₀ m hm b = Finset.filter (fun (x : Polygonal m hm) => ↑x ≤ b) (getnthpolyfun m hm '' ↑(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 (m : ℤ) (n : ℕ) (hm : m ≥ 3) : ↑(getlepoly₀ m hm n) = {x : Polygonal m hm | ↑x ≤ n}

def IsNKPolygonal (m : ℤ) (hm : m ≥ 3) (k n : ℕ) : Prop

Equations

• IsNKPolygonal m hm k n = ∃ (S : List ℕ), (S.all fun (b : ℕ) => decide (IsnPolygonal m hm 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 (m : ℤ) (hm : m ≥ 3) (k : ℕ) : DecidablePred (IsNKPolygonal m hm k)

Equations

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