-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
lemma eventually_atTop_nonneg_or_nonpos (hf : GrowsPolynomially f) :
    (∀ᶠ x in atTop, 0 ≤ f x) ∨ (∀ᶠ x in atTop, f x ≤ 0)

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ 1 < 2

Tactic:
norm_num

Result:
no goals

Proof state:
case h
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
heq : c₁ = c₂
c : ℝ
hc✝ : ∀ᶠ (x : ℝ) in atTop, f x = c
hpos : 0 ≤ c
a✝ : ℝ
hc : f a✝ = c
⊢ 0 ≤ f a✝

Tactic:
simpa only [hc]

Result:
no goals

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
n : ℕ
hn : n ≥ 1
hyp_ind : ∀ z ∈ Set.Ico (n₀ ⊔ 2) (2 ^ n * (n₀ ⊔ 2)), f z = f (n₀ ⊔ 2)
z : ℝ
hz : z ∈ Set.Ico (2 ^ n * (n₀ ⊔ 2)) (2 ^ (n + 1) * (n₀ ⊔ 2))
⊢ 0 ≤ 2

Tactic:
norm_num

Result:
no goals

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
n : ℕ
hn : n ≥ 1
hyp_ind : ∀ z ∈ Set.Ico (n₀ ⊔ 2) (2 ^ n * (n₀ ⊔ 2)), f z = f (n₀ ⊔ 2)
z : ℝ
hz : z ∈ Set.Ico (2 ^ n * (n₀ ⊔ 2)) (2 ^ (n + 1) * (n₀ ⊔ 2))
⊢ 0 ≤ z

Tactic:
calc (0 : ℝ) ≤ (2 : ℝ)^n * max n₀ 2 := by
              exact mul_nonneg (pow_nonneg (by norm_num) _) (by norm_num)
        _ ≤ z := by exact_mod_cast hz.1

Result:
no goals

Proof state:
case intro.inl
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
heq : c₁ = c₂
c : ℝ
hc : ∀ᶠ (x : ℝ) in atTop, f x = c
hpos : 0 ≤ c
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
exact Or.inl <| by filter_upwards [hc] with _ hc; simpa only [hc]

Result:
no goals

Proof state:
case h
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
⊢ 1 / 2 ≤ 3 / 4

Tactic:
norm_num

Result:
no goals

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
x : ℝ
hxlb : n₀ ⊔ 2 ≤ x
hxub : x < 2 * (n₀ ⊔ 2)
⊢ 1 * (n₀ ⊔ 2) ≤ 2 * (n₀ ⊔ 2)

Tactic:
gcongr

Result:
case h
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
x : ℝ
hxlb : n₀ ⊔ 2 ≤ x
hxub : x < 2 * (n₀ ⊔ 2)
⊢ 1 ≤ 2

Proof state:
case h
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
⊢ f x ≤ 0

Tactic:
have hu := hx (3/4 * x) h'

Result:
case h
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ f x ≤ 0

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
n : ℕ
hn : n ≥ 1
hyp_ind : ∀ z ∈ Set.Ico (n₀ ⊔ 2) (2 ^ n * (n₀ ⊔ 2)), f z = f (n₀ ⊔ 2)
z : ℝ
hz : z ∈ Set.Ico (2 ^ n * (n₀ ⊔ 2)) (2 ^ (n + 1) * (n₀ ⊔ 2))
z_nonneg : 0 ≤ z
le_2n : n₀ ⊔ 2 ≤ 2 ^ n * (n₀ ⊔ 2)
n₀_le_z : n₀ ≤ z
fz_eq_c₂fz : f z = c₂ * f z
z_to_half_z' : f (1 / 2 * z) = c₂ * f z
z_to_half_z : f (1 / 2 * z) = f z
⊢ n₀ ⊔ 2 ≤ 1 / 2 * z

Tactic:
calc max n₀ 2 ≤ ((1 : ℝ)/(2 : ℝ)) * (2 : ℝ) ^ 1 * max n₀ 2 := by simp
            _ ≤ ((1 : ℝ)/(2 : ℝ)) * (2 : ℝ) ^ n * max n₀ 2 := by gcongr; norm_num
            _ ≤ _ := by rw [mul_assoc]; gcongr; exact_mod_cast hz.1

Result:
no goals

Proof state:
case h
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
filter_upwards [h, eventually_ge_atTop 0] with x hx hx_nonneg

Result:
case h
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
⊢ f x ≤ 0

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
x : ℝ
hxlb : n₀ ⊔ 2 ≤ x
hxub : x < 2 * (n₀ ⊔ 2)
h₁ : n₀ ≤ 2 * (n₀ ⊔ 2)
h₂ : f (n₀ ⊔ 2) = c₂ * f (2 * (n₀ ⊔ 2))
⊢ 1 / 2 * (2 * (n₀ ⊔ 2)) ≤ x

Tactic:
simp [hxlb]

Result:
no goals

Proof state:
case h
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
heq : c₁ = c₂
c : ℝ
hc✝ : ∀ᶠ (x : ℝ) in atTop, f x = c
hneg : c < 0
x : ℝ
hc : f x = c
⊢ f x ≤ 0

Tactic:
exact le_of_lt <| by simpa only [hc]

Result:
no goals

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
n : ℕ
hn : n ≥ 1
hyp_ind : ∀ z ∈ Set.Ico (n₀ ⊔ 2) (2 ^ n * (n₀ ⊔ 2)), f z = f (n₀ ⊔ 2)
z : ℝ
hz : z ∈ Set.Ico (2 ^ n * (n₀ ⊔ 2)) (2 ^ (n + 1) * (n₀ ⊔ 2))
z_nonneg : 0 ≤ z
le_2n : n₀ ⊔ 2 ≤ 2 ^ n * (n₀ ⊔ 2)
n₀_le_z : n₀ ≤ z
fz_eq_c₂fz : f z = c₂ * f z
z_to_half_z' : f (1 / 2 * z) = c₂ * f z
z_to_half_z : f (1 / 2 * z) = f z
⊢ 2 ^ n = 1 / 2 * 2 ^ (n + 1)

Tactic:
rw [one_div, pow_add, pow_one]

Result:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
n : ℕ
hn : n ≥ 1
hyp_ind : ∀ z ∈ Set.Ico (n₀ ⊔ 2) (2 ^ n * (n₀ ⊔ 2)), f z = f (n₀ ⊔ 2)
z : ℝ
hz : z ∈ Set.Ico (2 ^ n * (n₀ ⊔ 2)) (2 ^ (n + 1) * (n₀ ⊔ 2))
z_nonneg : 0 ≤ z
le_2n : n₀ ⊔ 2 ≤ 2 ^ n * (n₀ ⊔ 2)
n₀_le_z : n₀ ≤ z
fz_eq_c₂fz : f z = c₂ * f z
z_to_half_z' : f (1 / 2 * z) = c₂ * f z
z_to_half_z : f (1 / 2 * z) = f z
⊢ 2 ^ n = 2⁻¹ * (2 ^ n * 2)

Proof state:
case intro.inr.h
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
heq : c₁ = c₂
c : ℝ
hc : ∀ᶠ (x : ℝ) in atTop, f x = c
hneg : c < 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
filter_upwards [hc] with x hc

Result:
case h
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
heq : c₁ = c₂
c : ℝ
hc✝ : ∀ᶠ (x : ℝ) in atTop, f x = c
hneg : c < 0
x : ℝ
hc : f x = c
⊢ f x ≤ 0

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
n : ℕ
hn : n ≥ 1
hyp_ind : ∀ z ∈ Set.Ico (n₀ ⊔ 2) (2 ^ n * (n₀ ⊔ 2)), f z = f (n₀ ⊔ 2)
z : ℝ
hz : z ∈ Set.Ico (2 ^ n * (n₀ ⊔ 2)) (2 ^ (n + 1) * (n₀ ⊔ 2))
z_nonneg : 0 ≤ z
le_2n : n₀ ⊔ 2 ≤ 2 ^ n * (n₀ ⊔ 2)
n₀_le_z : n₀ ≤ z
⊢ 1 / 2 * z ≤ z

Tactic:
linarith

Result:
no goals