internlm/Lean-Github huggingface dataset:
Theorem: log_ratio_mono
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
⊢ MonotoneOn (fun x => (x - 1).log / x.log) (Ici 2)
Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Ici _)
Proof state after:
case hf
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
⊢ ContinuousOn (fun x => (x - 1).log / x.log) (Ici 2)

case hf'
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
⊢ DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (interior (Ici 2))

case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
⊢ ∀ x ∈ interior (Ici 2), 0 ≤ deriv (fun x => (x - 1).log / x.log) x
Theorem: log_ratio_mono
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
Tactic:
intro x x2
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
⊢ HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
Theorem: log_ratio_mono
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
⊢ HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
Tactic:
have l0 : 0 < log x := Real.log_pos (by linarith)
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
l0 : 0 < x.log
⊢ HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
Theorem: log_ratio_mono
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
l0 : 0 < x.log
⊢ HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
Tactic:
refine HasDerivAt.div ?_ (Real.hasDerivAt_log (by positivity)) l0.ne'
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
l0 : 0 < x.log
⊢ HasDerivAt (fun x => (x - 1).log) (1 / (x - 1)) x
Theorem: log_ratio_mono
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
l0 : 0 < x.log
⊢ HasDerivAt (fun x => (x - 1).log) (1 / (x - 1)) x
Tactic:
exact HasDerivAt.log ((hasDerivAt_id _).sub_const _) (by linarith)
Proof state after:
no goals
Theorem: log_ratio_mono
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
⊢ 1 < x
Tactic:
linarith
Proof state after:
no goals
Theorem: log_ratio_mono
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
l0 : 0 < x.log
⊢ x ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: log_ratio_mono
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x2 : 2 ≤ x
l0 : 0 < x.log
⊢ x - 1 ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: log_ratio_mono
Proof state before:
case hf
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
⊢ ContinuousOn (fun x => (x - 1).log / x.log) (Ici 2)
Tactic:
exact d.continuousOn
Proof state after:
no goals
Theorem: log_ratio_mono
Proof state before:
case hf'
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
⊢ DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (interior (Ici 2))
Tactic:
exact d.mono interior_subset
Proof state after:
no goals
Theorem: log_ratio_mono
Proof state before:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
⊢ ∀ x ∈ interior (Ici 2), 0 ≤ deriv (fun x => (x - 1).log / x.log) x
Tactic:
intro x m
Proof state after:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : x ∈ interior (Ici 2)
⊢ 0 ≤ deriv (fun x => (x - 1).log / x.log) x
Theorem: log_ratio_mono
Proof state before:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : x ∈ interior (Ici 2)
⊢ 0 ≤ deriv (fun x => (x - 1).log / x.log) x
Tactic:
simp only [nonempty_Iio, interior_Ici', mem_Ioi] at m
Proof state after:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
⊢ 0 ≤ deriv (fun x => (x - 1).log / x.log) x
Theorem: log_ratio_mono
Proof state before:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
⊢ 0 ≤ deriv (fun x => (x - 1).log / x.log) x
Tactic:
have l0 : 0 < log x := Real.log_pos (by linarith)
Proof state after:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ deriv (fun x => (x - 1).log / x.log) x
Theorem: log_ratio_mono
Proof state before:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ deriv (fun x => (x - 1).log / x.log) x
Tactic:
simp only [(hd x m.le).deriv, one_div]
Proof state after:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ ((x - 1)⁻¹ * x.log - (x - 1).log * x⁻¹) / x.log ^ 2
Theorem: log_ratio_mono
Proof state before:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ ((x - 1)⁻¹ * x.log - (x - 1).log * x⁻¹) / x.log ^ 2
Tactic:
refine div_nonneg ?_ (by positivity)
Proof state after:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ (x - 1)⁻¹ * x.log - (x - 1).log * x⁻¹
Theorem: log_ratio_mono
Proof state before:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ (x - 1)⁻¹ * x.log - (x - 1).log * x⁻¹
Tactic:
simp only [sub_nonneg, mul_comm]
Proof state after:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ x⁻¹ * (x - 1).log ≤ (x - 1)⁻¹ * x.log
Theorem: log_ratio_mono
Proof state before:
case hf'_nonneg
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ x⁻¹ * (x - 1).log ≤ (x - 1)⁻¹ * x.log
Tactic:
apply mul_le_mul
Proof state after:
case hf'_nonneg.h₁
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ x⁻¹ ≤ (x - 1)⁻¹

case hf'_nonneg.h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ (x - 1).log ≤ x.log

case hf'_nonneg.c0
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ (x - 1).log

case hf'_nonneg.b0
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ (x - 1)⁻¹
Theorem: log_ratio_mono
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
⊢ 1 < x
Tactic:
linarith
Proof state after:
no goals
Theorem: log_ratio_mono
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ x.log ^ 2
Tactic:
positivity
Proof state after:
no goals
Theorem: log_ratio_mono
Proof state before:
case hf'_nonneg.h₁
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ x⁻¹ ≤ (x - 1)⁻¹
Tactic:
exact inv_le_inv_of_le (by linarith) (by linarith)
Proof state after:
no goals
Theorem: log_ratio_mono
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 < x - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: log_ratio_mono
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ x - 1 ≤ x
Tactic:
linarith
Proof state after:
no goals
Theorem: log_ratio_mono
Proof state before:
case hf'_nonneg.h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ (x - 1).log ≤ x.log
Tactic:
exact Real.log_le_log (by linarith) (by linarith)
Proof state after:
no goals
Theorem: log_ratio_mono
Proof state before:
case hf'_nonneg.c0
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ (x - 1).log
Tactic:
exact Real.log_nonneg (by linarith)
Proof state after:
no goals
Theorem: log_ratio_mono
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 1 ≤ x - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: log_ratio_mono
Proof state before:
case hf'_nonneg.b0
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ (x - 1)⁻¹
Tactic:
exact inv_nonneg.mpr (by linarith)
Proof state after:
no goals
Theorem: log_ratio_mono
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
x : ℝ
m : 2 < x
l0 : 0 < x.log
⊢ 0 ≤ x - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
zw : (Complex.abs z - 1) ^ 1 * Complex.abs z ≤ Complex.abs (f' d c z)
⊢ (Complex.abs z).log.log + 0.548 ≤ (Complex.abs (f' d c z)).log.log
Tactic:
generalize abs (f' d c z) = w at zw
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
w : ℝ
zw : (Complex.abs z - 1) ^ 1 * Complex.abs z ≤ w
⊢ (Complex.abs z).log.log + 0.548 ≤ w.log.log
Theorem: log_log_iter
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
w : ℝ
zw : (Complex.abs z - 1) ^ 1 * Complex.abs z ≤ w
⊢ (Complex.abs z).log.log + 0.548 ≤ w.log.log
Tactic:
generalize abs z = x at zw cz z4
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
cz : Complex.abs c ≤ x
z4 : 4 ≤ x
⊢ x.log.log + 0.548 ≤ w.log.log
Theorem: log_log_iter
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
cz : Complex.abs c ≤ x
z4 : 4 ≤ x
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
clear z c cz
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
z4 : 4 ≤ x
⊢ x.log.log + 0.548 ≤ w.log.log
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
z4 : 4 ≤ x
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
have x0 : 0 < x := by linarith
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
z4 : 4 ≤ x
x0 : 0 < x
⊢ x.log.log + 0.548 ≤ w.log.log
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
z4 : 4 ≤ x
x0 : 0 < x
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
have x1 : 1 < x := by linarith
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
⊢ x.log.log + 0.548 ≤ w.log.log
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
simp only [pow_one] at zw
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
⊢ x.log.log + 0.548 ≤ w.log.log
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
have lx1 : 1 < log (x-1) :=
  lt_trans (by norm_num) (lt_of_lt_of_le lt_log_3 (Real.log_le_log (by norm_num) (by linarith)))
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
⊢ x.log.log + 0.548 ≤ w.log.log
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
have lx : 1 < log x := lt_trans lx1 (Real.log_lt_log (by linarith) (by linarith))
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ x.log.log + 0.548 ≤ w.log.log
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
have ll0 : 0 ≤ log (x-1) / log x := by positivity
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
⊢ x.log.log + 0.548 ≤ w.log.log
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
have ll1 : log (x-1) / log x ≤ 1 :=
  div_le_one_of_le (Real.log_le_log (by linarith) (by linarith)) (by positivity)
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ x.log.log + 0.548 ≤ w.log.log
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ x.log.log + 0.548 ≤ w.log.log
Tactic:
calc log (log w)
  _ ≥ log (log ((x-1)*x)) := log_log_mono (by nlinarith) zw
  _ = log (log x + log (x-1)) := by rw [mul_comm, Real.log_mul (by positivity) (by linarith)]
  _ = log (log x) + log (1 + log (x-1) / log x) := by rw [log_add _ _ (by linarith) (by linarith)]
  _ ≥ log (log x) + log 2 * (log (x-1) / log x) := by bound [le_log_one_add ll0 ll1]
  _ ≥ log (log x) + 0.693 * 0.791 := by bound [lt_log_2]
  _ ≥ log (log x) + 0.548 := by bound
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (Complex.abs z - 1) ^ 1 * Complex.abs z ≤ Complex.abs (f' d c z)
Tactic:
refine iter_large (d := d) (n := 1) ?_ ?_ ?_ cz
Proof state after:
case refine_1
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 2 ≤ Complex.abs z

case refine_2
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Complex.abs z ≤ Complex.abs z
Theorem: log_log_iter
Proof state before:
case refine_1
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 2 ≤ Complex.abs z
Tactic:
linarith
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
case refine_2
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Complex.abs z ≤ Complex.abs z
Tactic:
exact le_refl _
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
z4 : 4 ≤ x
⊢ 0 < x
Tactic:
linarith
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
zw : (x - 1) ^ 1 * x ≤ w
z4 : 4 ≤ x
x0 : 0 < x
⊢ 1 < x
Tactic:
linarith
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
⊢ 1 < 1.098
Tactic:
norm_num
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
⊢ 0 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
⊢ 3 ≤ x - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
⊢ 0 < x - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
⊢ x - 1 < x
Tactic:
linarith
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ (x - 1).log / x.log ≥ (4 - 1).log / log 4
Tactic:
apply log_ratio_mono ?_ ?_ z4
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 4 ∈ Ici 2

c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ x ∈ Ici 2
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 4 ∈ Ici 2
Tactic:
simp only [mem_Ici]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 2 ≤ 4
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 2 ≤ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ x ∈ Ici 2
Tactic:
simp only [mem_Ici]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 2 ≤ x
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 2 ≤ x
Tactic:
linarith
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ (4 - 1).log / log 4 = log 3 / log 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 0 ≤ log 3
Tactic:
positivity
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 0 < log 4
Tactic:
positivity
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
⊢ 1.098 / 1.387 ≥ 0.791
Tactic:
norm_num
Proof state after:
no goals