Zulip Chat Archive

Stream: Xena Summer Projects

Topic: 2020 Summer Projects


view this post on Zulip 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.

view this post on Zulip 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..

view this post on Zulip 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.

view this post on Zulip Jalex Stark (May 06 2020 at 22:35):

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

view this post on Zulip 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 :-)

view this post on Zulip 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:

view this post on Zulip Kevin Buzzard (May 06 2020 at 23:14):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jalex Stark (Jul 27 2020 at 02:52):

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

view this post on Zulip Kevin Buzzard (Jul 27 2020 at 07:26):

Yes and yes

view this post on Zulip Yury G. Kudryashov (Jul 27 2020 at 19:25):

Could you please tell here what are the projects?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 27 2020 at 19:44):

They're just learning Lean

view this post on Zulip Yury G. Kudryashov (Jul 27 2020 at 23:36):

Thank you for the list.

view this post on Zulip aris zhu (Jul 29 2020 at 13:16):

Screenshot 2020-07-29 at 13.12.32.png

view this post on Zulip aris zhu (Jul 29 2020 at 13:16):

IMG_1C2EAE6ABE0E-1.jpeg

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 29 2020 at 13:18):

(we'll help you anyway, hold on)

view this post on Zulip aris zhu (Jul 29 2020 at 13:19):

Ok one sec pls

view this post on Zulip aris zhu (Jul 29 2020 at 13:19):

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

view this post on Zulip aris zhu (Jul 29 2020 at 13:20):

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

view this post on Zulip aris zhu (Jul 29 2020 at 13:21):

Let me try to get the source code out

view this post on Zulip 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)

view this post on Zulip aris zhu (Jul 29 2020 at 13:23):

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

view this post on Zulip Patrick Massot (Jul 29 2020 at 13:24):

Use $$ to enclose LaTeX code

view this post on Zulip aris zhu (Jul 29 2020 at 13:27):

Thanks so much

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip aris zhu (Jul 29 2020 at 14:36):

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

view this post on Zulip 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

view this post on Zulip aris zhu (Jul 29 2020 at 14:37):

Now the problem is with has_sum

view this post on Zulip Patrick Massot (Jul 29 2020 at 14:40):

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

view this post on Zulip Patrick Massot (Jul 29 2020 at 14:40):

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

view this post on Zulip Patrick Massot (Jul 29 2020 at 14:41):

It becomes a Prop if you give a limit candidate.

view this post on Zulip aris zhu (Jul 29 2020 at 14:41):

Oh I see, thanks a lot

view this post on Zulip 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 R\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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 N\mathbb{N} to R\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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 18:00):

See also docs#conditionally_complete_linear_order
real has an instance of this class.

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 18:00):

(and it is a conditionally_complete_lattice as well)

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 18:01):

Also it is a docs#complete_space

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 18:01):

So any docs#cauchy_seq converges

view this post on Zulip Patrick Massot (Jul 30 2020 at 18:20):

Aris, did you try to use the overview pages ?

view this post on Zulip aris zhu (Jul 30 2020 at 18:44):

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

view this post on Zulip aris zhu (Jul 30 2020 at 18:44):

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

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 31 2020 at 15:05):

This sounds like set.rangein data.set.basic

view this post on Zulip Jalex Stark (Jul 31 2020 at 15:11):

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

view this post on Zulip 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?

view this post on Zulip Jalex Stark (Jul 31 2020 at 17:18):

what does suggest say?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip aris zhu (Jul 31 2020 at 19:16):

Jalex Stark said:

what does suggest say?

What do you mean by suggest?

view this post on Zulip aris zhu (Jul 31 2020 at 19:17):

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

view this post on Zulip 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

view this post on Zulip aris zhu (Jul 31 2020 at 19:22):

wow suggest is a really cool feature!

view this post on Zulip 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

view this post on Zulip aris zhu (Jul 31 2020 at 19:33):

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

view this post on Zulip 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
https://www.google.com/search?q=suggest%20site%3Ahttps%3A%2F%2Fleanprover-community.github.io%2Fmathlib_docs%2F

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip aris zhu (Aug 03 2020 at 14:38):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jalex Stark (Aug 03 2020 at 14:51):

yes I meant that popup window

view this post on Zulip Jalex Stark (Aug 03 2020 at 14:51):

indeed it looks like rw mem_range is something you want

view this post on Zulip 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?

view this post on Zulip Jalex Stark (Aug 03 2020 at 14:52):

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

view this post on Zulip Jalex Stark (Aug 03 2020 at 14:52):

in general, aliases mostly get in the way

view this post on Zulip Reid Barton (Aug 03 2020 at 14:55):

anyways, docs#set.forall_range_iff is what you want

view this post on Zulip Reid Barton (Aug 03 2020 at 14:55):

also it's not a tactic

view this post on Zulip Reid Barton (Aug 03 2020 at 14:56):

tactics are things like rw, intro

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jalex Stark (Aug 03 2020 at 15:03):

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

view this post on Zulip aris zhu (Aug 03 2020 at 15:03):

what do you mean by open set?

view this post on Zulip Reid Barton (Aug 03 2020 at 15:05):

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

view this post on Zulip 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.

view this post on Zulip aris zhu (Aug 03 2020 at 15:06):

ok thanks so much

view this post on Zulip 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?

view this post on Zulip Jalex Stark (Aug 03 2020 at 16:02):

i'm not sure why you ask for a tactic

view this post on Zulip 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

view this post on Zulip Jalex Stark (Aug 03 2020 at 16:03):

and then you can use the cases tactic on that theorem

view this post on Zulip Jalex Stark (Aug 03 2020 at 16:03):

you should be able to find this theorem with library_search

view this post on Zulip 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

view this post on Zulip Jalex Stark (Aug 03 2020 at 16:05):

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

view this post on Zulip 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

view this post on Zulip Jalex Stark (Aug 03 2020 at 16:07):

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

view this post on Zulip aris zhu (Aug 03 2020 at 16:07):

ah yeah cases that is

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Aug 03 2020 at 16:16):

what is the whole error?

view this post on Zulip aris zhu (Aug 03 2020 at 16:17):

function expected at
  M > u 1
term has type
  Prop

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 03 2020 at 16:18):

maybe a missing ,

view this post on Zulip aris zhu (Aug 03 2020 at 16:19):

thanks so much, silly mistake...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Aug 03 2020 at 16:21):

Error messages are helpful.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Jalex Stark (Aug 04 2020 at 17:47):

open opens a namespace

view this post on Zulip Jalex Stark (Aug 04 2020 at 17:47):

open_locale brings in local notations and local instances

view this post on Zulip Jalex Stark (Aug 04 2020 at 17:48):

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

view this post on Zulip Jalex Stark (Aug 04 2020 at 17:49):

eg

import data.finset

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Aug 04 2020 at 21:24):

I think you are confused by precedence issues.

view this post on Zulip Patrick Massot (Aug 04 2020 at 21:25):

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

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 21:47):

(x is indeed the supremum)

view this post on Zulip 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)).

view this post on Zulip Reid Barton (Aug 05 2020 at 12:48):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Jason KY. (Aug 10 2020 at 13:54):

What is a?

view this post on Zulip aris zhu (Aug 10 2020 at 13:55):

a is a function, a : ℕ → ℝ

view this post on Zulip Jason KY. (Aug 10 2020 at 13:57):

pow_nonneg should do it

view this post on Zulip 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

view this post on Zulip aris zhu (Aug 10 2020 at 13:58):

thanks, it works!

view this post on Zulip 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?

view this post on Zulip Jason KY. (Aug 10 2020 at 14:02):

They are placeholders

view this post on Zulip 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

view this post on Zulip aris zhu (Aug 10 2020 at 14:05):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip aris zhu (Aug 10 2020 at 14:22):

or is there any place I can read more about ?

view this post on Zulip Jason KY. (Aug 10 2020 at 14:23):

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

view this post on Zulip Jason KY. (Aug 10 2020 at 14:24):

With notation a := partial_sum_to a

view this post on Zulip aris zhu (Aug 10 2020 at 14:26):

ok I will take a look! Thanks

view this post on Zulip 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

view this post on Zulip Jason KY. (Aug 10 2020 at 15:53):

le_iff_eq_or_lt

view this post on Zulip 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]?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 11 2020 at 17:43):

It's a sum of m things

view this post on Zulip aris zhu (Aug 12 2020 at 15:09):

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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Jalex Stark (Aug 12 2020 at 16:08):

You should be able to find it with library search

view this post on Zulip Jalex Stark (Aug 12 2020 at 16:08):

docs#library_search

view this post on Zulip Jalex Stark (Aug 12 2020 at 16:09):

But also tactic#linarith

view this post on Zulip aris zhu (Aug 12 2020 at 16:13):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 16:19):

you can just let f2 := f x

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 ≠ ∞.

view this post on Zulip 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"?

view this post on Zulip 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?

view this post on Zulip aris zhu (Aug 18 2020 at 14:39):

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

view this post on Zulip 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.

view this post on Zulip Shing Tak Lam (Aug 18 2020 at 14:42):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Aug 18 2020 at 14:56):

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

view this post on Zulip aris zhu (Aug 18 2020 at 14:58):

May I know what's wrong with the following?
I want to say that l[0,1)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.

view this post on Zulip Dan Stanescu (Aug 18 2020 at 15:09):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip aris zhu (Aug 21 2020 at 13:34):

ok Let me update it!

view this post on Zulip 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 :)

view this post on Zulip Ed (May 17 2021 at 06:22):

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

view this post on Zulip Kevin Buzzard (May 17 2021 at 06:30):

Who are you?

view this post on Zulip 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