nnreal

Stream: new members

[Parivash]

Hi,
I want to use this assumption $\sum_{i=0}^{+\infty} i*x_{i} = \frac{x}{1-x}$ for R>=0
I find this tactics tsum_coe_mul_geometric_of_norm_lt_1 , but it doesn't work for nnreal. Is there similar tactic for R>=0, or I should prove it for nnreal?

[Heather Macbeth]

Do you mean the geometric series? docs#tsum_geometric_nnreal

[Heather Macbeth]

Note that that's not what you wrote (you have some unspecified sequence $x_i$)

[Ruben Van de Velde]

Note that that's a theorem, not a tactic. Converting is a little annoying:

theorem nnreal.tsum_coe_mul_geometric_of_norm_lt_1 {r : ℝ≥0} (hr : r < 1) :
  ∑' (n : ℕ), (↑n) * r ^ n = r / (1 - r) ^ 2 :=
begin
  have hr' : ∥(r : ℝ)∥ < 1,
  { rw [real.norm_eq_abs, abs_lt],
    split,
    { refine lt_of_lt_of_le _ r.coe_nonneg, norm_num },
    { exact_mod_cast hr } },
  apply nnreal.coe_injective,
  convert tsum_coe_mul_geometric_of_norm_lt_1 hr',
  { norm_cast },
  { push_cast,
    rw nnreal.coe_sub hr.le,
    norm_cast },
end

[Parivash]

@Heather Macbeth
Thanks for your response, yes your right that's for $$ \sum_{i=o}{\infity}x_{i} = \frac{1}{1-x} $$ but I'm looking for another one.

[Parivash]

@Ruben Van de Velde
I really appreciated. Yes, That's the one I'm looking. Thank you

[Parivash]

What is the tactic for multiplying both side of equation to a constant. like $\frac {q}{v} = \frac{m}{n}$ is equal to $q = \frac{m}{n} \times v$

[Johan Commelin]

If you have a proof hv : v ≠ 0, then field_simp [hv] will usually do this for you.

[Parivash]

@Johan Commelin
Great, Thanks

[Parivash]

I want to use this assumption $\sum_{i=1}^{+\infty} x_{i} = \frac{x}{1-x}$
I find this tactic (tsum_geometric_nnreal), but it starts from zero instead of one. How can I tackle this issue?

[Johan Commelin]

@Parivash Do you already know how you would like to write your statement in Lean? Is it an issue to start the sum from i = 0? You will probably find that a lot of lemmas work more smoothly if you start from i = 0.

[Kevin Buzzard]

Start from zero and then take away the zero term

[Parivash]

@Johan Commelin
Actually, my handwriting proof was arranged in this shape. And, this is the last step of my proofing.

[Kevin Buzzard]

Write a #mwe if you're not sure how to prove something, so it's clear what the statement you want is.

[Kevin Buzzard]

There are several ways to sum from 1 in Lean

[Kevin Buzzard]

PS docs#tsum_geometric_nnreal is a theorem, not a tactic.

[Parivash]

@Kevin Buzzard
would you please introduce one of them which start from one and works for nnreal

[Kevin Buzzard]

Can you formalise the statement which you would like a proof of via a #mwe? In Lean it's not good enough just to say "how do I prove $\sum_{n\geq1}x^n=x/(1-x)$?" -- there are different ways of formalising this statement.

[Parivash]

@Kevin Buzzard

/- Background Copy-/
import analysis.specific_limits
import data.real.basic
import tactic
import algebra.group.defs
import logic.function.basic
import topology.algebra.infinite_sum
import topology.algebra.group_with_zero
import set_theory.ordinal_arithmetic
import algebra.geom_sum
import order.filter.archimedean
import order.iterate
import topology.instances.ennreal
import algebra.ring.boolean_ring
open ordinal
/- left_comm has_mul.mul mul_comm mul_assoc-/
mul_eq_of_eq_div' (h : b = c / a) : a * b = c :=
begin simp [h], rw [mul_comm c, mul_inv_cancel_left] end
/-!
# Topology on `ℝ≥0`
The natural topology on `ℝ≥0` (the one induced from `ℝ`), and a basic API.
## Main definitions
Instances for the following typeclasses are defined:
* `topological_space ℝ≥0`
* `topological_semiring ℝ≥0`
* `second_countable_topology ℝ≥0`
* `order_topology ℝ≥0`
* `has_continuous_sub ℝ≥0`
* `has_continuous_inv' ℝ≥0` (continuity of `x⁻¹` away from `0`)
Everything is inherited from the corresponding structures on the reals.
## Main statements
Various mathematically trivial lemmas are proved about the compatibility
of limits and sums in `ℝ≥0` and `ℝ`. For example
* `tendsto_coe {f : filter α} {m : α → ℝ≥0} {x : ℝ≥0} :
tendsto (λa, (m a : ℝ)) f (𝓝 (x : ℝ)) ↔ tendsto m f (𝓝 x)`
says that the limit of a filter along a map to `ℝ≥0` is the same in `ℝ` and `ℝ≥0`, and
* `coe_tsum {f : α → ℝ≥0} : ((∑'a, f a) : ℝ) = (∑'a, (f a : ℝ))`
says that says that a sum of elements in `ℝ≥0` is the same in `ℝ` and `ℝ≥0`.
Similarly, some mathematically trivial lemmas about infinite sums are proved,
a few of which rely on the fact that subtraction is continuous.
-/
noncomputable theory
open set topological_space metric filter
open_locale topological_space
namespace nnreal
open_locale nnreal big_operators
instance : topological_space ℝ≥0 := infer_instance -- short-circuit type class inference
section coe
variable {α : Type*}
variables [t2_space α]
-- Definitions of nnreal.tsum_coe_mul_geometric_of_norm_lt_1
theorem nnreal.tsum_coe_mul_geometric_of_norm_lt_1 {r : ℝ≥0} (hr : r < 1) :
∑' (n : ℕ), (↑n) * r ^ n = r / (1 - r) ^ 2 :=
begin
have hr' : ∥(r : ℝ)∥ < 1,
{ rw [real.norm_eq_abs, abs_lt],
split,
{ refine lt_of_lt_of_le _ r.coe_nonneg, norm_num },
{ exact_mod_cast hr } },
apply nnreal.coe_injective,
convert tsum_coe_mul_geometric_of_norm_lt_1 hr',
{ norm_cast },
{ push_cast,
rw nnreal.coe_sub hr.le,
norm_cast },
end
-- k1 : constant rate of condensation onto bare surface
-- k2: constant rate of evaporation from first layer
-- kads: Constant rate of Adsorption
-- kdes: Constant rate of Adsorption
-- P: Gas Pressure
-- q: Loading
-- A: Surface Area
-- Vads: volume adsorbed
-- V₀ : the volume of one adsorbed molecule
-- a, b, c, C, x, y : variables
lemma some_name (θ : ℕ → ℝ≥0 )(k1 k2 kads kdes a b C P q A V₀ Vads x y c: ℝ≥0 )
-- Equations
(hA : A = θ 0 + ∑' (k : ℕ), C * (θ 0 * x ^ k )) -- Total Surface Area
(hVads : Vads = 0 * θ 0 + ∑' (k : ℕ), C * ( θ 0 * (k * x ^ k))) -- total volume of adsorbed molecules
(hq : q/V₀ = Vads / A) -- The experimental observable loading
-- Definitions
(hC: C= y/x)
(hy: y= (k1/k2)*P)
(hx: x=(kads/kdes)*P)
--
(hc: c=k1/k2)
(ha: a=c*V₀)
(hb: b= kads/kdes)
-- Constraints
(hθ: θ 0 ≠ 0)
(hx2: x<1)
(hp: P ≠ 0)
(hx1: x ≠ 0)
(hv: V₀ ≠ 0)
:
q = a*P/((1-b*P)*(1-b*P+c/b))
:=

begin
rw tsum_mul_left at hA,
rw tsum_mul_left at hA,
rw ← mul_assoc at hA,
rw mul_comm C (θ 0) at hA,
rw ← mul_one (θ 0) at hA,
rw mul_assoc at hA,
rw mul_assoc at hA,
rw ← mul_add (θ 0) at hA,
rw one_mul at hA,
rw zero_mul at hVads,
rw zero_add at hVads,
rw tsum_mul_left at hVads,
rw tsum_mul_left at hVads,
rw ← mul_assoc at hVads,
rw mul_comm C (θ 0) at hVads,
rw mul_assoc at hVads,
rw hA at hq,
rw hVads at hq,
rw mul_div_mul_left at hq,
rw tsum_geometric_nnreal at hq,
end

In the last line I used tsum_geometric_nnreal, which it starts from zero. While I want to change it to one, so it should be x/(1-x) instead of 1/(1-x)

[Kevin Buzzard]

Thanks. I'm not at lean right now and Zulip doesn't have a "mark message unread" functionality do hopefully I'll remember to take a look later if nobody else does beforehand

[Mario Carneiro]

you can star messages you want to get back to

[Kevin Buzzard]

My number of starred messages is about to hit four figures :-/

[Mario Carneiro]

you need git stash for zulip messages

[Kevin Buzzard]

"I'm not at Lean right now" is (for me) usually a euphemism for "I'm still in bed". OK so I got up. @Parivash your code doesn't compile for me. Maybe test it on a new file?

[Kevin Buzzard]

@Parivash here is a more helpful way to ask your question:

import topology.instances.ennreal

open_locale nnreal

example (θ : ℕ → ℝ≥0)
  (k1 k2 kads kdes a b C P q A V₀ Vads x y c : ℝ≥0)
  (hq : q / V₀ =
          (C * ∑' (x_1 : ℕ), ↑x_1 * x ^ x_1) /
            (1 + C * ∑' (x_1 : ℕ), x ^ x_1)) : false :=
begin
  --rw tsum_geometric_nnreal at hq,
  admit,
end

This is called a minimal working example, a #mwe . I have removed all the irrelevant junk from your question (using the extract_goal tactic and the delete key) and we now have a question which hopefully represents something close to what you're asking about. Please learn these tricks in future, because if you don't ask good questions then multiple users have to take time doing the same work which you could have done.

[Kevin Buzzard]

The rewrite works fine for me.

[Parivash]

@Kevin Buzzard
Yes, your right. I'll do it.
Thanks

[Parivash]

Is there any other thought for taking out zero from this lemma docs#tsum_geometric_nnreal, or proving it for nnreal?

[Kevin Buzzard]

Can you write the lean code for what you actually want, rather than just repeating an informal description? Please read about #mwe

[Parivash]

@Kevin Buzzard
Okay, got it.
I'm seeking a way to prove this one:

import analysis.specific_limits
import data.real.basic
namespace nnreal
open_locale nnreal big_operators
lemma some_name (θ : ℕ → ℝ≥0 )(C q A B x: ℝ≥0 )
(hA : A = θ 0 * (1 + C * ∑' (k : ℕ), x ^ k )) :
q = θ 0 * (1 + C * (x/(1-x)))
:=
begin
sorry,
end

[Eric Wieser]

That's untrue (choose q = 1, θ = 0)

[Eric Wieser]

It's like saying "A = 1, prove q = 2` when you've given absolutely no information linking A and q.

[Eric Wieser]

Oh, I guess you meant to write A in both places?

[Parivash]

@Eric Wieser
Actually, the only thing that is important here is that applying this assumption $$\sum{i=1}{\+ infinity} x ^ i = x/(1-x) $$ of course this condition is true there (x<1)

[Eric Wieser]

Parivash, do you understand why your statement above is unprovable?

[Eric Wieser]

It's for the same reason that this is unprovable

lemma some_name (A q : ℝ≥0) (hA : A = 1) : q = 1 :=
begin
  sorry,
end

[Parivash]

@Eric Wieser
Eric, this is just part of proofing, I write this one to show what lemma I'm looking for, you know what I mean!

[Eric Wieser]

The idea behind a #mwe is that I don't have to try and work out what you mean, because the mwe should contain everything I need to know

[Eric Wieser]

So in this case, your #mwe is too minimized to actually demonstrate your problem any more

[Kevin Buzzard]

import analysis.complex.basic
import data.real.basic
namespace nnreal
open_locale nnreal big_operators
lemma some_name (θ : ℕ → ℝ≥0 )(C q A B x: ℝ≥0 )
(hA : A = θ 0 * (1 + C * ∑' (k : ℕ), x ^ k )) :
q = θ 0 * (1 + C * (x/(1-x)))
:=
begin
  rw tsum_geometric_nnreal at hA,
  -- works fine
sorry, sorry,
end
end nnreal

[Parivash]

@Kevin Buzzard
Thanks.
But actually, I need to use this assumption $\sum_{i=1}^{+\infty} x^{i} = \frac{x}{1-x}$
not this one :
$\sum_{i=0}^{+\infty} x^{i} = \frac{1}{1-x}$
Just we should change its starting point that I cannot find the lemma for it

[Eric Wieser]

Kevin Buzzard said:

Can you write the lean code for what you actually want, rather than just repeating an informal description? Please read about #mwe

@Parivash, the lean code you wrote didn't express what you actually wanted, which is why Kevin's answer didn't help you

[Eric Wieser]

Do you know how to state the assumption you actually want in lean?

[Yaël Dillies]

You want docs#tsum_eq_zero_add

[Eric Wieser]

You certainly will want that, but far more useful will be to first work out precisely how to state your question in lean

[Parivash]

@Yaël Dillies
Yes, in order to use this one I defined this one: (h1 : ∀ k, θ (k) = C * x ^ k * θ 0) and then use this: (hA : A = ∑' k, θ k)
But this doesn't work here because $\theta k$ starts from one not zero. So, I cannot use: docs#tsum_eq_zero_add.
Does it make sense?

[Yaël Dillies]

Once again, we are lacking context. Why does θ start at 1. Does that mean you're using docs#pnat?

[Kevin Buzzard]

Does it make sense?

No. The only thing that makes sense here is a #mwe . Click on the link.

[Parivash]

@Yaël Dillies
base on the equation 18 from this article $\theta$ must be start from one (in this article S represent $\theta$
Brunauer38-BET-theory1.pdf
Moreover, if we check this formula for k=0 we have θ 0 = C * θ 0, which is not correct. That's why I need to change starting point

[Yaël Dillies]

So what about formulating it as ∀ n, θ (n + 1) = C * θ 0 * x ^ (n + 1)? This will be much easier to use in the proof.

[Parivash]

(deleted)

[Eric Wieser]

@Parivash, your deleted comment looks like a valid point to me

[Eric Wieser]

The lemma in question requires add_comm_group, which nnreal is not

[Parivash]

@Eric Wieser
Yes, docs#tsum_eq_zero_add cannot be applied for nnreal. So, first, we should define such lemma for nnreal.

[Eric Wieser]

For your own work, that would be fine

[Eric Wieser]

But for mathlib, we might want to think about whether the lemma is still true under weaker assumptions

[Kevin Buzzard]

Here's a hack which proves it in the nnreal case:

import topology.algebra.infinite_sum
import topology.instances.nnreal

open_locale nnreal big_operators

theorem nnreal.tsum_eq_zero_add {f : ℕ → ℝ≥0} (hf : summable f) :
∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1) :=
begin
  apply subtype.ext,
  push_cast,
  let g : ℕ → ℝ := λ n, f n,
  have hg : summable g,
  { apply summable.map hf (nnreal.to_real_hom : ℝ≥0 →+ ℝ) continuous_induced_dom },
  exact tsum_eq_zero_add hg,
end

I just reduce to the case of reals and then use tsum_eq_zero_add there.

[Parivash]

@Kevin Buzzard
Thank you, professor Kevin Buzzard :)

[Parivash]

First, I hope that I followed #mwe rules here. If else, please give me some suggestions that I learn better.
@Yaël Dillies , I followed docs#tsum_eq_zero_add, and finally reach the below code. It was useful, but still, my problem doesn't solve.
As you see, tsum_geometric_nnreal, doesn't work here. Because instead of x^n, now we have x^(n+1)! Please look at the below code. So, do you have any suggestions to tackle this issue?

import analysis.complex.basic
import data.real.basic
namespace nnreal
open_locale nnreal big_operators

theorem nnreal.tsum_eq_zero_add {f : ℕ → ℝ≥0} (hf : summable f) :
∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1) :=
begin
  apply subtype.ext,
  push_cast,
  let g : ℕ → ℝ := λ n, f n,
  have hg : summable g,
  { apply summable.map hf (nnreal.to_real_hom : ℝ≥0 →+ ℝ) continuous_induced_dom },
  exact tsum_eq_zero_add hg,
end

lemma some_name (θ : ℕ → ℝ≥0 )(A C x q: ℝ≥0 )
-- Equations
(h1 : ∀ k, θ (k+1) = C * (θ 0 * x ^ (k+1))) (hA : A = ∑' (k : ℕ), θ k) -- Total Surface Area
(hx2: x<1)
: A = θ 0 *(1+C*(x/(1-x))) :=
begin
rw nnreal.tsum_eq_zero_add at hA,
simp only [h1] at hA {single_pass := tt},
rw tsum_mul_left at hA,
rw tsum_mul_left at hA,
rw ← mul_assoc at hA,
rw mul_comm C (θ 0) at hA,
rw ← mul_one (θ 0) at hA,
rw mul_assoc at hA,
rw mul_assoc at hA,
rw ← mul_add (θ 0) at hA,
rw one_mul at hA,
--rw tsum_geometric_nnreal at hA,
end

[Kevin Buzzard]

Just rewrite x^(n+1) as x^n*x and then take out the common factor of x from the sum. You see that you don't need the sum from 1?

simp_rw [pow_add, pow_one, tsum_mul_right] at hA,
rw tsum_geometric_nnreal hx2 at hA,

[Parivash]

@Kevin Buzzard
Excellent, good point!

[Parivash]

Hi,
How can I use # mul_assoc inside the summation?
Please fine code here:

import topology.algebra.infinite_sum
import topology.instances.nnreal
namespace nnreal
open_locale nnreal big_operators

theorem nnreal.tsum_eq_zero_add {f : ℕ → ℝ≥0} (hf : summable f) :
∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1) :=
begin
  apply subtype.ext,
  push_cast,
  let g : ℕ → ℝ := λ n, f n,
  have hg : summable g,
  { apply summable.map hf (nnreal.to_real_hom : ℝ≥0 →+ ℝ) continuous_induced_dom },
  exact tsum_eq_zero_add hg,
end

lemma some_name (θ : ℕ → ℝ≥0 )(C Vads x: ℝ≥0  )
-- Equations
(h1 : ∀ k, θ (k+1) = C * θ 0 * x ^ (k+1))
(hVads : Vads =  ∑' (k : ℕ),  k * θ k)
:
Vads = θ 0 * (C * ∑' (k : ℕ), k * x ^ k)
:=
begin
rw nnreal.tsum_eq_zero_add at hVads,
simp only [h1] at hVads {single_pass := tt},
simp at hVads,
rw mul_comm C (θ 0) at hVads,
--rw mul_assoc at hVads, !!
end

[Notification Bot]

A message was moved here from #rss > Recent Commits to mathlib:master by Kyle Miller.

[Kyle Miller]

@Parivash Does simp_rw [mul_assoc] at hVads work?

[Parivash]

@Kyle Miller
Great!
Yes, it works!
Thanks

[Parivash]

@Kyle Miller
Is there any way for changing the location of x^(x_1+1) with (x_+1).
Note: The above code is edited based on my new request.

[Parivash]

Hi,
I faced with an issue in closing this goal. Please find it here:

import analysis.complex.basic
import data.real.basic
namespace nnreal
open_locale nnreal big_operators

theorem nnreal.tsum_eq_zero_add {f : ℕ → ℝ≥0} (hf : summable f) :
∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1) :=
begin
  apply subtype.ext,
  push_cast,
  let g : ℕ → ℝ := λ n, f n,
  have hg : summable g,
  { apply summable.map hf (nnreal.to_real_hom : ℝ≥0 →+ ℝ) continuous_induced_dom },
  exact tsum_eq_zero_add hg,
end


theorem nnreal.tsum_coe_mul_geometric_of_norm_lt_1 {r : ℝ≥0} (hr : r < 1) :
∑' (n : ℕ), (↑n) * r ^ n = r / (1 - r) ^ 2 :=
begin
have hr' : ∥(r : ℝ)∥ < 1,
{ rw [real.norm_eq_abs, abs_lt],
split,
{ refine lt_of_lt_of_le _ r.coe_nonneg, norm_num },
{ exact_mod_cast hr } },
apply nnreal.coe_injective,
convert tsum_coe_mul_geometric_of_norm_lt_1 hr',
{ norm_cast },
{ push_cast,
rw nnreal.coe_sub hr.le,
norm_cast },
end

--- repeat
lemma some_name (θ : ℕ → ℝ≥0 )(C Vads x: ℝ≥0  )
-- Equations
(h1 : ∀ k, θ (k+1) = C * θ 0 * x ^ (k+1))
(hVads : Vads =  ∑' (k : ℕ),  k * (θ k))
:
Vads = θ 0 * (C * (x/(1-x)^2))
:=
begin
rw nnreal.tsum_eq_zero_add at hVads,
simp only [h1] at hVads {single_pass := tt},
simp at hVads,
simp_rw [mul_assoc] at hVads,
simp_rw [mul_comm] at hVads,
simp_rw [mul_assoc] at hVads,
rw tsum_mul_left at hVads,
rw tsum_mul_left at hVads,
--- rw [mul_comm] at hVads, !!!
--- rw nnreal.tsum_coe_mul_geometric_of_norm_lt_1 at hVads, !!!
end

[Eric Wieser]

What's your goal state at the end of that lemma?

[Parivash]

@Eric Wieser
It is a formula in Chemical Engineering, and I want to formalize it. I edited it, now just I don't know how to apply # tsum_geometric_nnreal and # nnreal.tsum_coe_mul_geometric_of_norm_lt_1.
Actually, I think I should rearrange it, but since it is inside the summation mul_comm, and mul_ assoc don't work! This is my issue!

[Eric Wieser]

By "what's your goal state", I mean "please paste what's in your 'Lean infoview' at the point where you get stuck"

[Eric Wieser]

(note that to link to a lemma, you need docs# before it, not just #)

[Parivash]

@Eric Wieser
Thanks for clarifying, I hope that now I answere your question!
This is the error after applying docs# tsum_geometric_nnreal :
rewrite tactic failed, did not find instance of the pattern in the target expression
∑' (n : ℕ), x ^ n

[Eric Wieser]

(no space after docs#)

[Eric Wieser]

That's not the entire goal state, that's just the error

[Eric Wieser]

Can you paste the whole thing in #backticks

[Eric Wieser]

The bit including the ⊢ and the : lines before it is the "goal state

[Parivash]

@Eric Wieser
Sure,

rewrite tactic failed, did not find instance of the pattern in the target expression
  ∑' (n : ℕ), ↑n * ?m_1 ^ n
state:
2 goals
θ : ℕ → ℝ≥0,
C Vads x : ℝ≥0,
h1 : ∀ (k : ℕ), θ (k + 1) = C * θ 0 * x ^ (k + 1),
hx2 : x < 1,
hx1 : x ≠ 0,
hVads : Vads = C * (θ 0 * (x * ∑' (x_1 : ℕ), (x ^ x_1 * ↑x_1 + x ^ x_1)))
⊢ Vads = θ 0 * (C * (x / (1 - x) ^ 2))

θ : ℕ → ℝ≥0,
C Vads x : ℝ≥0,
h1 : ∀ (k : ℕ), θ (k + 1) = C * θ 0 * x ^ (k + 1),
hVads : Vads = ∑' (k : ℕ), ↑k * θ k,
hx2 : x < 1,
hx1 : x ≠ 0
⊢ summable (λ (b : ℕ), ↑b * θ b)

[Eric Wieser]

Yes, the problem is that it doesn't match! The sum in hVads has a + in it, you probably want to try and pull that out of the sum

[Eric Wieser]

(note you should be looking at the first goal, not the second)

[Parivash]

Yes, I'm seeking a way to apply docs#tsum_geometric_nnreal and docs#nnreal.tsum_coe_mul_geometric_of_norm_lt_1.
I cannot rearrange hVads in a way to apply these!

[Kevin Buzzard]

rw tsum_geometric_nnreal hx2 at hVads -- do you understand why this fails?

[Parivash]

@Kevin Buzzard
Yes, I think, I need to change the location of x^x_1 with x_1 and of course, separate this assumption after $+$

[Kevin Buzzard]

Right, so you will need to find a result which says that the sum of (a_n + b_n) equals the sum of the a_n plus the sum of the b_n, and rewrite that first, and then you will be able to do the rewrite you want to do on the term which matches. The lemma you need will be called something like tsum_add or something like this, because we have a naming convention which says what lemmas like this should be called.

[Parivash]

Kevin Buzzard said:

Here's a hack which proves it in the nnreal case:

import topology.algebra.infinite_sum
import topology.instances.nnreal

open_locale nnreal big_operators

theorem nnreal.tsum_eq_zero_add {f : ℕ → ℝ≥0} (hf : summable f) :
∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1) :=
begin
  apply subtype.ext,
  push_cast,
  let g : ℕ → ℝ := λ n, f n,
  have hg : summable g,
  { apply summable.map hf (nnreal.to_real_hom : ℝ≥0 →+ ℝ) continuous_induced_dom },
  exact tsum_eq_zero_add hg,
end

I just reduce to the case of reals and then use tsum_eq_zero_add there.

Actually, as I applied this: nnreal.tsum_eq_zero_add , it added another goal like summable. How can I close this goal?

[Kevin Buzzard]

I don't know -- what's the goal? What's the tactic state? Do you know the maths proof?

[Parivash]

let me provide its code:

import analysis.complex.basic
import data.real.basic
namespace nnreal
open_locale nnreal big_operators

theorem nnreal.tsum_eq_zero_add {f : ℕ → ℝ≥0} (hf : summable f) :
∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1) :=
begin
  apply subtype.ext,
  push_cast,
  let g : ℕ → ℝ := λ n, f n,
  have hg : summable g,
  { apply summable.map hf (nnreal.to_real_hom : ℝ≥0 →+ ℝ) continuous_induced_dom },
  exact tsum_eq_zero_add hg,
end

lemma some_name (θ : ℕ → ℝ≥0 )(k1 k2 kads kdes a b C P q A V₀ Vads x y c: ℝ≥0  )
-- Equations
(h1 : ∀ k, θ (k+1) = (x ^ (k+1)) * C * θ 0) (hA : A = ∑' (k : ℕ), θ k)
-- Definitions

:
q = a*P/((1-b*P)*(1-b*P+c*P))
:=
begin
rw nnreal.tsum_eq_zero_add at hA,
end

[Parivash]

I could close the first goal, but I don't have any idea about the second one!

[Kevin Buzzard]

This is not a Lean question -- this is a mathematics question. your strategy is only mathematically valid if that sum converges so you need to find a maths proof that it conerges.

[Kevin Buzzard]

In maths we would not normally talk about an infinite sum $\sum_n a_n$ unless it converges. But Lean is different. It will allow you to write ∑' (b : ℕ), f b whether or not the sum converges, and it just defines the sum to be 0 if mathematically the sum doesn't converge. The convergence assumptions are still needed though, it's just that the theorems ask for them rather than the definitions.

[Kevin Buzzard]

You have a hypothesis A = ∑' (k : ℕ), θ k but perhaps this doesn't mean what you think it means. It doesn't mean "the sum is convergent and equals A", it means "either the sum is convergent and it equals A, or the sum does not converge and A=0".