`bigO_comp_continuous`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.Analysis.Landau
domain: Relativity
line: 87 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Relativity.Analysis.Landau on GitHub at line 87.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  84    _ ≤ (|c| + 1) * C * |g x| := by nlinarith [abs_nonneg c, abs_nonneg (g x)]
  85
  86/-- Composition with continuous function (placeholder: keep axiomatized for now). -/
  87theorem bigO_comp_continuous (f g : ℝ → ℝ) (h : ℝ → ℝ) (a : ℝ)
  88  [LandauCompositionFacts] :
  89  IsBigO f g a → IsBigO (fun x => h (f x)) (fun x => h (g x)) a :=
  90  LandauCompositionFacts.bigO_comp_continuous f g h a
  91
  92end Analysis
  93end Relativity
  94end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.