No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
18def IsBigO (f g : ℝ → ℝ) (a : ℝ) : Prop :=
proof body
Definition body.
19 ∃ C > 0, ∃ M > 0, ∀ x, |x - a| < M → |f x| ≤ C * |g x|
20
21/-- Little-o notation: ∀ ε > 0, ∃ M such that |f(x)| ≤ ε|g(x)| for |x-a| < M. -/
used by (14)
From the project-wide theorem graph. These declarations reference this one in their body.
-
bigO_add_subset
in IndisputableMonolith.Relativity.Analysis.Landau
decl_use
-
bigO_comp_continuous
in IndisputableMonolith.Relativity.Analysis.Landau
decl_use
-
bigO_const_mul
in IndisputableMonolith.Relativity.Analysis.Landau
decl_use
-
bigO_mul_subset
in IndisputableMonolith.Relativity.Analysis.Landau
decl_use
-
LandauCompositionFacts
in IndisputableMonolith.Relativity.Analysis.Landau
decl_use
-
bigO_add
in IndisputableMonolith.Relativity.Analysis.Limits
decl_use
-
bigO_comp
in IndisputableMonolith.Relativity.Analysis.Limits
decl_use
-
bigO_mul
in IndisputableMonolith.Relativity.Analysis.Limits
decl_use
-
const_is_O_one
in IndisputableMonolith.Relativity.Analysis.Limits
decl_use
-
IsBigOPower
in IndisputableMonolith.Relativity.Analysis.Limits
decl_use
-
linear_is_O_x
in IndisputableMonolith.Relativity.Analysis.Limits
decl_use
-
littleO_bigO_trans
in IndisputableMonolith.Relativity.Analysis.Limits
decl_use
-
littleO_implies_bigO
in IndisputableMonolith.Relativity.Analysis.Limits
decl_use
-
x_squared_is_O_x_squared
in IndisputableMonolith.Relativity.Analysis.Limits
decl_use
depends on (4)
Lean names referenced from this declaration's body.
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
that
in IndisputableMonolith.NumberTheory.PhiLadderLattice
decl_use
-
M
in IndisputableMonolith.Recognition
decl_use
-
M
in IndisputableMonolith.Recognition.Cycle3
decl_use