limsup_le_limsup

Stream: Is there code for X?

[Apurva Nakade]

Hi, what's a quick way to prove the following in mathlib4:

import Mathlib.Analysis.InnerProductSpace.Basic

open Filter

variable {V : Type _} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]

example
  (v w : V)
  (seq : ℕ → V)
  (htends : Tendsto (fun n => seq n) atTop (nhds v)) :
  Tendsto (fun n => ⟪seq n, w⟫_ℝ) atTop (nhds ⟪v, w⟫_ℝ) := by sorry

example
  (v w : V)
  (seq : ℕ → V)
  (htends : Tendsto (fun n => seq n) atTop (nhds v)) :
  limsup (fun n => ⟪seq n, w⟫_ℝ) atTop = ⟪v, w⟫_ℝ := by sorry

I'm not very comfortable with Filters so I'm having trouble reading the files. Thanks,

[Eric Wieser]

The first one is

example
  (v w : V)
  (seq : ℕ → V)
  (htends : Tendsto (fun n => seq n) atTop (nhds v)) :
  Tendsto (fun n => ⟪seq n, w⟫_ℝ) atTop (nhds ⟪v, w⟫_ℝ) :=
htends.inner tendsto_const_nhds

(docs#Filter.Tendsto.inner)

[Eric Wieser]

And the second is

example
  (v w : V)
  (seq : ℕ → V)
  (htends : Tendsto (fun n => seq n) atTop (nhds v)) :
  limsup (fun n => ⟪seq n, w⟫_ℝ) atTop = ⟪v, w⟫_ℝ :=
(htends.inner tendsto_const_nhds).limsup_eq

(docs#Filter.Tendsto.limsup_eq)

[Apurva Nakade]

Thank you! I was missing the _const_ in my searches!!

[Notification Bot]

Apurva Nakade has marked this topic as resolved.

[Notification Bot]

Apurva Nakade has marked this topic as unresolved.

[Apurva Nakade]

I'm stuck at another related question about limsup:

import Mathlib.Analysis.InnerProductSpace.Basic

open Filter

example
  (seq1 seq2 : ℕ → ℝ)
  (r : ℝ)
  (le : ∀ n, seq1 n ≤ seq2 n)
  (htends : Tendsto seq2 atTop (nhds r)):
  limsup seq1 atTop ≤ r  := by sorry

[Apurva Nakade]

I tried limsup_le_limsup but got stuck proving IsCoBoundedUnder and IsBoundedUnder

[Apurva Nakade]

Hello, just bumping this question again. Any pointers towards similar proofs involving limsup in mathlib would also be enough. A search for limsup_le_limsup returns very few results so I'm thinking that there is some other function that I'm missing.

[Yury G. Kudryashov]

See docs#Filter.Tendsto.isBoundedUnder_le

[Apurva Nakade]

Thank you!

[Yury G. Kudryashov]

A missing lemma: for a nontrivial filter, IsBounded implies IsCobounded. UPD: see docs#Filter.IsBounded.isCobounded_ge and docs#Filter.IsBounded.isCobounded_le

[Yury G. Kudryashov]

You will also need docs#Filter.IsBoundedUnder.mono_le

[Yury G. Kudryashov]

BTW, your example is not true: if seq2 tends to -1 while seq1 tends to -∞, then LHS equals 0 while RHS equals -1.

[Yury G. Kudryashov]

So, you have to assume that seq1 is cobounded (a.k.a. doesn't tend to -∞).

[Apurva Nakade]

Is this because of the way limsup is defined in mathlib when the limit is -\infty?

[Apurva Nakade]

TBH I thought cobounded was a weaker version of bounded

[Apurva Nakade]

I will add IsCobounded as a hypothesis and try to derive Boundedness

[Yury G. Kudryashov]

As you can see, docs#Filter.limsup assumes nothing about the function. So, it is defined for any function. If you dig deeper, then you can see that for real numbers it is equal to zero in case it should be undefined.

[Yury G. Kudryashov]

You need coboundedness of seq1 and boundedness of seq2. The latter follows from Tendsto.

[Notification Bot]

Apurva Nakade has marked this topic as resolved.

[Jireh Loreaux]

Composing with the coercion docs#Real.toEReal gives the "correct" limsup value.

[Apurva Nakade]

I need this as a part of a bigger analysis proof. I tried EReal at first but got stuck doing some arithmetic.

[Apurva Nakade]

Actually, very specifically, this code is failing if I coerce the inner products to EReal

example
  (v w : V)
  (seq : ℕ → V)
  (htends : Tendsto (fun n => seq n) atTop (nhds v)) :
  limsup (fun n => ⟪seq n, w⟫_ℝ) atTop = ⟪v, w⟫_ℝ :=
(htends.inner tendsto_const_nhds).limsup_eq

[Apurva Nakade]

I'm getting the error

typeclass instance problem is stuck, it is often due to metavariables
  OrderTopology ?m.152004

[Notification Bot]

Yury G. Kudryashov has marked this topic as unresolved.

[Yury G. Kudryashov]

Indeed, your function is not just inner _ _, it's Real.toEReal (inner _ _).

[Yury G. Kudryashov]

See docs#EReal.tendsto_coe

[Apurva Nakade]

I managed to get this to work. I had to go back and forth a few times between Real and EReal in my calculations and add a few helper haves but everything worked out in the end.

[Apurva Nakade]

The statements look really clean with EReal