C10/S01翻訳 (#49)

Author: s-taiga

MIL/C11_Integration_and_Measure_Theory/S01_Elementary_Integration.lean

@@ -11,16 +11,26 @@ open Topology Filter
 
 noncomputable section
 
+/- OMIT:
+Elementary Integration
+----------------------
+
+OMIT. -/
 /- TEXT:
 .. index:: integration
 
 .. _elementary_integration:
 
-Elementary Integration
+初等的な積分
 ----------------------
 
+TEXT. -/
+/- OMIT:
 We first focus on integration of functions on finite intervals in ``ℝ``. We can integrate
 elementary functions.
+OMIT. -/
+/- TEXT:
+ここではまず， ``ℝ`` の有限区間上の関数の積分に焦点を当てます．Mathlibでは初等関数を積分できます．
 EXAMPLES: -/
 -- QUOTE:
 open MeasureTheory intervalIntegral
@@ -35,13 +45,16 @@ example {a b : ℝ} (h : (0 : ℝ) ∉ [[a, b]]) : (∫ x in a..b, 1 / x) = Real
   integral_one_div h
 -- QUOTE.
 
-/- TEXT:
+/- OMIT:
 The fundamental theorem of calculus relates integration and differentiation.
 Below we give simplified statements of the two parts of this theorem. The first part
 says that integration provides an inverse to differentiation and the second one
 specifies how to compute integrals of derivatives.
 (These two parts are very closely related, but their optimal versions,
 which are not shown here, are not equivalent.)
+OMIT. -/
+/- TEXT:
+微積分の基本定理は積分と微分に関するものです．以下では，この定理の２つの部分を簡単に説明します．最初の部分は，積分が微分の逆を提供するということを，２番目では微分の積分を計算する方法を与えるものです．（この２つの部分は非常に密接に関連していますが，ここでは示していない最適版では等価になりません．）
 EXAMPLES: -/
 -- QUOTE:
 example (f : ℝ → ℝ) (hf : Continuous f) (a b : ℝ) : deriv (fun u ↦ ∫ x : ℝ in a..u, f x) b = f b :=
@@ -53,8 +66,11 @@ example {f : ℝ → ℝ} {a b : ℝ} {f' : ℝ → ℝ} (h : ∀ x ∈ [[a, b]]
   integral_eq_sub_of_hasDerivAt h h'
 -- QUOTE.
 
-/- TEXT:
+/- OMIT:
 Convolution is also defined in Mathlib and its basic properties are proved.
+OMIT. -/
+/- TEXT:
+畳み込みもまたMathlibで定義されており，その基本的な性質が証明されています．
 EXAMPLES: -/
 -- QUOTE:
 open Convolution