長めの例: 区間積分の具体計算

区間積分は，初等解析の例では norm_num や ring_nf と連携して計算できることがあります． まずは定数関数と恒等関数の積分を見ます．

section ConcreteIntervalIntegrals

example : ∫ _ : ℝ in (0)..(2), (3 : ℝ) = 6 := by
  norm_num

example : ∫ x : ℝ in (0)..(1), x = (1 / 2 : ℝ) := by
  norm_num

example : ∫ x : ℝ in (0)..(2), x = (2 : ℝ) := by
  norm_num

end ConcreteIntervalIntegrals

これらの例は，内部では区間積分に関する既存定理と実数計算を使っています． 複雑な被積分関数では norm_num だけで閉じないことも多く， その場合は微分積分学の基本定理や積分の線形性を明示的に使います．

演習問題

1. 定数関数の区間積分を計算してください．

   example : ∫ _ : ℝ in (1)..(4), (2 : ℝ) = 6 := by
     -- `norm_num` を試す．
     sorry
   

2. 区間の向きを反転したときの積分を調べてください．

   #check intervalIntegral.integral_symm
   

3. ∫ x in a..b, f x と ∫ x in b..a, f x の関係を使って，定数関数の例を逆向き区間で計算してください．

   example : ∫ _ : ℝ in (2)..(0), (3 : ℝ) = -6 := by
     -- `norm_num` を試す．
     sorry