Interval integrals

Stream: new members

[Julia Ramos Alves]

Hello again, I'm trying to solve some interval integrals but I'm very confused about how to go about them. Can someone help me understand which steps to take with the following test code?
lemma test : ∫ x in 0 .. (2 * real.pi), x = 2 * (real.pi)^2 :=

The imports I have are import analysis.fourier and import measure_theory.integral.interval_integral.

[Moritz Doll]

you want to use docs#integral_id

[Moritz Doll]

library_search only finds things that you have included so it could not find that

[Moritz Doll]

and as Kevin already said, giving a #mwe is really helpful. In this case it would be

import measure_theory.integral.interval_integral
import data.real

example : ∫ x in 0 .. (2 * real.pi), x = 2 * (real.pi)^2 :=
begin
  sorry,
end

(you get the code formatting by using four backticks)

[Anatole Dedecker]

simp should solve this, right ?

[Moritz Doll]

yes

[Julia Ramos Alves]

It still does not work, not even with simp, and I also have added import analysis.special_functions.integrals
I don't understand what is wrong. This is the whole code:

import measure_theory.integral.interval_integral
import data.real.basic
import analysis.special_functions.integrals

example : ∫ x in 0 .. (2 * real.pi), x = 2 * (real.pi)^2 :=
begin
  rw integral_id,
end

[Moritz Doll]

example : ∫ x in 0 .. (2 * real.pi), x = 2 * (real.pi)^2 :=
begin
  rw integral_id,
  ring,
end

nothing was wrong, rw just took care of the integral and then you have to solve obvious algebraic equalities

[Moritz Doll]

here is a good summary on what ring does: https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2022/Part_C/tactics/ring.html