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 := ⋯ } }

instance MeasureTheory.Measure.instIsZeroApplySetENNReal {α : Type u_1} {mα : MeasurableSpace α} : IsZeroApply (Measure α)

@[simp]

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

@[deprecated FunLike.coe_zero (since := "2026-10-23")]

theorem MeasureTheory.Measure.coe_zero {F : Type u_2} {α : Type u_4} {β : Type u_5} [FunLike F α β] [Zero F] [Zero β] [IsZeroApply F] : ⇑0 = 0

Alias of FunLike.coe_zero.

@[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.

instance MeasureTheory.Measure.instIsAddApplySetENNReal {α : Type u_1} {mα : MeasurableSpace α} : IsAddApply (Measure α)

@[simp]

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

@[deprecated FunLike.coe_add (since := "2026-10-23")]

theorem MeasureTheory.Measure.coe_add {F : Type u_2} {α : Type u_4} {β : Type u_5} [FunLike F α β] [Add F] [Add β] [IsAddApply F] (f g : F) : ⇑(f + g) = ⇑f + ⇑g

Alias of FunLike.coe_add.

@[deprecated add_apply (since := "2026-10-23")]

theorem MeasureTheory.Measure.add_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Add β} {inst✝² : Add F} [self : IsAddApply F] (f g : F) (x : α) : (f + g) x = f x + g x

Alias of add_apply.

@[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.

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

@[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

@[deprecated FunLike.coe_smul (since := "2026-10-23")]

theorem MeasureTheory.Measure.coe_smul {M : Type u_1} {F : Type u_2} {α : Type u_4} {β : Type u_5} [FunLike F α β] [SMul M F] [SMul M β] [IsSMulApply M F] (n : M) (f : F) : ⇑(n • f) = n • ⇑f

Alias of FunLike.coe_smul.

@[simp]

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

@[deprecated smul_apply (since := "2026-10-23")]

theorem MeasureTheory.Measure.smul_apply {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst✝ : FunLike F α β} {inst✝¹ : SMul M β} {inst✝² : SMul M F} [self : IsSMulApply M F] (f : F) (n : M) (x : α) : (n • f) x = n • f x

Alias of smul_apply.

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 = { toSMul := MeasureTheory.Measure.instSMul, mul_smul := ⋯, one_smul := ⋯ }

@[instance_reducible]

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

Equations

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

@[deprecated FunLike.coeAddHom (since := "2026-10-23")]

def MeasureTheory.Measure.coeAddHom (F : Type u_1) (α : Type u_2) (β : Type u_3) [FunLike F α β] [Add F] [Add β] [IsAddApply F] : F →ₙ+ α → β

Alias of FunLike.coeAddHom.

Equations

• MeasureTheory.Measure.coeAddHom = FunLike.coeAddHom

@[deprecated FunLike.coeAddHom_apply (since := "2026-10-23")]

theorem MeasureTheory.Measure.coeAddHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Add β] [IsAddApply F] (f : F) : (FunLike.coeAddHom F α β) f = ⇑f

Alias of FunLike.coeAddHom_apply.

@[deprecated FunLike.coe_sum (since := "2026-10-23")]

theorem MeasureTheory.Measure.coe_finsetSum {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [FunLike F α β] [AddCommMonoid β] [AddCommMonoid F] [IsZeroApply F] [IsAddApply F] (s : Finset ι) (f : ι → F) : ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)

Alias of FunLike.coe_sum.

@[deprecated sum_apply (since := "2026-10-23")]

theorem MeasureTheory.Measure.finsetSum_apply {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [FunLike F α β] [AddCommMonoid β] [AddCommMonoid F] [IsZeroApply F] [IsAddApply F] (s : Finset ι) (f : ι → F) (x : α) : (∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x

Alias of sum_apply.

@[instance_reducible]

noncomputable 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 = { toMulAction := MeasureTheory.Measure.instMulActionOfIsScalarTowerENNReal, smul_zero := ⋯, smul_add := ⋯ }

@[instance_reducible]

noncomputable 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 = { toDistribMulAction := MeasureTheory.Measure.instDistribMulActionOfIsScalarTowerENNReal, add_smul := ⋯, zero_smul := ⋯ }

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)