noncomputable def f (n : ℕ) (d r v : ℝ) : ℝ

Equations

• f n d r v = d * (r * ∑ k ∈ Finset.Icc 1 n, v ^ k + v ^ n) - (r * ∑ k ∈ Finset.Icc 1 n, ↑k * v ^ k + ↑n * v ^ n)

noncomputable def h (n : ℕ) (r v : ℝ) : ℝ

Equations

• h n r v = (r * ∑ k ∈ Finset.Icc 1 n, ↑k * v ^ k + ↑n * v ^ n) / (r * ∑ k ∈ Finset.Icc 1 n, v ^ k + v ^ n)

noncomputable def num_h (n : ℕ) (r v : ℝ) : ℝ

Equations

• num_h n r v = r * ∑ k ∈ Finset.Icc 1 n, ↑k * v ^ k + ↑n * v ^ n

noncomputable def den_h (n : ℕ) (r v : ℝ) : ℝ

Equations

• den_h n r v = r * ∑ k ∈ Finset.Icc 1 n, v ^ k + v ^ n

noncomputable def coeff (n : ℕ) (r : ℝ) (k : ℕ) : ℝ

Equations

• coeff n r k = if k = n then r + 1 else r

theorem h_eq_quotient (n : ℕ) (hn : n ≥ 1) (r v : ℝ) : h n r v = (∑ k ∈ Finset.Icc 1 n, coeff n r k * ↑k * v ^ k) / ∑ k ∈ Finset.Icc 1 n, coeff n r k * v ^ k

noncomputable def h_deriv_numerator_aux (n : ℕ) (r v : ℝ) : ℝ

Equations

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

theorem h_deriv_numerator_aux_pos (n : ℕ) (hn : n ≥ 2) (r v : ℝ) (hr : r > 0) (hv : v > 0) : h_deriv_numerator_aux n r v > 0

theorem den_h_pos (n : ℕ) (r v : ℝ) (hr : r > 0) (hv : v > 0) : den_h n r v > 0

theorem h_strict_mono (n : ℕ) (hn : n ≥ 2) (r : ℝ) (hr : r > 0) : StrictMonoOn (h n r) (Set.Ioi 0)

theorem h_tendsto_zero (n : ℕ) (hn : n ≥ 2) (r : ℝ) (hr : r > 0) : Filter.Tendsto (h n r) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)

theorem h_tendsto_atTop (n : ℕ) (hn : n ≥ 1) (r : ℝ) (hr : r > 0) : Filter.Tendsto (h n r) Filter.atTop (nhds ↑n)

theorem unique_root_f (n : ℕ) (hn : n ≥ 2) (d r : ℝ) (hd₀ : 1 < d) (hd₁ : d < ↑n) (hr : r > 0) : ∃! v : ℝ, 0 < v ∧ f n d r v = 0