Majorized predicate

This file defines the Majorized predicate, along with a few basic lemmas.

Main definitions

• Majorized f b exp means that f =o[atTop] (b ^ exp') for any exp' > exp. Intuitively, this means that the right order of f in terms of b is at most b ^ exp. This predicate is used in the definition of the MultiseriesExpansion.Approximates predicate.

def Tactic.ComputeAsymptotics.Majorized (f b : ℝ → ℝ) (exp : ℝ) : Prop

Majorized f g exp for real functions f and g means that for any exp' > exp, f =o[atTop] g ^ exp'. This is used to define the MultiseriesExpansion.Approximates predicate. The naming Majorized is non-standard because this notion is invented for the purposes of this tactic, and does not exists in literature.

theorem Tactic.ComputeAsymptotics.Majorized.of_eventuallyEq {f g b : ℝ → ℝ} {exp : ℝ} (h_eq : g =ᶠ[Filter.atTop] f) (h : Majorized f b exp) : Majorized g b exp

Replacing the first argument of Majorized by an eventually equal function preserves it.

theorem Tactic.ComputeAsymptotics.Majorized.self {f : ℝ → ℝ} {exp : ℝ} (h : Filter.Tendsto f Filter.atTop Filter.atTop) : Majorized (f ^ exp) f exp

For any function f tending to infinity, f ^ exp is majorized by f with exponent exp.

theorem Tactic.ComputeAsymptotics.Majorized.of_le {f b : ℝ → ℝ} {exp1 exp2 : ℝ} (h_lt : exp1 ≤ exp2) (h : Majorized f b exp1) : Majorized f b exp2

If f is majorized with exponent exp₁, then it is majorized with any exp₂ ≥ exp₁.

theorem Tactic.ComputeAsymptotics.Majorized.tendsto_zero_of_neg {f b : ℝ → ℝ} {exp : ℝ} (h_lt : exp < 0) (h : Majorized f b exp) : Filter.Tendsto f Filter.atTop (nhds 0)

If f is majorized with a negative exponent, then it tends to zero.

theorem Tactic.ComputeAsymptotics.Majorized.const {b : ℝ → ℝ} (h_tendsto : Filter.Tendsto b Filter.atTop Filter.atTop) {c : ℝ} : Majorized (fun (x : ℝ) => c) b 0

Constants are majorized with exponent exp = 0 by any functions which tends to infinity.

theorem Tactic.ComputeAsymptotics.Majorized.zero {b : ℝ → ℝ} {exp : ℝ} : Majorized 0 b exp

The zero function is majorized with any exponent.

theorem Tactic.ComputeAsymptotics.Majorized.smul {f b : ℝ → ℝ} {exp : ℝ} (h : Majorized f b exp) {c : ℝ} : Majorized (c • f) b exp

c • f is majorized with the same exponent as f for any constant c.

theorem Tactic.ComputeAsymptotics.Majorized.add {f g b : ℝ → ℝ} {exp f_exp g_exp : ℝ} (hf : Majorized f b f_exp) (hg : Majorized g b g_exp) (hf_exp : f_exp ≤ exp) (hg_exp : g_exp ≤ exp) : Majorized (f + g) b exp

The sum of two functions that are majorized with exponents f_exp and g_exp is majorized with exponent exp whenever exp ≥ max f_exp g_exp.

theorem Tactic.ComputeAsymptotics.Majorized.mul {f g b : ℝ → ℝ} {f_exp g_exp : ℝ} (hf : Majorized f b f_exp) (hg : Majorized g b g_exp) (h_pos : ∀ᶠ (t : ℝ) in Filter.atTop, 0 < b t) : Majorized (f * g) b (f_exp + g_exp)

The product of two functions that are majorized with exponents f_exp and g_exp is majorized with exponent f_exp + g_exp.

theorem Tactic.ComputeAsymptotics.Majorized.mul_bounded {f g basis_hd : ℝ → ℝ} {exp : ℝ} (hf : Majorized f basis_hd exp) (hg : g =O[Filter.atTop] fun (x : ℝ) => 1) : Majorized (f * g) basis_hd exp