Theory Integrals
theory Integrals
imports "HOL-Analysis.Analysis" General_Utils
begin
lemma
assumes "a < (b::real)"
shows frontier_ic: "frontier {a<..b} = {a,b}"
and frontier_ci: "frontier {a<..<b} = {a,b}"
using assms by(auto simp: frontier_def)
lemma ic_not_closed:
assumes "a < (b::real)"
shows "¬ closed {a<..b}"
using assms frontier_subset_eq frontier_ic greaterThanAtMost_iff by blast
lemma closure_ic_union_ci:
assumes "a < (b::real)" "b < c"
shows "closure ({a..<b} ∪ {b<..c}) = {a .. c}"
using assms by force
lemma interior_ic_ci_union:
assumes "a < (b::real)" "b < c"
shows "b ∉ (interior ({a..<b} ∪ {b<..c}))"
proof-
have "b ∉ ({a..<b} ∪ {b<..c})" by auto
then show ?thesis
using interior_subset by blast
qed
lemma frontier_ic_union_ci:
assumes "a < (b::real)" "b < c"
shows "b ∈ frontier ({a..<b} ∪ {b<..c})"
using closure_ic_union_ci assms interior_ic_ci_union
by(simp add: frontier_def)
lemma ic_union_ci_not_closed:
assumes "a < (b::real)" "b < c"
shows "¬ closed ({a..<b} ∪ {b<..c})"
proof-
have "b ∉ ({a..<b} ∪ {b<..c})" by auto
then show ?thesis
using assms frontier_subset_eq frontier_ic_union_ci[OF assms]
by (auto simp only: subset_iff)
qed
lemma integrable_continuous_:
fixes f :: "'b::euclidean_space ⇒ 'a::banach"
assumes "continuous_on (cbox a b) f"
shows "f integrable_on cbox a b"
by (simp add: assms integrable_continuous)
lemma removing_singletons_from_div:
assumes "∀t∈S. ∃c d::real. c < d ∧ {c..d} = t"
"{x} ∪ ⋃S = {a..b}" "a < x" "x < b"
"finite S"
shows "∃t∈S. x ∈ t"
proof(rule ccontr)
assume "¬(∃t∈S. x ∈ t)"
then have "∀t∈S. x ∉ t" by auto
then have "x ∉ ⋃S" by auto
then have i: "⋃S = {a..b} - {x}" using assms (2) by auto
have "x ∈ {a..b}" using assms by auto
then have "{a .. b} - {x} = {a..<x} ∪ {x<..b}" by auto
then have 0: "⋃S = {a..<x} ∪ {x<..b}" using i by auto
have 1:"closed (⋃S)"
apply(rule closed_Union)
proof-
show "finite S"
using assms by auto
show "∀T∈S. closed T" using assms by auto
qed
show False using 0 1 ic_union_ci_not_closed assms by auto
qed
lemma remove_singleton_from_division_of:
assumes "A division_of {a::real..b}" "a < b"
assumes "x ∈ {a..b}"
shows "∃c d. c < d ∧ {c..d} ∈ A ∧ x ∈ {c..d}"
proof -
from assms have "x islimpt {a..b}"
by (intro connected_imp_perfect) auto
also have "{a..b} = {x. {x..x} ∈ A} ∪ ({a..b} - {x. {x..x} ∈ A})"
using assms by auto
also have "x islimpt … ⟷ x islimpt {a..b} - {x. {x..x} ∈ A}"
proof (intro islimpt_Un_finite)
have "{x. {x..x} ∈ A} ⊆ Inf ` A"
proof safe
fix x assume "{x..x} ∈ A"
thus "x ∈ Inf ` A"
by (auto intro!: bexI[of _ "{x}"] simp: image_iff)
qed
moreover from assms have "finite A" by (auto simp: division_of_def)
hence "finite (Inf ` A)" by auto
ultimately show "finite {x. {x..x} ∈ A}" by (rule finite_subset)
qed
also have "{a..b} = ⋃A"
using assms by (auto simp: division_of_def)
finally have "x islimpt ⋃(A - range (λx. {x..x}))"
by (rule islimpt_subset) auto
moreover have "closed (⋃(A - range (λx. {x..x})))"
using assms by (intro closed_Union) auto
ultimately have "x ∈ (⋃(A - range (λx. {x..x})))"
by (auto simp: closed_limpt)
then obtain X where "x ∈ X" "X ∈ A" "X ∉ range (λx. {x..x})"
by blast
moreover from division_ofD(2)[OF assms(1) this(2)] division_ofD(3)[OF assms(1) this(2)]
division_ofD(4)[OF assms(1) this(2)]
obtain c d where "X = cbox c d" "X ⊆ {a..b}" "X ≠ {}" by blast
ultimately have "c ≤ d" by auto
have "c ≠ d"
proof
assume "c = d"
with ‹X = cbox c d› have "X = {c..c}" by auto
hence "X ∈ range (λx. {x..x})" by blast
with ‹X ∉ range (λx. {x..x})› show False by contradiction
qed
with ‹c ≤ d› have "c < d" by simp
with ‹X = cbox c d› and ‹x ∈ X› and ‹X ∈ A› show ?thesis
by auto
qed
lemma remove_singleton_from_tagged_division_of:
assumes "A tagged_division_of {a::real..b}" "a < b"
assumes "x ∈ {a..b}"
shows "∃k c d. c < d ∧ (k, {c..d}) ∈ A ∧ x ∈ {c..d}"
using remove_singleton_from_division_of[OF division_of_tagged_division[OF assms(1)] assms(2)]
using assms(3) by fastforce
lemma tagged_div_wo_singlestons:
assumes "p tagged_division_of {a::real..b}" "a < b"
shows "(p - {xk. ∃x y. xk = (x,{y})}) tagged_division_of cbox a b"
using remove_singleton_from_tagged_division_of[OF assms] assms
apply(auto simp add: tagged_division_of_def tagged_partial_division_of_def)
apply blast
apply blast
apply blast
by fastforce
lemma tagged_div_wo_empty:
assumes "p tagged_division_of {a::real..b}" "a < b"
shows "(p - {xk. ∃x. xk = (x,{})}) tagged_division_of cbox a b"
using remove_singleton_from_tagged_division_of[OF assms] assms
apply(auto simp add: tagged_division_of_def tagged_partial_division_of_def)
apply blast
apply blast
apply blast
by fastforce
lemma fine_diff:
assumes "γ fine p"
shows "γ fine (p - s)"
apply (auto simp add: fine_def)
using assms by auto
lemma tagged_div_tage_notin_set:
assumes "finite (s::real set)"
"p tagged_division_of {a..b}"
"γ fine p" "(∀(x, K)∈p. ∃c d::real. c < d ∧ K = {c..d})" "gauge γ"
shows "∃p' γ'. p' tagged_division_of {a..b} ∧
γ' fine p' ∧ (∀(x, K)∈p'. x ∉ s) ∧ gauge γ'"
proof-
have "(∀(x::real, K)∈p. ∃x'. x' ∉ s ∧ x'∈ interior K)"
proof-
{fix x::real
fix K
assume ass: "(x::real,K) ∈ p"
have "(∀(x, K)∈p. infinite (interior K))"
using assms(4) infinite_Ioo interior_atLeastAtMost_real
by (smt (verit) split_beta)
then have i: "infinite (interior K)" using ass by auto
have "∃x'. x' ∉ s ∧ x'∈ interior K"
using infinite_imp_nonempty[OF Diff_infinite_finite[OF assms(1) i]] by auto}
then show ?thesis by auto
qed
then obtain f where f: "(∀(x::real, K)∈p. (f (x,K)) ∉ s ∧ (f (x,K)) ∈ interior K)"
using choice_iff[where ?Q = "λ(x,K) x'. (x::real, K)∈p ⟶ x' ∉ s ∧ x' ∈ interior K"]
apply (auto simp add: case_prod_beta)
by metis
have f': "(∀(x::real, K)∈p. (f (x,K)) ∉ s ∧ (f (x,K)) ∈ K)"
using f interior_subset
by (auto simp add: case_prod_beta subset_iff)
let ?p' = "{m. (∃xK. m = ((f xK), snd xK) ∧ xK ∈ p)}"
have 0: "(∀(x, K)∈?p'. x ∉ s)"
using f
by (auto simp add: case_prod_beta)
have i: "finite {(f (a, b), b) |a b. (a, b) ∈ p}"
proof-
have a: "{(f (a, b), b) |a b. (a, b) ∈ p} = (%(a,b). (f(a,b),b)) ` p" by auto
have b: "finite p" using assms(2) by auto
show ?thesis using a b by auto
qed
have 1: "?p' tagged_division_of {a..b}"
using assms(2) f'
apply(auto simp add: tagged_division_of_def tagged_partial_division_of_def case_prod_beta)
apply(metis i)
apply blast
apply blast
by fastforce
have f_inj: "inj_on f p"
unfolding inj_on_def
proof (intro strip)
fix x y
assume "x ∈ p" "y ∈ p" "f x = f y"
then show "x = y"
using f tagged_division_ofD(5)[OF assms(2)]
by (smt (verit, del_insts) IntI case_prodE empty_iff)
qed
let ?γ' = "λx. if (∃xK ∈ p. f xK = x) then (γ o fst o the_inv_into p f) x else γ x"
have 2: "?γ' fine ?p'" using assms(3)
by (force simp add: fine_def case_prod_beta the_inv_into_f_f[OF f_inj])
have 3: "gauge ?γ'"
using assms(5) assms(3) f'
by (force simp add: fine_def gauge_def case_prod_beta the_inv_into_f_f[OF f_inj])
have "?p' tagged_division_of {a..b} ∧ ?γ' fine ?p' ∧ (∀(x, K)∈?p'. x ∉ s) ∧ gauge ?γ'"
using 0 1 2 3 by auto
then show ?thesis by meson
qed
lemma has_integral_bound_spike_finite:
fixes f :: "'a::euclidean_space ⇒ 'b::real_normed_vector"
assumes "0 ≤ B" and "finite S"
and f: "(f has_integral i) (cbox a b)"
and leB: "⋀x. x ∈ cbox a b - S ⟹ norm (f x) ≤ B"
shows "norm i ≤ B * measure lborel (cbox a b)"
proof -
define g where "g ≡ (λx. if x ∈ S then 0 else f x)"
then have "⋀x. x ∈ cbox a b - S ⟹ norm (g x) ≤ B"
using leB by simp
moreover have "(g has_integral i) (cbox a b)"
using has_integral_spike_finite [OF ‹finite S› _ f]
by (simp add: g_def)
ultimately show ?thesis
by (simp add: ‹0 ≤ B› g_def has_integral_bound)
qed
lemma has_integral_bound_:
fixes f :: "real ⇒ 'a::real_normed_vector"
assumes "a < b"
and "0 ≤ B"
and f: "(f has_integral i) (cbox a b)"
and "finite s"
and "∀x∈(cbox a b)-s. norm (f x) ≤ B"
shows "norm i ≤ B * measure lborel (cbox a b)"
using has_integral_bound_spike_finite assms by blast
corollary has_integral_bound_real':
fixes f :: "real ⇒ 'b::real_normed_vector"
assumes "0 ≤ B"
and f: "(f has_integral i) (cbox a b)"
and "finite s"
and "∀x∈(cbox a b)-s. norm (f x) ≤ B"
shows "norm i ≤ B * measure lborel {a..b}"
by (metis assms(1) assms(3) assms(4) box_real(2) f has_integral_bound_spike_finite)
lemma integral_has_vector_derivative_continuous_at':
fixes f :: "real ⇒ 'a::banach"
assumes "finite s"
and f: "f integrable_on {a..b}"
and x: "x ∈ {a..b} - s"
and fx: "continuous (at x within ({a..b} - s)) f"
shows "((λu. integral {a..u} f) has_vector_derivative f x) (at x within ({a..b} - s))"
proof -
let ?I = "λa b. integral {a..b} f"
{ fix e::real
assume "e > 0"
obtain d where "d>0" and d: "⋀x'. ⟦x' ∈ {a..b} - s; ¦x' - x¦ < d⟧ ⟹ norm(f x' - f x) ≤ e"
using ‹e>0› fx by (auto simp: continuous_within_eps_delta dist_norm less_imp_le)
have "norm (integral {a..y} f - integral {a..x} f - (y-x) *⇩R f x) ≤ e * ¦y - x¦"
if y: "y ∈ {a..b} - s" and yx: "¦y - x¦ < d" for y
proof (cases "y < x")
case False
have "f integrable_on {a..y}"
using f y by (simp add: integrable_subinterval_real)
then have Idiff: "?I a y - ?I a x = ?I x y"
using False x by (simp add: algebra_simps Henstock_Kurzweil_Integration.integral_combine)
have fux_int: "((λu. f u - f x) has_integral integral {x..y} f - (y-x) *⇩R f x) {x..y}"
apply (rule has_integral_diff)
using x y apply (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]])
using has_integral_const_real [of "f x" x y] False
apply simp
done
show ?thesis
using False
apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
apply (rule has_integral_bound_real'[where f="(λu. f u - f x)"])
using yx False d x y ‹e>0› apply (auto simp add: Idiff fux_int)
proof-
let ?M48= "mset_set s"
show "⋀z. y - x < d ⟹ (⋀x'. a ≤ x' ∧ x' ≤ b ∧ x' ∉ s ⟹ ¦x' - x¦ < d ⟹ norm (f x' - f x) ≤ e) ⟹ 0 < e ⟹ z ∉# ?M48 ⟹ a ≤ x ⟹ x ∉ s ⟹ y ≤ b ⟹ y ∉ s ⟹ x ≤ z ⟹ z ≤ y ⟹ norm (f z - f x) ≤ e"
using assms by auto
qed
next
case True
have "f integrable_on {a..x}"
using f x by (simp add: integrable_subinterval_real)
then have Idiff: "?I a x - ?I a y = ?I y x"
using True x y by (simp add: algebra_simps Henstock_Kurzweil_Integration.integral_combine)
have fux_int: "((λu. f u - f x) has_integral integral {y..x} f - (x - y) *⇩R f x) {y..x}"
apply (rule has_integral_diff)
using x y apply (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]])
using has_integral_const_real [of "f x" y x] True
by simp
have "norm (integral {a..x} f - integral {a..y} f - (x - y) *⇩R f x) ≤ e * ¦y - x¦"
using True
apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
apply (rule has_integral_bound_real'[where f="(λu. f u - f x)"])
using yx True d x y ‹e>0› apply (auto simp add: Idiff fux_int)
proof-
let ?M44= "mset_set s"
show " ⋀xa. x - y < d ⟹ y < x ⟹ (⋀x'. a ≤ x' ∧ x' ≤ b ∧ x' ∉ s ⟹ ¦x' - x¦ < d ⟹ norm (f x' - f x) ≤ e) ⟹ 0 < e ⟹ xa ∉# ?M44 ⟹ x ≤ b ⟹ x ∉ s ⟹ a ≤ y ⟹ y ∉ s ⟹ y ≤ xa ⟹ xa ≤ x ⟹ norm (f xa - f x) ≤ e"
using assms by auto
qed
then show ?thesis
by (simp add: algebra_simps norm_minus_commute)
qed
then have "∃d>0. ∀y∈{a..b} - s. ¦y - x¦ < d ⟶ norm (integral {a..y} f - integral {a..x} f - (y-x) *⇩R f x) ≤ e * ¦y - x¦"
using ‹d>0› by blast
}
then show ?thesis
by (simp add: has_vector_derivative_def has_derivative_within_alt bounded_linear_scaleR_left)
qed
lemma at_within_closed_interval_finite:
fixes x::real
assumes "a < x" "x < b" "x ∉ S" "finite S"
shows "(at x within {a..b} - S) = at x"
proof -
have "interior ({a..b} - S) = {a<..<b} - S"
using ‹finite S›
by (simp add: interior_diff finite_imp_closed)
then show ?thesis
using at_within_interior assms by fastforce
qed
lemma fundamental_theorem_of_calculus_interior_stronger':
fixes f :: "real ⇒ 'a::banach"
assumes "finite S"
and "a ≤ b" "⋀x. x ∈ {a <..< b} - S ⟹ (f has_vector_derivative f'(x)) (at x within {a..b} - S)"
and "continuous_on {a .. b} f"
shows "(f' has_integral (f b - f a)) {a .. b}"
using assms fundamental_theorem_of_calculus_interior_strong at_within_cbox_finite countable_finite
by (metis DiffD1 DiffD2 interior_atLeastAtMost_real interior_cbox interval_cbox)
lemma has_integral_substitution_general_:
fixes f :: "real ⇒ 'a::euclidean_space" and g :: "real ⇒ real"
assumes s: "finite s" and le: "a ≤ b"
and subset: "g ` {a..b} ⊆ {c..d}"
and f: "f integrable_on {c..d}" "continuous_on ({c..d} - (g ` s)) f"
and g : "continuous_on {a..b} g" "inj_on g ({a..b} ∪ s)"
and deriv [derivative_intros]:
"⋀x. x ∈ {a..b} - s ⟹ (g has_field_derivative g' x) (at x within {a..b})"
shows "((λx. g' x *⇩R f (g x)) has_integral (integral {g a..g b} f - integral {g b..g a} f)) {a..b}"
proof -
let ?F = "λx. integral {c..g x} f"
have cont_int: "continuous_on {a..b} ?F"
by (rule continuous_on_compose2[OF _ g(1) subset] indefinite_integral_continuous_1
f)+
have deriv: "⋀x. x ∈ {a..b} - s ⟹ (((λx. integral {c..x} f) ∘ g) has_vector_derivative g' x *⇩R f (g x))
(at x within ({a..b} - s))"
apply (rule has_vector_derivative_eq_rhs)
apply (rule vector_diff_chain_within)
apply (subst has_real_derivative_iff_has_vector_derivative [symmetric])
proof-
fix x::real
assume ass: "x ∈ {a..b} - s"
let ?f'3 = "g' x"
have i:"{a..b} - s ⊆ {a..b}" by auto
have ii: " (g has_vector_derivative g' x) (at x within {a..b})" using deriv[OF ass]
by (simp only: has_real_derivative_iff_has_vector_derivative)
show "(g has_real_derivative ?f'3) (at x within {a..b} - s)"
using has_vector_derivative_within_subset[OF ii i]
by (simp only: has_real_derivative_iff_has_vector_derivative)
next
let ?g'3 = "f o g"
show "⋀x. x ∈ {a..b} - s ⟹ ((λx. integral {c..x} f) has_vector_derivative ?g'3 x) (at (g x) within g ` ({a..b} - s))"
proof-
fix x::real
assume ass: "x ∈ {a..b} - s"
have "finite (g ` s)" using s by auto
then have i: "((λx. integral {c..x} f) has_vector_derivative f(g x)) (at (g x) within ({c..d} - g ` s))"
proof (rule integral_has_vector_derivative_continuous_at')
show " f integrable_on {c..d}" using f by auto
show "g x ∈ {c..d} - g ` s" using ass subset
by (smt (verit) Diff_iff g(2) inf_sup_ord(4) inj_on_image_mem_iff subsetD sup_ge1)
show "continuous (at (g x) within {c..d} - g ` s) f"
using ‹g x ∈ {c..d} - g ` s› continuous_on_eq_continuous_within f(2) by blast
qed
have ii: "g ` ({a..b} - s) ⊆ ({c..d} - g ` s)"
using subset g(2)
by (simp add: image_subset_iff inj_on_image_mem_iff)
then show "((λx. integral {c..x} f) has_vector_derivative ?g'3 x) (at (g x) within g ` ({a..b} - s))"
using has_vector_derivative_within_subset i by fastforce
qed
show "⋀x. x ∈ {a..b} - s ⟹ g' x *⇩R ?g'3 x = g' x *⇩R f (g x)" by auto
qed
have deriv: "(?F has_vector_derivative g' x *⇩R f (g x))
(at x within {a..b} - s)" if "x ∈ {a<..<b} - (s)" for x
using deriv[of x] that by (simp add: at_within_Icc_at o_def)
have "((λx. g' x *⇩R f (g x)) has_integral (?F b - ?F a)) {a..b}"
using cont_int
using fundamental_theorem_of_calculus_interior_stronger'[OF s le deriv]
by blast
also
from subset have "g x ∈ {c..d}" if "x ∈ {a..b}" for x using that by blast
from this[of a] this[of b] le have cd: "c ≤ g a" "g b ≤ d" "c ≤ g b" "g a ≤ d" by auto
have "integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f"
proof cases
assume "g a ≤ g b"
note le = le this
from cd have "integral {c..g a} f + integral {g a..g b} f = integral {c..g b} f"
by (meson Henstock_Kurzweil_Integration.integral_combine atLeastatMost_subset_iff f(1) integrable_on_subinterval le(2) order_refl)
with le show ?thesis
by (cases "g a = g b") (simp_all add: algebra_simps)
next
assume less: "¬g a ≤ g b"
then have le: "g a ≥ g b" by simp
from cd have "integral {c..g b} f + integral {g b..g a} f = integral {c..g a} f"
by (meson Henstock_Kurzweil_Integration.integral_combine atLeastatMost_subset_iff f(1) integrable_on_subinterval le order_refl)
with less show ?thesis
by (simp_all add: algebra_simps)
qed
finally show ?thesis .
qed
lemma has_integral_substitution_general__:
fixes f :: "real ⇒ 'a::euclidean_space" and g :: "real ⇒ real"
assumes s: "finite s" and le: "a ≤ b" and s_subset: "s ⊆ {a..b}"
and subset: "g ` {a..b} ⊆ {c..d}"
and f: "f integrable_on {c..d}" "continuous_on ({c..d} - (g ` s)) f"
and g : "continuous_on {a..b} g" "inj_on g {a..b}"
and deriv [derivative_intros]:
"⋀x. x ∈ {a..b} - s ⟹ (g has_field_derivative g' x) (at x within {a..b})"
shows "((λx. g' x *⇩R f (g x)) has_integral (integral {g a..g b} f - integral {g b..g a} f)) {a..b}"
using s_subset has_integral_substitution_general_[OF s le subset f g(1) _ deriv]
by (simp add: g(2) sup_absorb1)
lemma has_integral_substitution_general_':
fixes f :: "real ⇒ 'a::euclidean_space" and g :: "real ⇒ real"
assumes s: "finite s" and le: "a ≤ b" and s': "finite s'"
and subset: "g ` {a..b} ⊆ {c..d}"
and f: "f integrable_on {c..d}" "continuous_on ({c..d} - s') f"
and g : "continuous_on {a..b} g" "∀x∈s'. finite (g -` {x})" "surj_on s' g" "inj_on g ({a..b} ∪ ((s ∪ g -` s')))"
and deriv [derivative_intros]:
"⋀x. x ∈ {a..b} - s ⟹ (g has_field_derivative g' x) (at x within {a..b})"
shows "((λx. g' x *⇩R f (g x)) has_integral (integral {g a..g b} f - integral {g b..g a} f)) {a..b}"
proof-
have a: "g -` s' = ⋃{t. ∃x. t = g -` {x} ∧ x ∈ s'}"
using s s' by blast
have "finite (⋃{t. ∃x. t = g -` {x} ∧ x ∈ s'})" using s'
by (metis (no_types, lifting) ‹g -` s' = ⋃{g -` {x} |x. x ∈ s'}› finite_UN_I g(2) vimage_eq_UN)
then have 0: "finite (s ∪ (g -` s'))"
using a s by simp
have 1: "continuous_on ({c..d} - g ` (s ∪ g -` s')) f"
using f(2) surj_on_image_vimage_eq
by (metis Diff_mono Un_upper2 continuous_on_subset equalityE g(3) image_Un)
have 2: " (⋀x. x ∈ {a..b} - (s ∪ g -` s') ⟹ (g has_real_derivative g' x) (at x within {a..b}))"
using deriv by auto
show ?thesis using has_integral_substitution_general_[OF 0 assms(2) subset f(1) 1 g(1) g(4) 2]
by auto
qed
end