Zulip Chat Archive

Stream: new members

Topic: Integral of real.sqrt


view this post on Zulip James Arthur (Jan 08 2021 at 11:35):

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?

view this post on Zulip Kenny Lau (Jan 08 2021 at 11:37):

I think you need to open_locale something

view this post on Zulip Shing Tak Lam (Jan 08 2021 at 11:47):

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

view this post on Zulip James Arthur (Jan 08 2021 at 11:49):

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

view this post on Zulip James Arthur (Jan 08 2021 at 11:50):

IT WORKS, IT WAS JUST ME BEING STUPID!

view this post on Zulip Kevin Buzzard (Jan 08 2021 at 11:50):

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

view this post on Zulip James Arthur (Jan 08 2021 at 11:51):

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

view this post on Zulip Răzvan Flavius Panda (Jan 08 2021 at 11:52):

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

view this post on Zulip Răzvan Flavius Panda (Jan 08 2021 at 11:52):

image.png

view this post on Zulip Kevin Buzzard (Jan 08 2021 at 11:52):

I think we can save the spam for the discord


Last updated: May 14 2021 at 00:42 UTC