MeasureTheory.OuterMeasure.Induced

inducedOuterMeasure

variable {α : Type*} {P : α → Prop}
variable (m : ∀ s : α, P s → ℝ≥0∞)

/-- 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. -/
def extend (s : α) : ℝ≥0∞ :=
  ⨅ h : P s, m s h

theorem extend_eq {s : α} (h : P s) : extend m s = m s h := by simp [extend, h]

extendは\(\{s ∈ α | P (s)\}\)の値域で定義される関数をそうではない部分に対して\(\infty\)で拡張しています. extend_eqは実はiInf_posから直接従います.iInf_posを詳しく見ていきます.

@[simp]
theorem iInf_pos {p : Prop} {f : p → α} (hp : p) : ⨅ h : p, f h = f hp :=
  le_antisymm (iInf_le _ _) (le_iInf fun _ => le_rfl)

iInf_posの右辺のle_rflは以下の証明を行っています.

p : Prop
f : p → α
hp x✝ : p
⊢ f hp ≤ f x✝

ここでhp x✝はproof irrelevanceよりdefinitionally equalになっています.

以下のextend_emptyはextend_eqから直ちに従います.

variable (P0 : P ∅) (m0 : m ∅ P0 = 0)

include P0 m0 in
theorem extend_empty : extend m ∅ = 0 :=
  (extend_eq _ P0).trans m0

variable {m : ∀ s : Set α, P s → ℝ≥0∞}
variable (P0 : P ∅) (m0 : m ∅ P0 = 0)

/-- 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`). -/
def inducedOuterMeasure : OuterMeasure α :=
  OuterMeasure.ofFunction (extend m) (extend_empty P0 m0)

inducedOuterMeasureについて型の確認を行います. ofFunctionは第一引数にSet α → ℝ≥0∞を取り(OfFunctionを参照), 第二引数にm ∅ = 0を取ります. 実際にはextend mは(s : Set α) → P s → ℝ≥0∞の型をもち, P sはPropであるため, extend mはSet α → ℝ≥0∞の型を持ちます. また, extend_empty P0 m0はm ∅ = 0の型を持ちます. したがってinducedOuterMeasureはOuterMeasure αの型を持ちます.

trim

/-- 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. -/
def trim : OuterMeasure α :=
  inducedOuterMeasure (P := MeasurableSet) (fun s _ => m s) .empty m.empty

theorem le_trim : m ≤ m.trim := le_trim_iff.2 fun _ _ ↦ le_rfl

trimは全ての可測集合ではない集合に対しての外測度をinfを置き換えた外測度(外測度の可測集合への制限)です. この時, le_trim : m ≤ m.trimが成り立ちます.