English
If f and g grow polynomially, then their product f·g grows polynomially.
Русский
Если f и g растут полиномиально, то их произведение растёт полиномиально.
LaTeX
$$$\\text{GrowsPolynomially}(f) \\to \\text{GrowsPolynomially}(g) \\to \\text{GrowsPolynomially}(x \\mapsto f(x)\\,g(x))$$$
Lean4
protected theorem mul {f g : ℝ → ℝ} (hf : GrowsPolynomially f) (hg : GrowsPolynomially g) :
GrowsPolynomially fun x => f x * g x :=
by
suffices GrowsPolynomially fun x => |f x| * |g x| by
cases eventually_atTop_nonneg_or_nonpos hf with
| inl hf' =>
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
| inr hf' =>
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]
exact this
intro b hb
have hf := hf.abs b hb
have hg := hg.abs b hb
obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf
obtain ⟨c₃, hc₃_mem, c₄, hc₄_mem, hg⟩ := hg
refine ⟨c₁ * c₃, by change 0 < c₁ * c₃; positivity, ?_⟩
refine ⟨c₂ * c₄, by change 0 < c₂ * c₄; positivity, ?_⟩
filter_upwards [hf, hg] with x hf hg
intro u hu
refine ⟨?lb, ?ub⟩
case lb =>
calc
c₁ * c₃ * (|f x| * |g x|) = (c₁ * |f x|) * (c₃ * |g x|) := by ring
_ ≤ |f u| * |g u| := by
gcongr
· exact (hf u hu).1
· exact (hg u hu).1
case ub =>
calc
|f u| * |g u| ≤ (c₂ * |f x|) * (c₄ * |g x|) := by
gcongr
· exact (hf u hu).2
· exact (hg u hu).2
_ = c₂ * c₄ * (|f x| * |g x|) := by ring
