equal
deleted
inserted
replaced
178 proof (rule integral_FTC_atLeastAtMost) |
178 proof (rule integral_FTC_atLeastAtMost) |
179 fix x assume "0 \<le> x" "x \<le> b" |
179 fix x assume "0 \<le> x" "x \<le> b" |
180 show "DERIV (\<lambda>x. x * exp (-x)) x :> exp (-x) - x * exp (-x)" |
180 show "DERIV (\<lambda>x. x * exp (-x)) x :> exp (-x) - x * exp (-x)" |
181 by (auto intro!: DERIV_intros) |
181 by (auto intro!: DERIV_intros) |
182 show "isCont (\<lambda>x. exp (- x) - x * exp (- x)) x " |
182 show "isCont (\<lambda>x. exp (- x) - x * exp (- x)) x " |
183 by (intro isCont_intros isCont_exp') |
183 by (intro continuous_intros) |
184 qed fact |
184 qed fact |
185 also have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) = - exp (- b) - - exp (- 0)" |
185 also have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) = - exp (- b) - - exp (- 0)" |
186 by (rule integral_FTC_atLeastAtMost) (auto intro!: DERIV_intros) |
186 by (rule integral_FTC_atLeastAtMost) (auto intro!: DERIV_intros) |
187 finally show "1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)" |
187 finally show "1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)" |
188 by (auto simp: field_simps exp_minus inverse_eq_divide) |
188 by (auto simp: field_simps exp_minus inverse_eq_divide) |