Theorems · Theorem · measure theory
Measurable.lmarginal
∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] (μ : (i : δ) → MeasureTheory.Measure (X i))
[inst_1 : DecidableEq δ] {s : Finset δ} {f : ((i : δ) → X i) → ENNReal} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)],
Measurable f → Measurable (∫⋯∫⁻_s, f ∂μ)- Defined in
- Mathlib.MeasureTheory.Integral.Marginal
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 228 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- ENNRealstatement and proof · cited by 9,879
- Measurablestatement and proof · cited by 1,499
- MeasureTheory.SigmaFinitestatement and proof · cited by 526
- Measurable.compproof · cited by 234
- MeasureTheory.lmarginalstatement · cited by 28
- Measurable.lintegral_prod_rightproof · cited by 10
- measurable_updateFinset'proof · cited by 4
Cited by2
Results whose statement or proof uses this declaration.
- MeasureTheory.GridLines.T_insert_le_T_lmarginal_singletonproof · cited by 1
- MeasureTheory.GridLines.T_lmarginal_antitoneproof · cited by 1