From 46f5ec4d23be81490570a06cafe6661b79cbf631 Mon Sep 17 00:00:00 2001 From: s-taiga Date: Wed, 15 May 2024 23:09:35 +0900 Subject: [PATCH 1/2] =?UTF-8?q?C10/S02=E7=BF=BB=E8=A8=B3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- GLOSSARY.md | 1 + .../S02_Measure_Theory.lean | 28 +++++++++++++++++-- 2 files changed, 26 insertions(+), 3 deletions(-) diff --git a/GLOSSARY.md b/GLOSSARY.md index 0c62e1bf..095dee44 100644 --- a/GLOSSARY.md +++ b/GLOSSARY.md @@ -3,6 +3,7 @@ | 英語 | 日本語 | | --- | --- | | absorption laws | 吸収則 | +| almost everywhere | ほとんどいたるところ | | analysis | 解析学 | | arguments | 引数 | | arithmetic | 算術 | diff --git a/MIL/C10_Integration_and_Measure_Theory/S02_Measure_Theory.lean b/MIL/C10_Integration_and_Measure_Theory/S02_Measure_Theory.lean index eaa97eed..6b83a957 100644 --- a/MIL/C10_Integration_and_Measure_Theory/S02_Measure_Theory.lean +++ b/MIL/C10_Integration_and_Measure_Theory/S02_Measure_Theory.lean @@ -9,19 +9,32 @@ open Set Filter noncomputable section +/- OMIT: +Measure Theory +-------------- + +OMIT. -/ /- TEXT: .. index:: measure theory .. _measure_theory: -Measure Theory +測度論 -------------- +TEXT. -/ +/- OMIT: The general context for integration in Mathlib is measure theory. Even the elementary integrals of the previous section are in fact Bochner integrals. Bochner integration is a generalization of Lebesgue integration where the target space can be any Banach space, not necessarily finite dimensional. +OMIT. -/ +/- TEXT: +Mathlibにおける積分の一般的な文脈は測度論です．前節の初等積分でさえも，実際にはボホナー積分です．ボホナー積分はルベーグ積分の一般化で，対象の空間はバナッハ空間であれば何でもよく，必ずしも有限次元である必要はありません． + +TEXT. -/ +/- OMIT: The first component in the development of measure theory is the notion of a :math:`\sigma`-algebra of sets, which are called the *measurable* sets. @@ -33,6 +46,9 @@ Note that these axioms are redundant; if you ``#print MeasurableSpace``, you will see the ones that Mathlib uses. As the examples below show, countability assumptions can be expressed using the ``Encodable`` type class. +OMIT. -/ +/- TEXT: +測度論の発展における最初の要素は *可測* 集合と呼ばれる集合の :math:`\sigma`-代数の概念です．型クラス ``MeasurableSpace`` はこのような構造を持つ型を備えるためのものです．まず集合 ``empty`` と ``univ`` は可測です．可測集合の補集合も可測であり，可測集合の可算和または可算交差も可測です．これらの公理が冗長であることに注意してください; ``#print MeasurableSpace`` とタイプすると，Mathlibが使っている公理が表示されます．以下の例で示すように，可算性の仮定は ``Encodable`` 型クラスを使って表現することができます． BOTH: -/ -- QUOTE: variable {α : Type*} [MeasurableSpace α] @@ -62,7 +78,7 @@ example {f : ι → Set α} (h : ∀ b, MeasurableSet (f b)) : MeasurableSet ( MeasurableSet.iInter h -- QUOTE. -/- TEXT: +/- OMIT: Once a type is measurable, we can measure it. On paper, a measure on a set (or type) equipped with a :math:`\sigma`-algebra is a function from the measurable sets to @@ -74,6 +90,9 @@ So we extend the measure to any set ``s`` as the infimum of measures of measurable sets containing ``s``. Of course, many lemmas still require measurability assumptions, but not all. +OMIT. -/ +/- TEXT: +ある型が可測であれば，その型を測ることができます．書籍などにおいて， :math:`\sigma`-代数を備えた集合（または型）に対する測度とは，可測集合から拡張非負実数への関数であり，可算非交和上で加法的です．Mathlibでは，ある集合への測度の適用を記述するたびに可測の仮定を持ち出したくはありません．そこで， ``s`` を含む可測な集合の測度を最小値として，任意の集合 ``s`` に測度を拡張しています．もちろん，多くの補題では依然として可測の仮定を必要としますが，すべてではありません． BOTH: -/ -- QUOTE: open MeasureTheory @@ -91,13 +110,16 @@ example {f : ℕ → Set α} (hmeas : ∀ i, MeasurableSet (f i)) (hdis : Pairwi μ.m_iUnion hmeas hdis -- QUOTE. -/- TEXT: +/- OMIT: Once a type has a measure associated with it, we say that a property ``P`` holds *almost everywhere* if the set of elements where the property fails has measure 0. The collection of properties that hold almost everywhere form a filter, but Mathlib introduces special notation for saying that a property holds almost everywhere. +OMIT. -/ +/- TEXT: +ある型に測度が紐づけられると，ある特性 ``P`` が *ほとんどいたるところ* で保持されるとは，その特性が失敗する要素の集合が測度0であることを指します．ほとんどいたるところで保持される特性の集合はフィルタを形成しますが，Mathlibはある特性がほとんどいたるところで保持されることを言うための特別な記法を導入しています． EXAMPLES: -/ -- QUOTE: example {P : α → Prop} : (∀ᵐ x ∂μ, P x) ↔ ∀ᶠ x in μ.ae, P x := From 872618b96f4ca7ed9007ab051bfa8fa3ffb2187a Mon Sep 17 00:00:00 2001 From: s-taiga Date: Mon, 23 Sep 2024 16:13:19 +0900 Subject: [PATCH 2/2] =?UTF-8?q?=E8=A1=A8=E7=8F=BE=E5=BE=AE=E4=BF=AE?= =?UTF-8?q?=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../S02_Measure_Theory.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/MIL/C10_Integration_and_Measure_Theory/S02_Measure_Theory.lean b/MIL/C10_Integration_and_Measure_Theory/S02_Measure_Theory.lean index 6b83a957..a47724d0 100644 --- a/MIL/C10_Integration_and_Measure_Theory/S02_Measure_Theory.lean +++ b/MIL/C10_Integration_and_Measure_Theory/S02_Measure_Theory.lean @@ -48,7 +48,7 @@ As the examples below show, countability assumptions can be expressed using the ``Encodable`` type class. OMIT. -/ /- TEXT: -測度論の発展における最初の要素は *可測* 集合と呼ばれる集合の :math:`\sigma`-代数の概念です．型クラス ``MeasurableSpace`` はこのような構造を持つ型を備えるためのものです．まず集合 ``empty`` と ``univ`` は可測です．可測集合の補集合も可測であり，可測集合の可算和または可算交差も可測です．これらの公理が冗長であることに注意してください; ``#print MeasurableSpace`` とタイプすると，Mathlibが使っている公理が表示されます．以下の例で示すように，可算性の仮定は ``Encodable`` 型クラスを使って表現することができます． +測度論の発展における最初の要素は **可測** （measurable）集合と呼ばれる集合の :math:`\sigma`-代数の概念です．型クラス ``MeasurableSpace`` はこのような構造を持つ型を備えるためのものです．まず集合 ``empty`` と ``univ`` は可測です．可測集合の補集合も可測であり，可測集合の可算和または可算交差も可測です．これらの公理が冗長であることに注意してください; ``#print MeasurableSpace`` とタイプすると，Mathlibが使っている公理が表示されます．以下の例で示すように，可算性の仮定は ``Encodable`` 型クラスを使って表現することができます． BOTH: -/ -- QUOTE: variable {α : Type*} [MeasurableSpace α] @@ -92,7 +92,7 @@ Of course, many lemmas still require measurability assumptions, but not all. OMIT. -/ /- TEXT: -ある型が可測であれば，その型を測ることができます．書籍などにおいて， :math:`\sigma`-代数を備えた集合（または型）に対する測度とは，可測集合から拡張非負実数への関数であり，可算非交和上で加法的です．Mathlibでは，ある集合への測度の適用を記述するたびに可測の仮定を持ち出したくはありません．そこで， ``s`` を含む可測な集合の測度を最小値として，任意の集合 ``s`` に測度を拡張しています．もちろん，多くの補題では依然として可測の仮定を必要としますが，すべてではありません． +ある型が可測であれば，その型を測ることができます．書籍などにおいては， :math:`\sigma`-代数を備えた集合（または型）に対する測度とは，可測集合から拡張非負実数への関数であり，可算非交和上で加法的とされています．Mathlibでは，ある集合への測度の適用を記述するたびに可測の仮定を持ち出したくはありません．そこで， ``s`` を含む可測な集合の測度を最小値として，任意の集合 ``s`` に測度を拡張しています．もちろん，多くの補題では依然として可測の仮定を必要としますが，すべてではありません． BOTH: -/ -- QUOTE: open MeasureTheory @@ -119,7 +119,7 @@ but Mathlib introduces special notation for saying that a property holds almost everywhere. OMIT. -/ /- TEXT: -ある型に測度が紐づけられると，ある特性 ``P`` が *ほとんどいたるところ* で保持されるとは，その特性が失敗する要素の集合が測度0であることを指します．ほとんどいたるところで保持される特性の集合はフィルタを形成しますが，Mathlibはある特性がほとんどいたるところで保持されることを言うための特別な記法を導入しています． +ある型に測度が紐づけられると，ある特性 ``P`` が **ほとんどいたるところ** （almost everywhere）で保持されるとは，その特性が失敗する要素の集合が測度0であることを指します．ほとんどいたるところで保持される特性の集合はフィルタを形成しますが，Mathlibはある特性がほとんどいたるところで保持されることを言うための特別な記法を導入しています． EXAMPLES: -/ -- QUOTE: example {P : α → Prop} : (∀ᵐ x ∂μ, P x) ↔ ∀ᶠ x in μ.ae, P x :=