noncomputable def AriMagic.v_def (i : ℝ) : ℝ

Equations

• AriMagic.v_def i = (1 + i)⁻¹

noncomputable def AriMagic.f (i d r n : ℝ) : ℝ

Equations

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

noncomputable def AriMagic.S (i r : ℝ) : ℝ

Equations

• AriMagic.S i r = r / i - 1

noncomputable def AriMagic.K (i d r : ℝ) : ℝ

Equations

• AriMagic.K i d r = d * (1 - r / i) + r / (i ^ 2 * AriMagic.v_def i)

noncomputable def AriMagic.C (i d r : ℝ) : ℝ

Equations

• AriMagic.C i d r = d * r / i - r / (i ^ 2 * AriMagic.v_def i)

noncomputable def AriMagic.L (i : ℝ) : ℝ

Equations

• AriMagic.L i = Real.log (AriMagic.v_def i)

theorem AriMagic.f_eq_simplified (i d r n : ℝ) (hi : i ≠ 0) (hv : v_def i ≠ 0) : f i d r n = C i d r + v_def i ^ n * (S i r * n + K i d r)

theorem AriMagic.C_neg (i d r : ℝ) (hi : i ≠ 0) (hr : 0 < r) (hdi : d * i < 1 + i) : C i d r < 0

After some work I removed the assumption i>0 here.

theorem AriMagic.C_nonpos (i d r : ℝ) (hi : i ≠ 0) (hr : 0 < r) (hdi : d * i ≤ 1 + i) : C i d r ≤ 0

By Bjørn.

noncomputable def AriMagic.g (i d r n : ℝ) : ℝ

Equations

• AriMagic.g i d r n = AriMagic.S i r * Real.log (AriMagic.v_def i) * n + AriMagic.K i d r * Real.log (AriMagic.v_def i) + AriMagic.S i r

theorem AriMagic.f_deriv (i d r n : ℝ) (hi : i ≠ 0) (hi' : 1 + i > 0) : HasDerivAt (f i d r) (v_def i ^ n * g i d r n) n

theorem AriMagic.f_tendsto_atTop (i d r : ℝ) (hi : 0 < i) : Filter.Tendsto (f i d r) Filter.atTop (nhds (C i d r))

theorem AriMagic.f_continuous (i d r : ℝ) (hi : 0 < i) : ContinuousOn (f i d r) (Set.Ici 0)

theorem AriMagic.g_at_most_one_root (i d r : ℝ) (hi : 0 < i) (hr : 0 < r) : {n : ℝ | g i d r n = 0}.Subsingleton

theorem AriMagic.exists_pos_root_of_limits {f : ℝ → ℝ} {L : ℝ} (hcont : ContinuousOn f (Set.Ici 0)) (h0 : 0 < f 0) (hlim : Filter.Tendsto f Filter.atTop (nhds L)) (hL : L < 0) : ∃ x > 0, f x = 0

theorem AriMagic.injOn_of_deriv_ne_zero {f : ℝ → ℝ} {I : Set ℝ} (h_conv : Convex ℝ I) (h_diff : DifferentiableOn ℝ f I) (h_deriv : ∀ x ∈ I, deriv f x ≠ 0) : Set.InjOn f I

theorem AriMagic.injOn_of_deriv_ne_zero_Icc {f : ℝ → ℝ} {a b : ℝ} (hcont : ContinuousOn f (Set.Icc a b)) (hderiv : ∀ x ∈ Set.Ioo a b, deriv f x ≠ 0) : Set.InjOn f (Set.Icc a b)

theorem AriMagic.injOn_Ici_of_deriv_ne_zero {f : ℝ → ℝ} {a : ℝ} (hcont : ContinuousOn f (Set.Ici a)) (hderiv : ∀ x ∈ Set.Ioi a, deriv f x ≠ 0) : Set.InjOn f (Set.Ici a)

theorem AriMagic.root_between_implies_end_sign_Icc {f : ℝ → ℝ} {u v r : ℝ} (huv : u < v) (hr : r ∈ Set.Ioo u v) (hcont : ContinuousOn f (Set.Icc u v)) (hderiv : ∀ x ∈ Set.Ioo u v, deriv f x ≠ 0) (hu : 0 < f u) (hr_root : f r = 0) : f v < 0

theorem AriMagic.root_between_implies_end_sign_Icc₀ {f : ℝ → ℝ} {u v r : ℝ} (huv : u < v) (hr : r ∈ Set.Ioo u v) (hcont : ContinuousOn f (Set.Icc u v)) (hderiv : ∀ x ∈ Set.Ioo u v, deriv f x ≠ 0) (hu : 0 ≤ f u) (hr_root : f r = 0) : f v < 0

By Bjørn.

theorem AriMagic.root_implies_limit_ge_zero {f : ℝ → ℝ} {c r L : ℝ} (hcr : c < r) (hcont : ContinuousOn f (Set.Ici c)) (hdiff : DifferentiableOn ℝ f (Set.Ioi c)) (hderiv : ∀ x ∈ Set.Ioi c, deriv f x ≠ 0) (hc : f c < 0) (hr : f r = 0) (hlim : Filter.Tendsto f Filter.atTop (nhds L)) : L ≥ 0

theorem AriMagic.at_most_one_root_of_single_critical_point {f f' : ℝ → ℝ} {L : ℝ} (hcont : ContinuousOn f (Set.Ici 0)) (hderiv : ∀ x ∈ Set.Ioi 0, HasDerivAt f (f' x) x) (h0 : 0 < f 0) (hlim : Filter.Tendsto f Filter.atTop (nhds L)) (hL : L < 0) (hcrit : {x : ℝ | 0 < x ∧ f' x = 0}.Subsingleton) : {x : ℝ | 0 < x ∧ f x = 0}.Subsingleton

theorem AriMagic.at_most_one_root_of_single_critical_point₀ {f f' : ℝ → ℝ} {L : ℝ} (hcont : ContinuousOn f (Set.Ici 0)) (hderiv : ∀ x ∈ Set.Ioi 0, HasDerivAt f (f' x) x) (h0 : 0 ≤ f 0) (hlim : Filter.Tendsto f Filter.atTop (nhds L)) (hL : L < 0) (hcrit : {x : ℝ | 0 < x ∧ f' x = 0}.Subsingleton) : {x : ℝ | 0 < x ∧ f x = 0}.Subsingleton

By Bjørn.

theorem AriMagic.at_most_one_root_of_single_critical_point₀₀ {f f' : ℝ → ℝ} {L : ℝ} (hcont : ContinuousOn f (Set.Ici 0)) (hderiv : ∀ x ∈ Set.Ioi 0, HasDerivAt f (f' x) x) (h0 : 0 ≤ f 0) (hlim : Filter.Tendsto f Filter.atTop (nhds L)) (hL : L ≤ 0) (hcrit : {x : ℝ | 0 < x ∧ f' x = 0}.Subsingleton) : {x : ℝ | 0 < x ∧ f x = 0}.Subsingleton

By Bjørn.

theorem AriMagic.unique_solution_n {i d r : ℝ} (hd : 0 < d) (hi : 0 < i) (hr : 0 < r) (hdi : d < 1 + 1 / i) : ∃! n : ℝ, 0 < n ∧ have v := (1 + i)⁻¹; d * (r * ((1 - v ^ n) / i) + v ^ n) - (r * (v * (n * v ^ (n + 1) - (n + 1) * v ^ n + 1) / (v - 1) ^ 2) + n * v ^ n) = 0

theorem AriMagic.unique_solution_n₀ {i d r : ℝ} (hd : 0 < d) (hi : 0 < i) (hr : 0 < r) (hdi : d ≤ 1 + 1 / i) (h : ∃ (n : ℝ), 0 < n ∧ have v := (1 + i)⁻¹; d * (r * ((1 - v ^ n) / i) + v ^ n) - (r * (v * (n * v ^ (n + 1) - (n + 1) * v ^ n + 1) / (v - 1) ^ 2) + n * v ^ n) = 0) : ∃! n : ℝ, 0 < n ∧ have v := (1 + i)⁻¹; d * (r * ((1 - v ^ n) / i) + v ^ n) - (r * (v * (n * v ^ (n + 1) - (n + 1) * v ^ n + 1) / (v - 1) ^ 2) + n * v ^ n) = 0

By Bjørn. If d=1+1/i and if there is one solution, then it is unique.