Induced Outer Measure

We can extend a function defined on a subset of Set α to an outer measure. The underlying function is called extend, and the measure it induces is called inducedOuterMeasure.

Some lemmas below are proven twice, once in the general case, and one where the function m is only defined on measurable sets (i.e. when P = MeasurableSet). In the latter cases, we can remove some hypotheses in the statement. The general version has the same name, but with a prime at the end.

Tags

outer measure

def MeasureTheory.extend {α : Type u_1} {P : α → Prop} (m : (s : α) → P s → ENNReal) (s : α) : ENNReal

We can trivially extend a function defined on a subclass of objects (with codomain ℝ≥0∞) to all objects by defining it to be ∞ on the objects not in the class.

Equations

• MeasureTheory.extend m s = ⨅ (h : P s), m s h

theorem MeasureTheory.extend_eq {α : Type u_1} {P : α → Prop} (m : (s : α) → P s → ENNReal) {s : α} (h : P s) : extend m s = m s h

theorem MeasureTheory.extend_eq_top {α : Type u_1} {P : α → Prop} (m : (s : α) → P s → ENNReal) {s : α} (h : ¬P s) : extend m s = ⊤

theorem MeasureTheory.smul_extend {α : Type u_1} {P : α → Prop} (m : (s : α) → P s → ENNReal) {R : Type u_2} [Zero R] [SMulWithZero R ENNReal] [IsScalarTower R ENNReal ENNReal] [NoZeroSMulDivisors R ENNReal] {c : R} (hc : c ≠ 0) : c • extend m = extend fun (s : α) (h : P s) => c • m s h

theorem MeasureTheory.le_extend {α : Type u_1} {P : α → Prop} (m : (s : α) → P s → ENNReal) {s : α} (h : P s) : m s h ≤ extend m s

theorem MeasureTheory.extend_congr {α : Type u_1} {P : α → Prop} (m : (s : α) → P s → ENNReal) {β : Type u_2} {Pb : β → Prop} {mb : (s : β) → Pb s → ENNReal} {sa : α} {sb : β} (hP : P sa ↔ Pb sb) (hm : ∀ (ha : P sa) (hb : Pb sb), m sa ha = mb sb hb) : extend m sa = extend mb sb

@[simp]

theorem MeasureTheory.extend_top {α : Type u_2} {P : α → Prop} : (extend fun (x : α) (x : P x) => ⊤) = ⊤

theorem MeasureTheory.extend_iUnion_nat {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) {f : ℕ → Set α} (hm : ∀ (i : ℕ), P (f i)) (mU : m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) : extend m (⋃ (i : ℕ), f i) = ∑' (i : ℕ), extend m (f i)

theorem MeasureTheory.extend_empty {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (P0 : P ∅) (m0 : m ∅ P0 = 0) : extend m ∅ = 0

theorem MeasureTheory.extend_iUnion_le_tsum_nat' {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) (s : ℕ → Set α) : extend m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend m (s i)

theorem MeasureTheory.extend_mono' {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) ⦃s₁ s₂ : Set α⦄ (h₁ : P s₁) (hs : s₁ ⊆ s₂) : extend m s₁ ≤ extend m s₂

theorem MeasureTheory.extend_iUnion {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (P0 : P ∅) (m0 : m ∅ P0 = 0) (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Function.onFun Disjoint f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) {β : Type u_2} [Countable β] {f : β → Set α} (hd : Pairwise (Function.onFun Disjoint f)) (hm : ∀ (i : β), P (f i)) : extend m (⋃ (i : β), f i) = ∑' (i : β), extend m (f i)

theorem MeasureTheory.extend_union {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (P0 : P ∅) (m0 : m ∅ P0 = 0) (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Function.onFun Disjoint f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) {s₁ s₂ : Set α} (hd : Disjoint s₁ s₂) (h₁ : P s₁) (h₂ : P s₂) : extend m (s₁ ∪ s₂) = extend m s₁ + extend m s₂

def MeasureTheory.inducedOuterMeasure {α : Type u_1} {P : Set α → Prop} (m : (s : Set α) → P s → ENNReal) (P0 : P ∅) (m0 : m ∅ P0 = 0) : OuterMeasure α

Given an arbitrary function on a subset of sets, we can define the outer measure corresponding to it (this is the unique maximal outer measure that is at most m on the domain of m).

Equations

• MeasureTheory.inducedOuterMeasure m P0 m0 = MeasureTheory.OuterMeasure.ofFunction (MeasureTheory.extend m) ⋯

theorem MeasureTheory.le_inducedOuterMeasure {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} {μ : OuterMeasure α} : μ ≤ inducedOuterMeasure m P0 m0 ↔ ∀ (s : Set α) (hs : P s), μ s ≤ m s hs

theorem MeasureTheory.inducedOuterMeasure_union_of_false_of_nonempty_inter {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} {s t : Set α} (h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → ¬P u) : (inducedOuterMeasure m P0 m0) (s ∪ t) = (inducedOuterMeasure m P0 m0) s + (inducedOuterMeasure m P0 m0) t

If P u is False for any set u that has nonempty intersection both with s and t, then μ (s ∪ t) = μ s + μ t, where μ = inducedOuterMeasure m P0 m0.

E.g., if α is an (e)metric space and P u = diam u < r, then this lemma implies that μ (s ∪ t) = μ s + μ t on any two sets such that r ≤ edist x y for all x ∈ s and y ∈ t.

theorem MeasureTheory.inducedOuterMeasure_eq_extend' {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) (m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) {s : Set α} (hs : P s) : (inducedOuterMeasure m P0 m0) s = extend m s

theorem MeasureTheory.inducedOuterMeasure_eq' {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) (m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) {s : Set α} (hs : P s) : (inducedOuterMeasure m P0 m0) s = m s hs

theorem MeasureTheory.inducedOuterMeasure_eq_iInf {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) (m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) (s : Set α) : (inducedOuterMeasure m P0 m0) s = ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht

theorem MeasureTheory.inducedOuterMeasure_preimage {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) (m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) (f : α ≃ α) (Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s) (mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs) {A : Set α} : (inducedOuterMeasure m P0 m0) (⇑f ⁻¹' A) = (inducedOuterMeasure m P0 m0) A

theorem MeasureTheory.inducedOuterMeasure_exists_set {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) (m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) {s : Set α} (hs : (inducedOuterMeasure m P0 m0) s ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ (t : Set α), P t ∧ s ⊆ t ∧ (inducedOuterMeasure m P0 m0) t ≤ (inducedOuterMeasure m P0 m0) s + ε

theorem MeasureTheory.inducedOuterMeasure_caratheodory {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) (m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) (s : Set α) : MeasurableSet s ↔ ∀ (t : Set α), P t → (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t

To test whether s is Carathéodory-measurable we only need to check the sets t for which P t holds. See ofFunction_caratheodory for another way to show the Carathéodory-measurability of s.

If P is MeasurableSet for some measurable space, then we can remove some hypotheses of the above lemmas.

theorem MeasureTheory.extend_mono {α : Type u_1} [MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Function.onFun Disjoint f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (hs : s₁ ⊆ s₂) : extend m s₁ ≤ extend m s₂

theorem MeasureTheory.extend_iUnion_le_tsum_nat {α : Type u_1} [MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Function.onFun Disjoint f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) (s : ℕ → Set α) : extend m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend m (s i)

theorem MeasureTheory.inducedOuterMeasure_eq_extend {α : Type u_1} [MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Function.onFun Disjoint f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) {s : Set α} (hs : MeasurableSet s) : (inducedOuterMeasure m ⋯ m0) s = extend m s

theorem MeasureTheory.inducedOuterMeasure_eq {α : Type u_1} [MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Function.onFun Disjoint f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) {s : Set α} (hs : MeasurableSet s) : (inducedOuterMeasure m ⋯ m0) s = m s hs

def MeasureTheory.OuterMeasure.trim {α : Type u_1} [MeasurableSpace α] (m : OuterMeasure α) : OuterMeasure α

Given an outer measure m we can forget its value on non-measurable sets, and then consider m.trim, the unique maximal outer measure less than that function.

Equations

• m.trim = MeasureTheory.inducedOuterMeasure (fun (s : Set α) (x : MeasurableSet s) => m s) ⋯ ⋯

theorem MeasureTheory.OuterMeasure.le_trim_iff {α : Type u_1} [MeasurableSpace α] {m₁ m₂ : OuterMeasure α} : m₁ ≤ m₂.trim ↔ ∀ (s : Set α), MeasurableSet s → m₁ s ≤ m₂ s

theorem MeasureTheory.OuterMeasure.le_trim {α : Type u_1} [MeasurableSpace α] (m : OuterMeasure α) : m ≤ m.trim

theorem MeasureTheory.OuterMeasure.null_of_trim_null {α : Type u_1} [MeasurableSpace α] (m : OuterMeasure α) {s : Set α} (h : m.trim s = 0) : m s = 0

@[simp]

theorem MeasureTheory.OuterMeasure.trim_eq {α : Type u_1} [MeasurableSpace α] (m : OuterMeasure α) {s : Set α} (hs : MeasurableSet s) : m.trim s = m s

theorem MeasureTheory.OuterMeasure.trim_congr {α : Type u_1} [MeasurableSpace α] {m₁ m₂ : OuterMeasure α} (H : ∀ {s : Set α}, MeasurableSet s → m₁ s = m₂ s) : m₁.trim = m₂.trim

theorem MeasureTheory.OuterMeasure.trim_mono {α : Type u_1} [MeasurableSpace α] : Monotone trim

theorem MeasureTheory.OuterMeasure.trim_anti_measurableSpace {α : Type u_2} (m : OuterMeasure α) {m0 m1 : MeasurableSpace α} (h : m0 ≤ m1) : m.trim ≤ m.trim

OuterMeasure.trim is antitone in the σ-algebra.

theorem MeasureTheory.OuterMeasure.trim_le_trim_iff {α : Type u_1} [MeasurableSpace α] {m₁ m₂ : OuterMeasure α} : m₁.trim ≤ m₂.trim ↔ ∀ (s : Set α), MeasurableSet s → m₁ s ≤ m₂ s

theorem MeasureTheory.OuterMeasure.trim_eq_trim_iff {α : Type u_1} [MeasurableSpace α] {m₁ m₂ : OuterMeasure α} : m₁.trim = m₂.trim ↔ ∀ (s : Set α), MeasurableSet s → m₁ s = m₂ s

theorem MeasureTheory.OuterMeasure.trim_eq_iInf {α : Type u_1} [MeasurableSpace α] (m : OuterMeasure α) (s : Set α) : m.trim s = ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t

theorem MeasureTheory.OuterMeasure.trim_eq_iInf' {α : Type u_1} [MeasurableSpace α] (m : OuterMeasure α) (s : Set α) : m.trim s = ⨅ (t : { t : Set α // s ⊆ t ∧ MeasurableSet t }), m ↑t

theorem MeasureTheory.OuterMeasure.trim_trim {α : Type u_1} [MeasurableSpace α] (m : OuterMeasure α) : m.trim.trim = m.trim

@[simp]

theorem MeasureTheory.OuterMeasure.trim_top {α : Type u_1} [MeasurableSpace α] : ⊤.trim = ⊤

@[simp]

theorem MeasureTheory.OuterMeasure.trim_zero {α : Type u_1} [MeasurableSpace α] : trim 0 = 0

theorem MeasureTheory.OuterMeasure.trim_sum_ge {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} (m : ι → OuterMeasure α) : (sum fun (i : ι) => (m i).trim) ≤ (sum m).trim

theorem MeasureTheory.OuterMeasure.exists_measurable_superset_eq_trim {α : Type u_1} [MeasurableSpace α] (m : OuterMeasure α) (s : Set α) : ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ m t = m.trim s

theorem MeasureTheory.OuterMeasure.exists_measurable_superset_of_trim_eq_zero {α : Type u_1} [MeasurableSpace α] {m : OuterMeasure α} {s : Set α} (h : m.trim s = 0) : ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ m t = 0

theorem MeasureTheory.OuterMeasure.exists_measurable_superset_forall_eq_trim {α : Type u_1} [MeasurableSpace α] {ι : Sort u_2} [Countable ι] (μ : ι → OuterMeasure α) (s : Set α) : ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s

If μ i is a countable family of outer measures, then for every set s there exists a measurable set t ⊇ s such that μ i t = (μ i).trim s for all i.

theorem MeasureTheory.OuterMeasure.trim_binop {α : Type u_1} [MeasurableSpace α] {m₁ m₂ m₃ : OuterMeasure α} {op : ENNReal → ENNReal → ENNReal} (h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)) (s : Set α) : m₁.trim s = op (m₂.trim s) (m₃.trim s)

If m₁ s = op (m₂ s) (m₃ s) for all s, then the same is true for m₁.trim, m₂.trim, and m₃ s.

theorem MeasureTheory.OuterMeasure.trim_op {α : Type u_1} [MeasurableSpace α] {m₁ m₂ : OuterMeasure α} {op : ENNReal → ENNReal} (h : ∀ (s : Set α), m₁ s = op (m₂ s)) (s : Set α) : m₁.trim s = op (m₂.trim s)

If m₁ s = op (m₂ s) for all s, then the same is true for m₁.trim and m₂.trim.

theorem MeasureTheory.OuterMeasure.trim_add {α : Type u_1} [MeasurableSpace α] (m₁ m₂ : OuterMeasure α) : (m₁ + m₂).trim = m₁.trim + m₂.trim

trim is additive.

theorem MeasureTheory.OuterMeasure.trim_smul {α : Type u_1} [MeasurableSpace α] {R : Type u_2} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (c : R) (m : OuterMeasure α) : (c • m).trim = c • m.trim

trim respects scalar multiplication.

theorem MeasureTheory.OuterMeasure.trim_sup {α : Type u_1} [MeasurableSpace α] (m₁ m₂ : OuterMeasure α) : (m₁ ⊔ m₂).trim = m₁.trim ⊔ m₂.trim

trim sends the supremum of two outer measures to the supremum of the trimmed measures.

theorem MeasureTheory.OuterMeasure.trim_iSup {α : Type u_1} [MeasurableSpace α] {ι : Sort u_2} [Countable ι] (μ : ι → OuterMeasure α) : (⨆ (i : ι), μ i).trim = ⨆ (i : ι), (μ i).trim

trim sends the supremum of a countable family of outer measures to the supremum of the trimmed measures.

theorem MeasureTheory.OuterMeasure.restrict_trim {α : Type u_1} [MeasurableSpace α] {μ : OuterMeasure α} {s : Set α} (hs : MeasurableSet s) : ((restrict s) μ).trim = (restrict s) μ.trim

The trimmed property of a measure μ states that μ.toOuterMeasure.trim = μ.toOuterMeasure. This theorem shows that a restricted trimmed outer measure is a trimmed outer measure.