Zulip Chat Archive

Stream: new members

Topic: theorem Area_of_Circle


view this post on Zulip Mii Nguyen (Nov 28 2018 at 15:41):

Hello. I'm My, a very new beginner of Lean user. I come from Formal Abstract's group in Hanoi. Recently I try to formalize the theorem of 'Area of a circle'. So far I have

theorem Area_of_Circle (x: ℝ × ℝ) (r :ℝ) (r ≥ 0) [measure_theory.measure_space (ℝ × ℝ)] [measure_theory.measure_space (closed_ball (x) (r))]: measure_theory.volume(closed_ball (x) (r)) = 2 * real.pi * r^2 :=sorry

It seems to work. But if I defined the Circle, then use it in the theorem, it sends me an error 'don't know how to synthesize placeholder'

variables {x: ℝ × ℝ }{r: ℝ}

def Circle{x: ℝ × ℝ }{r: ℝ} {r ≥ 0} := closed_ball (x) (r)

theorem Area (r ≥ 0) [measure_theory.measure_space (ℝ × ℝ)] [measure_theory.measure_space (Circle)]: measure_theory.volume(Circle) = 2 * real.pi * r^2 :=sorry
#print Area

Could anyone please explain it to me? How can I defind a set the use it in theorem? Thank you very much for your time,
My

view this post on Zulip Johan Commelin (Nov 28 2018 at 15:45):

The [measure_theory.measure_space (ℝ × ℝ)] introduces a new measure (about which you can't say anything).

view this post on Zulip Kevin Buzzard (Nov 28 2018 at 15:45):

Yes -- you should delete this

view this post on Zulip Johan Commelin (Nov 28 2018 at 15:46):

You would want to use the existing measure. And probably you want to use integration to calculate the area.

view this post on Zulip Johan Commelin (Nov 28 2018 at 15:46):

So far there is very little about integration, as far as I know.

view this post on Zulip Johan Commelin (Nov 28 2018 at 15:46):

So I fear this is going to be a pretty hard exercise.

view this post on Zulip Johan Commelin (Nov 28 2018 at 15:50):

Or well, if you only want to state the theorem (not prove it), that should be possible.

view this post on Zulip Johan Commelin (Nov 28 2018 at 15:51):

@Mii Nguyen I think you should also make the x and r arguments to Circle explicit. (By using () instead of {}.) That way it is clearer about which circle you are talking.

view this post on Zulip Patrick Massot (Nov 28 2018 at 15:58):

I just had a look, it seems we have Lebesgue measure for R, but no product instance for measurable spaces, so that would be needed in order to state this theorem. It shouldn't be hard. As Johan wrote, you also need better understanding of implicit vs explicit arguments. A better starting point would be:

import analysis.measure_theory.lebesgue_measure
import analysis.exponential
open real

def Circle (x:  × ) (r: )  := closed_ball x r

theorem Area (x :  × ) {r : } (H : r  0) : measure_theory.volume(Circle x r) = some 2 * pi * r^2, _⟩ :=sorry

view this post on Zulip Patrick Massot (Nov 28 2018 at 15:59):

The underscore at the very end is an exercise to fill in, it must be replaced by a proof of 0 <= 2 * pi * r^2

view this post on Zulip Patrick Massot (Nov 28 2018 at 16:01):

After filling in this proof, Lean will still complain it doesn't know what measure to use on ℝ × ℝ but, as I wrote, this require adding something to mathlib

view this post on Zulip Patrick Massot (Nov 28 2018 at 16:03):

The some is a bit annoying, it's there in order to indicate that this disk has finite measure. I guess the interface is still very rough here

view this post on Zulip Chris Hughes (Nov 28 2018 at 16:09):

I thought the area of a circle was πr2\pi r^2 not 2πr22\pi r^2

view this post on Zulip Patrick Massot (Nov 28 2018 at 16:09):

also

view this post on Zulip Patrick Massot (Nov 28 2018 at 16:10):

And also I would call this a disk, not a circle, but that may be only in France

view this post on Zulip Patrick Massot (Nov 28 2018 at 16:21):

@Mii Nguyen do you want to work on the exercise of stating this theorem after admitting the existence of some relevant measure on the plane, or do you want to get an answer? I did the exercise, so I wouldn't cost me anything, but I don't want to ruin your training plan.

view this post on Zulip Mii Nguyen (Nov 28 2018 at 16:35):

Thank you for your advices!
@Johan Commelin I tried to use integration at the first time but I lost in the maze of intergration.lean
@Johan Commelin @Patrick Massot by that, I know that I need to work more in arguments. Thank you
I need to declare that Circle (dist) is measurable, so I use [measure_theory.measure_space (Circle)]
The exercise is good for me. So I will try to instance Lebesgue measure for RxR in mathlib.

view this post on Zulip Patrick Massot (Nov 28 2018 at 16:38):

Let me insist that correctly instantiating measure_space (ℝ × ℝ) is much harder than admitting its existence and finishing stating the disk area theorem. I suggest the later as a first exercise


Last updated: May 18 2021 at 17:44 UTC