Pointwise bounds up to constants

u ≼ v says that u a ≤ c * (v a + 1) for some constant c and every a: the bounds of Turing.MultiTapeTM.ComputableTidilyInO. The relation is a preorder, closed under sums, constant factors, products and powers of padded bounds, and composition. The tactic bigO splits a goal u ≼ v along sums, case distinctions, constant factors and powers of u and closes the parts by assumption, through two assumptions, by reflexivity or as constants.

Main definitions

• Turing.MultiTapeTM.BigOLe: pointwise bounds up to constants, with the notation u ≼ v.

def Turing.MultiTapeTM.BigOLe {α : Type u_1} (u v : α → ℕ) : Prop

u ≼ v: u is pointwise at most a constant times v + 1.

def Turing.MultiTapeTM.«term_≼_» : Lean.TrailingParserDescr

u ≼ v: u is pointwise at most a constant times v + 1.

theorem Turing.MultiTapeTM.BigOLe.of_le {α : Type u_1} {u v : α → ℕ} (h : ∀ (a : α), u a ≤ v a) : BigOLe u v

theorem Turing.MultiTapeTM.BigOLe.of_le_linear {α : Type u_1} {u v : α → ℕ} (k k' : ℕ) (h : ∀ (a : α), u a ≤ k * v a + k') : BigOLe u v

A linear pointwise bound.

theorem Turing.MultiTapeTM.BigOLe.refl {α : Type u_1} (u : α → ℕ) : BigOLe u u

theorem Turing.MultiTapeTM.BigOLe.trans {α : Type u_1} {u v w : α → ℕ} (h₁ : BigOLe u v) (h₂ : BigOLe v w) : BigOLe u w

@[instance_reducible]

instance Turing.MultiTapeTM.BigOLe.instTransForallNat {α : Type u_1} : Trans BigOLe BigOLe BigOLe

theorem Turing.MultiTapeTM.BigOLe.trans_le {α : Type u_1} {u v w : α → ℕ} (h : BigOLe u v) (h' : ∀ (a : α), v a ≤ w a) : BigOLe u w

A bound followed by a larger function.

theorem Turing.MultiTapeTM.BigOLe.const {α : Type u_1} (k : ℕ) (v : α → ℕ) : BigOLe (fun (x : α) => k) v

theorem Turing.MultiTapeTM.BigOLe.add {α : Type u_1} {u v w : α → ℕ} (h₁ : BigOLe u w) (h₂ : BigOLe v w) : BigOLe (fun (a : α) => u a + v a) w

theorem Turing.MultiTapeTM.BigOLe.ite {α : Type u_1} {u v w : α → ℕ} (c : α → Prop) [DecidablePred c] (h₁ : BigOLe u w) (h₂ : BigOLe v w) : BigOLe (fun (a : α) => if c a then u a else v a) w

Case distinctions, within the larger of the bounds.

theorem Turing.MultiTapeTM.BigOLe.const_mul {α : Type u_1} {u v : α → ℕ} (k : ℕ) (h : BigOLe u v) : BigOLe (fun (a : α) => k * u a) v

theorem Turing.MultiTapeTM.BigOLe.comp {α : Type u_1} {β : Type u_2} {u v : α → ℕ} (h : BigOLe u v) (g : β → α) : BigOLe (fun (b : β) => u (g b)) fun (b : β) => v (g b)

theorem Turing.MultiTapeTM.BigOLe.mul_left {α : Type u_1} {v w : α → ℕ} (u : α → ℕ) (h : BigOLe v w) (hw : ∀ (a : α), 1 ≤ w a) : BigOLe (fun (a : α) => u a * v a) fun (a : α) => u a * w a

A factor bounded by a positive function.

theorem Turing.MultiTapeTM.BigOLe.mul {α : Type u_1} {u v u' v' : α → ℕ} (h₁ : BigOLe u u') (h₂ : BigOLe v v') : BigOLe (fun (a : α) => u a * v a) fun (a : α) => (u' a + 1) * (v' a + 1)

Products, of padded bounds: a bound by 0 says nothing about a factor.

theorem Turing.MultiTapeTM.BigOLe.pow {α : Type u_1} {u v : α → ℕ} (h : BigOLe u v) (n : ℕ) : BigOLe (fun (a : α) => u a ^ n) fun (a : α) => (v a + 1) ^ n

Powers, of padded bounds.

theorem Turing.MultiTapeTM.BigOLe.le_pow {α : Type u_1} (v : α → ℕ) {n : ℕ} (hn : n ≠ 0) : BigOLe v fun (a : α) => (v a + 1) ^ n

A bound below a positive power of itself.

theorem Turing.MultiTapeTM.BigOLe.le_pow_of {α : Type u_1} {u v : α → ℕ} {n : ℕ} (h : BigOLe u v) (hn : n ≠ 0 := by norm_num) : BigOLe u fun (a : α) => (v a + 1) ^ n

A bound below a positive power of a larger bound.

theorem Turing.MultiTapeTM.BigOLe.pow_le {α : Type u_1} {u v : α → ℕ} {n m : ℕ} (h : BigOLe u v) (hnm : n ≤ m := by norm_num) : BigOLe (fun (a : α) => u a ^ n) fun (a : α) => (v a + 1) ^ m

Powers into a larger power, of padded bounds.

def Turing.MultiTapeTM.tacticBigO : Lean.ParserDescr

Splits a goal u ≼ v along the sums, constant factors and powers of u, closing the parts by assumption, through two assumptions, by reflexivity or as constants.