-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
lemma growsPolynomially_log : GrowsPolynomially Real.log

Proof state:
⊢ GrowsPolynomially log

Tactic:
intro b hb

Result:
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (c₁ * log x) (c₂ * log x)

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ x ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ 1 * x = x

Tactic:
rw [one_mul]

Result:
no goals

Proof state:
case lb
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ 1 / 2 * log x ≤ log u

case ub
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ log u ≤ 1 * log x

Tactic:
case lb => calc
  1 / 2 * Real.log x = Real.log x + (-1 / 2) * Real.log x := by ring
    _ ≤ Real.log x + Real.log b := by
            gcongr
            rw [neg_div, neg_mul, ← neg_le]
            refine le_of_lt (hx x ?_)
            calc b * x ≤ 1 * x := by gcongr; exact le_of_lt hb.2
                     _ = x := by rw [one_mul]
    _ = Real.log (b * x) := by rw [← Real.log_mul (by positivity) (by positivity), mul_comm]
    _ ≤ Real.log u := by gcongr; exact hu.1

Result:
case ub
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ log u ≤ 1 * log x

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
⊢ 0 < 1 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b * x ≤ 1 * x

Tactic:
gcongr

Result:
case h
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b ≤ 1

Proof state:
case bc
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ -1 / 2 * log x ≤ log b

Tactic:
rw [neg_div, neg_mul, ← neg_le]

Result:
case bc
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ -log b ≤ 1 / 2 * log x

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ log x + log b = log (b * x)

Tactic:
rw [← Real.log_mul (by positivity) (by positivity), mul_comm]

Result:
no goals

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ log (b * x) ≤ log u

Tactic:
gcongr

Result:
case hxy
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b * x ≤ u

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (c₁ * log x) (c₂ * log x)

Tactic:
have hb₀ : 0 < b := hb.1

Result:
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (c₁ * log x) (c₂ * log x)

Proof state:
case hxy
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ u ≤ x

Tactic:
exact hu.2

Result:
no goals

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
⊢ ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (1 / 2 * log x) (c₂ * log x)

Tactic:
refine ⟨1, by norm_num, ?_⟩

Result:
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (1 / 2 * log x) (1 * log x)

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
⊢ 1 > 0

Tactic:
norm_num

Result:
no goals

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ 1 / 2 * log x ≤ log u

Tactic:
calc
1 / 2 * Real.log x = Real.log x + (-1 / 2) * Real.log x := by ring
_ ≤ Real.log x + Real.log b := by
 gcongr
 rw [neg_div, neg_mul, ← neg_le]
 refine le_of_lt (hx x ?_)
 calc b * x ≤ 1 * x := by gcongr; exact le_of_lt hb.2
          _ = x := by rw [one_mul]
_ = Real.log (b * x) := by rw [← Real.log_mul (by positivity) (by positivity), mul_comm]
_ ≤ Real.log u := by gcongr; exact hu.1

Result:
no goals

Proof state:
case h
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
⊢ ∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (1 / 2 * log x) (1 * log x)

Tactic:
intro u hu

Result:
case h
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ log u ∈ Set.Icc (1 / 2 * log x) (1 * log x)

Proof state:
case hx
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ 0 < u

Tactic:
calc 0 < b * x := by positivity
   _ ≤ u := by exact hu.1

Result:
no goals

Proof state:
case h
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b ≤ 1

Tactic:
exact le_of_lt hb.2

Result:
no goals

Proof state:
case hxy
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b * x ≤ u

Tactic:
exact hu.1

Result:
no goals

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
⊢ 1 / 2 > 0

Tactic:
norm_num

Result:
no goals

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ 1 / 2 * log x = log x + -1 / 2 * log x

Tactic:
ring

Result:
no goals