7.3. 可測関数の定義🔗

拡大実数直線 \eRR のBorel集合族を \calB(\eRR) と書く．

Lemma7.3.1

uses 0

Used by 2

Reverse dependency previews

Preview

Definition 7.3.2

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

Tagsleanok

拡大実数直線のBorel集合族. \calB(\eRR)=\sigma(\{[-\infty,a]\mid a\in\RR\}) である．

Lean code for Lemma7.3.1●1 theorem

theoremdefined in NoteKsk/«07mble-funcs».lean

complete

theorem NoteKsk.Chapter07.borel_eReal_eq_generate_Iic_real :
  borel EReal =
    NoteKsk.generatedSigmaAlgebra (Set.range fun a ↦ Set.Iic ↑a)

theorem NoteKsk.Chapter07.borel_eReal_eq_generate_Iic_real :
  borel EReal =
    NoteKsk.generatedSigmaAlgebra
      (Set.range fun a ↦ Set.Iic ↑a)

Mathlib proves `borel_eq_generateFrom_Iic` for all endpoints in an ordered
Borel space.  The lecture notes use only finite real endpoints in `EReal`; this
bridge theorem records that form.

Proof for Lemma 7.3.1

uses 0

[-\infty,a]:=\{x\in\eRR\mid x\le a\} と書き， \mathcal G:=\{[-\infty,a]\mid a\in\RR\} とおく．各 [-\infty,a] の補集合は (a,\infty] であり，これは \eRR の通常の順序位相で開集合だから，[-\infty,a] は閉集合である．よって \mathcal G\subset\calB(\eRR) である．したがって

\sigma(\mathcal G)\subset\calB(\eRR)

である．

逆向きを示す． p,q\in\QQ,\ p<q に対して

(p,\infty]=\eRR\setminus[-\infty,p]\in\sigma(\mathcal G)

であり，また

[-\infty,q)=\bigcup_{n=1}^{\infty}[-\infty,q-\frac1n]\in\sigma(\mathcal G)

である．したがって

(p,q)=(p,\infty]\cap[-\infty,q)\in\sigma(\mathcal G)

も成り立つ．

拡大実数直線 \eRR の通常の順序位相は

\{[-\infty,q)\mid q\in\QQ\} \cup \{(p,q)\mid p,q\in\QQ,\ p<q\} \cup \{(p,\infty]\mid p\in\QQ\}

を可算基底にもつ．この基底の各元は \sigma(\mathcal G) に属する．したがって任意の開集合は可算個の基底元の和集合として書けるので， \sigma(\mathcal G) に属する．よって

\calB(\eRR)\subset\sigma(\mathcal G)

である．以上より等号が成り立つ．

可測空間 (X,\calM) と E\in\calM に対して，E 上に制限された \sigma-加法族を

\calM(E):=\{E\cap A\mid A\in\calM\}

と書く．特にLebesgue可測集合 E \in \calL_d 上に制限されたLebesgue \sigma-加法族を

\calL_d(E):=\{E\cap A \mid A\in \calL_d\}

と書く．

Definition7.3.2

Statement uses 2

Statement dependency previews

Preview

Definition 7.2.2

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Tagsleanok

可測関数. 可測空間 (X,\calM) 上の拡大実数値関数 f:X \to \eRR が\calM-可測関数であるとは，

f:(X,\calM)\to (\eRR,\calB(\eRR))

がDefinition 7.2.2の意味で可測写像であることをいう．特にX がLebesgue可測集合で \calM=\calL_d(X) のとき，f をLebesgue可測関数という．また，\calMがBorel \sigma-加法族のとき，f をBorel可測関数という．

Lean code for Definition7.3.2●3 definitions

abbrevdefined in NoteKsk/Defs.lean

complete

abbrev NoteKsk.MeasurableERealFunction.{u_1} (α : Type u_1)
  [MeasurableSpace α] : Type u_1

abbrev NoteKsk.MeasurableERealFunction.{u_1}
  (α : Type u_1) [MeasurableSpace α] :
  Type u_1

Definition body

abbrev MeasurableERealFunction (α : Type*) [MeasurableSpace α] : Type _ :=
  { f : α → EReal // Measurable f }

Extended-real-valued measurable functions on a measurable space.

abbrevdefined in NoteKsk/Defs.lean

complete

abbrev NoteKsk.MeasurableRealFunction.{u_1} (α : Type u_1)
  [MeasurableSpace α] : Type u_1

abbrev NoteKsk.MeasurableRealFunction.{u_1}
  (α : Type u_1) [MeasurableSpace α] :
  Type u_1

Definition body

abbrev MeasurableRealFunction (α : Type*) [MeasurableSpace α] : Type _ :=
  { f : α → ℝ // Measurable f }

Real-valued measurable functions on a measurable space.

abbrevdefined in NoteKsk/Defs.lean

complete

abbrev NoteKsk.NonnegativeMeasurableERealFunction.{u_1} (α : Type u_1)
  [MeasurableSpace α] : Type u_1

abbrev NoteKsk.NonnegativeMeasurableERealFunction.{u_1}
  (α : Type u_1) [MeasurableSpace α] :
  Type u_1

Definition body

abbrev NonnegativeMeasurableERealFunction (α : Type*) [MeasurableSpace α] : Type _ :=
  { f : α → EReal // Measurable f ∧ 0 ≤ f }

Nonnegative extended-real-valued measurable functions.

Definition7.3.3

uses 1

Used by 3

Reverse dependency previews

Preview

Proposition 7.5.1

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

Tagsleanok

可測関数空間の記号. 可測空間 (X,\calM) 上の拡大実数値可測関数全体を M(X;\eRR) と書く．文脈から値域が明らかなときは M(X):=M(X;\eRR) と略記する．また，実数値可測関数全体を M(X;\RR)，非負可測関数全体を M^+(X):=\{f\in M(X;\eRR)\mid f\ge 0\} と書く．

\sigma-加法族を明示したいときは M(X,\calM;\eRR) のように書く．可測集合 E\in\calM について M(E;\eRR) と書く場合は，相対可測空間 (E,\calM(E)) 上の可測関数全体を意味する．

Lean code for Definition7.3.3●3 definitions

abbrevdefined in NoteKsk/Defs.lean

complete

abbrev NoteKsk.MeasurableERealFunction.{u_1} (α : Type u_1)
  [MeasurableSpace α] : Type u_1

abbrev NoteKsk.MeasurableERealFunction.{u_1}
  (α : Type u_1) [MeasurableSpace α] :
  Type u_1

Definition body

abbrev MeasurableERealFunction (α : Type*) [MeasurableSpace α] : Type _ :=
  { f : α → EReal // Measurable f }

Extended-real-valued measurable functions on a measurable space.

abbrevdefined in NoteKsk/Defs.lean

complete

abbrev NoteKsk.MeasurableRealFunction.{u_1} (α : Type u_1)
  [MeasurableSpace α] : Type u_1

abbrev NoteKsk.MeasurableRealFunction.{u_1}
  (α : Type u_1) [MeasurableSpace α] :
  Type u_1

Definition body

abbrev MeasurableRealFunction (α : Type*) [MeasurableSpace α] : Type _ :=
  { f : α → ℝ // Measurable f }

Real-valued measurable functions on a measurable space.

abbrevdefined in NoteKsk/Defs.lean

complete

abbrev NoteKsk.NonnegativeMeasurableERealFunction.{u_1} (α : Type u_1)
  [MeasurableSpace α] : Type u_1

abbrev NoteKsk.NonnegativeMeasurableERealFunction.{u_1}
  (α : Type u_1) [MeasurableSpace α] :
  Type u_1

Definition body

abbrev NonnegativeMeasurableERealFunction (α : Type*) [MeasurableSpace α] : Type _ :=
  { f : α → EReal // Measurable f ∧ 0 ≤ f }

Nonnegative extended-real-valued measurable functions.

Theorem7.3.4

Statement uses 2

Statement dependency previews

Preview

Lemma 7.2.5

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

Used by 4

Reverse dependency previews

Preview

Proposition 7.4.2

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

Tagsleanok

可測関数の判定法. (X,\calM) を可測空間とし，f:X\to\eRR とする．次は同値である．

f は \calM-可測である
任意の a\in\RR に対して

\{x\in X \mid f(x)>a\}

は \calM に属する
任意の a\in\RR に対して

\{x\in X \mid f(x)\ge a\}

は \calM に属する
任意の a\in\RR に対して

\{x\in X \mid f(x)<a\}

は \calM に属する
任意の a\in\RR に対して

\{x\in X \mid f(x)\le a\}

は \calM に属する

Lean code for Theorem7.3.4●2 theorems

theoremdefined in NoteKsk/«07mble-funcs».lean

complete

theorem NoteKsk.Chapter07.measurable_ereal_criterion_all_thresholds.{u_1}
  {α : Type u_1} [MeasurableSpace α] (f : α → EReal) :
  Measurable f ↔
    (∀ (a : EReal), MeasurableSet {x | f x > a}) ∧
      (∀ (a : EReal), MeasurableSet {x | f x ≥ a}) ∧
        (∀ (a : EReal), MeasurableSet {x | f x < a}) ∧
          ∀ (a : EReal), MeasurableSet {x | f x ≤ a}

theorem NoteKsk.Chapter07.measurable_ereal_criterion_all_thresholds.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (f : α → EReal) :
  Measurable f ↔
    (∀ (a : EReal),
        MeasurableSet {x | f x > a}) ∧
      (∀ (a : EReal),
          MeasurableSet {x | f x ≥ a}) ∧
        (∀ (a : EReal),
            MeasurableSet {x | f x < a}) ∧
          ∀ (a : EReal),
            MeasurableSet {x | f x ≤ a}

theoremdefined in NoteKsk/«07mble-funcs».lean

complete

theorem NoteKsk.Chapter07.measurable_ereal_real_level_criterion.{u_1}
  {α : Type u_1} [MeasurableSpace α] (f : α → EReal) :
  Measurable f ↔
    (∀ (a : ℝ), MeasurableSet {x | f x > ↑a}) ∧
      (∀ (a : ℝ), MeasurableSet {x | f x ≥ ↑a}) ∧
        (∀ (a : ℝ), MeasurableSet {x | f x < ↑a}) ∧
          ∀ (a : ℝ), MeasurableSet {x | f x ≤ ↑a}

theorem NoteKsk.Chapter07.measurable_ereal_real_level_criterion.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (f : α → EReal) :
  Measurable f ↔
    (∀ (a : ℝ),
        MeasurableSet {x | f x > ↑a}) ∧
      (∀ (a : ℝ),
          MeasurableSet {x | f x ≥ ↑a}) ∧
        (∀ (a : ℝ),
            MeasurableSet
              {x | f x < ↑a}) ∧
          ∀ (a : ℝ),
            MeasurableSet {x | f x ≤ ↑a}

Lecture-note criterion `thm:lebesgue-measurable-function-criterion`.

The blueprint states the criterion with thresholds `a : ℝ`.  The theorem above
is the mathlib-native all-`EReal` version; this statement keeps the exact
lecture form as a bridge for later chapters.

Remark (拡大実数の閾値). 上の判定法では閾値を a\in\RR としたが， a\in\eRR としても同値な判定法が得られる．有限の a については上の定理で扱っている．また a=\infty や a=-\infty の場合も，例えば \{f<\infty\}=\bigcup_{n=1}^{\infty}\{f<n\}， \{f>-\infty\}=\bigcup_{n=1}^{\infty}\{f>-n\} のように，実数閾値のレベル集合から可算和・可算共通部分で表せる．以後は必要に応じて，実数閾値版と拡大実数閾値版を区別せずに使う．

Remark (レベル集合の略記). 以後，f:X\to\eRR と B\subset\eRR に対して

\{f\in B\}:=\{x\in X\mid f(x)\in B\} = f^{-1}(B)

と書く．また a\in\RR に対して

\begin{aligned} \{f>a\} &:=\{x\in X\mid f(x)>a\} = f^{-1}( (a,\infty] ),\\ \{f\ge a\}&:=\{x\in X\mid f(x)\ge a\} = f^{-1}( [a,\infty] )\\ \end{aligned}

などと書く．さらに f,g:X\to\eRR に対して

\{f>g\}:=\{x\in X\mid f(x)>g(x)\}

などと書く．定義域 X は文脈から判断する．

Proof for Theorem 7.3.4

uses 0

(1) \Rightarrow (2)quad (a,\infty]\in \calB(\eRR) だから，可測性の定義より f^{-1}((a,\infty])=\{x\in X \mid f(x)>a\} は可測である．

(2) \Rightarrow (3)quad 任意の a\in\RR に対して

\{f\ge a\} = \bigcap_{n=1}^{\infty}\left\{f>a-\frac1n\right\}

である．右辺は可測集合の可算共通部分だから可測である．

(3) \Rightarrow (4)quad

\{f<a\}=X\setminus\{f\ge a\}

だから可測である．

(4) \Rightarrow (5)quad

\{f\le a\} = \bigcap_{n=1}^{\infty}\left\{f<a+\frac1n\right\}

だから可測である．

(5) \Rightarrow (1)quad

\mathcal G:=\{[-\infty,a]\mid a\in\RR\}

とおく．仮定より f^{-1}(\mathcal G)\subset\calM である． \calM は \sigma-加法族だから

\sigma(f^{-1}(\mathcal G))\subset\calM

である．一方，lem:commute-induce-generate-sigma-algebra,lem:borel-eRRより

f^{-1}(\calB(\eRR)) =f^{-1}(\sigma(\mathcal G)) =\sigma(f^{-1}(\mathcal G))

である．したがって任意の B\in\calB(\eRR) に対して f^{-1}(B)\in\calM であり，f は \calM-可測である．