Theorems · Theorem · measure theory

intervalIntegrable_of_odd

∀ {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_odd._auto_1 →
          autoParam (‖f (min 0 b)‖ₑ ≠ ⊤) intervalIntegrable_of_odd._auto_3 →
            IntervalIntegrable f MeasureTheory.volume a b

An odd function is interval integrable (with respect to the volume measure) on every interval iff 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

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup