Theory meeting, Feb. 27th

[Lyle Kopnicky]

We'll continue to discuss the exercises from Chapter 21, "The Real Numbers", of Logic and Proof (https://leanprover.github.io/logic_and_proof). Please try to work the exercises beforehand. At the meeting anyone will be able to present and contribute to the discussion.

Wednesday, February 27th, 2018, 6:30-8:30pm

Location:
Collective Agency

3050 SE Division, Suite 245 · Portland, OR

We'll be in the second floor conference room, not in the Collective Agency suite. It's just off the lobby area in the middle of the second floor. Elevator access is available.


RSVP at: https://www.meetup.com/Portland-Functional-Programming-Study-Group/events/mpwwbqyzdbkc/

[Lyle Kopnicky]

I’ve made a scheduling mistake - I forgot I had bought a ticket to a concert this Wednesday, quite some time ago. It’s an earlier concert so there’s no way I can make the meeting.

Would folks be open to rescheduling to the following day, on Thursday? Or to the following Wednesday? Either is open for the conference room right now.

--
You received this message because you are subscribed to the Google Groups "pdxfunc" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pdxfunc+u...@googlegroups.com.
To post to this group, send email to pdx...@googlegroups.com.
Visit this group at https://groups.google.com/group/pdxfunc.
For more options, visit https://groups.google.com/d/optout.

[Ed Snow]

I'm good with either option.

[Matt Rice]

I'm good with either option as well, leaning towards the later option,
merely because that allows more time to work on it.
But sooner is fine too as I have made at least some progress.

On Sun, Feb 24, 2019 at 9:40 PM Ed Snow <edsn...@gmail.com> wrote:
>
> I'm good with either option.
>

[Lyle Kopnicky]

I’ve rescheduled it for the 28th.

Then you will have more time to work on the next chapter. :)

[Lyle Kopnicky]

Another fun meeting. Matt walked us through his proof in Lean of Exercise 1. He was getting stuck at some point near the end of the proof and we were able to find a slight error in an earlier part of the proof that got him unstuck.

Ed showed us his colorful, visual proof of Exercise 4, which he mailed out above.

Then I walked us through exercises 5, 8, and 6a.

We were really scratching our heads over 6b. That’s where you have to prove that the product of two Cauchy sequences is a Cauchy sequence. I think I just came up with the insight to solve the problem.

In 6a, we had to prove that the sum of two Cauchy sequences is Cauchy. When we were given an epsilon, we used the trick of dividing it in half. That is, show that sequence p converges to within a distance of epsilon/2, and sequence q converges to a within distance of epsilon/2. Therefore the sum converges to a distance within epsilon.

We were stumped on 6b because we can’t just take the square root of epsilon. But there’s no need. All you have to do is take the fact that p converges to within a distance of 1, and q converges to within a distance of epsilon. Multiply them, and it converges to within a distance of epsilon.

Maybe. I have to try to work out the proof.

- Lyle

[Jesse Cooke]

I doubt I have my notes from college anymore, but I vaguely remember working with Cauchy sequences in one of my analysis classes. I'll have to do some reading on the topic soon. This all sounds super fun; wish I had the bandwidth to join in!

[Lyle Kopnicky]

Glad we inspired you to revisit the topic, Jesse! Hope you have a chance to join in sometime.

[Lyle Kopnicky]

I’ve finally completed all the exercises. I also made some minor corrections based on what we discussed in the meeting. I’ve attached my solutions.

- Lyle

[jim rothstein]

Hi Lyle:

Beautiful solutions!     I've been trying to prove   pq is Cauchy if both are (Exercise 21.6 #4)   and got myself fouled up in absolute value signs.

Maybe I missed something obvious:

You wrote:

Combining these, we have for all i, j ≥ N that |pi−pj ||qi−qj | < e.
It’s a straightforward case analysis on negative versus positive
factors to show that |(pi − pj )(qi − qj )| <e .

 

First,   is last statement what we need to prove?

Second,  you did not use triangle inequality.    I had to use  

|   |a|  - |b| |  <=   |a-b|    (reverse? triangle inequality)

(see https://math.stackexchange.com/questions/127372/reverse-triangle-inequality-proof)

I will write up my solution tomorrow;   would you mind checking my  | inequalities|?

Thx

jim

On Wed, Mar 6, 2019 at 9:29 PM Lyle Kopnicky <lyle...@gmail.com> wrote:

I’ve finally completed all the exercises. I also made some minor corrections based on what we discussed in the meeting. I’ve attached my solutions.

- Lyle

--

[Lyle Kopnicky]

Thanks, Jim!

Responses inline:

On Wed, Mar 6, 2019 at 10:05 PM jim rothstein <jimrot...@gmail.com> wrote:

Hi Lyle:

Beautiful solutions!     I've been trying to prove   pq is Cauchy if both are (Exercise 21.6 #4)   and got myself fouled up in absolute value signs.

Maybe I missed something obvious:

You wrote:

Combining these, we have for all i, j ≥ N that |pi−pj ||qi−qj | < e.
It’s a straightforward case analysis on negative versus positive
factors to show that |(pi − pj )(qi − qj )| <e .

 

First,   is last statement what we need to prove?

Perhaps I did a bit of hand-waving there. I’m assuming that the product of absolute values is the absolute value of the product. Simple to prove and I almost felt we should take it as a given. There’s a proof here: 

https://math.stackexchange.com/questions/633642/prove-that-the-absolute-value-of-a-product-is-the-product-of-the-absolute-values. 

Second,  you did not use triangle inequality.    I had to use  

|   |a|  - |b| |  <=   |a-b|    (reverse? triangle inequality)

(see https://math.stackexchange.com/questions/127372/reverse-triangle-inequality-proof)

No, I didn’t use the triangle inequality in that proof. I’m not quite sure what proof the authors had in mind, that would require the triangle inequality. Maybe that comment belonged with 7a? I used the triangle inequality there. 

I will write up my solution tomorrow;   would you mind checking my  | inequalities|?

Sure, will do.

[jim rothstein]

Hi Lyle:

Attached is my handwritten "solution" to product of 2 Cauchy sequences.

It is NOT a great proof,  can't seem to tame absolute values with much ease.   Might even be very wrong.

But please do look   at "Need to Show"   (page 1 bottom)  I think it is different from you proved.

On page 2 my strategy is to show pq is bounded and then note that bound turns out to be Cauchy itself.

jim