Well-formed bases #

Main definitions #

WellFormedBasis basis: a predicate meaning that all functions from basis tend to atTop, and basis is sorted such that if g goes after f in basis, then log f =o[atTop] log g.

def Tactic.ComputeAsymptotics.WellFormedBasis (basis : Basis) :

WellFormedBasis basis means that all functions from basis tend to atTop, and basis is sorted such that if g goes after f in basis, then log f =o[atTop] log g.

We use two types Basis and WellFormedBasis instead of a single bundled one because it it lets us to use the List API for Basis.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.nil :

WellFormedBasis []

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.single (f : ℝ → ℝ) (hf : Filter.Tendsto f Filter.atTop Filter.atTop) :

WellFormedBasis [f]

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.of_sublist {basis basis' : Basis} (h : List.Sublist basis basis') (h_basis : WellFormedBasis basis') :

WellFormedBasis basis

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.tail {basis_hd : ℝ → ℝ} {basis_tl : Basis} (h : WellFormedBasis (basis_hd :: basis_tl)) :

WellFormedBasis basis_tl

The tail of a well-formed basis is well-formed.

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.of_append_right {left right : Basis} (h : WellFormedBasis (left ++ right)) :

WellFormedBasis right

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.compare_left_aux {basis : Basis} {f : ℝ → ℝ} (h : WellFormedBasis basis) (h_comp : ∀ (g : ℝ → ℝ), List.getLast? basis = some g → (Real.log ∘ f) =o[Filter.atTop ] (Real.log ∘ g)) (g : ℝ → ℝ) :

g ∈ basis → (Real.log ∘ f) =o[Filter.atTop ] (Real.log ∘ g)

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.compare_right_aux {basis : Basis} {f : ℝ → ℝ} (h : WellFormedBasis basis) (h_comp : ∀ (g : ℝ → ℝ), List.head? basis = some g → (Real.log ∘ g) =o[Filter.atTop ] (Real.log ∘ f)) (g : ℝ → ℝ) :

g ∈ basis → (Real.log ∘ g) =o[Filter.atTop ] (Real.log ∘ f)

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.append {left right : Basis} (h_left : WellFormedBasis left) (h_right : WellFormedBasis right) (h : ∀ f ∈ left, ∀ g ∈ right, (Real.log ∘ g) =o[Filter.atTop ] (Real.log ∘ f)) :

WellFormedBasis (left ++ right)

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.cons {basis : Basis} {f : ℝ → ℝ} (h_basis : WellFormedBasis basis) (hf_tendsto : Filter.Tendsto f Filter.atTop Filter.atTop) (hf : ∀ g ∈ basis, (Real.log ∘ g) =o[Filter.atTop ] (Real.log ∘ f)) :

WellFormedBasis (f :: basis)

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.insert {left right : Basis} {f : ℝ → ℝ} (h : WellFormedBasis (left ++ right)) (hf_tendsto : Filter.Tendsto f Filter.atTop Filter.atTop) (hf_comp_left : ∀ (g : ℝ → ℝ), List.getLast? left = some g → (Real.log ∘ f) =o[Filter.atTop ] (Real.log ∘ g)) (hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[Filter.atTop ] (Real.log ∘ f)) :

WellFormedBasis (left ++ f :: right)

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.push {basis : Basis} {f : ℝ → ℝ} (h : WellFormedBasis basis) (hf_tendsto : Filter.Tendsto f Filter.atTop Filter.atTop) (hf_comp : ∀ (g : ℝ → ℝ), List.getLast? basis = some g → (Real.log ∘ f) =o[Filter.atTop ] (Real.log ∘ g)) :

WellFormedBasis (basis ++ [f])

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.tendsto_atTop {basis : Basis} (h : WellFormedBasis basis) {f : ℝ → ℝ} (hf : f ∈ basis) :

Filter.Tendsto f Filter.atTop Filter.atTop

All functions from a well-formed basis tend to atTop.

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.eventually_pos {basis : Basis} (h : WellFormedBasis basis) :

∀ᶠ (x : ℝ) in Filter.atTop , ∀ f ∈ basis, 0 < f x

Eventually all functions from a well-formed basis are positive.

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.head_eventually_pos {basis_hd : ℝ → ℝ} {basis_tl : Basis} (h : WellFormedBasis (basis_hd :: basis_tl)) :

∀ᶠ (x : ℝ) in Filter.atTop , 0 < basis_hd x

The first function in a well-formed basis is eventually positive.

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.tail_isLittleO_head {hd : ℝ → ℝ} {tl : Basis} (h : WellFormedBasis (hd :: tl)) {f : ℝ → ℝ} (hf : f ∈ tl) :

(Real.log ∘ f) =o[Filter.atTop ] (Real.log ∘ hd)

All functions in the tail of a well-formed basis are little-o of the basis' head.

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.push_log_last {basis_hd : ℝ → ℝ} {basis_tl : Basis} (h_basis : WellFormedBasis (basis_hd :: basis_tl)) :

WellFormedBasis (basis_hd :: basis_tl ++ [Real.log ∘ (basis_hd :: basis_tl).getLast ⋯])

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.pow_isLittleO_pow_of_log {f g : ℝ → ℝ} (a b : ℝ) (hf : ∀ᶠ (x : ℝ) in Filter.atTop , 0 < f x) (hg : Filter.Tendsto g Filter.atTop Filter.atTop) (h : (Real.log ∘ f) =o[Filter.atTop ] (Real.log ∘ g)) (hb : 0 < b) :

(f ^ a) =o[Filter.atTop ] (g ^ b)

Auxillary lemma. If function f is eventually positive, g tends to atTop, and log f =o[atTop] log g then for any a and b > 0, then f^a =o[atTop] g^b.

source

theorem Tactic.ComputeAsymptotics.WellFormedBasis.tail_pow_majorized_head {hd f : ℝ → ℝ} {tl : Basis} (h_basis : WellFormedBasis (hd :: tl)) (hf : f ∈ tl) (r : ℝ) :

Majorized (f ^ r) hd 0

Any power of function from a well-formed basis' tail is Majorized by basis' head with zero exponent.

Basis extensions #

source

inductive Tactic.ComputeAsymptotics.BasisExtension :

Basis → Type

The type of extensions of a given basis, defined as an inductive type. Given a basis : Basis and ex : BasisExtension basis of it, one can use getBasis to produce a basis basis' for which basis <+ basis'. Moreover, all such bases for which basis is a sublist can be obtained in this manner. In this sense BasisExtension is a Type-valued analogue of List.Sublist.