tactics to calculate the area of ​​a circle

Stream: general

[ZHAO Jinxiang]

import Mathlib

example : (MeasureTheory.volume {(a, b) : ℝ × ℝ | a ^ 2 + b ^ 2 < 1}).toReal = π := by
  sorry

Is there any tactics to calc this?

[Kevin Buzzard]

You don't want a tactic to prove this -- you want a theorem in the library. The proof isn't "apply some generally and widely-applicable technique" such as the technique which simultaneously proves $(x+y)^2=x^2+2xy+y^2$ and $(x+y)(x-y)=x^2-y^2$. The result you want reduces (after some calculation) to an explicit integral, and integrals are an art. Tactics are science.

[Edward van de Meent]

i feel like there should be a better way to spell "the circle around 0,0" than just writing out the definition... i gave it a try, but it seems that with current mathlib, you get (ball ((WithLp.equiv 2 (ℝ × ℝ)).symm (0,0)) 1)? but there isn't a MeasureSpace instance for WithLp 2 (ℝ × ℝ)...

[Eric Wieser]

example : (MeasureTheory.volume (ball (!₂[(0 : ℝ), 0]) 1)).toReal = π := by
  sorry

works

[Eric Wieser]

But we should probably add the missing

instance : MeasurableSpace (WithLp p (ℝ × ℝ)) := Prod.instMeasurableSpace
instance : BorelSpace (WithLp p (ℝ × ℝ)) := Prod.borelSpace

[Eric Wieser]

Which makes your version work

[Eric Wieser]

(We already did this for the Pi version)

[Edward van de Meent]

shouldn't you at some point have to prove that the product topology is compatible with the new norm?

[Edward van de Meent]

i.e. shouldn't there be a MetricSpace instance here? there already is. i really should look first

[Eric Wieser]

I think the result you're thinking of is that we should prove that WithLp.equiv is measure preserving on prod types (which we got for Pi types in #7037)

[Yury G. Kudryashov]

Should we have a generic MeasurableSpace instance on WithLp p X instead?

[Yury G. Kudryashov]

BTW I think that #new members is a better channel for questions like this one.

[Eric Wieser]

Yury G. Kudryashov said:

Should we have a generic MeasurableSpace instance on WithLp p X instead?

Seems reasonable, though we should check whether we decided against this in the previous discussion

[Eric Wieser]

It looks like inheriting the MeasurableSpace would be ok, but inheriting the MeasureSpace would create diamonds

[Johan Commelin]

Kevin Buzzard said:

The result you want reduces (after some calculation) to an explicit integral, and integrals are an art. Tactics are science.

I think we can aim for a bit more. There are various software packages out there that will calculate a bunch of integrals for you. And some of them can even leave step-by-step traces of how the computation goes.
It would be great to tactify that. And of course it will not be able to handle every integral out there. But if it handles the common cases, that will already be good.

[Ruben Van de Velde]

That sounds like a Project - maybe someone could file an issue