9.3. 順序と大きさ🔗

Proposition9.3.1

Statement uses 2

Statement dependency previews

Preview

Proposition 8.2.4

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Proposition 9.3.2

Loading preview

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

✓L∃∀N

Tagsleanok

単調性. f,g\in\calL^1(X) とする．もし f\le g a.e. on X ならば \int_X f\,d\mu\le \int_X g\,d\mu が成り立つ．

Lean code for Proposition9.3.1●2 theorems

theoremdefined in NoteKsk/«09lintegral-prop».lean

complete

theorem NoteKsk.Chapter09.integral_mono_ae_real.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  (hg : MeasureTheory.Integrable g μ) (hfg : f ≤ᵐ[μ] g) :
  ∫ (x : α), f x ∂μ ≤ ∫ (x : α), g x ∂μ

theorem NoteKsk.Chapter09.integral_mono_ae_real.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f g : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  (hg : MeasureTheory.Integrable g μ)
  (hfg : f ≤ᵐ[μ] g) :
  ∫ (x : α), f x ∂μ ≤ ∫ (x : α), g x ∂μ

theoremdefined in NoteKsk/«09lintegral-prop».lean

complete

theorem NoteKsk.Chapter09.integral_mono_real.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  (hg : MeasureTheory.Integrable g μ) (hfg : f ≤ g) :
  ∫ (x : α), f x ∂μ ≤ ∫ (x : α), g x ∂μ

theorem NoteKsk.Chapter09.integral_mono_real.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f g : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  (hg : MeasureTheory.Integrable g μ)
  (hfg : f ≤ g) :
  ∫ (x : α), f x ∂μ ≤ ∫ (x : α), g x ∂μ

Proof for Proposition 9.3.1

uses 0

零集合上で値を変えても積分値は変わらない（Proposition 9.2.3）ので，f\le g が各点で成り立つとしてよい．このとき g^+ + f^- \ge f^+ + g^- である．実際，これは g^+-g^- \ge f^+-f^- と同値である． Proposition 8.2.4を非負関数に適用すると

\int_X g^+\,d\mu+\int_X f^-\,d\mu \ge \int_X f^+\,d\mu+\int_X g^-\,d\mu

である．両辺を移項して \int_X f\,d\mu\le \int_X g\,d\mu を得る．

Proposition9.3.2

uses 1used by 0✓L∃∀N

Tagsleanok

定数による評価. \mu(X)<\infty とし，a,b \in \RR が a\le f(x)\le b a.e. on X を満たすとする．このとき a\,\mu(X)\le \int_X f\,d\mu\le b\,\mu(X) が成り立つ．

Lean code for Proposition9.3.2●1 theorem

theoremdefined in NoteKsk/«09lintegral-prop».lean

complete

theorem NoteKsk.Chapter09.integral_bounds_of_ae_const_le.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ] {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ) {a b : ℝ}
  (ha : (fun x ↦ a) ≤ᵐ[μ] f) (hb : f ≤ᵐ[μ] fun x ↦ b) :
  a * μ.real Set.univ ≤ ∫ (x : α), f x ∂μ ∧
    ∫ (x : α), f x ∂μ ≤ b * μ.real Set.univ

theorem NoteKsk.Chapter09.integral_bounds_of_ae_const_le.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ]
  {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  {a b : ℝ} (ha : (fun x ↦ a) ≤ᵐ[μ] f)
  (hb : f ≤ᵐ[μ] fun x ↦ b) :
  a * μ.real Set.univ ≤
      ∫ (x : α), f x ∂μ ∧
    ∫ (x : α), f x ∂μ ≤
      b * μ.real Set.univ

Proof for Proposition 9.3.2

uses 0

a.e. で a1_X\le f\le b1_X だから，Proposition 9.3.1より \int_X a1_X\,d\mu\le \int_X f\,d\mu\le \int_X b1_X\,d\mu である．定数関数の積分 \int_X c1_X\,d\mu=c\,\mu(X) を用いれば結論を得る．

Proposition9.3.3

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 9.5.1

Loading preview

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

✓L∃∀N

Tagsleanok

絶対値による評価. f\in\calL^1(X) ならば \left|\int_X f\,d\mu\right|\le \int_X |f|\,d\mu が成り立つ．

Lean code for Proposition9.3.3●2 theorems

theoremdefined in NoteKsk/«09lintegral-prop».lean

complete

theorem NoteKsk.Chapter09.abs_integral_le_integral_abs.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : α → ℝ) :
  |∫ (x : α), f x ∂μ| ≤ ∫ (x : α), |f x| ∂μ

theorem NoteKsk.Chapter09.abs_integral_le_integral_abs.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  (f : α → ℝ) :
  |∫ (x : α), f x ∂μ| ≤
    ∫ (x : α), |f x| ∂μ

theoremdefined in NoteKsk/«09lintegral-prop».lean

complete

theorem NoteKsk.Chapter09.norm_integral_le_integral_norm.{u_1, u_2}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : α → E) :
  ‖∫ (x : α), f x ∂μ‖ ≤ ∫ (x : α), ‖f x‖ ∂μ

theorem NoteKsk.Chapter09.norm_integral_le_integral_norm.{u_1,
    u_2}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {E : Type u_2} [NormedAddCommGroup E]
  [NormedSpace ℝ E] (f : α → E) :
  ‖∫ (x : α), f x ∂μ‖ ≤
    ∫ (x : α), ‖f x‖ ∂μ

Proof for Proposition 9.3.3

uses 0

a.e. で -|f|\le f\le |f| だから，Proposition 9.3.1より -\int_X |f|\,d\mu\le \int_X f\,d\mu\le \int_X |f|\,d\mu である．したがって絶対値をとればよい．

Remark (ベクトル値の場合). 有限次元ベクトル値関数 F:X\to\RR^n についても，絶対値をノルムに置き換えた評価

\left\|\int_X F\,d\mu\right\| \le \int_X \|F\|\,d\mu

が成り立つ．この講義のこの段階では，必要なら各成分ごとに実数値関数の積分として読めば十分である．後でより一般のベクトル値積分を扱うときも，この評価が基本になる．

Proposition9.3.4

Statement uses 2

Statement dependency previews

Preview

Proposition 8.3.3

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 9.5.1

Loading preview

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

✓L∃∀N

Tagsleanok

積分が 0 であることの判定. f\in\calL^1(X) とする．このとき次は同値である．

\int_X |f|\,d\mu=0
f=0 a.e. on X

Lean code for Proposition9.3.4●1 theorem

theoremdefined in NoteKsk/«09lintegral-prop».lean

complete

theorem NoteKsk.Chapter09.integral_abs_eq_zero_iff_ae_eq_zero.{u_1}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) :
  ∫ (x : α), |f x| ∂μ = 0 ↔ f =ᵐ[μ] 0

theorem NoteKsk.Chapter09.integral_abs_eq_zero_iff_ae_eq_zero.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ) :
  ∫ (x : α), |f x| ∂μ = 0 ↔ f =ᵐ[μ] 0

Proof for Proposition 9.3.4

uses 0

(2) \Rightarrow (1)quad |f|=0 a.e. だから，Proposition 9.2.3より \int_X |f|\,d\mu=0 である．

(1) \Rightarrow (2)quad |f| は非負可測関数であり， Proposition 8.3.3より |f|=0 a.e. on X である．これは f=0 a.e. と同値である．

Proposition9.3.5

uses 1used by 1✓L∃∀N

Tagsleanok

非負関数のChebyshev不等式. f\in M^+(X) とし，\alpha>0 とする．このとき

\mu(\{x\in X\mid f(x)\ge \alpha\}) \le \alpha^{-1}\int_X f\,d\mu

が成り立つ．

Lean code for Proposition9.3.5●1 theorem

theoremdefined in NoteKsk/«09lintegral-prop».lean

complete

theorem NoteKsk.Chapter09.chebyshev_lintegral.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal}
  (hf : AEMeasurable f μ) {ε : ENNReal} (hε0 : ε ≠ 0) (hεtop : ε ≠ ⊤) :
  μ {x | ε ≤ f x} ≤ (∫⁻ (x : α), f x ∂μ) / ε

theorem NoteKsk.Chapter09.chebyshev_lintegral.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ENNReal}
  (hf : AEMeasurable f μ) {ε : ENNReal}
  (hε0 : ε ≠ 0) (hεtop : ε ≠ ⊤) :
  μ {x | ε ≤ f x} ≤
    (∫⁻ (x : α), f x ∂μ) / ε

Mathlib's Chebyshev/Markov inequality is naturally stated with `ENNReal`
measures and lower Lebesgue integrals.

Proof for Proposition 9.3.5

uses 0

A:=\{x\in X\mid f(x)\ge \alpha\} とおく．すると \alpha 1_A\le f だから，単調性より \alpha\mu(A)=\int_X \alpha1_A\,d\mu\le \int_X f\,d\mu である．両辺を \alpha で割ればよい．

Corollary9.3.6

uses 1

Used by 2

Reverse dependency previews

Preview

Corollary 9.3.7

Loading preview

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

✓L∃∀N

Tagsleanok

Chebyshev不等式. f\in\calL^1(X) とし，\alpha>0 とする．このとき \mu(\{x \in X \mid |f(x)|\ge \alpha\})\le \alpha^{-1}\int_X |f|\,d\mu が成り立つ．

Lean code for Corollary9.3.6●1 theorem

theoremdefined in NoteKsk/«09lintegral-prop».lean

complete

theorem NoteKsk.Chapter09.chebyshev_integrable_abs.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ) {a : ℝ} (ha : 0 < a) :
  μ {x | a ≤ |f x|} ≤
    (∫⁻ (x : α), ENNReal.ofReal |f x| ∂μ) / ENNReal.ofReal a

theorem NoteKsk.Chapter09.chebyshev_integrable_abs.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  {a : ℝ} (ha : 0 < a) :
  μ {x | a ≤ |f x|} ≤
    (∫⁻ (x : α),
        ENNReal.ofReal |f x| ∂μ) /
      ENNReal.ofReal a

The lecture statement
`μ {x | a ≤ |f x|} ≤ a⁻¹ ∫ |f| dμ` is formalized in `ENNReal` form.
The right-hand side uses the lower Lebesgue integral of `ENNReal.ofReal |f|`.

Proof for Corollary 9.3.6

uses 0

Proposition 9.3.5を |f| に適用すればよい．

Remark (Chebyshev不等式の使い途). Chebyshev不等式は，「積分で測った大きさ」から「大きい値をとる集合の測度」を評価する道具である．ここでは \|f\|_1:=\int_X |f|\,d\mu と書くことにすると，

\mu(\{|f|\ge \alpha\})\le \frac{\|f\|_1}{\alpha}

である．したがって \|f\|_1 が小さい関数は，大きな値をとる集合も小さい．また f\in\calL^1(X) なら \mu(\{|f|\ge R\})\le \|f\|_1/R\to0 (R\to\infty) であるから，可積分関数の大きな値は測度の意味でまれにしか現れない．

確率測度の場合，これは「期待値が小さければ，大きな偏差が起こる確率も小さい」という Markov 不等式そのものである．確率論で確率変数の尾確率を評価するときに最初に使う基本的な不等式である．

Corollary9.3.7

uses 1used by 0✓L∃∀N

L^1 収束は測度収束を導く. f_n-f\in\calL^1(X) (n\in\NN) とし，

\int_X |f_n-f|\,d\mu\to0

とする．このとき任意の \eps>0 に対して

\mu(\{x\in X\mid |f_n(x)-f(x)|\ge \eps\})\to0

が成り立つ．

Lean code for Corollary9.3.7●1 theorem

theoremdefined in NoteKsk/«09lintegral-prop».lean

complete

theorem NoteKsk.Chapter09.chebyshev_integrable_abs.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ) {a : ℝ} (ha : 0 < a) :
  μ {x | a ≤ |f x|} ≤
    (∫⁻ (x : α), ENNReal.ofReal |f x| ∂μ) / ENNReal.ofReal a

theorem NoteKsk.Chapter09.chebyshev_integrable_abs.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {f : α → ℝ}
  (hf : MeasureTheory.Integrable f μ)
  {a : ℝ} (ha : 0 < a) :
  μ {x | a ≤ |f x|} ≤
    (∫⁻ (x : α),
        ENNReal.ofReal |f x| ∂μ) /
      ENNReal.ofReal a

The lecture statement
`μ {x | a ≤ |f x|} ≤ a⁻¹ ∫ |f| dμ` is formalized in `ENNReal` form.
The right-hand side uses the lower Lebesgue integral of `ENNReal.ofReal |f|`.

Proof for Corollary 9.3.7

uses 0

Chebyshev不等式を f_n-f に適用すると，

\mu(\{|f_n-f|\ge \eps\}) \le \eps^{-1}\int_X |f_n-f|\,d\mu

である．右辺は 0 に収束するので結論を得る．