C10/S03翻訳 (#53)

Author: s-taiga

GLOSSARY.md

@@ -21,6 +21,7 @@
 | cauchy sequence | コーシー列 |
 | closed sets | 閉集合 |
 | closure | 閉包 |
+| change-of-variables | 変数変換 |
 | chapter | 章 |
 | cluster point | 集積点 |
 | codomain | 終域 |
@@ -43,6 +44,7 @@
 | distributive lattice | 分配束 |
 | divisibility relation | 整除関係 |
 | domain | 始域 |
+| dominated convergence theorem | 優収束定理 |
 | entourage | 近縁 |
 | eta-reduction | η簡約 |
 | Euclidean algorithm | ユークリッドの互助法 |
@@ -80,6 +82,7 @@
 | least upper bound | 最小上界 |
 | library | Mathlib（Mathlibを指していることが明白である場合） |
 | logical connective | 論理結合子 |
+| mass | 体積量 |
 | measure theory | 測度論 |
 | meet | 交わり |
 | metric space | 距離空間 |

MIL/C11_Integration_and_Measure_Theory/S03_Integration.lean

@@ -15,12 +15,19 @@ noncomputable section
 variable {α : Type*} [MeasurableSpace α]
 variable {μ : Measure α}
 
+/- OMIT:
+Integration
+-----------
+
+OMIT. -/
 /- TEXT:
 .. _integration:
 
-Integration
+積分
 -----------
 
+TEXT. -/
+/- OMIT:
 Now that we have measurable spaces and measures we can consider integrals.
 As explained above, Mathlib uses a very general notion of
 integration that allows any Banach space as the target.
@@ -29,6 +36,9 @@ carry around assumptions, so we define integration in such a way
 that an integral is equal to zero if the function in question is
 not integrable.
 Most lemmas having to do with integrals have integrability assumptions.
+OMIT. -/
+/- TEXT:
+可測空間と測度を得たので，積分を考えることができます．上記で説明したように，Mathlibは非常に一般的な積分の概念を使っており，どのようなバナッハ空間でも積分の対象とすることができます．いつものように，仮定をいちいち持ち出す記法は避けたいので，対象の関数が可積分でなければ0に等しくなるように積分を定義します．積分に関連するほとんどの補題は可積分の仮定を持っています．
 EXAMPLES: -/
 -- QUOTE:
 section
@@ -39,24 +49,30 @@ example {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) :
   integral_add hf hg
 -- QUOTE.
 
-/- TEXT:
+/- OMIT:
 As an example of the complex interactions between our various conventions, let us see how to integrate constant functions.
 Recall that a measure ``μ`` takes values in ``ℝ≥0∞``, the type of extended non-negative reals.
 There is a function ``ENNReal.toReal : ℝ≥0∞ → ℝ`` which sends ``⊤``,
 the point at infinity, to zero.
 For any ``s : Set α``, if ``μ s = ⊤``, then nonzero constant functions are not integrable on ``s``.
 In that case, their integrals are equal to zero by definition, as is ``(μ s).toReal``.
 So in all cases we have the following lemma.
+OMIT. -/
+/- TEXT:
+これまで見てきた諸々の事実を複雑に組み合わせた例として，定数関数の積分方法を見てみましょう．測度 ``μ`` は非負実数を拡張した型である ``ℝ≥0∞`` の値をとることを思い出してください．関数 ``ENNReal.toReal : ℝ≥0∞ → ℝ`` は無限遠点 ``⊤`` を0に送ります．任意の ``s : Set α`` に対して，もし ``μ s = ⊤`` ならば，非零定数関数は ``s`` 上で積分できません．その場合，積分は定義から ``(μ s).toReal`` となり，0に等しくなります．したがって，すべての場合において次の補題が成り立ちます．
 EXAMPLES: -/
 -- QUOTE:
 example {s : Set α} (c : E) : ∫ x in s, c ∂μ = (μ s).toReal • c :=
   setIntegral_const c
 -- QUOTE.
 
-/- TEXT:
+/- OMIT:
 We now quickly explain how to access the most important theorems in integration theory, starting
 with the dominated convergence theorem. There are several versions in Mathlib,
 and here we only show the most basic one.
+OMIT. -/
+/- TEXT:
+ここでは積分理論の最も重要な定理を導く方法を，優収束定理から手短に説明します．Mathlibにはいくつかバリエーションが存在しますが，ここでは最も基本的なものだけを紹介します．
 EXAMPLES: -/
 -- QUOTE:
 open Filter
@@ -68,8 +84,11 @@ example {F : ℕ → α → E} {f : α → E} (bound : α → ℝ) (hmeas : ∀
   tendsto_integral_of_dominated_convergence bound hmeas hint hbound hlim
 -- QUOTE.
 
-/- TEXT:
+/- OMIT:
 Then we have Fubini's theorem for integrals on product type.
+OMIT. -/
+/- TEXT:
+これによって直積型の積分に対するフビニの定理が得られます．
 EXAMPLES: -/
 -- QUOTE:
 example {α : Type*} [MeasurableSpace α] {μ : Measure α} [SigmaFinite μ] {β : Type*}
@@ -80,9 +99,12 @@ example {α : Type*} [MeasurableSpace α] {μ : Measure α} [SigmaFinite μ] {β
 
 end
 
-/- TEXT:
+/- OMIT:
 There is a very general version of convolution that applies to any
 continuous bilinear form.
+OMIT. -/
+/- TEXT:
+畳み込みには任意の連続双線形形式に適用できる非常に一般的なバージョンがあります．
 EXAMPLES: -/
 section
 
@@ -102,12 +124,15 @@ example (f : G → E) (g : G → E') (L : E →L[𝕜] E' →L[𝕜] F) (μ : Me
 
 end
 
-/- TEXT:
+/- OMIT:
 Finally, Mathlib has a very general version of the change-of-variables formula.
 In the statement below, ``BorelSpace E`` means the
 :math:`\sigma`-algebra on ``E`` is generated by the open sets of ``E``,
 and ``IsAddHaarMeasure μ`` means that the measure ``μ`` is left-invariant,
 gives finite mass to compact sets, and give positive mass to open sets.
+OMIT. -/
+/- TEXT:
+最後に，Mathlibには非常に一般的な変数変換の公式があります．以下の文において， ``BorelSpace E`` は ``E`` 上の :math:`\sigma`-代数が ``E`` 開集合によって生成されることを意味し， ``IsAddHaarMeasure μ`` は ``μ`` が左不変であり，コンパクト集合に有限の体積量を与え，開集合に正の体積量を与えることを意味します．
 EXAMPLES: -/
 -- QUOTE:
 example {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]