Theorems · Theorem · measure theory

MeasureTheory.setToFun_of_le_map

∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {β : Type u_7}
  {x : MeasurableSpace β} {μ' : MeasureTheory.Measure β} {φ : α → β} {T' : Set β → E →L[ℝ] F}
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ' T' C') {f : β → E},
  MeasureTheory.Integrable (f ∘ φ) μ →
    MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map φ μ) →
      Measurable φ →
        μ' ≤ MeasureTheory.Measure.map φ μ →
          (∀ (s : Set β) (x_1 : E), MeasurableSet s → (T' s) x_1 = (T (φ ⁻¹' s)) x_1) →
            MeasureTheory.setToFun μ' T' hT' f = MeasureTheory.setToFun μ T hT (f ∘ φ)

Defined in

Mathlib.MeasureTheory.Integral.SetToL1

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace