Zulip Chat Archive

Stream: new members

Topic: bounding limits


view this post on Zulip Alex Kontorovich (Oct 01 2020 at 19:56):

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!

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 20:12):

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.

view this post on Zulip Heather Macbeth (Oct 01 2020 at 22:10):

@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₂ :=

view this post on Zulip Heather Macbeth (Oct 01 2020 at 22:11):

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)?

view this post on Zulip Alex Kontorovich (Oct 01 2020 at 23:22):

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!

view this post on Zulip Heather Macbeth (Oct 01 2020 at 23:25):

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.

view this post on Zulip Heather Macbeth (Oct 01 2020 at 23:32):

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).

view this post on Zulip Alex Kontorovich (Oct 01 2020 at 23:32):

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...

view this post on Zulip Alex Kontorovich (Oct 01 2020 at 23:38):

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...

view this post on Zulip Heather Macbeth (Oct 01 2020 at 23:38):

(just to continue with a guide to the more general approaches -- here's a file I wrote setting up the function xx1x\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 )

view this post on Zulip Yury G. Kudryashov (Oct 01 2020 at 23:48):

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

view this post on Zulip Heather Macbeth (Oct 01 2020 at 23:53):

Yury, what setting are you planning to work in?

view this post on Zulip Heather Macbeth (Oct 01 2020 at 23:54):

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

view this post on Zulip Heather Macbeth (Oct 01 2020 at 23:54):

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

view this post on Zulip Yury G. Kudryashov (Oct 01 2020 at 23:56):

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.

view this post on Zulip Heather Macbeth (Oct 02 2020 at 00:02):

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


Last updated: May 11 2021 at 14:11 UTC