bigO_const_mul

formal source

  68    _ = (C₁ * C₂) * |f x * g x| := by rw [abs_mul]
  69
  70/-- Scalar multiplication: c · O(f) = O(g) when f = O(g). -/
  71theorem bigO_const_mul (c : ℝ) (f g : ℝ → ℝ) (a : ℝ) :
  72  IsBigO f g a → IsBigO (fun x => c * f x) g a := by
  73  intro hf
  74  rcases hf with ⟨C, hCpos, M, hMpos, hbound⟩
  75  have hCpos' : 0 < (|c| + 1) * C := by
  76    have h1 : 0 < |c| + 1 := by have := abs_nonneg c; linarith
  77    exact mul_pos h1 hCpos
  78  refine ⟨(|c| + 1) * C, hCpos', M, hMpos, ?_⟩
  79  intro x hx
  80  have hx' := hbound x hx
  81  calc |c * f x|
  82      = |c| * |f x| := abs_mul _ _
  83    _ ≤ |c| * (C * |g x|) := mul_le_mul_of_nonneg_left hx' (abs_nonneg c)
  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