Integral of real.sqrt

Stream: new members

[James Arthur]

Hi,
I'm trying to prove the area of a circle and so I need to do the integral of a sqrt, this is th current setup,

import data.real.basic analysis.special_functions.trigonometric
import measure_theory.interval_integral
import data.real.sqrt

example (r : ℝ) (x : ℝ) : ∫ (real.sqrt x) in 0..r, x = r :=
begin
  sorry
end

and it gives me an error I don't understnad, it gives,

invalid binder, atomic identifier expected

What does this mean / how can I fix it?

[Kenny Lau]

I think you need to open_locale something

[Shing Tak Lam]

Also isn't the syntax ∫ x in (0 : ℝ) .. r, real.sqrt x?

[James Arthur]

Ooooh, is it? I went from the integral of x example where it gets confusing and assumed it was like deriv

[James Arthur]

IT WORKS, IT WAS JUST ME BEING STUPID!

[Kevin Buzzard]

lucky Zulip doesn't have that capital letter warning bot like the discord ;-)

[James Arthur]

haha, indeed. I can use all the caps I want!

[Răzvan Flavius Panda]

oh, now I WANT TO TRY THAT to see what the bot does

[Răzvan Flavius Panda]

image.png

[Kevin Buzzard]

I think we can save the spam for the discord