continuousAt_iff_isLittleO

Stream: Is there code for X?

[Alex Kontorovich]

Is this missing from the library? (It's easy to chain together, but is it worth adding separately?)

import Mathlib

open Topology

theorem continuousAt_iff_isLittleO {f : ℂ → ℂ} {z : ℂ} :
    (ContinuousAt f z) ↔ (fun w ↦ f w - f z) =o[𝓝 z] (1 : ℂ → ℂ) := by
  sorry

[Alex Kontorovich]

(Of course more generally than ℂ...)

[Alex Kontorovich]

Also something like this?

import Mathlib

theorem Asymptotics.tendsto_zero_iff_isLittleO {α : Type*} {E : Type*} [NormedRing E]
    {f : α → E} {l : Filter α} : (Filter.Tendsto f l (nhds 0)) ↔ f =o[l] (1 : α → E) := by
  sorry

[Michael Stoll]

I was looking for very similar statements just yesterday, so +1 from me!

[Anatole Dedecker]

Does docs#Asymptotics.isLittleO_one_iff do the trick?

[Alex Kontorovich]

Argh... I wish exact? could've found it... :(

[Alex Kontorovich]

How about the other one, is this worth adding?

import Mathlib

open Topology

theorem continuousAt_iff_isLittleO {f : ℂ → ℂ} {z : ℂ} :
    (ContinuousAt f z) ↔ (fun w ↦ f w - f z) =o[𝓝 z] (1 : ℂ → ℂ) := by
  convert (Asymptotics.isLittleO_one_iff (f' := fun (w:ℂ) => f w - f z) (l := 𝓝 z) (F := ℂ)).symm
  exact Iff.symm tendsto_sub_nhds_zero_iff

[Alex Kontorovich]

Is there a bug in this?

@[simp]
theorem Asymptotics.isLittleO_one_iff{α : Type u_1} (F : Type u_4) {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {f' : α → E'} {l : Filter α} [One F] [NormOneClass F] :
(f' =o[l] fun (_x : α) => 1) ↔ Filter.Tendsto f' l (nhds 0)

What does F have to do with anything? The map f' goes from α → E', the filter is on α; why is it asking me about F?...

[Jireh Loreaux]

That's 1 : F

[Jireh Loreaux]

if you click the source code you'll see it.

[Alex Kontorovich]

Ah, thanks. So I can set F := E' in applications... I guess that level of generality makes sense...

[Jireh Loreaux]

That's also the reason F is an explicit argument (i.e., the RHS of the iff doesn't reference it).

[Alex Kontorovich]

So is this a good thing to add?

import Mathlib

open Topology

namespace Asymptotics

theorem continuousAt_iff_isLittleO {α : Type*} {E : Type*} [NormedRing E] [NormOneClass E]
    [TopologicalSpace α] {f : α → E} {x : α} :
    (ContinuousAt f x) ↔ (fun (y : α) ↦ f y - f x) =o[𝓝 x] (fun (_ : α) ↦ (1 : E)) := by
  convert (Asymptotics.isLittleO_one_iff (f' := fun (y : α) => f y - f x) (l := 𝓝 x) (F := E)).symm
  exact Iff.symm tendsto_sub_nhds_zero_iff

end Asymptotics

[Jireh Loreaux]

Looks good. I can't find it.

[Jireh Loreaux]

Potentially just use a generic constant instead of 1 for convenience (or add both versions).