## Stream: Xena Summer Projects

### Topic: 2020 Summer Projects

#### Kevin Buzzard (May 06 2020 at 17:08):

I am running summer projects from 30th June to the end of August. I will give two talks per week on Discord and generally will help beginners. The idea is that a student should, at the end of it, have a github repository containing working Lean code, and a little write-up explaining what they have done.

Far more details are here. Things will only get going at the end of June, but I'm setting this up now because people are asking what to do next.

#### Anton Lorenzen (May 06 2020 at 18:48):

I would be interested! Is this open to not-anymore-but-been-very-recently undergrads too? How open are you to projects that are more on the logic/computation side of maths and have very little overlap with algebra? And would it be possible to start only at the third week or so? German exams are always a bit later than those in the English-speaking world..

#### Kevin Buzzard (May 06 2020 at 19:28):

I can't offer much supervision on the logic/computation side of things, but you're welcome to join in.

#### Jalex Stark (May 06 2020 at 22:35):

There are people around here that know things about computation :)

#### Kevin Buzzard (May 06 2020 at 23:12):

Right :-) This whole thing is just a myth, I'm not going to supervise anything, I'm just going to bring a bunch of people together and get them to ask questions on the chat :-)

#### Kevin Buzzard (May 06 2020 at 23:14):

Actually I am hoping that my performance will be better than in 2018, when I knew very little about Lean and the students realised very early on that they were better off asking Chris Hughes :rolling_on_the_floor_laughing:

#### Kevin Buzzard (May 06 2020 at 23:14):

This time I feel much better equipped to deal with basic questions

#### Yury G. Kudryashov (May 26 2020 at 08:04):

If some of the students will want to fill in some gaps in our analysis library, then I'm ready to help mentoring them.

#### Kevin Buzzard (May 26 2020 at 09:49):

I think that in June when I am out of marking hell I will try and do the analogue of what Patrick/Ryan/Rocky are doing -- go through Imperial's undergraduate course and figure out what is missing. I have not been paying attention to analysis development in mathlib, although I have been keeping more of an eye on algebra/number theory.

#### Jalex Stark (Jul 27 2020 at 02:52):

do you have students? are they mostly interacting on discord?

Yes and yes

#### Yury G. Kudryashov (Jul 27 2020 at 19:25):

Could you please tell here what are the projects?

#### Kevin Buzzard (Jul 27 2020 at 19:43):

People are doing Dedekind domains, working on why 144 is the largest square in the Fibonacci sequence, doing basic number theory (several groups -- stuff we have already, or probably don't want, in mathlib), basic group theory that we have in mathlib already etc

#### Kevin Buzzard (Jul 27 2020 at 19:44):

They're just learning Lean

#### Yury G. Kudryashov (Jul 27 2020 at 23:36):

Thank you for the list.

#### aris zhu (Jul 29 2020 at 13:16):

Screenshot 2020-07-29 at 13.12.32.png

#### aris zhu (Jul 29 2020 at 13:16):

IMG_1C2EAE6ABE0E-1.jpeg

#### aris zhu (Jul 29 2020 at 13:17):

I am trying to formulate the summation expression as shown in the picture, but I am not sure why my code gives me error, can someone help me pls?

#### Patrick Massot (Jul 29 2020 at 13:18):

It would be much easier to help you if you could copy-paste code (and LaTeX code) instead of images.

#### aris zhu (Jul 29 2020 at 13:18):

In particular, a_n is a sequence. My approach to formulate the series is to first express the sum as a function mapping from an int n to the result of summation, then let series be a sequence of sum

Ok one sec pls

#### aris zhu (Jul 29 2020 at 13:19):

(sum : λ n : ℕ, ∑ i in range n, (rpow (u n) n))

#### aris zhu (Jul 29 2020 at 13:20):

Erm sorry I don’t have the source code for the summation expression

#### aris zhu (Jul 29 2020 at 13:21):

Let me try to get the source code out

#### Patrick Massot (Jul 29 2020 at 13:23):

import topology.algebra.infinite_sum

open finset
open_locale big_operators

variables (a : ℕ → ℝ)
#check λ N, ∑ n in (range N), (a n)^n

#check has_sum (λ n, (a n)^n)


#### aris zhu (Jul 29 2020 at 13:23):

$\sum_{n=1}^{\infty} a_n^n$

#### Patrick Massot (Jul 29 2020 at 13:24):

Use  to enclose LaTeX code

Thanks so much

#### aris zhu (Jul 29 2020 at 14:06):

The provided code had no problem, but when I put the sum as one hypothesis, ie
(sum : λ N, ∑ n in (range N), (a n)^n), it gives error under $\lambda$ saying that type expected at λ N, ∑ n in (range N), (a n)^n term has type ℕ → ℝ. why is it so?

#### Patrick Massot (Jul 29 2020 at 14:22):

What you write has no meaning and, without further context, it's hard to guess what you imagine the meaning would be

#### Kevin Buzzard (Jul 29 2020 at 14:33):

@aris zhu please post compiling code with all imports and within triple back ticks like Patrick did

#### aris zhu (Jul 29 2020 at 14:36):

Oh I see, having just one summation expression is just a definition, cannot be a hypothesis.

#### aris zhu (Jul 29 2020 at 14:37):

import topology.algebra.infinite_sum

open finset
open_locale big_operators

variables (a : ℕ → ℝ)
#check λ N, ∑ n in (range N), (a n)^n

#check has_sum (λ n, (a n)^n)

/-
import analysis.special_functions.pow
import data.real.basic
import algebra.big_operators
-/

notation |x| := abs x

def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

open_locale big_operators

lemma series_of_root_numbers_converges
(a : ℕ → ℝ) (l : ℝ) (h_seq : seq_limit a l) (hu : ∀ n : ℕ, a n ≥ 0)
(l_pos : l ≥ 0) (l_lt_one: l < 1) :
-- (sum : λ N, ∑ n in (range N), (a n)^n) :
has_sum (λ n, (a n) ^ n) :=
begin
sorry
end


#### aris zhu (Jul 29 2020 at 14:37):

Now the problem is with has_sum

#### Patrick Massot (Jul 29 2020 at 14:40):

You should read more careful the result of my #check has_sum

#### Patrick Massot (Jul 29 2020 at 14:40):

It is not a Prop but a predicate on real numbers.

#### Patrick Massot (Jul 29 2020 at 14:41):

It becomes a Prop if you give a limit candidate.

#### aris zhu (Jul 29 2020 at 14:41):

Oh I see, thanks a lot

#### aris zhu (Jul 30 2020 at 16:25):

May I know if there is a way to search in the mathlib about any theorem I want to use? Particularly I want to use completeness of $\mathbb{R}$ so that I can prove that a sequence of real numbers which is bounded above has a supremum. Recently I have been randomly looking into the mathlib folders to see if I can happen to find what I need, but it seems like a rather inefficient way.

#### Kevin Buzzard (Jul 30 2020 at 16:28):

Usually one talks about the supremum of a set, not a sequence. Due to the total function principle, every set has a sup :-) it's just that the sup might be 37 and not obey the properties of a sup.

#### Jalex Stark (Jul 30 2020 at 16:33):

in order to find it just by navigating the the mathlib source by eye, you'll have to guess the right level of generality for the result

#### Jalex Stark (Jul 30 2020 at 16:34):

if you search supremum here https://leanprover-community.github.io/mathlib_docs/
the first result is in order.complete_lattice

#### aris zhu (Jul 30 2020 at 17:38):

I am sorry I don’t think I get entirely what you are saying, Kevin. I think you are pointing out my misunderstanding that I should talk about the sup of a set instead of a sequence, or rather a mapping from $\mathbb{N}$ to $\mathbb{R}$. So I should focus on the set formed from output of the mapping from natural number, ie the range of the mapping.

Then I don’t know what you mean by total function principle. I searched online, and only found definition on total function. May I know what the principle you are referring to is and so it leads to your conclusion that every set has a sup? And then I can probably understand what you mean by not obeying the properties of sup

#### Kevin Buzzard (Jul 30 2020 at 17:41):

There's something in lean called Sup or sup, I forget, but it makes sense for every set of reals. However it only satisfies the axioms of a supremum for nonempty bounded sets. You should locate its definition in data.real.basic or wherever it is and then take a look at the lemmas after it, maybe they'll help. I'm sorry I can't help more, I can't access lean right now

#### Yury G. Kudryashov (Jul 30 2020 at 18:00):

real has an instance of this class.

#### Yury G. Kudryashov (Jul 30 2020 at 18:00):

(and it is a conditionally_complete_lattice as well)

#### Yury G. Kudryashov (Jul 30 2020 at 18:01):

Also it is a docs#complete_space

#### Yury G. Kudryashov (Jul 30 2020 at 18:01):

So any docs#cauchy_seq converges

#### Patrick Massot (Jul 30 2020 at 18:20):

Aris, did you try to use the overview pages ?

#### aris zhu (Jul 30 2020 at 18:44):

Thank you Kevin and Yuri, I will take a look at those.

#### aris zhu (Jul 30 2020 at 18:44):

Patrick, i don’t know what are overview pages, what are those?

#### Bryan Gin-ge Chen (Jul 30 2020 at 18:51):

https://leanprover-community.github.io/mathlib-overview.html

You can reach this from the menu on the top right of the community website under "Learn -> Library overview".

#### aris zhu (Jul 31 2020 at 14:57):

May I know what is the tactics I can use so that I can define a set as the range of a function? Particularly I would like to define a mapping from N to R, ie sequence, and define the range of the mapping as a set of R

#### Kevin Buzzard (Jul 31 2020 at 15:05):

This sounds like set.rangein data.set.basic

#### Jalex Stark (Jul 31 2020 at 15:11):

the first three results for searching "range" at the #docs are all relevant

#### aris zhu (Jul 31 2020 at 16:51):

Thanks for the tips.

Currently I want to prove that a set is non-empty. I want to prove that given (u : ℕ → ℝ), (∃ (x : ℝ), x ∈ range u). To prove this, I have typed use u 1 to provide the possible value of x, but then I am stuck on the expression ⊢ u 1 ∈ range u. I tried to unfold it, getting ⊢ u 1 ∈ {x : ℝ | ∃ (y : ℕ), u y = x}, but still don't know what should be the appropriate tactics to close this goal. What should be the tactics to prove this?

#### Jalex Stark (Jul 31 2020 at 17:18):

what does suggest say?

#### Jalex Stark (Jul 31 2020 at 17:18):

i think your goal is defeq to \ex y, u y = u 1, so use 1 should work

#### Kevin Buzzard (Jul 31 2020 at 17:31):

yeah @aris zhu you're on the right track. The dsimp tactic will try to unfold definitions and change your goal to something which is the same by definition, but hopefully simpler to understand, so you could try that before Jalex' suggestion, but in fact Jalex' suggestion should work straight out of the box. I'm back in London now so could hopefully be more helpful.

#### Reid Barton (Jul 31 2020 at 17:33):

There will also be some lemma with a name like set.mem_range that exactly proves things like u 1 ∈ range u.

#### aris zhu (Jul 31 2020 at 19:16):

Jalex Stark said:

what does suggest say?

What do you mean by suggest?

#### aris zhu (Jul 31 2020 at 19:17):

Thanks for helping me. use 1 works, however, dsimp does not, neither does set.mem_range.

#### Bryan Gin-ge Chen (Jul 31 2020 at 19:18):

suggest is the name of a tactic, it works similarly to library_search except it returns more options, see tactic#suggest

#### aris zhu (Jul 31 2020 at 19:22):

wow suggest is a really cool feature!

#### aris zhu (Jul 31 2020 at 19:24):

btw, via suggest I also managed to use set.mem_range_self 1 to close the goal, and subsequently there are a lot of refine tactics statements being suggested

#### aris zhu (Jul 31 2020 at 19:33):

suggest makes me feel like Lean is almost possible to do proofs on its own! :thinking:

#### Jalex Stark (Jul 31 2020 at 21:29):

at the risk of excessively repeating myself, this google search takes you to the definition of suggest as the first hit

#### Jalex Stark (Jul 31 2020 at 21:31):

aris zhu said:

suggest makes me feel like Lean is almost possible to do proofs on its own! :thinking:

automation does a lot of work in any modern proof library, in fact moreso in the isabelle and coq libraries than in mathlib. for anyone who likes functional programming enough, there are several open issues in the mathlib github repo describing potential tactics that can automate more for us.

#### aris zhu (Aug 03 2020 at 14:36):

Currently I have hM : M ≤ x ↔ ∀ (z : ℝ), z ∈ f_range u → z ≤ x. What is the tactics allow me to change it to something like hM : M ≤ x ↔ ∀ (n : ℕ), u n ≤ x? f_range u is just the range of function u.

#### aris zhu (Aug 03 2020 at 14:38):

This time suggest just gives me a lot of refine commands, which are rather useless

#### Jalex Stark (Aug 03 2020 at 14:41):

If you do have : M ≤ x ↔ ∀ (n : ℕ), u n ≤ x, then tactics which try to figure things out will know what you're trying to figure out

#### Jalex Stark (Aug 03 2020 at 14:42):

another thing I would do here is write
#check mem_range or #check set.mem_range and look at the autocomplete suggestions

#### aris zhu (Aug 03 2020 at 14:50):

Jalex Stark said:

another thing I would do here is write
#check mem_range or #check set.mem_range and look at the autocomplete suggestions

Regarding the autocomplete suggestions, do you mean the pop-up window? or something in the Lean Infoview pane? Screenshot-2020-08-03-at-15.48.08.png

#### Jalex Stark (Aug 03 2020 at 14:51):

yes I meant that popup window

#### Jalex Stark (Aug 03 2020 at 14:51):

indeed it looks like rw mem_range is something you want

#### Reid Barton (Aug 03 2020 at 14:52):

aris zhu said:

f_range u is just the range of function u.

What does this mean? Is f_range something you defined?

#### Jalex Stark (Aug 03 2020 at 14:52):

you'll have to help it see through your f_range, though

#### Jalex Stark (Aug 03 2020 at 14:52):

in general, aliases mostly get in the way

#### Reid Barton (Aug 03 2020 at 14:55):

anyways, docs#set.forall_range_iff is what you want

#### Reid Barton (Aug 03 2020 at 14:55):

also it's not a tactic

#### Reid Barton (Aug 03 2020 at 14:56):

tactics are things like rw, intro

#### aris zhu (Aug 03 2020 at 14:57):

Reid Barton said:

aris zhu said:

f_range u is just the range of function u.

What does this mean? Is f_range something you defined?

Yes I defined myself, very close to the definition in mathlib, because I realize that the name overlaps with the range used for $\sum$, so to avoid clashes in names, I defined another f_range, with all its related types specifically being related to what I am proving

#### Jalex Stark (Aug 03 2020 at 14:58):

well if you want access to the many lemmas we have about ranges of functions, you should use the mathlib range

#### Jalex Stark (Aug 03 2020 at 14:58):

in particular, reid points out the the thing you want to prove is already a lemma in the library about mathlib's range

#### aris zhu (Aug 03 2020 at 14:59):

Reid Barton said:

anyways, docs#set.forall_range_iff is what you want

yeah I got this from establishing a lemma like jalex suggested, and used rw hM and suggest to figure out exact set.forall_range_iff

#### Jalex Stark (Aug 03 2020 at 15:01):

also, the typical way to deal with name collisions is namespaces. set.range is the thing we're talking about here, and finset.range is probably the one you've seen used with sums

#### Jalex Stark (Aug 03 2020 at 15:03):

i would typically not open set and instead just say set.range when I need it

#### aris zhu (Aug 03 2020 at 15:03):

what do you mean by open set?

#### Reid Barton (Aug 03 2020 at 15:05):

https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#namespaces

#### Reid Barton (Aug 03 2020 at 15:06):

If you're not already using open then there is no danger of a name collision between set.range and finset.range.

#### aris zhu (Aug 03 2020 at 15:06):

ok thanks so much

#### aris zhu (Aug 03 2020 at 15:54):

Say i have a proposition to be proven, but involves the discussion of comparison of two variables, say a and b. Is there a tactic which I can split the goal into three with different conditions, a > b,a < b, a = b, and then prove the proposition respectively?

#### Jalex Stark (Aug 03 2020 at 16:02):

i'm not sure why you ask for a tactic

#### Jalex Stark (Aug 03 2020 at 16:03):

i think what you want is the theorem that a < b \or a = b \or b < a

#### Jalex Stark (Aug 03 2020 at 16:03):

and then you can use the cases tactic on that theorem

#### Jalex Stark (Aug 03 2020 at 16:03):

you should be able to find this theorem with library_search

#### aris zhu (Aug 03 2020 at 16:04):

because split allows me to split the goal into two, if it can be split, so I thought there is a way to split inequalities as well

#### Jalex Stark (Aug 03 2020 at 16:05):

the thing you want to split on is not in the goal

#### Dan Stanescu (Aug 03 2020 at 16:05):

Is this what you're asking for:

rcases lt_trichotomy a b with h1|h2|h3,


@aris zhu

#### Jalex Stark (Aug 03 2020 at 16:07):

when we split on hypotheses, that's called cases instead of split

#### aris zhu (Aug 03 2020 at 16:07):

ah yeah cases that is

#### Jalex Stark (Aug 03 2020 at 16:07):

if you just want to split on p \or \not p for some specific p, you can use by_cases p

#### aris zhu (Aug 03 2020 at 16:16):

If I were to write by_cases (M > u 1), it gives me error on >, saying that the inequality is not a Prop, I wonder why inequality is not considered Type Prop?

#### Reid Barton (Aug 03 2020 at 16:16):

what is the whole error?

#### aris zhu (Aug 03 2020 at 16:17):

function expected at
M > u 1
term has type
Prop


#### Reid Barton (Aug 03 2020 at 16:18):

You've made some other error which is hard to guess without knowing what you've written

#### Reid Barton (Aug 03 2020 at 16:18):

maybe a missing ,

#### aris zhu (Aug 03 2020 at 16:19):

thanks so much, silly mistake...

#### Reid Barton (Aug 03 2020 at 16:20):

Also, if you read the error message, you'll see it's telling you that M > u 1 is a Prop

#### Reid Barton (Aug 03 2020 at 16:21):

but it was expecting a function--probably because you had something after (M > u 1) which Lean interpreted as an argument to it.

#### Reid Barton (Aug 03 2020 at 16:25):

but sometimes they take some puzzle solving to interpret--if Lean is confused, obviously it doesn't know why it's confused, so it's your job to guess why that might be

#### aris zhu (Aug 04 2020 at 16:49):

Is there a lemma to convert ¬(A ↔ B) to ¬A ↔ B? I found something similar like not_iff but it doesn't seem to work

#### Shing Tak Lam (Aug 04 2020 at 17:09):

I'm not sure that's true constructively, so you'd need classical logic to prove that. Is there an error about type class instances?

Putting open_locale classical in your file should allow you to use not_iff. (or if you can show that B is decidable that would work as well)

#### aris zhu (Aug 04 2020 at 17:40):

ah I didn't put open_locale classical. What is the difference between open and open_locale? I searched in the mathlib and found open_locale used for declaring notation as local notation, but for me it seems like a redundant explanation since "opening" a namespace is to use the terms in the namespace in the current script. Also, is there a place describing this kind of dependencies, where I need to add open or open_locale so that I can use the lemmas?

#### Jalex Stark (Aug 04 2020 at 17:47):

open opens a namespace

#### Jalex Stark (Aug 04 2020 at 17:47):

open_locale brings in local notations and local instances

#### Jalex Stark (Aug 04 2020 at 17:48):

anything you can do with open you can also do with dot notation

#### Jalex Stark (Aug 04 2020 at 17:49):

eg

import data.finset

#check card
#check finset.card
open finset
#check card


#### aris zhu (Aug 04 2020 at 21:18):

Can I clarify with this theorem: theorem exists_sup (S : set ℝ) : (∃ x, x ∈ S) → (∃ x, ∀ y ∈ S, y ≤ x) → ∃ x, ∀ y, x ≤ y ↔ ∀ z ∈ S, z ≤ y. I believe that (∃ x, x ∈ S) means non-empty set S, (∃ x, ∀ y ∈ S, y ≤ x) means set S is bounded above by x. And what I am confused about is ∃ x, ∀ y, x ≤ y ↔ ∀ z ∈ S, z ≤ y. At first I thought that x is the supremum, but then after some considerations, I feel that x is rather a lower bound of the set of upper bounds of S. As such the last sentence should add z ≤ x to show that x is also an upper bounds of S to make it a supremum?

#### Patrick Massot (Aug 04 2020 at 21:24):

I think you are confused by precedence issues.

#### Patrick Massot (Aug 04 2020 at 21:25):

Try adding parentheses while checking that Lean still thinks this is the same definition.

#### Kevin Buzzard (Aug 04 2020 at 21:47):

(x is indeed the supremum)

#### aris zhu (Aug 05 2020 at 12:45):

Patrick Massot said:

Try adding parentheses while checking that Lean still thinks this is the same definition.

I am sorry but I still cannot figure out why. The reason I got confused about this, is because I want to use this theorem to identify the supremum, i.e. x, and then derive the conclusion ∀ ε > 0, ∃ n₀, u n₀ ≥ x - ε. What I did is to set up the lemma have lemma : ∃ x, ∀ y, x ≤ y ↔ ∀ z ∈ S, z ≤ y, and used the theorem, together with non-emptiness and bounded above, to prove the lemma. Then when I want to use that lemma to prove ∀ ε > 0, ∃ n₀, u n₀ ≥ x - ε, I just cannot figure out a way, and I realize that it lacks some "bounds" to x in ∃ x, ∀ y, x ≤ y ↔ ∀ z ∈ S, z ≤ y. In terms of precedence, I believe it is ∃ x, (∀ y, (x ≤ y ↔ ∀ z ∈ S, z ≤ y)).

#### Reid Barton (Aug 05 2020 at 12:48):

This is slightly tricky. Hint: the fact that ↔ is used is important.

#### Kevin Buzzard (Aug 05 2020 at 13:30):

You're right about the precedence. If you let y=x then you see in particular that x is an upper bound.

#### aris zhu (Aug 05 2020 at 14:30):

Thanks for helping me clarify the statement and tips for understanding why it is an upper bound. This actually helps me to realize that my problem was to prematurely specialize a ∀ lemma, then I cannot properly use contrapose to prove the result.

#### aris zhu (Aug 10 2020 at 13:52):

I want to get from n : ℕ, a n ≥ 0 to deduce a n ^ n ≥ 0? suggest doesn't give any useful hint. I think the name is probably related to pos, pow, and I found one that is closest to what I need, (at least I think it is), exact nat.pos_pow_of_pos _ _, but it is not working for me. The error gives

invalid type ascription, term has type
0 < ?m_1 ^ ?m_2
but is expected to have type
a n ^ n ≥ 0


I don't understand the error message regarding m_1, m_2, what are those types? So that I can understand what is wrong with the expression and potentially fix it

#### Jason KY. (Aug 10 2020 at 13:54):

What is a?

#### aris zhu (Aug 10 2020 at 13:55):

a is a function, a : ℕ → ℝ

#### Jason KY. (Aug 10 2020 at 13:57):

pow_nonneg should do it

#### Jason KY. (Aug 10 2020 at 13:57):

example (n : ℕ) (a : ℕ → ℝ) (ha : ∀ n, 0 ≤ a n) : 0 ≤ a n ^ n :=
begin
apply pow_nonneg,
exact ha n,
end


#### aris zhu (Aug 10 2020 at 13:58):

thanks, it works!

#### aris zhu (Aug 10 2020 at 13:59):

could you just also explain to me what m_2, m_1 are? are they some kind of general types? if so, how would I know if N or R is a "sub-type" of m_2, m_1?

#### Jason KY. (Aug 10 2020 at 14:02):

They are placeholders

#### Jason KY. (Aug 10 2020 at 14:03):

pow_pos is for showing positive  <  while you have \le so lean cant find things to put in the placeholders

#### aris zhu (Aug 10 2020 at 14:05):

oh i see, so I should use nonneg and nonpos when I see ≥ 0 and ≤ 0

#### aris zhu (Aug 10 2020 at 14:13):

Now I am stuck on this problem, from h : ∀ (n : ℕ), a n ^ n ≥ 0 to deduce 0 ≤ ∑ (n : ℕ) in range m, a n ^ n - ∑ (n : ℕ) in range n, a n ^ n, where nm : ℕ. In my mind I think what I need to do is to simplify the summation expression to something like 0 ≤ ∑ (n : ℕ) in (range m - range n), a n ^ n, and then probably I can directly exact h. What can I do with the summation expression to simplify it?

#### Jason KY. (Aug 10 2020 at 14:22):

I've done something similar before simplifying sum to finset.Ico before. Take a look at: https://github.com/JasonKYi/M4000x_LEAN_formalisation/blob/master/src/M40002/M40002_C4.lean#L148 and see if it helps

#### aris zhu (Aug 10 2020 at 14:22):

or is there any place I can read more about ∑?

#### Jason KY. (Aug 10 2020 at 14:23):

Its a local definition def partial_sum_to (a : ℕ → ℝ) (n : ℕ) := finset.sum (finset.range n) a

#### Jason KY. (Aug 10 2020 at 14:24):

With notation  a := partial_sum_to a

#### aris zhu (Aug 10 2020 at 14:26):

ok I will take a look! Thanks

#### aris zhu (Aug 10 2020 at 15:46):

What would be the tactics to split n ≤ m into n < m and n = m? I tried by_cases n < m but they don't seem to work that well because it ignores the original condition

#### Jason KY. (Aug 10 2020 at 15:53):

le_iff_eq_or_lt

#### aris zhu (Aug 10 2020 at 20:01):

@Jason KY. , regarding (∑ a) m - (∑ a) n = finset.sum (finset.Ico n m) a, why is it Ico instead of Ioc? I thought that it should be [n + 1, m], i.e. (n, m]?

#### Jason KY. (Aug 10 2020 at 20:11):

(∑ a) m is the sum of a n from n = 0 to a = m -1 and finset.Ico n m is the set of nats from n to m -1. The maths works out so I'm not sure whats the confusion

#### aris zhu (Aug 11 2020 at 12:38):

oh I though that (∑ a) m is the sum of a n to n = m instead of n = m - 1. Thanks for the clarification

#### Kevin Buzzard (Aug 11 2020 at 17:43):

It's a sum of m things

#### aris zhu (Aug 12 2020 at 15:09):

How can I break an extremely long line into two lines in Lean?

#### aris zhu (Aug 12 2020 at 15:10):

Is it the same as what we do for calc environment, i.e. add ... in front of the line?

#### Bryan Gin-ge Chen (Aug 12 2020 at 15:12):

You can just break the line and it should be fine. Lean (usually) ignores whitespace (including line breaks).

#### aris zhu (Aug 12 2020 at 15:59):

I am sorry that I cannot find it in library API but what is the theorem I can used to prove that if n ≤ N and ¬n = N, then n < N? I tried with something like le_not_eq, but there doesn't seem to have any option related to this

#### Jalex Stark (Aug 12 2020 at 16:08):

You should be able to find it with library search

#### Jalex Stark (Aug 12 2020 at 16:08):

docs#library_search

#### Jalex Stark (Aug 12 2020 at 16:09):

But also tactic#linarith

#### aris zhu (Aug 12 2020 at 16:13):

I tried with linarith but it cannot be used in this situation

#### Dan Stanescu (Aug 12 2020 at 16:22):

This works and I got it with library_search:

example (n N : ℕ) (h1 : n ≤ N) (h2 : n ≠ N) : n < N := lt_of_le_of_ne h1 h2


#### aris zhu (Aug 12 2020 at 16:29):

ok I think my problem was that I didn't put ne in my search, instead I place not_eq. Thanks for the help

#### aris zhu (Aug 14 2020 at 16:15):

regarding specialize tactics, what is the way to retain the original hypothesis? I see in the documentation that it "tries to clear the previous one", can I choose not to do it?

#### Kevin Buzzard (Aug 14 2020 at 16:19):

you can just let f2 := f x

#### aris zhu (Aug 17 2020 at 16:48):

Is there a reason why for nat.mul_div_mul, that is m > 0 → m * n / (m * k) = n / k, have the restriction m > 0? Why is it not m ≠ 0?

#### Kevin Buzzard (Aug 17 2020 at 17:32):

they're equivalent of course, because it's a theorem about naturals, but probably there is some standard form, although I very much doubt the standard way to express this is m>0 because > is persona non grata usually.

#### Yury G. Kudryashov (Aug 17 2020 at 22:04):

One of the reasons to use 0 < m instead of m ≠ 0 is that 0 < m and m ≤ n immediately imply 0 < n.

#### Yury G. Kudryashov (Aug 17 2020 at 22:05):

Unfortunately, we have no "normal form" here; e.g., many theorems about ennreals use < ∞ and many use ≠ ∞.

#### aris zhu (Aug 18 2020 at 14:37):

Kevin Buzzard said:

they're equivalent of course, because it's a theorem about naturals, but probably there is some standard form, although I very much doubt the standard way to express this is m>0 because > is persona non grata usually.

What do you mean by "> is persona non grata usually"?

#### aris zhu (Aug 18 2020 at 14:38):

Yury G. Kudryashov said:

One of the reasons to use 0 < m instead of m ≠ 0 is that 0 < m and m ≤ n immediately imply 0 < n.

So is it a design choice so that other theorems/lemmas can derive results easier?

#### aris zhu (Aug 18 2020 at 14:39):

what is ennreal? I search on the mathlib and cannot figure what category it means..

#### Shing Tak Lam (Aug 18 2020 at 14:42):

mathlib prefers < and ≤ over > and ≥, hence you'll see m > 0 written as 0 < m in mathlib.

#### Shing Tak Lam (Aug 18 2020 at 14:42):

ennreal is here https://leanprover-community.github.io/mathlib_docs/data/real/ennreal.html

#### aris zhu (Aug 18 2020 at 14:46):

Shing Tak Lam said:

ennreal is here https://leanprover-community.github.io/mathlib_docs/data/real/ennreal.html

yes I found the link, but I don't understand what ennreal means, so just curious if it stands for something?

#### Kevin Buzzard (Aug 18 2020 at 14:56):

extended (i.e. contains infinity) non-negative reals

#### aris zhu (Aug 18 2020 at 14:58):

May I know what's wrong with the following?
I want to say that $l \in [0, 1)$, and after checking through mathlib I believe I should use def Ico (a b : α) := {x | a ≤ x ∧ x < b} in data.set.intervals.basic, so I wrote hl : l ∈ Ico 0 1, but then error message failed to synthesize type class instance for is given. I did import data.set.intervals.basic at the top.

#### Dan Stanescu (Aug 18 2020 at 15:09):

Try l ∈ Ico (0:\R) 1.

#### aris zhu (Aug 21 2020 at 12:02):

Hi all! I have finally finished proving my question in Lean! My personal goal for this UROP was to finish proving one question by the end of August, and I managed to do it, even one week faster haha. Thanks for everyone in this channel who has helped me along the way. It was a very different experience I had for proving using code instead of pen and paper. You can checkout my git repo at https://github.com/qsmy41/ICL-UROP---LeanProver

@Jason KY. I used two of your lemmas, and in my repo I commented that the two lemmas are from you. I am not sure if this is the right way to do it, and not sure if you mind me using some of your work. Could you give me some suggestions?

#### Kevin Buzzard (Aug 21 2020 at 13:31):

Well done @aris zhu , you can join the club of people who I have indoctrinated :D You should make a better README where you explain in maths terms what the theorem is and how you proved it.

#### aris zhu (Aug 21 2020 at 13:34):

ok Let me update it!

#### Jason KY. (Aug 21 2020 at 13:56):

I dont mind how you would like to credit. The way you've done so far is perfectly fine by me :)

#### Ed (May 17 2021 at 06:22):

The discord link is invalid. Is there a new one?

Who are you?

#### Ed (May 17 2021 at 07:05):

A final year CS undergraduate from the university of Bath. I was speaking to a friend who graduated from maths at ICL last year about category theory and theorem provers. He mentioned lean and that you were welcoming of students from outside ICL. He also mentioned that there was a discord, sent me a link to this forum, and said I should join if I was interested.

I looked up a few videos on YouTube and decided I was interested. So, here I am!

Last updated: May 18 2021 at 11:11 UTC