bounding limits

Stream: new members

[Alex Kontorovich]

Hello! I see theorems like cau_seq.lim_le here https://leanprover-community.github.io/mathlib_docs/data/real/cau_seq_completion.html which say f(n)<x -> lim f < x. If I know that f(n) and g(n) are Cauchy sequences, and f(n)<= g(n), is there really not a theorem that says lim f <= lim g? (Or am I missing something stupid?) Thanks!

[Kevin Buzzard]

I think these lemmas you're looking at don't say what you think they say. <= and < are defined on Cauchy sequences such that f <= g iff lim(f)<=lim(g) (when the limits exist). The lemmas lt_lim and lim_lt are not used at all in mathlib. The theorem you want will probably be expressed in terms of filters and will probably be there.

[Heather Macbeth]

@Alex Kontorovich Here's the statement, for limits rather than Cauchy sequences:
docs#le_of_tendsto_of_tendsto'

lemma le_of_tendsto_of_tendsto' {f g : β → α} {b : filter β} {a₁ a₂ : α} [ne_bot b]
  (hf : tendsto f b (𝓝 a₁)) (hg : tendsto g b (𝓝 a₂)) (h : ∀ x, f x ≤ g x) :
  a₁ ≤ a₂ :=

[Heather Macbeth]

Did you specifically want it to be about Cauchy sequences (or will it be enough for you to have it for limits, together with having access to a theorem saying that a Cauchy sequence has a limit)?

[Alex Kontorovich]

Hmm interesting. I'm trying to mimic the mathlib proof of exp_bound:

https://github.com/leanprover-community/mathlib/blob/4851857/src/data/complex/exponential.lean#L1021

Line 1025 says:

refine lim_le (cau_seq.le_of_exists ⟨n, λ j hj, _⟩),

This converts the goal which is a statement about limits into a statement about jth terms of the defining sequences (the right side of which is constant). Kevin, are you saying there's some way to do that more directly, since <= is already "defined" on Cauchy sequences?... Thanks!

[Heather Macbeth]

Can I ask what context you're working in? Is it a different bound involving the exponential function? The special_functions library is especially ad hoc, so tricks that are needed for the exponential function because of its particular definition might not translate to other contexts.

[Heather Macbeth]

For example, exp is defined literally via a Cauchy sequence, but there is also a full library on infinite sums
https://leanprover-community.github.io/mathlib_docs/topology/algebra/infinite_sum.html
which would provide an alternative framework (maybe it didn't exist when the exp file was written).

[Alex Kontorovich]

Yes, I'm playing around with exp... I managed to prove that, if |x|<1/2, then |exp(x)-(1+x)|<1 (again, very ugly code, sorry):

theorem expBnd : ∀ x:ℂ , complex.abs x < 1/2 → complex.abs (complex.exp x - (1+x))< 1:=
begin
    intros,

    have rwrw1: complex.abs (complex.exp x - 1 - x) ≤ complex.abs x ^ 2,
    {
        refine complex.abs_exp_sub_one_sub_id_le _,
        linarith,
    },
    have rwrw2: complex.abs x ^ 2 < 1/2 * 1/2,
    {
        have rw3: complex.abs x ^ 2 = complex.abs x  * complex.abs x,
        {
            ring,
        },
        rw rw3,
        refine mul_lt_mul'' _ _ _ _ ,
        linarith,
        have rw5: (2:ℝ )⁻¹ =1/2,
        {
            rw  division_def,
            ring,
        },
        rw rw5,
        exact a,
        exact absnonneg x,
        exact absnonneg x,
    },
    have rwrw3: (1:ℝ )/2*1/2 =1/4,
    {
        ring,
    },
    have rwrw4: complex.abs (complex.exp x - 1 - x) < 1/2 * 1/2,
    {
        exact gt_of_gt_of_ge rwrw2 rwrw1,
    },
    have rwrw5: complex.abs (complex.exp x - 1 - x) = complex.abs (complex.exp x - (1 + x)),
    {
        ring,
    },
    have rwrw6: (1:ℝ )/4<1, by linarith,
    rw ←  rwrw5,
    rw rwrw3 at rwrw4,
    linarith,
end

but now I'm trying to see how to do it without calling complex.abs_exp_sub_one_sub_id_le, by directly accessing the series. Of course the human proof is trivial:

|exp(x)-(1+x)| \le |x|^2/2+|x|^3/3!+...\le |x|^2+|x|^3+... \le 1

since |x|<1/2...

[Alex Kontorovich]

And the proof of complex.abs_exp_sub_one_sub_id_le uses exp_bound...

But thanks for the tip Heather, I'll try to mess around with infinite_sum...

[Heather Macbeth]

(just to continue with a guide to the more general approaches -- here's a file I wrote setting up the function $x\mapsto x^{-1}$ (where defined) in a Banach algebra, using the infinite sum framework I pointed to above:
https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/units.html
and, btw, since last week @Yury G. Kudryashov has started seriously working towards analytic functions "done right"!
https://github.com/leanprover-community/mathlib/pull/4291#issuecomment-699684052 )

[Yury G. Kudryashov]

I'd say @Sebastien Gouezel already did most of the work but we need some glue to use it for exp, sin, etc.

[Heather Macbeth]

Yury, what setting are you planning to work in?

[Heather Macbeth]

Will you do single-variable power series in Banach algebras?

[Heather Macbeth]

Or something more general that unites the above theory with the theory of several complex variables?

[Yury G. Kudryashov]

The first step will be to define a function from mv_power_series (fin n) to continuous_multilinear_maps on A^n and from power_series to A, where A is an algebra.

[Heather Macbeth]

You could conceivably work on modules over A rather than just A^n. But I'm not sure there's any point.