## Stream: new members

### Topic: nnreal

#### Parivash (Mar 24 2022 at 14:32):

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 (Mar 24 2022 at 14:48):

Do you mean the geometric series? docs#tsum_geometric_nnreal

#### Heather Macbeth (Mar 24 2022 at 14:48):

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

#### Ruben Van de Velde (Mar 24 2022 at 14:52):

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 (Mar 24 2022 at 15:58):

@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 (Mar 24 2022 at 16:00):

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

#### Parivash (Mar 26 2022 at 02:09):

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 (Mar 26 2022 at 02:19):

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

@Johan Commelin
Great, Thanks

#### Parivash (Mar 30 2022 at 01:05):

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 (Mar 30 2022 at 05:47):

@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 (Mar 30 2022 at 06:21):

Start from zero and then take away the zero term

#### Parivash (Mar 30 2022 at 13:15):

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

#### Kevin Buzzard (Mar 30 2022 at 13:25):

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

#### Kevin Buzzard (Mar 30 2022 at 13:26):

There are several ways to sum from 1 in Lean

#### Kevin Buzzard (Mar 30 2022 at 13:26):

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

#### Parivash (Apr 01 2022 at 13:17):

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

#### Kevin Buzzard (Apr 01 2022 at 15:31):

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 (Apr 02 2022 at 00:44):

@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
-- kdes: Constant rate of Adsorption
-- P: Gas Pressure
-- A: Surface Area
-- 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
-- Definitions
(hC: C= y/x)
(hy: y= (k1/k2)*P)
--
(hc: c=k1/k2)
(ha: a=c*V₀)
-- 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 mul_comm C (θ 0) at hVads,
rw hA 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 (Apr 02 2022 at 07:12):

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 (Apr 02 2022 at 07:13):

you can star messages you want to get back to

#### Kevin Buzzard (Apr 02 2022 at 07:58):

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

#### Mario Carneiro (Apr 02 2022 at 07:59):

you need git stash for zulip messages

#### Kevin Buzzard (Apr 02 2022 at 08:03):

"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 (Apr 02 2022 at 08:15):

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,
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 (Apr 02 2022 at 08:48):

The rewrite works fine for me.

#### Parivash (Apr 02 2022 at 11:39):

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

#### Parivash (Apr 03 2022 at 14:46):

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

#### Kevin Buzzard (Apr 03 2022 at 14:50):

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

#### Parivash (Apr 03 2022 at 17:19):

@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 (Apr 03 2022 at 18:08):

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

#### Eric Wieser (Apr 03 2022 at 18:09):

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

#### Eric Wieser (Apr 03 2022 at 18:10):

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

#### Parivash (Apr 03 2022 at 18:17):

@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 (Apr 03 2022 at 18:19):

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

#### Eric Wieser (Apr 03 2022 at 18:20):

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 (Apr 03 2022 at 18:24):

@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 (Apr 03 2022 at 18:25):

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 (Apr 03 2022 at 18:26):

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

#### Kevin Buzzard (Apr 03 2022 at 18:26):

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 (Apr 03 2022 at 18:36):

@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 (Apr 03 2022 at 18:42):

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 (Apr 03 2022 at 18:43):

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

#### Eric Wieser (Apr 03 2022 at 18:45):

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

#### Parivash (Apr 03 2022 at 20:36):

@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 (Apr 03 2022 at 20:37):

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

#### Kevin Buzzard (Apr 03 2022 at 21:04):

Does it make sense?

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

#### Parivash (Apr 03 2022 at 21:13):

@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 (Apr 03 2022 at 21:16):

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

(deleted)

#### Eric Wieser (Apr 04 2022 at 07:11):

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

#### Eric Wieser (Apr 04 2022 at 07:13):

The lemma in question requires add_comm_group, which nnreal is not

#### Parivash (Apr 04 2022 at 11:42):

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

#### Eric Wieser (Apr 04 2022 at 12:51):

For your own work, that would be fine

#### Eric Wieser (Apr 04 2022 at 12:51):

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

#### Kevin Buzzard (Apr 04 2022 at 16:46):

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 },
end


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

#### Parivash (Apr 04 2022 at 18:13):

@Kevin Buzzard
Thank you, professor Kevin Buzzard :)

#### Parivash (Apr 04 2022 at 19:57):

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 },
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
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 (Apr 04 2022 at 20:53):

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 (Apr 04 2022 at 21:46):

@Kevin Buzzard
Excellent, good point!

#### Parivash (Apr 14 2022 at 03:55):

Hi,
How can I use # mul_assoc inside the summation?

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 },
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
simp only [h1] at hVads {single_pass := tt},
rw mul_comm C (θ 0) at hVads,
end


#### Notification Bot (Apr 14 2022 at 04:04):

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

#### Kyle Miller (Apr 14 2022 at 04:06):

@Parivash Does simp_rw [mul_assoc] at hVads work?

@Kyle Miller
Great!
Yes, it works!
Thanks

#### Parivash (Apr 14 2022 at 14:15):

@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 (Apr 17 2022 at 15:36):

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 },
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
simp only [h1] at hVads {single_pass := tt},
--- rw [mul_comm] at hVads, !!!
--- rw nnreal.tsum_coe_mul_geometric_of_norm_lt_1 at hVads, !!!
end


#### Eric Wieser (Apr 17 2022 at 18:09):

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

#### Parivash (Apr 18 2022 at 14:32):

@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 (Apr 18 2022 at 14:48):

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 (Apr 18 2022 at 14:49):

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

#### Parivash (Apr 18 2022 at 15:00):

@Eric Wieser
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 (Apr 18 2022 at 15:01):

(no space after docs#)

#### Eric Wieser (Apr 18 2022 at 15:01):

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

#### Eric Wieser (Apr 18 2022 at 15:01):

Can you paste the whole thing in #backticks

#### Eric Wieser (Apr 18 2022 at 15:02):

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

#### Parivash (Apr 18 2022 at 15:02):

@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,
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,
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 (Apr 18 2022 at 15:04):

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 (Apr 18 2022 at 15:05):

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

#### Parivash (Apr 18 2022 at 15:08):

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 (Apr 18 2022 at 15:09):

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

#### Parivash (Apr 18 2022 at 15:13):

@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 (Apr 18 2022 at 16:15):

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 (Apr 24 2022 at 14:35):

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 },
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 (Apr 24 2022 at 14:36):

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

#### Parivash (Apr 24 2022 at 14:37):

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 },
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
end


#### Parivash (Apr 24 2022 at 14:38):

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

#### Kevin Buzzard (Apr 24 2022 at 14:39):

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 (Apr 24 2022 at 14:42):

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 (Apr 24 2022 at 14:43):

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

Last updated: Dec 20 2023 at 11:08 UTC