MeasureTheory.integrable_condexpIndSMul

theorem MeasureTheory.integrable_condexpIndSMul : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [inst_1 : NormedSpace ℝ G] (hm : m ≤ m0) [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (x : G), MeasureTheory.Integrable (↑↑(MeasureTheory.condexpIndSMul hm hs hμs x)) μ

The theorem `MeasureTheory.integrable_condexpIndSMul` states that for any type `α`, and any normed additive commutative group `G`, given two measurable spaces `m` and `m0` over `α`, a measure `μ` over `α`, a set `s` of `α`, a real normed space structure over `G`, and an element `x` of `G`: If `m` is a sub-measurable space of `m0`, the trimmed measure `μ.trim hm` is sigma-finite, the set `s` is measurable, and the measure of the set `s` is finite (i.e., not infinity), then the conditional expectation of the set `s` scaled by multiplication with the element `x`, denoted as `MeasureTheory.condexpIndSMul hm hs hμs x`, is integrable with respect to the measure `μ`. In simpler terms, if we have a space that is measurable and has finite measure, the expected value of the set, scaled by a certain factor, is finite when integrated over the measure space.

More concisely: Given a sub-measurable space `m` of a sigma-finite measurable space `m0` over a type `α`, a finite measure `μ` over `α`, an element `x` in a real normed space with respect to a normed additive commutative group `G`, and a measurable set `s` in `α` with finite measure, the conditional expectation of `s` scaled by multiplication with `x` is integrable with respect to `μ`.