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.

@[reducible, inline]

abbrev Tactic.ComputeAsymptotics.Basis : Type

List of functions used to construct monomials in multiseries.

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

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.

theorem Tactic.ComputeAsymptotics.WellFormedBasis.nil : WellFormedBasis []

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

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

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.

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

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)

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)

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)

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)

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)

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])

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.

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.

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.

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.

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 ⋯])

Basis extensions

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.

• nil : BasisExtension []
• keep (basis_hd : ℝ → ℝ) {basis_tl : Basis} (ex : BasisExtension basis_tl) : BasisExtension (basis_hd :: basis_tl)
• insert {basis : Basis} (f : ℝ → ℝ) (ex : BasisExtension basis) : BasisExtension basis

def Tactic.ComputeAsymptotics.BasisExtension.getBasis {basis : Basis} (ex : BasisExtension basis) : Basis

The basis after applying a basis extension.

theorem Tactic.ComputeAsymptotics.BasisExtension.sublist_getBasis {basis : Basis} {ex : BasisExtension basis} : List.Sublist basis ex.getBasis

theorem Tactic.ComputeAsymptotics.BasisExtension.insert_tail_wellFormedBasis {basis : Basis} {f : ℝ → ℝ} {ex_tl : BasisExtension basis} (h_basis : WellFormedBasis (insert f ex_tl).getBasis) : WellFormedBasis ex_tl.getBasis