Theorems · Theorem · real analysis

intervalIntegral.integrable_deriv_smul_comp_iff_of_deriv_nonneg

∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), 0 ≤ f' x) →
        (IntervalIntegrable (fun x => f' x • (g ∘ f) x) MeasureTheory.volume a b ↔
          IntervalIntegrable g MeasureTheory.volume (f a) (f b))

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace