LandauCompositionFacts
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.
claimAssume 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 in Recognition Science
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.
scope and limits
- Does not derive the composition rule from continuity of h or other assumptions.
- Does not extend the property to little-o notation.
- Does not supply explicit constants C or M for the composed functions.
- Does not restrict the class of admissible functions h.
Lean usage
theorem apply_comp (f g h : ℝ → ℝ) (a : ℝ) [LandauCompositionFacts] (hf : IsBigO f g a) : IsBigO (fun x => h (f x)) (fun x => h (g x)) a := LandauCompositionFacts.bigO_comp_continuous f g h a hfformal statement (Lean)
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)). -/