diff --git a/MIL/C10_Integration_and_Measure_Theory/S01_Elementary_Integration.lean b/MIL/C10_Integration_and_Measure_Theory/S01_Elementary_Integration.lean index cb7f5171..3041528e 100644 --- a/MIL/C10_Integration_and_Measure_Theory/S01_Elementary_Integration.lean +++ b/MIL/C10_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: +微積分の基本定理は積分と微分に関するものです.以下では,この定理の2つの部分を簡単に説明します.最初の部分は,積分が微分の逆を提供するということを,2番目では微分の積分を計算する方法を与えるものです.(この2つの部分は非常に密接に関連していますが,ここでは示していない最適版では等価になりません.) 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