12/20/2023 0 Comments Terence mathThis is slightly different from standard mathematical notation, but is not too difficult to get used to. Also note that Lean does not require parentheses when applying functions: we write D k here rather than D(k) (which in fact does not compile in Lean unless one puts a space between the D and the parentheses). We could have made this quantification explicit if we so chose, for instance using ∀ k : ℕ, 0 ≤ D k instead of ∀ k, 0 ≤ D k, but it is not necessary to do so. Because a and D have the natural numbers ℕ as their domain, the dummy variable k in these hypotheses is automatically being quantified over ℕ. One thing to note here is that Lean is quite good at filling in implied ranges of variables. This is fairly straightforward the one thing is that the property of being monotone decreasing already has a name in Lean’s Mathlib, namely Antitone, and it is generally a good idea to use the Mathlib provided terminology (because that library contains a lot of useful lemmas about such terms). Now we add in the hypotheses, which in Lean convention are usually given names starting with h. (One can choose to “hardwire” the non-negativity hypothesis into the by making D take values in the nonnegative reals (denoted NNReal in Lean), but this turns out to be inconvenient, because the laws of algebra and summation that we will need are clunkier on the non-negative reals (which are not even a group) than on the reals (which are a field). The main variables here are the sequences and, which in Lean are best modeled by functions a, D from the natural numbers ℕ to the reals ℝ. Now we have to declare the hypotheses and variables. (If you like, you can follow this tour in that playground, by clicking on the screenshots of the Lean code.) I start by importing Lean’s math library, and starting an example of a statement to state and prove: For this quick project, it was convenient to use the online Lean playground, rather than my local IDE, so the screenshots will look a little different from those in the previous post. The next step is to formalize the statement of the lemma in Lean. I decided that this was a good enough blueprint for me to work with. With a little bit of pen and paper effort, I obtained This is already a human-readable proof, but in order to formalize it more easily in Lean, I decided to rewrite it as a chain of inequalities, starting at and ending at. Since is non-negative, and by hypothesis, we haveīut by the monotone hypothesis on the left-hand side is at least, giving the claim. The main idea of the proof here is to use the telescoping series identity Here I tried to draw upon the lessons I had learned from the PFR formalization project, and to first set up a human readable proof of the lemma before starting the Lean formalization – a lower-case “blueprint” rather than the fancier Blueprint used in the PFR project. Let and be sequences of real numbers indexed by natural numbers, with non-increasing and non-negative. Here I would like to walk through the process I used for a slightly longer proof I worked out recently, after seeing the following challenge from Damek Davis: to formalize (in a civilized fashion) the proof of the following lemma: The deduction was deliberately chosen to be short and only showcased a small number of Lean tactics. In my previous post, I walked through the task of formally deducing one lemma from another in Lean 4.
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |