def «term_=O[_]_» : Lean.TrailingParserDescr

Equations

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

def Asymptotics.IsOmega {α : Type} {E : Type u_1} {F : Type u_2} [Norm E] [Norm F] (l : Filter α) (f : α → E) (g : α → F) : Prop

Equations

• Asymptotics.IsOmega l f g = g =O[l] f

structure Algorithm (α : Type) (β : Type) : Type

• func : α → β
• time : α → ℝ

theorem composition_time {α : Type} {β : Type} {γ : Type} (f : Algorithm α β) (g : Algorithm β γ) : ∃ (h : Algorithm α γ), h.func = g.func ∘ f.func ∧ h.time = f.time + g.time ∘ f.func

def self_composition {α : Type} (func : α → α) : ℕ → α → α

Equations

• self_composition func 0 = id
• self_composition func (Nat.succ n) = func ∘ self_composition func n