Formalizing formula

Stream: new members

[Parivash]

Hi,
How can I formulize this formula in Lean?
image.png

[Alex J. Best]

Without more context its not clear what the things in the formula are to us, so its difficult to say what formalizing that would even mean. Are they vectors with cross product for example? or is x just some multiplication operation

[Parivash]

x, y, teta0, and teta are variables which can be considered as positive numbers, actually I don't know how to use indices here.

[Riccardo Brasca]

You should try to be more precise, Lean is very very picky about precision... at the end this is one of the reason why we formalize.

What do you mean by "one dimensional variables"? Elements of a one-dimensional vector space (over ℝ?)?

[Parivash]

@Riccardo Brasca
did you know how to use indices here?

[Riccardo Brasca]

In VS Code you can write f \ 3 (without the spaces) to get f₃.

[Parivash]

@Riccardo Brasca
No, my means is it change from 1 to infinity

[Riccardo Brasca]

I don't understand your question...

[Yury G. Kudryashov]

A sequence is usually represented as a map from natural numbers to some type.

[Parivash]

Actually, This is what I'm trying to formulize:
Proof-Shape.pdf

[Yury G. Kudryashov]

This is a sequence of formulas, not a text.

[Yury G. Kudryashov]

If you want to formalize something, I suggest that first you write it down with all the details. Imagine that you're writing a paper but the reader is going to (pretend to) be a very dumb person.

[Yury G. Kudryashov]

So, you should write all the "theorem", "consider a sequence of real/ rational/ integer/... numbers" etc

[Parivash]

@Yury G. Kudryashov
Okay, then how can I relate these theorems to each other?
Because my final formula depends on all theorems.

[Yury G. Kudryashov]

Before answering this question, I need to see a textbook/paper quality text, not a sequence of formulas. E.g., what mathematical theorem are you trying to prove (with all "let ..., then ...")?

[Parivash]

@Yury G. Kudryashov
the last formula which is written in pdf.

[Yury G. Kudryashov]

The last formula is a formula, not a statement of a theorem.

[Parivash]

@Yury G. Kudryashov
you know there are some formula like Vads, A, and \theta, that we just consider them as assumption, and then substitute them in formula.

[Parivash]

@Yury G. Kudryashov
Yes, that's formula, it should not be formula?

[Yury G. Kudryashov]

What is your background? Math/CS/...? Undergrad/grad/...?

[Parivash]

I'm PhD, Chemical engineering

[Parivash]

Now I want to formuliz equations in chemical engineering.

[Yury G. Kudryashov]

You can't formalize equations. You can formalize theorems. E.g.,

For any natural number $n$, we have $\sum_{k=1}^n k=\frac{n(n+1)}{2}$

or

If $a < b$ and $b < c$, then $a < c$.

[Yury G. Kudryashov]

Or

If $a_0=1$ and for all $n$ we have $a_{n+1}=2a_n$, then for all $n$ we have $a_n=2^n$.

[Yury G. Kudryashov]

E.g., in your PDF you try to prove

$$\frac{q}{V_0}=\frac{C\times \frac{x}{(1-x)^2}}{1+C\times\frac{x}{1-x}}$$

based on some assumptions on $q$, $V_0$, $C$, and $x$ listed above.

[Yury G. Kudryashov]

But it is not clear what you assume about these numbers and what you deduce from the assumptions.

[Yury G. Kudryashov]

If you want to formalize some statement, you need to list all of your assumptions. What are the types of these variables (real/rational/elements of any field/...)? What are the constraints (probably, you should assume $x\ne 1$ and $1+Cx\ne x$, otherwise you'll have a zero in the denominator)? What relations on these variables do you assume?

[Parivash]

@Yury G. Kudryashov
assumption1.pdf
the assumption is showen in this file.

[Eric Wieser]

Note you can type $\LaTeX$ directly into Zulip between double $$s (like $$this$$)

[Eric Wieser]

docs#tsum_geometric_of_lt_1 looks like the closest thing to "assumption" 8 (using assumption 9), and docs#tsum_coe_mul_geometric_of_norm_lt_1 is alost "assumption" 7. Both sum from i=0 instead of i=1, but that's manageable.

[Yury G. Kudryashov]

Assumption 8 is not an assumption. It is a formula that is true for all $0<x<1$.

[Yury G. Kudryashov]

You need to separate assumptions from intermediate computations etc.

[Yury G. Kudryashov]

The first few lines look like

Given real numbers $x$, $y$, and $\theta_0$, consider the sequence $$\theta_i=x^{i-1}y\theta_0$. Put $C=\frac{y}{x}$, then we can rewrite the previous formula as $\theta_i=Cx^i\theta_0$.

[Yury G. Kudryashov]

Please try to rewrite the rest of the page in this style. State explicitly whether you introduce new notation, use a well-known fact, or draw conclusions from previous formulae.

[Parivash]

@Yury G. Kudryashov
Great, How can I write $$ \theta_i=C*x^{i)\*theta_0$$ and introduce them in lean, and how can I relate multiple theorem to each other?

[Yury G. Kudryashov]

Let me repeat again. To start this discussion, I need a complete text written in the style outlined above. Not a bunch of formulas.

[Yury G. Kudryashov]

Or at least a list of all assumptions (not intermediate calculations!) and the conclusion.

[Yury G. Kudryashov]

The quoted text can be written as

import data.real.basic

example (x y C : ℝ) (θ : ℕ → ℝ) (hθ : ∀ k : ℕ, θ k = x ^ (k - 1 : ℤ) * y * θ 0)
  (hC : C = y / x) : sorry :=
begin
  have hθ' : ∀ k : ℕ, θ k = C * x ^ k * θ 0,
  { sorry },
  sorry
end

[Yury G. Kudryashov]

Here the first sorry is the main statement you're going to prove (and probably you're going to have more assumptions) while the other two sorry's are for missing proof parts

[Yury G. Kudryashov]

If I take you final formula as the goal, then it looks like

import data.real.basic

example (x y C : ℝ) (θ : ℕ → ℝ) (hθ : ∀ k : ℕ, θ k = x ^ (k - 1 : ℤ) * y * θ 0)
  (hC : C = y / x) (q V₀ : ℝ) /- missing assumptions -/ :
  q / V₀ = (C * (x / (1 - x) ^ 2)) / (1 + C * (x / (1 - x))) :=
begin
  have hθ' : ∀ k : ℕ, θ k = C * x ^ k * θ 0,
  { sorry },
  sorry
end

[Yury G. Kudryashov]

Now I'll wait till you write a readable text that you're going to formalize. Imagine that you're writing a section for a calculus textbook.

[Parivash]

Like this one you means?
Proof-Shape.pdf

[Mario Carneiro]

No. That is a list of equations lacking any context for what is an assumption, what is a definition and what is an assertion. It is very important to distinguish these things in formalization

[Mario Carneiro]

(There is also another category of thing, a "typing assertion", represented as (x y C : ℝ) (θ : ℕ → ℝ) in Yury's example and omitted entirely in yours. In mathematics this is usually done by some sentence like "Suppose $x,y,C$ are real numbers and $\theta_n$ is a sequence of reals. Then..." This is also important for giving context for the theorem statement, and it is required in lean.)

[Yury G. Kudryashov]

I did show how the text may start above

[Yury G. Kudryashov]

Again: you don't see pages like your Proof-Shape.pdf in a good calculus textbook.

[Yury G. Kudryashov]

You see lots of words that explain what happens.

[Mario Carneiro]

That point is worth underscoring. Formalizing mathematics is not just "remove all the words". Instead the words correspond to specific bits of lean syntax, and without them it's impossible to tell which bits of lean syntax to stick together to get the proof you want

[Yury G. Kudryashov]

(and you see quite a few words in a well-documented lean file too)

[Parivash]

@Yury G. Kudryashov
Okay, I know what is your mean, you are right I should explain variable with more detail, let's arrange it and send it tomorrow, if you are okay?

[Parivash]

@Yury G. Kudryashov
Sorry for my delay in sending Pdf
Please find sequence formula in this file. Sequence-of-Equations.pdf

[Yury G. Kudryashov]

This is still a sequence of formulas, not a readable mathematical text.

[Parivash]

@Yury G. Kudryashov
at the end of file I explained type of all variables and constrains.

[Yury G. Kudryashov]

Here is a readable mathematical text: https://ncatlab.org/nlab/show/Urysohn%27s+lemma (of course, on a completely different topic)

[Yury G. Kudryashov]

We can't help you before you write a text with at least this amount of details.

[Yury G. Kudryashov]

Start with a statement of a theorem.

[Parivash]

@Yury G. Kudryashov
Okay, I'll separate a final equation which we want to prove with Axioms

[Parivash]

@Yury G. Kudryashov
Hi, I hope that this file provide enough detail. Editted.pdf

[Yury G. Kudryashov]

This is better. A few more questions.

• Am I right that you forgot to add the assumption $x<1$? Otherwise, the series $\sum_{i=0}^\infty \theta_i$ diverges.
• You write $\theta\in\mathbb R$. Do you actually mean $\theta_i\in\mathbb R$?
• What is $V0$? Is it $V_0$?
• You have $k_i$, $r_{ei}$, $r_{Ci-1}$, and $r_{ci-1}$. Am I right that you never use these and Axioms 4-7 in the rest of the text?

[Yury G. Kudryashov]

BTW, Axiom 9 for $i=0$ implies $C=1$.

[Yury G. Kudryashov]

(assuming $\theta_0\ne 0$)

[Parivash]

Thanks for looking,
Yes, $V_{0}$ is my means
$\theta_{i} \in \mathbb{R}$
all k $\in \mathbb{R}$
Actually, Axiom 4-7 is necessary for proofing $\theta_{i}$ which is $\theta_{i} = C*x_{i}*\theta_{0}$ that here I consider it as axiom, So, now we can ignore them.

• Yes, $\theta_{0} \neq 0$

[Yury G. Kudryashov]

If you want to prove a formula for $\theta_i$, then you should define them in some other way.

[Yury G. Kudryashov]

What about the formula for $\theta_i$ for $i=0$?

[Yury G. Kudryashov]

You get $\theta_0 = Cx^0\theta_0=C\theta_0$, hence $C=1$.

[Parivash]

can we define two goals here?
proofing it is so simple if we can prove them let me provide its formula.

[Parivash]

Please consider $\theta_{0} \neq 0$ all through the proofing.

[Parivash]

Yes, C=1 make sense that is a constant.

[Yury G. Kudryashov]

So, you want to prove this:

import analysis.specific_limits

lemma some_name (θ : ℕ → ℝ) (a b C P q A V₀ Vads x : ℝ)
  (hθ : ∀ k, θ k = x ^ k * θ 0) (hA : A = ∑' k, θ k)
  (hVads : Vads = V₀ * ∑' k : ℕ, k * θ k) (hq : q = Vads / A) :
  q = a * P / ((1 - b * P) * (1 - b * P + C * P)) :=

[Yury G. Kudryashov]

(probably, you need more assumptions like hx0 : 0 ≤ x and hx1 : x < 1)

[Yury G. Kudryashov]

You can use docs#tsum_geometric_of_lt_1 and docs#tsum_coe_mul_geometric_of_norm_lt_1

[Parivash]

@Yury G. Kudryashov
the assumption that you mentioned works, that's correct.

[Parivash]

@Yury G. Kudryashov
Yes, that is what I'm trying to proof.

[Yury G. Kudryashov]

OK, it only took a few days to formalize the statement... Now you should try to prove it. Have you done some tutorials (e.g., the natural numbers game)?

[Yury G. Kudryashov]

If not, then I recommend to start with tutorials.

[Parivash]

@Yury G. Kudryashov
Yes, I played natural number game

[Yury G. Kudryashov]

Then you can try to prove your lemma using lemmas I mentioned above.

[Parivash]

@Yury G. Kudryashov
Okay,
One more question, if I want to prove $\theta_{i}$ along with mentioned final goal, How can I do it?
we can prove it in a way that we say $\theta_{2} = (x^{1})*\theta_{1}$ and $\theta_{3} = (x^{2})*\theta_{1}$ So, finally we reach result that $\theta_{i} = (x^{i-1})*\theta_{1}$
Actually, I'm not sure this is a reliable way for proofing or not!
if yes, how we can relate. them to each other?

[Yakov Pechersky]

Yes, you can prove it using the htheta assumption that Yury wrote it. In a sense, your theta_i is the way you wrote it by definition