Theorems · Theorem · measure theory

MeasureTheory.integrableOn_Icc_deriv_smul_iff_of_deriv_nonneg

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

Defined in

Mathlib.MeasureTheory.Function.JacobianOneDim

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace