IndisputableMonolith.Relativity.Analysis.Landau

   1import Mathlib
   2import IndisputableMonolith.Relativity.Analysis.Limits
   3
   4/-!
   5# Rigorous Landau Notation
   6
   7Implements f ∈ O(g) as proper Filter predicate with arithmetic operations.
   8Provides lemmas for manipulating asymptotic expressions.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace Relativity
  13namespace Analysis
  14
  15/-- Hypothesis class capturing composition bounds for big-O. -/
  16class LandauCompositionFacts : Prop where
  17  bigO_comp_continuous : ∀ (f g h : ℝ → ℝ) (a : ℝ),
  18    IsBigO f g a → IsBigO (fun x => h (f x)) (fun x => h (g x)) a
  19
  20/-! Membership notation: f ∈ O(g) would be nice but causes parsing issues in Lean 4.
  21    Use IsBigO and IsLittleO directly. -/
  22
  23/-- O(f) + O(g) ⊆ O(max(f,g)). -/
  24theorem bigO_add_subset (f g : ℝ → ℝ) (a : ℝ) :
  25  ∀ h₁ h₂, IsBigO h₁ f a → IsBigO h₂ g a →
  26    IsBigO (fun x => h₁ x + h₂ x) (fun x => max (|f x|) (|g x|)) a := by
  27  intro h₁ h₂ hf hg
  28  rcases hf with ⟨C₁, hC₁pos, M₁, hM₁pos, hf⟩
  29  rcases hg with ⟨C₂, hC₂pos, M₂, hM₂pos, hg⟩
  30  refine ⟨C₁ + C₂, by linarith, min M₁ M₂, lt_min hM₁pos hM₂pos, ?_⟩
  31  intro x hx
  32  have hx₁ : |x - a| < M₁ := lt_of_lt_of_le hx (min_le_left _ _)
  33  have hx₂ : |x - a| < M₂ := lt_of_lt_of_le hx (min_le_right _ _)
  34  have hf' := hf x hx₁
  35  have hg' := hg x hx₂
  36  -- Triangle inequality and bounds
  37  have hmax_nonneg : 0 ≤ max (|f x|) (|g x|) := le_max_of_le_left (abs_nonneg _)
  38  calc |h₁ x + h₂ x|
  39      ≤ |h₁ x| + |h₂ x| := abs_add_le _ _
  40    _ ≤ C₁ * |f x| + C₂ * |g x| := add_le_add hf' hg'
  41    _ ≤ C₁ * max (|f x|) (|g x|) + C₂ * max (|f x|) (|g x|) := by
  42        have h1 : C₁ * |f x| ≤ C₁ * max (|f x|) (|g x|) :=
  43          mul_le_mul_of_nonneg_left (le_max_left _ _) (le_of_lt hC₁pos)
  44        have h2 : C₂ * |g x| ≤ C₂ * max (|f x|) (|g x|) :=
  45          mul_le_mul_of_nonneg_left (le_max_right _ _) (le_of_lt hC₂pos)
  46        exact add_le_add h1 h2
  47    _ = (C₁ + C₂) * max (|f x|) (|g x|) := by ring
  48    _ = (C₁ + C₂) * |max (|f x|) (|g x|)| := by rw [abs_of_nonneg hmax_nonneg]
  49
  50/-- O(f) · O(g) ⊆ O(f·g). -/
  51theorem bigO_mul_subset (f g : ℝ → ℝ) (a : ℝ) :
  52  ∀ h₁ h₂, IsBigO h₁ f a → IsBigO h₂ g a →
  53    IsBigO (fun x => h₁ x * h₂ x) (fun x => f x * g x) a := by
  54  intro h₁ h₂ hf hg
  55  rcases hf with ⟨C₁, hC₁pos, M₁, hM₁pos, hf⟩
  56  rcases hg with ⟨C₂, hC₂pos, M₂, hM₂pos, hg⟩
  57  refine ⟨C₁ * C₂, by nlinarith, min M₁ M₂, lt_min hM₁pos hM₂pos, ?_⟩
  58  intro x hx
  59  have hx₁ : |x - a| < M₁ := lt_of_lt_of_le hx (min_le_left _ _)
  60  have hx₂ : |x - a| < M₂ := lt_of_lt_of_le hx (min_le_right _ _)
  61  have hf' := hf x hx₁
  62  have hg' := hg x hx₂
  63  calc |h₁ x * h₂ x|
  64      = |h₁ x| * |h₂ x| := abs_mul _ _
  65    _ ≤ (C₁ * |f x|) * (C₂ * |g x|) :=
  66        mul_le_mul hf' hg' (abs_nonneg _) (by linarith [mul_nonneg (le_of_lt hC₁pos) (abs_nonneg (f x))])
  67    _ = (C₁ * C₂) * (|f x| * |g x|) := by ring
  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
  95