Limit of composition

Stream: Is there code for X?

[Gareth Ma]

Is there something like this?

example (f g : ℕ → ℝ) (h : f =O[atTop] g) (F : ℝ → ℝ) (hF : Monotone F) :
    (F ∘ f) =O[atTop] (F ∘ g) := by
  sorry

The idea is simply that if $f(x) \leq Cg(x)$ then $F(f(x)) \leq F(Cg(x))$ from monotonenes. Add the absolute values yourself...

[Gareth Ma]

Also is Moogle down or are there no results?

Screenshot-2024-03-12-at-23.01.38.png

[Kevin Buzzard]

Jesse told me earlier today that it was server migration.

[Gareth Ma]

Oh I might need some positivity conditions, but yes

[Anatole Dedecker]

I’m getting tired but I don’t think this is true ? Sticking to natural numbers for simplicity, take $f(n)=n +1$, $g(n) = n$, $F(n)=n!$. Then for sure $f=O(g)$ but $\frac{F(f(n))}{F(g(n))} = n+1$ so we don’t have $F\circ f=O(F\circ g)$

[Anatole Dedecker]

(deleted)

[Gareth Ma]

You probably mean to flip it around? But I think you’re correct

[Anatole Dedecker]

Ah yes flipping it seems to work (fixed)

[Gareth Ma]

No I think $n! \not \in O((n + 1)!)$.

[Gareth Ma]

Yeah

[Gareth Ma]

My original goal was to prove that $\log(1 + o(1)) = O(1)$, and my plan was first prove $1 + x \leq \exp(x)$ i.e. $1 + x = O(\exp(x))$, then take log for $\log(1 + x) = O(x)$

[Gareth Ma]

Actually wait, I can just take log of the inequality directly to get $\log(1 + x) \leq \log(\exp(x))$... :man_facepalming: okay I'm getting tired too

[Gareth Ma]

Thanks for the help

[Anatole Dedecker]

Aaaaaah no I deleted the wrong message

[Gareth Ma]

Haha you can recover in the EDITED history

[Anatole Dedecker]

Yes but not restore the LaTeX...

[Gareth Ma]

:(

[Gareth Ma]

I can read it from the history :D

[Jesse Michael Han]

Gareth Ma said:

Also is Moogle down or are there no results?

Screenshot-2024-03-12-at-23.01.38.png

Moogle is back online! happy moogling

[Notification Bot]

A message was moved from this topic to #general > Moogle down by Jireh Loreaux.