長めの例: 区間積分の線形性¶
積分の線形性は，関数の可積分性を仮定して使います．
区間積分では IntervalIntegrable f volume a b がよく現れます．
section LinearityOfIntervalIntegral
example {f g : ℝ → ℝ} {a b : ℝ}
(hf : IntervalIntegrable f volume a b)
(hg : IntervalIntegrable g volume a b) :
∫ x : ℝ in a..b, f x + g x =
(∫ x : ℝ in a..b, f x) + ∫ x : ℝ in a..b, g x := by
exact intervalIntegral.integral_add hf hg
example (c : ℝ) (f : ℝ → ℝ) (a b : ℝ) :
∫ x : ℝ in a..b, c * f x = c * ∫ x : ℝ in a..b, f x := by
exact intervalIntegral.integral_const_mul c f
end LinearityOfIntervalIntegral
紙の数学では，積分の線形性はほとんど自明に使います． Lean では，被積分関数が適切に積分可能であることが theorem の仮定に現れます． 定数倍については theorem が仮定なしの形で使えることもありますが，これは積分が定義上全関数に拡張されているためです． 本格的な解析では，可積分性の仮定を明示して使うのが安全です．
演習問題¶
積分の和に関する線形性を intervalIntegral.integral_add で証明してください．