证明集合内的整合

Question

我正在尝试使用微积分基本定理来证明引理 lm1:

lemma lm1:
fixes f :: "real ⇒ real"
assumes "∀x∈{a..b}. (f has_vector_derivative f' x) (at x within {a .. b})"
"∀x∈{a..b}. a ≤ x"
"∀x∈{a..b}. x ≤ b"
shows "∀x∈{a..b}. (f' has_integral (f x - f a)) {a .. x}"

这只是下面引理lm2的扩展，证明了整集的积分。

lemma lm2:
fixes f :: "real ⇒ real"
assumes "∀x∈{a..b}. (f has_vector_derivative f' x) (at x within {a .. b})"
"a ≤ b"
shows "∀x∈{a..b}. (f' has_integral (f b - f a)) {a .. b}"
using assms
apply(simp add: fundamental_theorem_of_calculus)

相反，我想证明积分对集合中的任何值都是正确的，而不仅仅是下限和上限。我怎样才能显示这个？

Answer 1

首先，lm1 中的第二个和第三个假设是微不足道的：

lemma "∀x∈{a..b}. a ≤ x ⟷ True" by simp
lemma "∀x∈{a..b}. x ≤ b ⟷ True" by simp

因此，您最好假设 "a <= b"。要应用 fundamental_theorem_of_calculus "for any value in the set"，您还需要变量边界的导数，

∀x∈{a..b}. ∀y∈{a..x}. (f has_vector_derivative f' y) (at y within {a..x})

您可以在证明中使用 has_vector_derivative_within_subset：

lemma lm1':
fixes f :: "real ⇒ real"
assumes "∀x∈{a..b}. (f has_vector_derivative f' x) (at x within {a .. b})"
assumes "a ≤ b"
shows "∀x∈{a..b}. (f' has_integral (f x - f a)) {a .. x}"
using assms
apply safe
apply (rule fundamental_theorem_of_calculus)
 apply simp
apply safe
apply (rule has_vector_derivative_within_subset[where s="{a .. b}"])
 apply simp
apply simp
done

或更紧凑：

using assms
by (auto intro!: fundamental_theorem_of_calculus
  intro: has_vector_derivative_within_subset[where s="{a .. b}"])

证明集合内的整合

Proving integration within a set

isabelle