index

Stream: new members

[Parivash]

Hi,
how can I define this formula in lean
θ(i)= x(i-1)yθ0
and this one:
∑ {i=0}^{+∞}[i*θi]

[Parivash]

Hi,
how can I define this formula in lean
θ(i)= x(i-1)yθ0
and this one:
∑ {i=0}^{+∞}[i*θi]

[Notification Bot]

This topic was moved here from #general > index by Rob Lewis.

[Stuart Presnell]

I'm not sure what you mean by the first formula. What are x and y here?

[Stuart Presnell]

Also, it will be easier for people to read your mathematical notation in Zulip if you can surround it in #backticks (as explained at this link)

[Parivash]

Actually, this is a formula which is in my mind, and I want to formalize it. x and y and θ are variables, and when the index of θ is i the index of x get i-1 . and another formula related to summation, how we can define ∑ and its range in lean?

[Eric Wieser]

What indices are allowed? Integers? Naturals?

[Arthur Paulino]

@Parivash Is this what you mean?

$$\theta_i(x, y, \theta_0) = x_{i - 1} \times y \times \theta_0$$ $$S(x, y, \theta_0) = \sum_{i = 0}^{+\infty} (i \times \theta_i(x, y, \theta_0))$$

[Arthur Paulino]

Your formulas have some ambiguities and parsing them can be done in multiple ways

[Parivash]

@Arthur Paulino
Yes, exactly, you know how can I formalizing them in Lean?

[Parivash]

@Eric Wieser
Natural numbers

[Arthur Paulino]

Parivash said:

Arthur Paulino
Yes, exactly, you know how can I formalizing them in Lean?

I'm not very familiar with maths in Lean, but in order to get proper help from other members, I think you need to provide more information about your variables. Namely, x, y and θ₀. What are they? Reals? I know x isn't just a real number because it's indexed.

[Parivash]

@Arthur Paulino
i is indices, θ and y and θ0 are variables which their type are naturals.

[Arthur Paulino]

And x?

[Parivash]

@Arthur Paulino
that's also natural

[Parivash]

@Arthur Paulino
I want to show that
teta(2)=x(1) * y * teta0
teta(3)=x(2) * y * teta0
teta(4)=x(3) * y * teta0
and ...
so we can say :
teta(i)=x(i-1) * y * teta0
does it make sense?

[Arthur Paulino]

I don't understand how you're indexing a natural number

[Parivash]

@Arthur Paulino
i=1,2,3,4,...
what is the problem?

[Arthur Paulino]

The problem is that $x_{i-1}$ is coming out of nowhere when computing $\theta_i$ with input $x, y, \theta_0$

[Kyle Miller]

@Parivash Probably the first step to formalize something on a computer is to make sure it's formalized on paper. That means specifying what all the symbols are and their types.

It might be clear to you what this is all supposed to mean, but if we don't know exactly what you mean, it's hard to guess which way to formalize it in Lean.

[Kyle Miller]

Parivash said:

i=1,2,3,4,...
what is the problem?

In your original sum, it starts with i=0. Is this a correction?

If the sum starts with i=0, then you have $\theta_0$, which has $x_{-1}$ in it, which is why I think Eric was asking about whether the indices might be integers.

[Kyle Miller]

For example, maybe you mean x denotes real numbers indexed by naturals (starting with 0)? In lean that would be x : nat -> real

[Stuart Presnell]

(deleted)

[Parivash]

@Arthur Paulino
oooh, i got it,
i start with 1 and (i-1) is power
that's this
teta(i) = x ^ (i-1) * y * teta0
so, we have
teta(1)= x^ (0) * y * teta0 = y* teta0
teta(2) = x^ (1) * y * teta0
teta(3) = x ^(2) * y * teta0
sorry, this is my mistake, i-1 is power of x, and i is index of teta

[Parivash]

@Kyle Miller
sum is start with 0

[Stuart Presnell]

So you have an initial value θ0 and two numbers x and y. From this data you're defining a sequence of values of θi, where:

θ1 = (x^0) * y * θ0
θ2 = (x^1) * y * θ0
θ3 = (x^2) * y * θ0
...

And then you want the sum S = ∑ i * θi. Is that correct?

[Parivash]

@Stuart Presnell
exactlly

[Stuart Presnell]

If that's right then the y * θ0 factors out of the sum:

$$S = θ_0 + ∑_{i=1}^{∞} i * θ_i \\ = θ_0 + ∑_{i=1}^{∞} i * x^{i-1} * y * θ_0 \\ = θ_0 + y * θ_0 * ∑_{i=1}^{∞} i * x^{i-1}$$

[Stuart Presnell]

So the sum in the last line is 1 + 2x + 3x^2 + 4x^3 + ...

[Stuart Presnell]

So if x is a positive natural number then this summation diverges to infinity.

[Parivash]

@Stuart Presnell
let me provide a hand writing of proof: CamScanner-02-17-2022-16.54.pdf

[Parivash]

@Stuart Presnell
Sorry, Please start it with i= 0 and consider this suggestion C=y/x
So, that will be correct

[Parivash]

@Stuart Presnell
if it is not clear let me know

[Stuart Presnell]

Ok, I could follow that

[Stuart Presnell]

Again, if x is a natural number then your two sums are infinite

[Stuart Presnell]

I'll have to leave the thread now, but I'm sure someone else can help you now that we can better see what you're doing.

[Parivash]

@Stuart Presnell
No, we can use this assumption
sum (i=1 to infity)(x^i) = x/(1-x)

[Parivash]

@Stuart Presnell
and
sum (i=1 to infity)(i*x^i) = x/(1-x)^2

[Kyle Miller]

Parivash said:

No, we can use this assumption
sum (i=1 to infity)(x^i) = x/(1-x)

That's valid iff $\lvert x\rvert < 1$, so if $x$ is a positive natural number it can't be applied.

[Parivash]

@Kyle Miller
yes, we can apply this condition, that works

[Parivash]

?

[Parivash]

(deleted)

[Parivash]

(deleted)

[Kevin Buzzard]

right now you are asserting something false, and Lean can only do true things, so we are stuck.

[Arthur Paulino]

I honestly still haven't understood what you're intending to do mathematically, sorry.
You have presented a θ function and a formula that does a summation on θ. But I don't know what you're trying to prove with those.
I'd recommend a cleaner (fresh) start on this thread so more people have an easier time jumping in.
You can start by writing your equations in a non-ambiguous way and then explicitly stating what you want to prove with them

[Parivash]

@Arthur Paulino
Okay, Let's explain everything clearly, I'm sure formula is true, that's hand writing proof.

[Stuart Presnell]

Just on the issue of using indices: for any type α (e.g. the reals or the natural numbers), an infinite sequence of terms of that type can be represented by a function f : ℕ → α. So then you have terms f 0, f 1, f 1, etc.

[Stuart Presnell]

Another thing to remember is that Lean/mathlib is based on proofs rather than calculations. In some mathematics software, like Mathematica or Maple, you might type in an expression and the get the computer to do a series of operations, transformations, and calculations on it. For example, you might type in a summation and hope that the software can work out the answer. But mathlib isn't like that — in general it can't work out calculations for you. [Perhaps you already know this. But I just want to make sure you're not hoping to use mathlib for something it's not suited for.]

[Stuart Presnell]

In mathlib you're always working toward a proof of some statement that you've written. So you have to have a particular destination in mind: a theorem statement that you want to prove. If you can state clearly what theorem you're trying to prove, then perhaps people here can help you to state it in the formal language of mathlib, and to prove it.

[Stuart Presnell]

One more thing: because mathlib is based in type theory, it demands to know the type of every variable you write down. So if you write a formula involving some variable x you need to say what kind of a thing x is — what type it belongs to (i.e. a real number, a natural number, an integer, etc.) You also need to state explicitly any facts you're assuming about the variables you use: for example, if |x| < 1 then you'll need to say this explicitly. The level of detail required can be quite surprising: sometimes when we're formalising a proof we discover that we were assuming things that seem so obvious that we didn't even think about them!

[Parivash]

@Stuart Presnell
your means that I cannot formulize formula in a way which is written by humans?
I need to write sequence of formula to prove my final goal

[Arthur Paulino]

Parivash, I think you could try tackling simpler problems on paper first. Just to get familiar with the mathematical "proving dialect". There's a certain way to say things in mathematics that I don't think you're quite familiar with yet.

If you look at mathematical sources, they're not just sequences of symbols and formulas. Mathematical texts are... well... texts. And throughout the texts, you should be able to understand the intention of the author as you read it.

[Stuart Presnell]

You certainly can write a formal proof in a way that looks similar to the proofs you would write on paper. If you're trying to prove an equation between two formulas A = Z, and your paper proof involves writing a sequence of formulas B, C, D, ... and showing that A = B, B = C, C = D, etc. then you can write a formal proof that follows the same pattern.

[Parivash]

@Stuart Presnell
Yes, I just want to write a formal proof,
you know many of equations that I used are hypothesis and we accept it like Vads and A formula that I introduce you previously, I just want to substitute them in main formula but I don't know how to write sigma or apply index!

[Stuart Presnell]

If you post a link to the PDF that you sent to me then someone may show you how to write some of the formulas. If not, I’ll try to do this tomorrow.

[Parivash]

@Stuart Presnell
I really appreciated. I posted it as formalizing formula. Thanks