What are the requirements to contributing to Mathlib

Stream: mathlib4

[Planck Anderson]

I have the following assumptions in Lean:

hyp_frac_divergence : Tendsto (fun n ↦ (x (n + 1) - x n) / (y (n + 1) - y n)) atTop atTop
hyp_y_attop : Tendsto y atTop atTop
hyp_y_strictlymono : StrictMono y

I want to prove:

Tendsto x atTop atTop

Intuitively, this follows because the discrete derivative of x over y tends to infinity, and y tends to infinity as well.

Are there any existing lemmas or standard techniques in Lean's mathlib to help prove this directly?
Perhaps something like a monotone comparison principle or a sum lower-bound argument?

why I need to prove it because, I wanna prove stolz theorem when th
e limit is infinite

theorem StolzPosInfinity
    (x : ℕ → ℝ)
    (y : ℕ → ℝ)
    (hyp_y_strictlymono : StrictMono y)
    (hyp_y_attop : Tendsto y atTop atTop)
    (hyp_frac_divergence :
        Tendsto (fun n ↦ (x (n + 1) - x n) / (y (n+1) - y n))
        atTop (atTop : Filter ℝ)
        ) :
    Tendsto (fun n ↦ x n / y n) atTop atTop
:= by

I need

have h_x_at_top : Tendsto x atTop atTop := by sorry

[Kenny Lau]

@Planck Anderson your first code blocks weren't showing properly because you have extra spaces

[Planck Anderson]

Thanks for your reminder！

here are our updated code relevant to this question

we have

h_diff : ∀ n ≥ N₁, x (n+1) - x n > K * (y (n+1) - y n)

we wanna prove this

have h_sum_diff1 : ∀ n ≥ N₁, x n - x N₁ >  K * (y n - y N₁) := by sorry

this is the only "sorry" in our proof to prove the stolz theorem (when the limit is positive infinite

theorem StolzPosInfinity
    -- Stolz Theorem (Case 2) :
    -- Let x(n), y(n) : ℕ → ℝ be two sequences.
    -- Suppose that y(n) is strictly monotone and y(n) → +∞.
    -- If ( x(n + 1) - x_(n) ) / ( y(n + 1) - y(n) ) → +∞, then
    -- x(n) / y(n) → +∞
    (x : ℕ → ℝ)
    (y : ℕ → ℝ)
    (hyp_y_strictlymono : StrictMono y)
    (hyp_y_attop : Tendsto y atTop atTop)
    (hyp_frac_divergence :
        Tendsto (fun n ↦ (x (n + 1) - x n) / (y (n+1) - y n))
        atTop (atTop : Filter ℝ)
        ) :
    Tendsto (fun n ↦ x n / y n) atTop atTop
:= by

We are going to prove the stolz theorm, we proved the theorem when the limit is not infinite successfully

theorem StolzFinite
    -- Stolz Theorem (Case 1) :
    -- Let x(n), y(n) : ℕ → ℝ be two sequences.
    -- Suppose that y(n) is strictly monotone and y(n) → +∞.
    -- If ( x(n + 1) - x_(n) ) / ( y(n + 1) - y(n) ) → L, then
    -- x(n) / y(n) → L
    (x : ℕ → ℝ)
    (y : ℕ → ℝ)
    {L : ℝ}
    (hyp_y_strictlymono : StrictMono y)
    (hyp_y_attop : Tendsto y atTop atTop)
    (hyp_frac_convergence :
        Tendsto (fun n ↦ (x (n + 1) - x n) / (y (n+1) - y n))
        atTop (nhds L)
        ) :
    Tendsto (fun n ↦ x n / y n) atTop (nhds L)

[Planck Anderson]

we wanna use stolz theorem to solve the The problem of the sum of k-squares of natural numbers, but we found there is no such theorem in Mathlib, so our team proved stolz theorem and wanna contribute it to mathlib. As we are all 5-days beginner in lean but with true enthusiasm. The proof may not be readable and simplified enough.

we proved

theorem StolzFinite
    -- Stolz Theorem (Case 1) :
    -- Let x(n), y(n) : ℕ → ℝ be two sequences.
    -- Suppose that y(n) is strictly monotone and y(n) → +∞.
    -- If ( x(n + 1) - x_(n) ) / ( y(n + 1) - y(n) ) → L, then
    -- x(n) / y(n) → L
    (x : ℕ → ℝ)
    (y : ℕ → ℝ)
    {L : ℝ}
    (hyp_y_strictlymono : StrictMono y)
    (hyp_y_attop : Tendsto y atTop atTop)
    (hyp_frac_convergence :
        Tendsto (fun n ↦ (x (n + 1) - x n) / (y (n+1) - y n))
        atTop (nhds L)
        ) :
    Tendsto (fun n ↦ x n / y n) atTop (nhds L)
:= by

theorem StolzPosInfinity
    -- Stolz Theorem (Case 2) :
    -- Let x(n), y(n) : ℕ → ℝ be two sequences.
    -- Suppose that y(n) is strictly monotone and y(n) → +∞.
    -- If ( x(n + 1) - x_(n) ) / ( y(n + 1) - y(n) ) → +∞, then
    -- x(n) / y(n) → +∞
    (x : ℕ → ℝ)
    (y : ℕ → ℝ)
    (hyp_y_strictlymono : StrictMono y)
    (hyp_y_attop : Tendsto y atTop atTop)
    (hyp_frac_divergence :
        Tendsto (fun n ↦ (x (n + 1) - x n) / (y (n+1) - y n))
        atTop (atTop : Filter ℝ)
        ) :
    Tendsto (fun n ↦ x n / y n) atTop atTop
:= by

theorem StolzNegInfinity
    -- Stolz Theorem (Case 3) :
    -- Let x(n), y(n) : ℕ → ℝ be two sequences.
    -- Suppose that y(n) is strictly monotone and y(n) → +∞.
    -- If ( x(n + 1) - x_(n) ) / ( y(n + 1) - y(n) ) → -∞, then
    -- x(n) / y(n) → -∞
    (x : ℕ → ℝ)
    (y : ℕ → ℝ)
    (hyp_y_strictlymono : StrictMono y)
    (hyp_y_attop : Tendsto y atTop atTop)
    (hyp_frac_divergence :
        Tendsto (fun n ↦ (x (n + 1) - x n) / (y (n+1) - y n))
        atTop (atBot : Filter ℝ)
        ) :
    Tendsto (fun n ↦ x n / y n) atTop (atBot : Filter ℝ)
:= by

We think this theorem is really basic in Mathematics analysis, so I hope we can grab this oppotunity to leave our proof in Mathlib, which could inspire us a lot to learn lean in the future.

[Patrick Massot]

If you go to https://leanprover-community.github.io/ and look at the menu, the last section is called “Contributing” and contains several links to web pages explaining the technical process as well and the coding style that is expected. You can study this and then open a contribution proposal. For most people, the first contribution are very tedious, with many comments and modifications. It can be a bit discouraging. But this process is extremely instructive and the greatest way to reach the next level in your Lean training.

[Kenny Lau]

@Planck Anderson if you do decide to go through with the PR, feel free to ping me with the link, and i'll leave some comments. just be prepared, as Patrick said, that you might need to modify it many times.