1/(n+1) is decreasing

Stream: Is there code for X?

[Michael Stoll]

Looking for

import Mathlib

example : Antitone (fun n : ℕ ↦ (n + 1 : ℝ)⁻¹) := sorry

but having problems finding it in Mathlib...

@loogle Antitone, Inv.inv

[loogle]

:search: Antitone.inv, Monotone.inv, and 1 more

[Eric Rodriguez]

example : Antitone (fun n : ℕ ↦ (n + 1 : ℝ)⁻¹) := by
  intros a b h
  apply inv_le_inv_of_le
  · positivity
  gcongr

[Eric Rodriguez]

but inv_0 lemmas are lacking...

[Michael Stoll]

Thanks; I had a similar proof.
The real question is, I guess, whether some form of this should be in Mathlib.

[Damiano Testa]

Btw, there is a current thread with a similar problem of missing inv\0 lemmas.

I personally would expect the inv\0 lemmas to exist.

[Michael Stoll]

There is docs#inv_le_inv₀, but it only applies to a LinearOrderedCommGroupWithZero, which I think the reals are not.

[Kevin Buzzard]

Yeah I think that's for general valuation theory, which demands that 0 is the smallest element. Can I interest you in NNReal?

[Michael Stoll]

Un-#xy: I need this for

lemma not_summable_indicator_one_div_natCast {m : ℕ} (hm : m ≠ 0) (k : ZMod m) :
    ¬ Summable (Set.indicator {n : ℕ | (n : ZMod m) = k} fun n : ℕ ↦ (1 / n : ℝ)) := sorry

which I use in turn to show that Dirichlet L-series have absicssa of absolute convergence equal to 1.
Going via NNReal looks like a significant detour here.

[Arend Mellendijk]

I have some antitoneOn lemmas for invat #9984, but they might be a bit of a hassle to use here.

[Kevin Buzzard]

Just out of interest, why do we care that the abscissa of absolute convergence is equal to one? (Other than the "because it's there" reason). Presumably for all applications it suffices to know that it's at most 1?

[Michael Stoll]

I think "because it's there" is a sufficient reason! :smile: