7.6. 不等式・極限で作られる関数🔗

Proposition7.6.1

uses 1used by 0✓L∃∀N

Tagsleanok

比較からできる集合. (X,\calM) を可測空間とし， f,g\in M(X) とする．このとき次の集合はすべて \calM に属する．

\{x\in X \mid f(x)>g(x)\},\quad \{x\in X \mid f(x)\ge g(x)\},\quad \{x\in X \mid f(x)=g(x)\}

Lean code for Proposition7.6.1●3 theorems

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

complete

theorem NoteKsk.Chapter07.measurableSet_gt_of_measurable.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f g : α → EReal} (hf : Measurable f)
  (hg : Measurable g) : MeasurableSet {x | f x > g x}

theorem NoteKsk.Chapter07.measurableSet_gt_of_measurable.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f g : α → EReal} (hf : Measurable f)
  (hg : Measurable g) :
  MeasurableSet {x | f x > g x}

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

complete

theorem NoteKsk.Chapter07.measurableSet_ge_of_measurable.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f g : α → EReal} (hf : Measurable f)
  (hg : Measurable g) : MeasurableSet {x | f x ≥ g x}

theorem NoteKsk.Chapter07.measurableSet_ge_of_measurable.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f g : α → EReal} (hf : Measurable f)
  (hg : Measurable g) :
  MeasurableSet {x | f x ≥ g x}

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

complete

theorem NoteKsk.Chapter07.measurableSet_eq_of_measurable.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f g : α → EReal} (hf : Measurable f)
  (hg : Measurable g) : MeasurableSet {x | f x = g x}

theorem NoteKsk.Chapter07.measurableSet_eq_of_measurable.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f g : α → EReal} (hf : Measurable f)
  (hg : Measurable g) :
  MeasurableSet {x | f x = g x}

Proof for Proposition 7.6.1

uses 0

まず \{f>g\}=\bigcup_{q\in\QQ}(\{f>q\}\cap\{g<q\}) を示す．左辺に x が属するとする．すると f(x)>g(x) だから，有理数の稠密性より g(x)<q<f(x) を満たす q\in\QQ が存在する．したがって x は右辺に属する．逆向きは明らかである．右辺は可測集合の可算和だから可測である．

続いて

\{f\ge g\}=X\setminus\{g>f\}

だから可測である．

そして

\{f=g\}=\{f\ge g\}\cap\{g\ge f\}

だから可測である．

Definition7.6.2

uses 0used by 1✓L∃∀N

Tagsleanok

各点の上限・下限・上極限・下極限・極限関数. 関数列 f_n:X\to\eRR に対し， \sup_n f_n,\ \inf_n f_n,\ \limsup_{n\to\infty}f_n,\ \liminf_{n\to\infty}f_n を各点 x\in X で次のように定義する．

\begin{aligned} &\left(\sup_{n}f_n\right)(x) := \sup \{f_n(x) \mid n \in \NN \}, &&\left(\inf_{n}f_n\right)(x) := \inf \{f_n(x) \mid n \in \NN \},\\ &\left(\limsup_{n \to \infty} f_n\right)(x) := \inf_{n\in\NN}\sup\{f_k(x)\mid k\ge n\}, &&\left(\liminf_{n \to \infty} f_n\right)(x) := \sup_{n\in\NN}\inf\{f_k(x)\mid k\ge n\}. \end{aligned}

さらに，すべての x\in X で \lim_{n\to\infty}f_n(x) が \eRR の意味で存在するとき，極限関数 \lim_{n\to\infty}f_n:X\to\eRR を

\left(\lim_{n\to\infty}f_n\right)(x) :=\lim_{n\to\infty}f_n(x)

で定義する．このとき関数として

\lim_{n\to\infty}f_n =\limsup_{n\to\infty}f_n =\liminf_{n\to\infty}f_n

である．

Lean code for Definition7.6.2●4 definitions

defdefined in NoteKsk/Defs.lean

complete

def NoteKsk.pointwiseSup.{u_1} {α : Type u_1} (f : ℕ → α → EReal) :
  α → EReal

def NoteKsk.pointwiseSup.{u_1} {α : Type u_1}
  (f : ℕ → α → EReal) : α → EReal

Definition body

def pointwiseSup {α : Type*} (f : ℕ → α → EReal) : α → EReal :=
  fun x => ⨆ n, f n x

Pointwise supremum of a sequence of extended-real-valued functions.

defdefined in NoteKsk/Defs.lean

complete

def NoteKsk.pointwiseInf.{u_1} {α : Type u_1} (f : ℕ → α → EReal) :
  α → EReal

def NoteKsk.pointwiseInf.{u_1} {α : Type u_1}
  (f : ℕ → α → EReal) : α → EReal

Definition body

def pointwiseInf {α : Type*} (f : ℕ → α → EReal) : α → EReal :=
  fun x => ⨅ n, f n x

Pointwise infimum of a sequence of extended-real-valued functions.

defdefined in NoteKsk/Defs.lean

complete

def NoteKsk.pointwiseLimsup.{u_1} {α : Type u_1} (f : ℕ → α → EReal) :
  α → EReal

def NoteKsk.pointwiseLimsup.{u_1}
  {α : Type u_1} (f : ℕ → α → EReal) :
  α → EReal

Definition body

def pointwiseLimsup {α : Type*} (f : ℕ → α → EReal) : α → EReal :=
  fun x => Filter.limsup (fun n => f n x) Filter.atTop

Pointwise limsup of a sequence of extended-real-valued functions.

defdefined in NoteKsk/Defs.lean

complete

def NoteKsk.pointwiseLiminf.{u_1} {α : Type u_1} (f : ℕ → α → EReal) :
  α → EReal

def NoteKsk.pointwiseLiminf.{u_1}
  {α : Type u_1} (f : ℕ → α → EReal) :
  α → EReal

Definition body

def pointwiseLiminf {α : Type*} (f : ℕ → α → EReal) : α → EReal :=
  fun x => Filter.liminf (fun n => f n x) Filter.atTop

Pointwise liminf of a sequence of extended-real-valued functions.

Proposition7.6.3

uses 1used by 1✓L∃∀N

Tagsleanok

可算上限・可算下限の可測性. (X,\calM) を可測空間とし， f_n\in M(X) (n\in\NN) とする．このとき，

\sup_{n}f_n, \qquad \inf_{n}f_n

は \calM-可測である．

Lean code for Proposition7.6.3●2 theorems

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

complete

theorem NoteKsk.Chapter07.measurable_pointwiseSup.{u_1} {α : Type u_1}
  [MeasurableSpace α] (f : ℕ → α → EReal)
  (hf : ∀ (n : ℕ), Measurable (f n)) :
  Measurable (NoteKsk.pointwiseSup f)

theorem NoteKsk.Chapter07.measurable_pointwiseSup.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (f : ℕ → α → EReal)
  (hf : ∀ (n : ℕ), Measurable (f n)) :
  Measurable (NoteKsk.pointwiseSup f)

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

complete

theorem NoteKsk.Chapter07.measurable_pointwiseInf.{u_1} {α : Type u_1}
  [MeasurableSpace α] (f : ℕ → α → EReal)
  (hf : ∀ (n : ℕ), Measurable (f n)) :
  Measurable (NoteKsk.pointwiseInf f)

theorem NoteKsk.Chapter07.measurable_pointwiseInf.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (f : ℕ → α → EReal)
  (hf : ∀ (n : ℕ), Measurable (f n)) :
  Measurable (NoteKsk.pointwiseInf f)

Proof for Proposition 7.6.3

uses 0

任意の a\in\RR に対して

\left\{\sup_n f_n>a\right\} = \bigcup_{n=1}^{\infty}\{f_n>a\}

である．右辺は可測集合の可算和だから可測である．よって \sup_n f_n は可測である．

また任意の a\in\RR に対して

\left\{\inf_n f_n<a\right\} = \bigcup_{n=1}^{\infty}\{f_n<a\}

である．右辺は可測集合の可算和だから可測である．よって \inf_n f_n も可測である．

Proposition7.6.4

uses 1used by 1✓L∃∀N

Tagsleanok

上極限・下極限・極限関数の可測性. (X,\calM) を可測空間とし， f_n\in M(X) (n\in\NN) とする．このとき

\limsup_{n\to\infty}f_n,\qquad \liminf_{n\to\infty}f_n

は \calM-可測である．さらに，もし各点で極限が存在し，

f=\lim_{n\to\infty}f_n

とおくなら，f も \calM-可測である．

Lean code for Proposition7.6.4●4 theorems

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

complete

theorem NoteKsk.Chapter07.measurable_pointwiseLimsup.{u_1} {α : Type u_1}
  [MeasurableSpace α] (f : ℕ → α → EReal)
  (hf : ∀ (n : ℕ), Measurable (f n)) :
  Measurable (NoteKsk.pointwiseLimsup f)

theorem NoteKsk.Chapter07.measurable_pointwiseLimsup.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (f : ℕ → α → EReal)
  (hf : ∀ (n : ℕ), Measurable (f n)) :
  Measurable (NoteKsk.pointwiseLimsup f)

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

complete

theorem NoteKsk.Chapter07.measurable_pointwiseLiminf.{u_1} {α : Type u_1}
  [MeasurableSpace α] (f : ℕ → α → EReal)
  (hf : ∀ (n : ℕ), Measurable (f n)) :
  Measurable (NoteKsk.pointwiseLiminf f)

theorem NoteKsk.Chapter07.measurable_pointwiseLiminf.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (f : ℕ → α → EReal)
  (hf : ∀ (n : ℕ), Measurable (f n)) :
  Measurable (NoteKsk.pointwiseLiminf f)

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

complete

theorem NoteKsk.Chapter07.measurable_of_eq_pointwiseLimsup.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f : ℕ → α → EReal} {g : α → EReal}
  (hf : ∀ (n : ℕ), Measurable (f n))
  (hg : g = NoteKsk.pointwiseLimsup f) : Measurable g

theorem NoteKsk.Chapter07.measurable_of_eq_pointwiseLimsup.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f : ℕ → α → EReal} {g : α → EReal}
  (hf : ∀ (n : ℕ), Measurable (f n))
  (hg : g = NoteKsk.pointwiseLimsup f) :
  Measurable g

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

complete

theorem NoteKsk.Chapter07.measurable_of_pointwise_tendsto.{u_1} {α : Type u_1}
  [MeasurableSpace α] {f : ℕ → α → EReal} {g : α → EReal}
  (hf : ∀ (n : ℕ), Measurable (f n))
  (hlim :
    ∀ (x : α),
      Filter.Tendsto (fun n ↦ f n x) Filter.atTop (nhds (g x))) :
  Measurable g

theorem NoteKsk.Chapter07.measurable_of_pointwise_tendsto.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {f : ℕ → α → EReal} {g : α → EReal}
  (hf : ∀ (n : ℕ), Measurable (f n))
  (hlim :
    ∀ (x : α),
      Filter.Tendsto (fun n ↦ f n x)
        Filter.atTop (nhds (g x))) :
  Measurable g

Pointwise convergence version of `prop:measurable-limsup-liminf`.

The proof can be filled by identifying the pointwise limit with both limsup and
liminf.  It is kept as a named statement because later integration chapters
usually refer to this form directly.

Proof for Proposition 7.6.4

uses 0

定義により

\limsup_{n\to\infty}f_n = \inf_{n\in\NN}\sup_{k\ge n}f_k, \qquad \liminf_{n\to\infty}f_n = \sup_{n\in\NN}\inf_{k\ge n}f_k.

右辺は可測関数に対する可算上限・可算下限で作られているから可測である．

さらに各点で極限が存在するなら

f=\limsup_{n\to\infty}f_n=\liminf_{n\to\infty}f_n

だから f は可測である．