Theorems · Theorem · measure theory

intervalIntegrable_of_even

∀ {E : Type u_5} [inst : NormedAddCommGroup E] {f : ℝ → E},
  (∀ (x : ℝ), f x = f (-x)) →
    (∀ (x : ℝ), 0 < x → IntervalIntegrable f MeasureTheory.volume 0 x) →
      ∀ {a b : ℝ},
        autoParam (‖f (min 0 a)‖ₑ ≠ ⊤) intervalIntegrable_of_even._auto_1 →
          autoParam (‖f (min 0 b)‖ₑ ≠ ⊤) intervalIntegrable_of_even._auto_3 →
            IntervalIntegrable f MeasureTheory.volume a b

An even function is interval integrable (with respect to the volume measure) on every interval if it is interval integrable (with respect to the volume measure) on every interval of the form 0..x, for positive x.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

1 results in Mathlib

Foundations

Depth 253 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroup