trans_eventuallyLE — Mathlib

English

If k is eventually nonnegative along l, and g,g' decay along l, and g ≤ᶠ[l] f ≤ᶠ[l] g', then f decays along l with k.

Русский

Если k неотрицательно почти наверняка вдоль l, и g,g' затухают вдоль l, и g ≤ f ≤ g' почти наверняка вдоль l, то f затухает вдоль l по k.

LaTeX

$$$(0 \le^\!l k) \wedge \mathrm{SuperpolynomialDecay}(l,k,g) \wedge \mathrm{SuperpolynomialDecay}(l,k,g') \wedge (g \le^\!l f) \wedge (f \le^\!l g') \Rightarrow \mathrm{SuperpolynomialDecay}(l,k,f)$$$

Lean4

theorem trans_eventuallyLE (hk : 0 ≤ᶠ[l] k) (hg : SuperpolynomialDecay l k g) (hg' : SuperpolynomialDecay l k g')
    (hfg : g ≤ᶠ[l] f) (hfg' : f ≤ᶠ[l] g') : SuperpolynomialDecay l k f := fun z =>
  tendsto_of_tendsto_of_tendsto_of_le_of_le' (hg z) (hg' z)
    (by filter_upwards [hfg, hk] with x hx (hx' : 0 ≤ k x) using by gcongr)
    (by filter_upwards [hfg', hk] with x hx (hx' : 0 ≤ k x) using by gcongr)

Похожие утверждения