noncomputable def Misc.P001.P1.f (n : ℕ) : ℝ

Equations

• Misc.P001.P1.f n = (fun (x : ℝ) => (↑n ^ (↑n)⁻¹) ^ x)^[n] 1

theorem Misc.P001.P1.thm₁ : f 2 = √2 ^ √2

theorem Misc.P001.P1.f_lt {n : ℕ} (h : 1 < n) : f n < ↑n

theorem Misc.P001.P1.thm₂ : f 2003 < 2003

theorem Misc.P001.P2.sum_mul_le_112_of_sum_eq_12 {a b c : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a + b + c = 12) : a * b * c + a * b + b * c + c * a ≤ 112

theorem Misc.P001.P3.thm_6_div_mul_succ_mul {n : ℕ} : 6 ∣ n * (n + 1) * (2 * n + 1)

theorem Misc.P001.P4.main {b : ℝ} {n : ℕ} (hb : b ≠ 1) : (∑ k ∈ Finset.range n, (↑n - ↑k) * b ^ k) * (b - 2) + ↑n = ∑ k ∈ Finset.range n, (b - ↑n + ↑k) * b ^ k

def Misc.P001.P5.le (n m : ℕ) : Prop

Equations

• Misc.P001.P5.le n m = ∃ (f : ℕ → ℕ) (k : ℕ), f 0 = n ∧ f k = m ∧ ∀ (k : ℕ), f k.succ = (f k).succ

theorem Misc.P001.P5.le_iff_nat_le {n m : ℕ} : le n m ↔ n ≤ m

def Misc.P001.P5.f : ℕ → ℕ → ℕ

Equations

• Misc.P001.P5.f x✝ 0 = x✝
• Misc.P001.P5.f x✝ m.succ = Misc.P001.P5.f (x✝ + 1) m

theorem Misc.P001.P5.thm₁ {n m : ℕ} : f n (m + 1) = f n m + 1

theorem Misc.P001.P5.thm₂ {n : ℕ} : f n n = n * 2

class Misc.P001.P6.World : Type 1

• HorseT : Type
• Horse : Set HorseT
• WhiteHorse : Set HorseT
• horse_univ {e : HorseT} : e ∈ Horse
• exi_non_white_horse : ∃ (e : HorseT), e ∉ WhiteHorse

@[instance_reducible]

instance Misc.P001.P6.instInhabitedWorld : Inhabited World

Equations

• Misc.P001.P6.instInhabitedWorld = { default := { HorseT := String, Horse := Set.univ, WhiteHorse := ∅, horse_univ := Misc.P001.P6.instInhabitedWorld._proof_1, exi_non_white_horse := Misc.P001.P6.instInhabitedWorld._proof_2 } }

theorem Misc.P001.P6.whiteHorse_ne_horse [W : World] : World.WhiteHorse ≠ World.Horse

class Misc.P001.P7.World : Type 1

• Person : Type
• drinks : Person → Prop
• nonempty_person : Nonempty Person

@[instance_reducible]

instance Misc.P001.P7.instInhabitedWorld : Inhabited World

Equations

• Misc.P001.P7.instInhabitedWorld = { default := { Person := String, drinks := fun (x : String) => False, nonempty_person := Misc.P001.P7.instInhabitedWorld._proof_1 } }

theorem Misc.P001.P7.exi_imp_forall_drinks [W : World] : ∃ (p : World.Person), World.drinks p → ∀ (p' : World.Person), World.drinks p'

class Misc.P001.P8.World : Type 1

• Woman : Type
• sterile : Woman → Prop
• humanityDiesOut : Prop
• nonempty_woman : Nonempty Woman
• humanityDiesOut_of_forall_sterile : (∀ (w : Woman), sterile w) → humanityDiesOut

@[instance_reducible]

instance Misc.P001.P8.instInhabitedWorld : Inhabited World

Equations

• Misc.P001.P8.instInhabitedWorld = { default := { Woman := String, sterile := fun (x : String) => False, humanityDiesOut := False, nonempty_woman := Misc.P001.P7.instInhabitedWorld._proof_1, humanityDiesOut_of_forall_sterile := Misc.P001.P8.instInhabitedWorld._proof_1 } }

theorem Misc.P001.P8.exi_imp_humanityDiesOut [W : World] : ∃ (w : World.Woman), World.sterile w → World.humanityDiesOut

@[reducible, inline]

noncomputable abbrev Misc.P001.P9.μ : MeasureTheory.Measure ℝ

Equations

• Misc.P001.P9.μ = MeasureTheory.volume

theorem Misc.P001.P9.integral_congr {f g : ℝ → ℝ} {a b : ℝ} (ha : a ≤ b) (h : ∀ (x : ℝ), a ≤ x → x ≤ b → f x = g x) : ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ

theorem Misc.P001.P9.one_add_sqrt_two_pos : 0 < 1 + √2

theorem Misc.P001.P9.log_one_add_sqrt_two_pos : 0 < Real.log (1 + √2)

theorem Misc.P001.P9.log_one_add_sqrt_two_nonneg : 0 ≤ Real.log (1 + √2)

theorem Misc.P001.P9.integrable_of_continuous {f : ℝ → ℝ} {a b : ℝ} (h : Continuous f) : IntervalIntegrable f μ a b

theorem Misc.P001.P9.integral_exp {a b : ℝ} : ∫ (x : ℝ) in a..b, Real.exp x ∂μ = Real.exp b - Real.exp a

theorem Misc.P001.P10.aux₁ {r N n c : ℕ} {a : ℕ → ℕ} (h₂ : ∀ (n : ℕ), a n ≤ r) (h₃ : ∀ (n : ℕ), ∃ (k : ℕ), (∏ i ∈ Finset.range n, ↑(a i)) ^ (↑n)⁻¹ = ↑k) (hrN : r < N) (hn : N ≤ n) (h₄ : 1 ≤ c) (H₁ : ∀ (k : ℕ), N ≤ k → k ≤ n → (∏ i ∈ Finset.range k, ↑(a i)) ^ (↑k)⁻¹ = ↑c) : a n ≤ c

theorem Misc.P001.P10.aux₂ {r N n c : ℕ} {w : ℝ} {a : ℕ → ℕ} (h₃ : ∀ (n : ℕ), ∃ (k : ℕ), (∏ i ∈ Finset.range n, ↑(a i)) ^ (↑n)⁻¹ = ↑k) (hw : max (↑r) (Real.logb (1 + 1 / ↑r) ↑r) + 1 = w) (hN : w < ↑N) (hr : 1 ≤ r) (hrN : r < N) (hn : N ≤ n) (hc : ∏ i ∈ Finset.range N, ↑(a i) = ↑c ^ ↑N) (h₅ : c ≤ r) (H : ∀ (k : ℕ), N ≤ k → k < n → a k = c) (h₁ : ∀ (n : ℕ), 1 ≤ a n) (h₄ : 1 ≤ c) (H₁ : ∀ (k : ℕ), N ≤ k → k ≤ n → (∏ i ∈ Finset.range k, ↑(a i)) ^ (↑k)⁻¹ = ↑c) : c ≤ a n

theorem Misc.P001.P10.aux₃ {r : ℕ} {a : ℕ → ℕ} (h₁ : ∀ (n : ℕ), a n ≠ 0) (h₂ : ∀ (n : ℕ), a n ≤ r) (h₃ : ∀ (n : ℕ), ∃ (k : ℕ), (∏ i ∈ Finset.range n, ↑(a i)) ^ (↑n)⁻¹ = ↑k) : ∃ (c : ℕ) (N : ℕ), ∀ (n : ℕ), N ≤ n → a n = c

theorem Misc.P001.P10.main {a : ℕ → ℕ} (h₁ : ∀ (n : ℕ), a n ≠ 0) (h₂ : ∀ (n : ℕ), a n ≤ 2025) (h₃ : ∀ (n : ℕ), ∃ (k : ℕ), (∏ i ∈ Finset.range n, ↑(a i)) ^ (↑n)⁻¹ = ↑k) : ∃ (c : ℕ) (N : ℕ), ∀ (n : ℕ), N ≤ n → a n = c

theorem Misc.P001.P10.cntrex₁ : ¬∀ {a : ℕ → ℕ}, (∀ (n : ℕ), a n ≤ 2025) → (∀ (n : ℕ), n ≠ 0 → ∃ (k : ℤ), k ^ n = ↑(∏ i : Fin n, a ↑i)) → ∃ (c : ℕ) (N : ℕ), c ≠ 0 ∧ N ≠ 0 ∧ ∀ n ≥ N, a n = c

theorem Misc.P001.P10.main_alt_pnat {a : ℕ+ → ℕ+} (h₁ : ∀ (n : ℕ+), ↑(a n) ≤ 2025) (h₂ : ∀ (n : ℕ+), ∃ (k : ℤ), k ^ ↑n = ↑↑(∏ i : Fin ↑n, a ⟨↑i + 1, ⋯⟩)) : ∃ (c : ℕ+) (N : ℕ+), ∀ (n : ℕ+), ↑n ≥ ↑N → a n = c

theorem Misc.P001.P11.thm₁ {x : ℂ} : Complex.sqrt 2 + x.sqrt = 2 ↔ x = 6 - 4 * Complex.sqrt 2

theorem Misc.P001.P11.thm₂ : √(6 - 4 * √2) = 2 - √2

theorem Misc.P001.P12.thm₃ {a b c : ℤ} (ha : -1 < a) (hb : -1 < b) (hc : -1 < c) : 3 * a * b * c ≤ a ^ 3 + b ^ 3 + c ^ 3

theorem Misc.P001.P13.aux₁ {i j : ℕ} : i < j ↔ 2 ^ i + i < 2 ^ j + j

theorem Misc.P001.P13.aux₂ {i j : ℕ} : i ≤ j ↔ 2 ^ i + i ≤ 2 ^ j + j

theorem Misc.P001.P13.thm₁ {x : ℤ} : 2 ^ x + ↑x = 37 ↔ x = 5