LeanPool.QuasiBorelSpaces.MeasureTheory.Measure

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.MeasureTheory.Measure.

theorem MeasureTheory.Measure.measurable_map' {A : Type u_1} {B : Type u_2} {C : Type u_3} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C] {f : A → B → C} (hf : Measurable fun (x : A × B) => match x with | (x, y) => f x y) {μ : A → Measure B} (hμ₁ : Measurable μ) [∀ (x : A), IsFiniteMeasure (μ x)] : Measurable fun (x : A) => map (f x) (μ x)

theorem MeasureTheory.Measure.measurable_apply {A : Type u_1} {B : Type u_2} [MeasurableSpace A] [MeasurableSpace B] {μ : A → Measure B} (hμ : Measurable μ) (hμ' : ProbabilityTheory.IsSFiniteKernel { toFun := μ, measurable' := hμ }) {i : A → Set B} (hi : Measurable fun (x : B × A) => x.1 ∈ i x.2) : Measurable fun (x : A) => (μ x) (i x)

noncomputable def MeasureTheory.Measure.mapOption {A : Type u_1} {B : Type u_2} [MeasurableSpace A] [MeasurableSpace B] (f : A → Option B) (μ : Measure A) : Measure B

The push-forward of a measure by a partial function.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasureTheory.Measure.lintegral_mapOption {A : Type u_1} {B : Type u_2} [MeasurableSpace A] [MeasurableSpace B] {k : B → ENNReal} (hk : Measurable k) {f : A → Option B} (hf : Measurable f) (μ : Measure A) : ∫⁻ (b : B), k b ∂mapOption f μ = ∫⁻ (a : A), (f a).elim 0 k ∂μ

instance MeasureTheory.Measure.instMeasurableSMul₂ENNReal_leanPool {B : Type u_2} [MeasurableSpace B] : MeasurableSMul₂ ENNReal (Measure B)