bigO_comp_continuous
plain-language theorem explainer
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.
Claim. Assuming 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.