-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
protected lemma GrowsPolynomially.mul {f g : ℝ → ℝ} (hf : GrowsPolynomially f)
    (hg : GrowsPolynomially g) : GrowsPolynomially fun x => f x * g x

Proof state:
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hg✝ : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x|) u ∈ Set.Icc (c₁ * (fun x => |f x|) x) (c₂ * (fun x => |f x|) x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => |g x|) u ∈ Set.Icc (c₃ * (fun x => |g x|) x) (c₄ * (fun x => |g x|) x)
⊢ c₁ * c₃ > 0

Tactic:
show 0 < c₁ * c₃

Result:
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hg✝ : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x|) u ∈ Set.Icc (c₁ * (fun x => |f x|) x) (c₂ * (fun x => |f x|) x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => |g x|) u ∈ Set.Icc (c₃ * (fun x => |g x|) x) (c₄ * (fun x => |g x|) x)
⊢ 0 < c₁ * c₃

Proof state:
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hg✝ : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x|) u ∈ Set.Icc (c₁ * (fun x => |f x|) x) (c₂ * (fun x => |f x|) x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => |g x|) u ∈ Set.Icc (c₃ * (fun x => |g x|) x) (c₄ * (fun x => |g x|) x)
⊢ 0 < c₁ * c₃

Tactic:
positivity

Result:
no goals

Proof state:
case inr.inl
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x => |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x|
⊢ GrowsPolynomially fun x => -(|f x| * |g x|)

Tactic:
exact this.neg

Result:
no goals

Proof state:
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hg✝ : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x|) u ∈ Set.Icc (c₁ * (fun x => |f x|) x) (c₂ * (fun x => |f x|) x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => |g x|) u ∈ Set.Icc (c₃ * (fun x => |g x|) x) (c₄ * (fun x => |g x|) x)
⊢ c₂ * c₄ > 0

Tactic:
show 0 < c₂ * c₄

Result:
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hg✝ : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x|) u ∈ Set.Icc (c₁ * (fun x => |f x|) x) (c₂ * (fun x => |f x|) x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => |g x|) u ∈ Set.Icc (c₃ * (fun x => |g x|) x) (c₄ * (fun x => |g x|) x)
⊢ 0 < c₂ * c₄

Proof state:
case inl
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x => |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x => f x * g x

Tactic:
cases eventually_atTop_nonneg_or_nonpos hg with
| inl hg' =>
  have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by
    filter_upwards [hf', hg'] with x hx₁ hx₂
    rw [abs_of_nonneg hx₁, abs_of_nonneg hx₂]
  rwa [iff_eventuallyEq hmain]
| inr hg' =>
  have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
    filter_upwards [hf', hg'] with x hx₁ hx₂
    simp [abs_of_nonneg hx₁, abs_of_nonpos hx₂]
  simp only [iff_eventuallyEq hmain, neg_mul]
  exact this.neg

Result:
no goals

Proof state:
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hg : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf :
  ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x|) u ∈ Set.Icc (c₁ * (fun x => |f x|) x) (c₂ * (fun x => |f x|) x)
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun x => |f x| * |g x|) u ∈ Set.Icc (c₁ * (fun x => |f x| * |g x|) x) (c₂ * (fun x => |f x| * |g x|) x)

Tactic:
have hg := hg.abs b hb

Result:
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hg✝ : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf :
  ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x|) u ∈ Set.Icc (c₁ * (fun x => |f x|) x) (c₂ * (fun x => |f x|) x)
hg :
  ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x, (fun x => |g x|) u ∈ Set.Icc (c₁ * (fun x => |g x|) x) (c₂ * (fun x => |g x|) x)
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun x => |f x| * |g x|) u ∈ Set.Icc (c₁ * (fun x => |f x| * |g x|) x) (c₂ * (fun x => |f x| * |g x|) x)

Proof state:
case inr.inl
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x => |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
⊢ GrowsPolynomially fun x => f x * g x

Tactic:
have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
  filter_upwards [hf', hg'] with x hx₁ hx₂
  rw [abs_of_nonpos hx₁, abs_of_nonneg hx₂, neg_neg]

Result:
case inr.inl
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x => |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x|
⊢ GrowsPolynomially fun x => f x * g x

Proof state:
case h
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x => |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
x : ℝ
hx₁ : f x ≤ 0
hx₂ : g x ≤ 0
⊢ f x * g x = |f x| * |g x|

Tactic:
simp [abs_of_nonpos hx₁, abs_of_nonpos hx₂]

Result:
no goals

Proof state:
case h₁
f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf✝ :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x|) u ∈ Set.Icc (c₁ * (fun x => |f x|) x) (c₂ * (fun x => |f x|) x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg✝ :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => |g x|) u ∈ Set.Icc (c₃ * (fun x => |g x|) x) (c₄ * (fun x => |g x|) x)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ c₁ * |f x| ≤ |f u|

Tactic:
exact (hf u hu).1

Result:
no goals

Proof state:
case inr
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x => |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ GrowsPolynomially fun x => f x * g x

Tactic:
cases eventually_atTop_nonneg_or_nonpos hg with
| inl hg' =>
  have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
    filter_upwards [hf', hg'] with x hx₁ hx₂
    rw [abs_of_nonpos hx₁, abs_of_nonneg hx₂, neg_neg]
  simp only [iff_eventuallyEq hmain, neg_mul]
  exact this.neg
| inr hg' =>
  have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by
    filter_upwards [hf', hg'] with x hx₁ hx₂
    simp [abs_of_nonpos hx₁, abs_of_nonpos hx₂]
  simp only [iff_eventuallyEq hmain, neg_mul]
  exact this

Result:
no goals