Integrals of odd functions over symmetric intervals #
An odd integrand into a real normed space integrates to zero over an interval [-R, R]
symmetric about the origin.
No integrability hypothesis is needed. The substitution t ↦ -t carries [-R, R] to itself, so
intervalIntegral.integral_comp_neg identifies the integral with the integral of t ↦ g (-t);
oddness turns that into the negative of the original, and in a real vector space an element equal
to its own negative is zero. In particular the statement is also true (vacuously, both sides being
0) when g fails to be integrable.
Main results #
intervalIntegral.integral_eq_zero_of_odd—∫ t in -R..R, g t = 0for oddg.
@[simp]
theorem
intervalIntegral.integral_eq_zero_of_odd
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{g : ℝ → E}
(hodd : Function.Odd g)
(R : ℝ)
:
An odd integrand integrates to zero over a symmetric interval. No integrability
hypothesis is needed: the substitution t ↦ -t maps [-R, R] to itself, so the integral equals
its own negative.