The ℝ≥0∞-module of measures

This file provides an ℝ≥0∞-module structure on the space of measures.

Tags

measure, module

@[instance_reducible]

instance MeasureTheory.Measure.instZero {α : Type u_1} {mα : MeasurableSpace α} : Zero (Measure α)

Equations

• MeasureTheory.Measure.instZero = { zero := let __OuterMeasure := 0; { toOuterMeasure := __OuterMeasure, m_iUnion := ⋯, trim_le := ⋯ } }

@[simp]

theorem MeasureTheory.Measure.zero_toOuterMeasure {α : Type u_1} {mα : MeasurableSpace α} : toOuterMeasure 0 = 0

@[simp]

theorem MeasureTheory.Measure.coe_zero {α : Type u_1} {mα : MeasurableSpace α} : ⇑0 = 0

@[simp]

theorem MeasureTheory.OuterMeasure.toMeasure_zero {α : Type u_1} [mα : MeasurableSpace α] (h : mα ≤ OuterMeasure.caratheodory 0) : toMeasure 0 h = 0

@[simp]

theorem MeasureTheory.OuterMeasure.toMeasure_eq_zero {α : Type u_1} {mα : MeasurableSpace α} {μ : OuterMeasure α} (h : mα ≤ μ.caratheodory) : μ.toMeasure h = 0 ↔ μ = 0

theorem MeasureTheory.Measure.apply_eq_zero_of_isEmpty {α : Type u_1} {mα : MeasurableSpace α} [IsEmpty α] (μ : Measure α) (s : Set α) : μ s = 0

instance MeasureTheory.Measure.instSubsingletonOfIsEmpty {α : Type u_1} {mα : MeasurableSpace α} [IsEmpty α] : Subsingleton (Measure α)

theorem MeasureTheory.Measure.eq_zero_of_isEmpty {α : Type u_1} {mα : MeasurableSpace α} [IsEmpty α] (μ : Measure α) : μ = 0

@[simp]

theorem MeasureTheory.Measure.ofMeasurable_zero {α : Type u_1} {mα : MeasurableSpace α} : ofMeasurable (fun (x : Set α) (x_1 : MeasurableSet x) => 0) ⋯ ⋯ = 0

@[instance_reducible]

instance MeasureTheory.Measure.instInhabited {α : Type u_1} {mα : MeasurableSpace α} : Inhabited (Measure α)

Equations

• MeasureTheory.Measure.instInhabited = { default := 0 }

@[instance_reducible]

instance MeasureTheory.Measure.instAdd {α : Type u_1} {mα : MeasurableSpace α} : Add (Measure α)

Equations

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

@[simp]

theorem MeasureTheory.Measure.add_toOuterMeasure {α : Type u_1} {mα : MeasurableSpace α} (μ₁ μ₂ : Measure α) : (μ₁ + μ₂).toOuterMeasure = μ₁.toOuterMeasure + μ₂.toOuterMeasure

@[simp]

theorem MeasureTheory.Measure.coe_add {α : Type u_1} {mα : MeasurableSpace α} (μ₁ μ₂ : Measure α) : ⇑(μ₁ + μ₂) = ⇑μ₁ + ⇑μ₂

theorem MeasureTheory.Measure.add_apply {α : Type u_1} {mα : MeasurableSpace α} (μ₁ μ₂ : Measure α) (s : Set α) : (μ₁ + μ₂) s = μ₁ s + μ₂ s

@[instance_reducible]

instance MeasureTheory.Measure.instSMul {α : Type u_1} {R : Type u_3} {mα : MeasurableSpace α} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] : SMul R (Measure α)

Equations

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

@[simp]

theorem MeasureTheory.Measure.smul_toOuterMeasure {α : Type u_1} {R : Type u_3} {mα : MeasurableSpace α} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (c : R) (μ : Measure α) : (c • μ).toOuterMeasure = c • μ.toOuterMeasure

@[simp]

theorem MeasureTheory.Measure.coe_smul {α : Type u_1} {R : Type u_3} {mα : MeasurableSpace α} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (c : R) (μ : Measure α) : ⇑(c • μ) = c • ⇑μ

@[simp]

theorem MeasureTheory.Measure.coe_nnreal_smul {α : Type u_1} {mα : MeasurableSpace α} (c : NNReal) (μ : Measure α) : ↑c • μ = c • μ

@[simp]

theorem MeasureTheory.Measure.smul_apply {α : Type u_1} {R : Type u_3} {mα : MeasurableSpace α} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (c : R) (μ : Measure α) (s : Set α) : (c • μ) s = c • μ s

instance MeasureTheory.Measure.instSMulCommClassOfENNReal {α : Type u_1} {R : Type u_3} {R' : Type u_4} {mα : MeasurableSpace α} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] [SMul R' ENNReal] [IsScalarTower R' ENNReal ENNReal] [SMulCommClass R R' ENNReal] : SMulCommClass R R' (Measure α)

instance MeasureTheory.Measure.instIsScalarTowerOfENNReal {α : Type u_1} {R : Type u_3} {R' : Type u_4} {mα : MeasurableSpace α} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] [SMul R' ENNReal] [IsScalarTower R' ENNReal ENNReal] [SMul R R'] [IsScalarTower R R' ENNReal] : IsScalarTower R R' (Measure α)

instance MeasureTheory.Measure.instIsCentralScalar {α : Type u_1} {R : Type u_3} {mα : MeasurableSpace α} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] [SMul Rᵐᵒᵖ ENNReal] [IsCentralScalar R ENNReal] : IsCentralScalar R (Measure α)

@[instance_reducible]

instance MeasureTheory.Measure.instMulActionOfIsScalarTowerENNReal {α : Type u_1} {R : Type u_3} {mα : MeasurableSpace α} [Monoid R] [MulAction R ENNReal] [IsScalarTower R ENNReal ENNReal] : MulAction R (Measure α)

Equations

• MeasureTheory.Measure.instMulActionOfIsScalarTowerENNReal = Function.Injective.mulAction MeasureTheory.Measure.toOuterMeasure ⋯ ⋯

@[instance_reducible]

instance MeasureTheory.Measure.instAddCommMonoid {α : Type u_1} {mα : MeasurableSpace α} : AddCommMonoid (Measure α)

Equations

• MeasureTheory.Measure.instAddCommMonoid = Function.Injective.addCommMonoid MeasureTheory.Measure.toOuterMeasure ⋯ ⋯ ⋯ ⋯

def MeasureTheory.Measure.coeAddHom {α : Type u_1} {mα : MeasurableSpace α} : Measure α →+ Set α → ENNReal

Coercion to function as an additive monoid homomorphism.

Equations

• MeasureTheory.Measure.coeAddHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MeasureTheory.Measure.coeAddHom_apply {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) : coeAddHom μ = ⇑μ

@[simp]

theorem MeasureTheory.Measure.coe_finsetSum {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} (I : Finset ι) (μ : ι → Measure α) : ⇑(∑ i ∈ I, μ i) = ∑ i ∈ I, ⇑(μ i)

@[deprecated MeasureTheory.Measure.coe_finsetSum (since := "2026-04-08")]

theorem MeasureTheory.Measure.coe_finset_sum {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} (I : Finset ι) (μ : ι → Measure α) : ⇑(∑ i ∈ I, μ i) = ∑ i ∈ I, ⇑(μ i)

Alias of MeasureTheory.Measure.coe_finsetSum.

theorem MeasureTheory.Measure.finsetSum_apply {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} (I : Finset ι) (μ : ι → Measure α) (s : Set α) : (∑ i ∈ I, μ i) s = ∑ i ∈ I, (μ i) s

@[deprecated MeasureTheory.Measure.finsetSum_apply (since := "2026-04-08")]

theorem MeasureTheory.Measure.finset_sum_apply {α : Type u_1} {ι : Type u_2} {mα : MeasurableSpace α} (I : Finset ι) (μ : ι → Measure α) (s : Set α) : (∑ i ∈ I, μ i) s = ∑ i ∈ I, (μ i) s

Alias of MeasureTheory.Measure.finsetSum_apply.

@[instance_reducible]

instance MeasureTheory.Measure.instDistribMulActionOfIsScalarTowerENNReal {α : Type u_1} {R : Type u_3} {mα : MeasurableSpace α} [Monoid R] [DistribMulAction R ENNReal] [IsScalarTower R ENNReal ENNReal] : DistribMulAction R (Measure α)

Equations

• MeasureTheory.Measure.instDistribMulActionOfIsScalarTowerENNReal = Function.Injective.distribMulAction { toFun := MeasureTheory.Measure.toOuterMeasure, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

@[instance_reducible]

instance MeasureTheory.Measure.instModuleOfIsScalarTowerENNReal {α : Type u_1} {R : Type u_3} {mα : MeasurableSpace α} [Semiring R] [Module R ENNReal] [IsScalarTower R ENNReal ENNReal] : Module R (Measure α)

Equations

• MeasureTheory.Measure.instModuleOfIsScalarTowerENNReal = Function.Injective.module R { toFun := MeasureTheory.Measure.toOuterMeasure, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

instance MeasureTheory.Measure.instIsTorsionFreeOfENNReal {α : Type u_1} {R : Type u_3} {mα : MeasurableSpace α} [Semiring R] [Module R ENNReal] [IsScalarTower R ENNReal ENNReal] [Module.IsTorsionFree R ENNReal] : Module.IsTorsionFree R (Measure α)

@[simp]

theorem MeasureTheory.Measure.ennreal_smul_eq_zero {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {c : ENNReal} : c • μ = 0 ↔ c = 0 ∨ μ = 0

@[simp]

theorem MeasureTheory.Measure.coe_nnreal_smul_apply {α : Type u_1} {mα : MeasurableSpace α} (c : NNReal) (μ : Measure α) (s : Set α) : (c • μ) s = ↑c * μ s

@[simp]

theorem MeasureTheory.Measure.nnreal_smul_coe_apply {α : Type u_1} {mα : MeasurableSpace α} (c : NNReal) (μ : Measure α) (s : Set α) : c • μ s = ↑c * μ s

theorem MeasureTheory.Measure.ae_smul_measure {α : Type u_1} {R : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} {p : α → Prop} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (h : ∀ᵐ (x : α) ∂μ, p x) (c : R) : ∀ᵐ (x : α) ∂c • μ, p x

theorem MeasureTheory.Measure.ae_smul_measure_le {α : Type u_1} {R : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (c : R) : ae (c • μ) ≤ ae μ

theorem MeasureTheory.Measure.ae_ennreal_smul_measure_iff {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {c : ENNReal} {p : α → Prop} (hc : c ≠ 0) : (∀ᵐ (x : α) ∂c • μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p x

@[simp]

theorem MeasureTheory.Measure.ae_ennreal_smul_measure_eq {α : Type u_1} {mα : MeasurableSpace α} {c : ENNReal} (hc : c ≠ 0) (μ : Measure α) : ae (c • μ) = ae μ

theorem MeasureTheory.Measure.ae_smul_measure_iff {α : Type u_1} {R : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Semiring R] [IsDomain R] [Module R ENNReal] [IsScalarTower R ENNReal ENNReal] [Module.IsTorsionFree R ENNReal] {c : R} {p : α → Prop} (hc : c ≠ 0) : (∀ᵐ (x : α) ∂c • μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p x

@[simp]

theorem MeasureTheory.Measure.ae_smul_measure_eq {α : Type u_1} {R : Type u_3} {mα : MeasurableSpace α} [Semiring R] [IsDomain R] [Module R ENNReal] [IsScalarTower R ENNReal ENNReal] [Module.IsTorsionFree R ENNReal] {c : R} (hc : c ≠ 0) (μ : Measure α) : ae (c • μ) = ae μ

theorem MeasureTheory.Measure.measure_eq_left_of_subset_of_measure_add_eq {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} {s t : Set α} (h : (μ + ν) t ≠ ⊤) (h' : s ⊆ t) (h'' : (μ + ν) s = (μ + ν) t) : μ s = μ t

theorem MeasureTheory.Measure.measure_eq_right_of_subset_of_measure_add_eq {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} {s t : Set α} (h : (μ + ν) t ≠ ⊤) (h' : s ⊆ t) (h'' : (μ + ν) s = (μ + ν) t) : ν s = ν t

theorem MeasureTheory.Measure.measure_toMeasurable_add_inter_left {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} {s t : Set α} (hs : MeasurableSet s) (ht : (μ + ν) t ≠ ⊤) : μ (toMeasurable (μ + ν) t ∩ s) = μ (t ∩ s)

theorem MeasureTheory.Measure.measure_toMeasurable_add_inter_right {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} {s t : Set α} (hs : MeasurableSet s) (ht : (μ + ν) t ≠ ⊤) : ν (toMeasurable (μ + ν) t ∩ s) = ν (t ∩ s)