LandauCompositionFacts
plain-language theorem explainer
LandauCompositionFacts axiomatizes preservation of big-O bounds under arbitrary composition at a point. Analysts manipulating asymptotic expansions in relativity models cite it to justify replacing f with h(f) inside O(g) expressions. The declaration is a bare class definition with no proof body, serving as a hypothesis interface instantiated downstream via a trivial stub.
Claim. Assume functions $f,g,h:ℝ→ℝ$ and point $a∈ℝ$. If there exist $C>0$, $M>0$ such that $|f(x)|≤C|g(x)|$ whenever $|x-a|<M$, then the same bound holds for the composed functions $h∘f$ and $h∘g$.
background
The module implements Landau notation as Filter predicates on real functions. IsBigO(f,g,a) means ∃C>0,∃M>0 such that |f(x)|≤C|g(x)| for |x-a|<M; IsLittleO strengthens this to arbitrary ε>0. The class LandauCompositionFacts packages the additional hypothesis that these bounds survive composition with any h. It is imported from Limits and referenced by CirclePhaseLift results that supply explicit log-derivative bounds M.
proof idea
The declaration is a class definition with no proof body. It simply declares the field bigO_comp_continuous as the required Prop. Downstream code instantiates it via landauFactsStub by returning the input IsBigO assumption unchanged, then applies the field directly in bigO_comp_continuous.
why it matters
The class enables the bigO_comp_continuous theorem that applies composition inside asymptotic expressions. It supplies the hypothesis interface needed for Landau manipulations in the Relativity.Analysis module and is instantiated in NewFixtures.landauFactsStub. The construction keeps the composition rule axiomatic, consistent with the module's placeholder treatment of continuous-function composition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.