∀ {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