Little oh for functions whose domain isn't all of ℝ

Stream: new members

[Quinn Culver]

What's the best way to prove a little oh relationship for functions whose domain isn't all of ℝ? ChatGPT suggests either 1. extending the functions in some trivial way to all of ℝ or 2. lifting variables and functions.

Option 2. seems a lot more appealing, but I cannot get it to work.

Is option 2. better? Is option 1. considered okay even though it feels 'hacky'?

The following MWE shows what I'm trying to achieve. As is, the Theorem statement throws the error indicated below it.

import Mathlib

open Filter Asymptotics Topology Set

noncomputable def f (x:NNReal) : ℝ := 1/x

noncomputable def f' (x:NNReal) : ℝ := -1/x^2

/-
Goal: use lean's little oh notation to express that a function with domain that's not all of ℝ is approximately equal to its first order taylor approximation.
-/

-- Define the little-oh approximation within the non-negative reals
theorem first_order_taylor_approx_little_oh (x₀ : NNReal) :
  (λ (x : NNReal) => f x - (f x₀ + (f' x₀) * (x - x₀))) =o[𝓝 x₀] (λ x => x - x₀) := sorry
--throws error: "failed to synthesize Norm NNReal"

[Eric Wieser]

@Yury G. Kudryashov may be able to comment on whether #9675 would help here