Boundedness Theorem for Continuous Functions

Stream: Is there code for X?

[rtertr (Sonia)]

Hi, is there a theorem stating that if a function is continuous and
lim(x-->infinity) f(x) < infinity
and lim(x-->-infinity) f(x) < infinity, then f(x) < infinity? :)

[Kevin Buzzard]

What does f(x)<infinity even mean? What is the codomain of your function?

[rtertr (Sonia)]

Oh yeah it is real. I wanna show that the function is bounded ∃C:ℝ, ∀x:E, ‖f x‖ ≤ C

[Jireh Loreaux]

What is E?

[Kevin Buzzard]

I think that what you're asking is how to prove that if you know $f:\R\to\R$ is continuous, and $\exists B,C,\forall x\geq B, f(x)\leq C$ and $\exists B',C',\forall x\leq -B', f(x)\leq C'$ then there exists $C''$ such that $\forall x, f(x)\leq C''$ (because $f$ is continuous and hence bounded on $[-B',B]$). But this conversation is demonstrating that the best way to ask a question is to formalise the question in Lean and not hope that the readers can do so.

[rtertr (Sonia)]

Yes, thank you. Sorry if I was a bit vague :smile:

[Eric Rodriguez]

and for that, docs#continuous.exists_forall_le' could help but may be a bit hard to use without understanding of filters. formalising using docs#is_compact.exists_forall_ge may be easier

[rtertr (Sonia)]

Ah, thank you :smile: The thing is I already proved what I wanted, so I don't technically need the theorem. But I was just writing about my process, and I wanted to see if such theorem actually existed, and I had just not been able to find it when I first started working. :smiley_cat:

[Jireh Loreaux]

Note: I don't think we have your result as stated. If I try some formalizations of your statement, it would look something like this:

import analysis.normed.field.basic

open filter bornology

example (f : C(ℝ, ℝ)) (hf_lt₁ : is_bounded_under (<) at_top f)
  (hf_lt₂ : is_bounded_under (<) at_bot f) :
  bdd_above (set.range f) := sorry

-- you can put the two properties at `∞` and `-∞` together using `⊔` on the respective filters.
example (f : C(ℝ, ℝ)) (hf_lt : is_bounded_under (<) (at_top ⊔ at_bot ) f) :
  bdd_above (set.range f) := sorry

-- here is another filter that represents the idea "at +∞ or -∞"
example (f : C(ℝ, ℝ)) (hf_lt : is_bounded_under (<) (comap norm at_top) f) :
  bdd_above (set.range f) := sorry

-- yet another filter using `bornology.cobounded`
example (f : C(ℝ, ℝ)) (hf_lt : is_bounded_under (<) (cobounded ℝ) f) :
  bdd_above (set.range f) := sorry

I don't think we have any of these (or similar statements) explicitly in mathlib, but I could be wrong.

[rtertr (Sonia)]

Ah, okay, thank you very much! That is good to know! :D