theorem sixteen_times_le_cube {a : ℕ} (ha : 4 ≤ a) : 16 * a ≤ a ^ 3

theorem four_times_sq_le_cube {a : ℕ} (ha : 4 ≤ a) : 4 * a ^ 2 ≤ a ^ 3

theorem add_le_pow_two {R : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] {p q r s : ℕ} (hp : p ≤ r) (hq : q ≤ r) (hr : r + 1 ≤ s) : 2 ^ p + 2 ^ q ≤ 2 ^ s

theorem add_le_pow_two₃ {R : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] {p q r s t : ℕ} (hp : p ≤ s) (hq : q ≤ s) (hr : r ≤ s + 1) (ht : s + 2 ≤ t) : 2 ^ p + 2 ^ q + 2 ^ r ≤ 2 ^ t

theorem add_le_pow_two_add_cube {a : ℕ} {R : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] {p q r : ℕ} (ha : 4 ≤ a) (hp : p ≤ r) (hq : q ≤ r) : 2 ^ p + 2 ^ q ≤ 2 ^ (r + a ^ 3)

theorem calculation_1 {a : ℕ} (s : ℤ) : 4 * ↑(defaultD a) ^ (-2) * ↑(defaultD a) ^ (s + 3) = 4 * ↑(defaultD a) ^ (s + 1)

theorem calculation_2 {a : ℕ} (s : ℤ) : 8⁻¹ * ↑(defaultD a) ^ (-3) * ↑(defaultD a) ^ (s + 3) = 8⁻¹ * ↑(defaultD a) ^ s

theorem calculation_10 {a : ℕ} (h : 100 < ↑(defaultD a)) : (100 + 4 * ↑(defaultD a) ^ (-2) + 8⁻¹ * ↑(defaultD a) ^ (-3)) * ↑(defaultD a) ^ (-1) < 2

theorem calculation_3 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {x y : ℤ} (h : x + 3 < y) : 100 * ↑(defaultD a) ^ (x + 3) + 4 * ↑(defaultD a) ^ (-2) * ↑(defaultD a) ^ (x + 3) + 8⁻¹ * ↑(defaultD a) ^ (-3) * ↑(defaultD a) ^ (x + 3) + 8 * ↑(defaultD a) ^ y < 10 * ↑(defaultD a) ^ y

theorem calculation_4 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s_1 s_2 s_3 : ℤ} {dist_a dist_b dist_c dist_d : ℝ} (lt_1 : dist_a < 100 * ↑(defaultD a) ^ (s_1 + 3)) (lt_2 : dist_b < 8 * ↑(defaultD a) ^ s_3) (lt_3 : dist_c < 8⁻¹ * ↑(defaultD a) ^ s_1) (lt_4 : dist_d < 4 * ↑(defaultD a) ^ s_2) (three : s_1 + 3 < s_3) (plusOne : s_2 = s_1 + 1) : dist_a + dist_d + dist_c + dist_b < 10 * ↑(defaultD a) ^ s_3

theorem calculation_logD_64 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] : Real.logb (↑(defaultD a)) 64 < 1

theorem calculation_5 {a : ℕ} {dist_1 dist_2 : ℝ} (h : dist_1 ≤ (2 ^ ↑a) ^ 6 * dist_2) : 2 ^ (-↑𝕔 * ↑a) * dist_1 ≤ 2 ^ (-(↑𝕔 - 6) * ↑a) * dist_2

theorem calculation_6 (a : ℕ) (s : ℤ) : ↑(defaultD a) ^ (s + 3) = ↑(defaultD a) ^ (s + 2) * ↑(defaultD a)

theorem calculation_7 (a : ℕ) (s : ℤ) : 100 * (↑(defaultD a) ^ (s + 2) * ↑(defaultD a)) = ↑(defaultA a) ^ (𝕔 * a) * (100 * ↑(defaultD a) ^ (s + 2))

theorem calculation_8 {a : ℕ} {dist_1 dist_2 : ℝ} (h : dist_1 * 2 ^ (↑𝕔 * ↑a) ≤ dist_2) : dist_1 ≤ 2 ^ (-↑𝕔 * ↑a) * dist_2

theorem calculation_9 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (h : 1 ≤ 2 ^ (-(↑𝕔 - 6) * ↑a)) : False

theorem calculation_11 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (s : ℤ) : 100 * ↑(defaultD a) ^ (s + 2) + 4 * ↑(defaultD a) ^ (s + 1) < 128 * ↑(defaultD a) ^ (s + 2)

theorem calculation_12 {a : ℕ} (s : ℝ) : 128 * ↑(defaultD a) ^ (s + 2) = 2 ^ (2 * 𝕔 * a ^ 2 + 4) * (8 * ↑(defaultD a) ^ s)

theorem calculation_13 {a : ℕ} : 2 ^ (2 * 𝕔 * a ^ 3 + 4 * a) = ↑(defaultA a) ^ (2 * 𝕔 * a ^ 2 + 4)

theorem calculation_14 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (n : ℕ) : 2 ^ (↑(defaultZ a) * ↑n / 2 - (2 * ↑𝕔 + 1) * ↑a ^ 3) ≤ 2 ^ (↑(defaultZ a) * ↑n / 2 - (2 * ↑𝕔 * ↑a ^ 3 + 4 * ↑a))

theorem calculation_15 {a : ℕ} {dist zon : ℝ} (h : 2 ^ zon ≤ 2 ^ (2 * 𝕔 * a ^ 3 + 4 * a) * dist) : 2 ^ (zon - (2 * ↑𝕔 * ↑a ^ 3 + 4 * ↑a)) ≤ dist

theorem calculation_16 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (s : ℤ) : 4 * ↑(defaultD a) ^ s < 100 * ↑(defaultD a) ^ (s + 1)

theorem calculation_7_7_4 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {n : ℕ} : 1 ≤ 2 ^ (defaultZ a * (n + 1)) - 4

theorem near_1_geometric_bound {t : ℝ} (ht : t ∈ Set.Icc 0 1) : (1 - 2 ^ (-t))⁻¹ ≤ 2 * (ENNReal.ofReal t)⁻¹

A bound on the sum of a geometric series whose ratio is close to 1.

theorem calculation_convexity_bound {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {n : ℕ} {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ∑ k ∈ Finset.range n, (↑(defaultD a) ^ (-t)) ^ k ≤ 2 * (ENNReal.ofReal t)⁻¹

theorem calculation_7_6_2 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {n : ℕ} : ∑ k ∈ Finset.range n, (↑(defaultD a) ^ (-(defaultκ a / 2))) ^ k ≤ 2 ^ (10 * a + 2)

theorem calculation_150 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] : ↑𝕔 * (3 / 2) * ↑a ^ 2 * defaultκ a ≤ 1

theorem sq_le_two_pow_of_four_le {a : ℕ} (a4 : 4 ≤ a) : a ^ 2 ≤ 2 ^ a

theorem calculation_6_1_6 {a : ℕ} (a4 : 4 ≤ a) : 8 * a ^ 4 ≤ 2 ^ (2 * a + 3)