bigO_comp_continuous
The theorem asserts that if f is big-O of g near a point a, then post-composition by any real function h preserves the big-O relation. Analysts formalizing asymptotic manipulations in relativistic models would cite it when composing big-O expressions. The proof is a one-line term wrapper that directly projects the matching field from the LandauCompositionFacts typeclass instance.
claimAssuming the LandauCompositionFacts hypothesis, if there exist $C>0$ and $M>0$ such that $|f(x)|$ is bounded by $C|g(x)|$ for all $|x-a|<M$, then the same bound holds for the compositions $h(f(x))$ and $h(g(x))$.
background
The module supplies rigorous Landau notation by encoding big-O as an explicit predicate on real functions. The definition IsBigO f g a states that positive constants C and M exist so that |f(x)| ≤ C |g(x)| whenever |x-a| < M. LandauCompositionFacts is a hypothesis class that bundles several manipulation rules for these predicates, including the composition property stated here.
proof idea
The proof is a term-mode one-liner that applies the bigO_comp_continuous field of the supplied LandauCompositionFacts instance to the arguments f, g, h, a and the hypothesis IsBigO f g a. No additional tactics or reductions occur.
why it matters in Recognition Science
The result supplies the composition rule required by the LandauCompositionFacts class and is referenced by the stub instance landauFactsStub in NewFixtures. It belongs to the collection of lemmas for arithmetic and composition of asymptotic expressions in the rigorous Landau notation developed for relativity analysis. The property remains axiomatized rather than derived from the IsBigO definition, marking a point where a future first-principles proof could close the hypothesis.
scope and limits
- Does not assume or require continuity of h.
- Does not derive the composition rule from the explicit definition of IsBigO.
- Does not address little-o notation or other asymptotic relations.
- Does not restrict the domain or codomain beyond real-valued functions.
formal statement (Lean)
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 :=
proof body
Term-mode proof.
90 LandauCompositionFacts.bigO_comp_continuous f g h a
91
92end Analysis
93end Relativity
94end IndisputableMonolith