`stretch_bound`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.Analysis.Limits
domain: Relativity
line: 167 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Relativity.Analysis.Limits on GitHub at line 167.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 164    _ = ε * |h x| := by rw [hε'C]
 165
 166/-- Stub lemma: linear bound under rescaling. -/
 167lemma stretch_bound (c : ℝ) : |c| + 1 > 0 := by
 168  have : 0 ≤ |c| := abs_nonneg _
 169  linarith
 170
 171/-! **Little-o Multiplication**: If f = o(g) and h is bounded, then f·h = o(g·h).
 172    This is a placeholder for the actual asymptotic result. -/
 173
 174end Analysis
 175end Relativity
 176end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.