Theory HOL-Analysis.Change_Of_Vars
section‹Change of Variables Theorems›
theory Change_Of_Vars
imports Vitali_Covering_Theorem Determinants
Determinant_Linear_Function Euclidean_Space_Transfer
begin
subsection ‹Measurable Shear and Stretch›
proposition
fixes a :: "real^'n"
assumes "m ≠ n" and ab_ne: "cbox a b ≠ {}" and an: "0 ≤ a$n"
shows measurable_shear_interval: "(λx. χ i. if i = m then x$m + x$n else x$i) ` (cbox a b) ∈ lmeasurable"
(is "?f ` _ ∈ _")
and measure_shear_interval:
"measure lebesgue ((λx. χ i. if i = m then x$m + x$n else x$i) ` cbox a b)
= measure lebesgue (cbox a b)" (is "?Q")
proof -
have lin: "linear ?f"
by (rule linearI) (auto simp: plus_vec_def scaleR_vec_def algebra_simps)
show fab: "?f ` cbox a b ∈ lmeasurable"
by (simp add: lin measurable_linear_image_interval)
let ?c = "χ i. if i = m then b$m + b$n else b$i"
let ?mn = "axis m 1 - axis n (1::real)"
have eq1: "measure lebesgue (cbox a ?c)
= measure lebesgue (?f ` cbox a b)
+ measure lebesgue (cbox a ?c ∩ {x. ?mn ∙ x ≤ a$m})
+ measure lebesgue (cbox a ?c ∩ {x. ?mn ∙ x ≥ b$m})"
proof (rule measure_Un3_negligible)
show "cbox a ?c ∩ {x. ?mn ∙ x ≤ a$m} ∈ lmeasurable" "cbox a ?c ∩ {x. ?mn ∙ x ≥ b$m} ∈ lmeasurable"
by (auto simp: convex_Int convex_halfspace_le convex_halfspace_ge bounded_Int measurable_convex)
have "negligible {x. ?mn ∙ x = a$m}"
by (metis ‹m ≠ n› axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane)
moreover have "?f ` cbox a b ∩ (cbox a ?c ∩ {x. ?mn ∙ x ≤ a $ m}) ⊆ {x. ?mn ∙ x = a$m}"
using ‹m ≠ n› antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis')
ultimately show "negligible ((?f ` cbox a b) ∩ (cbox a ?c ∩ {x. ?mn ∙ x ≤ a $ m}))"
by (rule negligible_subset)
have "negligible {x. ?mn ∙ x = b$m}"
by (metis ‹m ≠ n› axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane)
moreover have "(?f ` cbox a b) ∩ (cbox a ?c ∩ {x. ?mn ∙ x ≥ b$m}) ⊆ {x. ?mn ∙ x = b$m}"
using ‹m ≠ n› antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis')
ultimately show "negligible (?f ` cbox a b ∩ (cbox a ?c ∩ {x. ?mn ∙ x ≥ b$m}))"
by (rule negligible_subset)
have "negligible {x. ?mn ∙ x = b$m}"
by (metis ‹m ≠ n› axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane)
moreover have "(cbox a ?c ∩ {x. ?mn ∙ x ≤ a $ m} ∩ (cbox a ?c ∩ {x. ?mn ∙ x ≥ b$m})) ⊆ {x. ?mn ∙ x = b$m}"
using ‹m ≠ n› ab_ne
apply (clarsimp simp: algebra_simps mem_box_cart inner_axis')
by (smt (verit, ccfv_SIG) interval_ne_empty_cart(1))
ultimately show "negligible (cbox a ?c ∩ {x. ?mn ∙ x ≤ a $ m} ∩ (cbox a ?c ∩ {x. ?mn ∙ x ≥ b$m}))"
by (rule negligible_subset)
show "?f ` cbox a b ∪ cbox a ?c ∩ {x. ?mn ∙ x ≤ a $ m} ∪ cbox a ?c ∩ {x. ?mn ∙ x ≥ b$m} = cbox a ?c" (is "?lhs = _")
proof
show "?lhs ⊆ cbox a ?c"
by (auto simp: mem_box_cart add_mono) (meson add_increasing2 an order_trans)
show "cbox a ?c ⊆ ?lhs"
apply (clarsimp simp: algebra_simps image_iff inner_axis' lambda_add_Galois [OF ‹m ≠ n›])
by (smt (verit, del_insts) mem_box_cart(2) vec_lambda_beta)
qed
qed (fact fab)
let ?d = "χ i. if i = m then a $ m - b $ m else 0"
have eq2: "measure lebesgue (cbox a ?c ∩ {x. ?mn ∙ x ≤ a $ m}) + measure lebesgue (cbox a ?c ∩ {x. ?mn ∙ x ≥ b$m})
= measure lebesgue (cbox a (χ i. if i = m then a $ m + b $ n else b $ i))"
proof (rule measure_translate_add[of "cbox a ?c ∩ {x. ?mn ∙ x ≤ a$m}" "cbox a ?c ∩ {x. ?mn ∙ x ≥ b$m}"
"(χ i. if i = m then a$m - b$m else 0)" "cbox a (χ i. if i = m then a$m + b$n else b$i)"])
show "(cbox a ?c ∩ {x. ?mn ∙ x ≤ a$m}) ∈ lmeasurable"
"cbox a ?c ∩ {x. ?mn ∙ x ≥ b$m} ∈ lmeasurable"
by (auto simp: convex_Int convex_halfspace_le convex_halfspace_ge bounded_Int measurable_convex)
have "⋀x. ⟦x $ n + a $ m ≤ x $ m⟧
⟹ x ∈ (+) (χ i. if i = m then a $ m - b $ m else 0) ` {x. x $ n + b $ m ≤ x $ m}"
using ‹m ≠ n›
by (rule_tac x="x - (χ i. if i = m then a$m - b$m else 0)" in image_eqI)
(simp_all add: mem_box_cart)
then have imeq: "(+) ?d ` {x. b $ m ≤ ?mn ∙ x} = {x. a $ m ≤ ?mn ∙ x}"
using ‹m ≠ n› by (auto simp: mem_box_cart inner_axis' algebra_simps)
have "⋀x. ⟦0 ≤ a $ n; x $ n + a $ m ≤ x $ m;
∀i. i ≠ m ⟶ a $ i ≤ x $ i ∧ x $ i ≤ b $ i⟧
⟹ a $ m ≤ x $ m"
using ‹m ≠ n› by force
then have "(+) ?d ` (cbox a ?c ∩ {x. b $ m ≤ ?mn ∙ x})
= cbox a (χ i. if i = m then a $ m + b $ n else b $ i) ∩ {x. a $ m ≤ ?mn ∙ x}"
using an ab_ne
apply (simp add: cbox_translation [symmetric] translation_Int interval_ne_empty_cart imeq)
apply (auto simp: mem_box_cart inner_axis' algebra_simps if_distrib all_if_distrib)
by (metis (full_types) add_mono mult_2_right)
moreover have "a $ m ≤ b $ m"
by (metis ab_ne interval_ne_empty_cart(1))
ultimately show "cbox a ?c ∩ {x. ?mn ∙ x ≤ a $ m} ∪
(+) ?d ` (cbox a ?c ∩ {x. b $ m ≤ ?mn ∙ x}) =
cbox a (χ i. if i = m then a $ m + b $ n else b $ i)" (is "?lhs = ?rhs")
using an ‹m ≠ n›
by (force simp: mem_box_cart inner_axis' algebra_simps if_distrib all_if_distrib)
have "negligible{x. ?mn ∙ x = a$m}"
by (metis ‹m ≠ n› axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane)
moreover have "(cbox a ?c ∩ {x. ?mn ∙ x ≤ a $ m} ∩
(+) ?d ` (cbox a ?c ∩ {x. b $ m ≤ ?mn ∙ x})) ⊆ {x. ?mn ∙ x = a$m}"
using ‹m ≠ n› antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis')
ultimately show "negligible (cbox a ?c ∩ {x. ?mn ∙ x ≤ a $ m} ∩
(+) ?d ` (cbox a ?c ∩ {x. b $ m ≤ ?mn ∙ x}))"
by (rule negligible_subset)
qed
have ac_ne: "cbox a ?c ≠ {}"
by (smt (verit, del_insts) ab_ne an interval_ne_empty_cart(1) vec_lambda_beta)
have ax_ne: "cbox a (χ i. if i = m then a $ m + b $ n else b $ i) ≠ {}"
using ab_ne an
by (smt (verit, ccfv_threshold) interval_ne_empty_cart(1) vec_lambda_beta)
have eq3: "measure lebesgue (cbox a ?c) = measure lebesgue (cbox a (χ i. if i = m then a$m + b$n else b$i)) + measure lebesgue (cbox a b)"
by (simp add: content_cbox_if_cart ab_ne ac_ne ax_ne algebra_simps prod.delta_remove
if_distrib [of "λu. u - z" for z] prod.remove)
show ?Q
using eq1 eq2 eq3 by (simp add: algebra_simps)
qed
proposition
fixes S :: "(real^'n) set"
assumes "S ∈ lmeasurable"
shows measurable_stretch: "((λx. χ k. m k * x$k) ` S) ∈ lmeasurable" (is "?f ` S ∈ _")
and measure_stretch: "measure lebesgue ((λx. χ k. m k * x$k) ` S) = ¦prod m UNIV¦ * measure lebesgue S"
(is "?MEQ")
proof -
have "(?f ` S) ∈ lmeasurable ∧ ?MEQ"
proof (cases "∀k. m k ≠ 0")
case True
have m0: "0 < ¦prod m UNIV¦"
using True by simp
have "(indicat_real (?f ` S) has_integral ¦prod m UNIV¦ * measure lebesgue S) UNIV"
proof (clarsimp simp add: has_integral_alt [where i=UNIV])
fix e :: "real"
assume "e > 0"
have "(indicat_real S has_integral (measure lebesgue S)) UNIV"
using assms lmeasurable_iff_has_integral by blast
then obtain B where "B>0"
and B: "⋀a b. ball 0 B ⊆ cbox a b ⟹
∃z. (indicat_real S has_integral z) (cbox a b) ∧
¦z - measure lebesgue S¦ < e / ¦prod m UNIV¦"
by (simp add: has_integral_alt [where i=UNIV]) (metis (full_types) divide_pos_pos m0 m0 ‹e > 0›)
show "∃B>0. ∀a b. ball 0 B ⊆ cbox a b ⟶
(∃z. (indicat_real (?f ` S) has_integral z) (cbox a b) ∧
¦z - ¦prod m UNIV¦ * measure lebesgue S¦ < e)"
proof (intro exI conjI allI)
let ?C = "Max (range (λk. ¦m k¦)) * B"
show "?C > 0"
using True ‹B > 0› by (simp add: Max_gr_iff)
show "ball 0 ?C ⊆ cbox u v ⟶
(∃z. (indicat_real (?f ` S) has_integral z) (cbox u v) ∧
¦z - ¦prod m UNIV¦ * measure lebesgue S¦ < e)" for u v
proof
assume uv: "ball 0 ?C ⊆ cbox u v"
with ‹?C > 0› have cbox_ne: "cbox u v ≠ {}"
using centre_in_ball by blast
let ?α = "λk. u$k / m k"
let ?β = "λk. v$k / m k"
have invm0: "⋀k. inverse (m k) ≠ 0"
using True by auto
have "ball 0 B ⊆ (λx. χ k. x $ k / m k) ` ball 0 ?C"
proof clarsimp
fix x :: "real^'n"
assume x: "norm x < B"
have [simp]: "¦Max (range (λk. ¦m k¦))¦ = Max (range (λk. ¦m k¦))"
by (meson Max_ge abs_ge_zero abs_of_nonneg finite finite_imageI order_trans rangeI)
have "norm (χ k. m k * x $ k) ≤ norm (Max (range (λk. ¦m k¦)) *⇩R x)"
by (rule norm_le_componentwise_cart) (auto simp: abs_mult intro: mult_right_mono)
also have "… < ?C"
using x ‹0 < (MAX k. ¦m k¦) * B› ‹0 < B› zero_less_mult_pos2 by fastforce
finally have "norm (χ k. m k * x $ k) < ?C" .
then show "x ∈ (λx. χ k. x $ k / m k) ` ball 0 ?C"
using stretch_Galois [of "inverse ∘ m"] True by (auto simp: image_iff field_simps)
qed
then have Bsub: "ball 0 B ⊆ cbox (χ k. min (?α k) (?β k)) (χ k. max (?α k) (?β k))"
using cbox_ne uv image_stretch_interval_cart [of "inverse ∘ m" u v, symmetric]
by (force simp: field_simps)
obtain z where zint: "(indicat_real S has_integral z) (cbox (χ k. min (?α k) (?β k)) (χ k. max (?α k) (?β k)))"
and zless: "¦z - measure lebesgue S¦ < e / ¦prod m UNIV¦"
using B [OF Bsub] by blast
have ind: "indicat_real (?f ` S) = (λx. indicator S (χ k. x$k / m k))"
using True stretch_Galois [of m] by (force simp: indicator_def)
show "∃z. (indicat_real (?f ` S) has_integral z) (cbox u v) ∧
¦z - ¦prod m UNIV¦ * measure lebesgue S¦ < e"
proof (simp add: ind, intro conjI exI)
have "((λx. indicat_real S (χ k. x $ k/ m k)) has_integral z *⇩R ¦prod m UNIV¦)
((λx. χ k. x $ k * m k) ` cbox (χ k. min (?α k) (?β k)) (χ k. max (?α k) (?β k)))"
using True has_integral_stretch_cart [OF zint, of "inverse ∘ m"]
by (simp add: field_simps prod_dividef)
moreover have "((λx. χ k. x $ k * m k) ` cbox (χ k. min (?α k) (?β k)) (χ k. max (?α k) (?β k))) = cbox u v"
using True image_stretch_interval_cart [of "inverse ∘ m" u v, symmetric]
image_stretch_interval_cart [of "λk. 1" u v, symmetric] ‹cbox u v ≠ {}›
by (simp add: field_simps image_comp o_def)
ultimately show "((λx. indicat_real S (χ k. x $ k/ m k)) has_integral z *⇩R ¦prod m UNIV¦) (cbox u v)"
by simp
have "¦z *⇩R ¦prod m UNIV¦ - ¦prod m UNIV¦ * measure lebesgue S¦
= ¦prod m UNIV¦ * ¦z - measure lebesgue S¦"
by (metis (no_types, opaque_lifting) abs_abs abs_scaleR mult.commute real_scaleR_def right_diff_distrib')
also have "… < e"
using zless True by (simp add: field_simps)
finally show "¦z *⇩R ¦prod m UNIV¦ - ¦prod m UNIV¦ * measure lebesgue S¦ < e" .
qed
qed
qed
qed
then show ?thesis
by (auto simp: has_integral_integrable integral_unique lmeasure_integral_UNIV measurable_integrable)
next
case False
then obtain k where "m k = 0" and prm: "prod m UNIV = 0"
by auto
have nfS: "negligible (?f ` S)"
by (rule negligible_subset [OF negligible_standard_hyperplane_cart]) (use ‹m k = 0› in auto)
then show ?thesis
by (simp add: negligible_iff_measure prm)
qed
then show "(?f ` S) ∈ lmeasurable" ?MEQ
by metis+
qed
proposition
fixes f :: "real^'n::{finite,wellorder} ⇒ real^'n::_"
assumes "linear f" "S ∈ lmeasurable"
shows measurable_linear_image_cart: "(f ` S) ∈ lmeasurable"
and measure_linear_image_cart: "measure lebesgue (f ` S) = ¦matrix_det (matrix f)¦ * measure lebesgue S" (is "?Q f S")
proof -
have "∀S ∈ lmeasurable. (f ` S) ∈ lmeasurable ∧ ?Q f S"
proof (rule induct_linear_elementary [OF ‹linear f›]; intro ballI)
fix f g and S :: "(real,'n) vec set"
assume "linear f" and "linear g"
and f [rule_format]: "∀S ∈ lmeasurable. f ` S ∈ lmeasurable ∧ ?Q f S"
and g [rule_format]: "∀S ∈ lmeasurable. g ` S ∈ lmeasurable ∧ ?Q g S"
and S: "S ∈ lmeasurable"
then have gS: "g ` S ∈ lmeasurable"
by blast
show "(f ∘ g) ` S ∈ lmeasurable ∧ ?Q (f ∘ g) S"
using f [OF gS] g [OF S] matrix_compose [OF ‹linear g› ‹linear f›]
by (simp add: o_def image_comp abs_mult det_mul)
next
fix f :: "real^'n::_ ⇒ real^'n::_" and i and S :: "(real^'n::_) set"
assume "linear f" and 0: "⋀x. f x $ i = 0" and "S ∈ lmeasurable"
then have "¬ inj f"
by (metis (full_types) linear_injective_imp_surjective one_neq_zero surjE vec_component)
have detf: "matrix_det (matrix f) = 0"
using ‹¬ inj f› det_nz_iff_inj[OF ‹linear f›] by blast
show "f ` S ∈ lmeasurable ∧ ?Q f S"
proof
show "f ` S ∈ lmeasurable"
using lmeasurable_iff_indicator_has_integral ‹linear f› ‹¬ inj f› negligible_UNIV negligible_linear_singular_image by blast
have "measure lebesgue (f ` S) = 0"
by (meson ‹¬ inj f› ‹linear f› negligible_imp_measure0 negligible_linear_singular_image)
also have "… = ¦matrix_det (matrix f)¦ * measure lebesgue S"
by (simp add: detf)
finally show "?Q f S" .
qed
next
fix c and S :: "(real^'n::_) set"
assume "S ∈ lmeasurable"
show "(λa. χ i. c i * a $ i) ` S ∈ lmeasurable ∧ ?Q (λa. χ i. c i * a $ i) S"
proof
show "(λa. χ i. c i * a $ i) ` S ∈ lmeasurable"
by (simp add: ‹S ∈ lmeasurable› measurable_stretch)
show "?Q (λa. χ i. c i * a $ i) S"
by (simp add: measure_stretch [OF ‹S ∈ lmeasurable›, of c] axis_def matrix_def det_diagonal)
qed
next
fix m :: "'n" and n :: "'n" and S :: "(real, 'n) vec set"
assume "m ≠ n" and "S ∈ lmeasurable"
let ?h = "λv::(real, 'n) vec. χ i. v $ Transposition.transpose m n i"
have lin: "linear ?h"
by (rule linearI) (simp_all add: plus_vec_def scaleR_vec_def)
have meq: "measure lebesgue ((λv::(real, 'n) vec. χ i. v $ Transposition.transpose m n i) ` cbox a b)
= measure lebesgue (cbox a b)" for a b
proof (cases "cbox a b = {}")
case True then show ?thesis
by simp
next
case False
then have him: "?h ` (cbox a b) ≠ {}"
by blast
have eq: "?h ` (cbox a b) = cbox (?h a) (?h b)"
by (auto simp: image_iff lambda_swap_Galois mem_box_cart) (metis transpose_involutory)+
show ?thesis
using him prod.permute [OF permutes_swap_id, where S=UNIV and g="λi. (b - a)$i", symmetric]
by (simp add: eq content_cbox_cart False)
qed
have "(χ i j. if Transposition.transpose m n i = j then 1 else 0) = (χ i j. if j = Transposition.transpose m n i then 1 else (0::real))"
by (auto intro!: Cart_lambda_cong)
then have "matrix ?h = transpose(χ i j. mat 1 $ i $ Transposition.transpose m n j)"
by (auto simp: matrix_eq transpose_def axis_def mat_def matrix_def)
then have 1: "¦matrix_det (matrix ?h)¦ = 1"
by (simp add: det_permute_columns permutes_swap_id sign_swap_id abs_mult)
show "?h ` S ∈ lmeasurable ∧ ?Q ?h S"
using measure_linear_sufficient [OF lin ‹S ∈ lmeasurable›] meq 1 by force
next
fix m n :: "'n" and S :: "(real, 'n) vec set"
assume "m ≠ n" and "S ∈ lmeasurable"
let ?h = "λv::(real, 'n) vec. χ i. if i = m then v $ m + v $ n else v $ i"
have lin: "linear ?h"
by (rule linearI) (auto simp: algebra_simps plus_vec_def scaleR_vec_def vec_eq_iff)
consider "m < n" | " n < m"
using ‹m ≠ n› less_linear by blast
then have 1: "matrix_det(matrix ?h) = 1"
proof cases
assume "m < n"
have *: "matrix ?h $ i $ j = (0::real)" if "j < i" for i j :: 'n
proof -
have "axis j 1 = (χ n. if n = j then 1 else (0::real))"
using axis_def by blast
then have "(χ p q. if p = m then axis q 1 $ m + axis q 1 $ n else axis q 1 $ p) $ i $ j = (0::real)"
using ‹j < i› axis_def ‹m < n› by auto
with ‹m < n› show ?thesis
by (auto simp: matrix_def axis_def cong: if_cong)
qed
show ?thesis
using ‹m ≠ n› by (subst det_upperdiagonal [OF *]) (auto simp: matrix_def axis_def cong: if_cong)
next
assume "n < m"
have *: "matrix ?h $ i $ j = (0::real)" if "j > i" for i j :: 'n
proof -
have "axis j 1 = (χ n. if n = j then 1 else (0::real))"
using axis_def by blast
then have "(χ p q. if p = m then axis q 1 $ m + axis q 1 $ n else axis q 1 $ p) $ i $ j = (0::real)"
using ‹j > i› axis_def ‹m > n› by auto
with ‹m > n› show ?thesis
by (auto simp: matrix_def axis_def cong: if_cong)
qed
show ?thesis
using ‹m ≠ n›
by (subst det_lowerdiagonal [OF *]) (auto simp: matrix_def axis_def cong: if_cong)
qed
have meq: "measure lebesgue (?h ` (cbox a b)) = measure lebesgue (cbox a b)" for a b
proof (cases "cbox a b = {}")
case True then show ?thesis by simp
next
case False
then have ne: "(+) (χ i. if i = n then - a $ n else 0) ` cbox a b ≠ {}"
by auto
let ?v = "χ i. if i = n then - a $ n else 0"
have "?h ` cbox a b
= (+) (χ i. if i = m ∨ i = n then a $ n else 0) ` ?h ` (+) ?v ` (cbox a b)"
using ‹m ≠ n› unfolding image_comp o_def by (force simp: vec_eq_iff)
then have "measure lebesgue (?h ` (cbox a b))
= measure lebesgue ((λv. χ i. if i = m then v $ m + v $ n else v $ i) `
(+) ?v ` cbox a b)"
by (rule ssubst) (rule measure_translation)
also have "… = measure lebesgue ((λv. χ i. if i = m then v $ m + v $ n else v $ i) ` cbox (?v +a) (?v + b))"
by (metis (no_types, lifting) cbox_translation)
also have "… = measure lebesgue ((+) ?v ` cbox a b)"
using ‹m ≠ n› ne
by (subst measure_shear_interval) (auto simp: cbox_translation)
also have "… = measure lebesgue (cbox a b)"
by (rule measure_translation)
finally show ?thesis .
qed
show "?h ` S ∈ lmeasurable ∧ ?Q ?h S"
using measure_linear_sufficient [OF lin ‹S ∈ lmeasurable›] meq 1 by force
qed
with assms show "(f ` S) ∈ lmeasurable" "?Q f S"
by metis+
qed
proposition
fixes f :: "'a :: euclidean_space ⇒ 'a"
assumes "linear f" "S ∈ lmeasurable"
shows measurable_linear_image: "(f ` S) ∈ lmeasurable"
and measure_linear_image: "measure lebesgue (f ` S) = ¦eucl.det f¦ * measure lebesgue S"
proof -
note [transfer_rule] = transfer_measure_bij_rules transfer_eucl_bij_rules
show "measure lebesgue (f ` S) = ¦eucl.det f¦ * measure lebesgue S"
using measure_linear_image_cart[where ?'n = "'a basis", untransferred, OF assms] .
show "(f ` S) ∈ lmeasurable"
using measurable_linear_image_cart[where ?'n = "'a basis", untransferred, OF assms] .
qed
lemma
fixes f :: "'a::euclidean_space ⇒ 'a"
assumes f: "orthogonal_transformation f" and S: "S ∈ lmeasurable"
shows measurable_orthogonal_image: "f ` S ∈ lmeasurable"
and measure_orthogonal_image: "measure lebesgue (f ` S) = ¦eucl.det f¦ * measure lebesgue S"
proof -
have "linear f"
by (simp add: f orthogonal_transformation_linear)
then show "f ` S ∈ lmeasurable"
by (metis S measurable_linear_image)
show "measure lebesgue (f ` S) = ¦eucl.det f¦ * measure lebesgue S"
using S f ‹linear f› measure_linear_image by blast
qed
proposition measure_semicontinuous_with_hausdist_explicit:
assumes "bounded S" and neg: "negligible(frontier S)" and "e > 0"
obtains d where "d > 0"
"⋀T. ⟦T ∈ lmeasurable; ⋀y. y ∈ T ⟹ ∃x. x ∈ S ∧ dist x y < d⟧
⟹ measure lebesgue T < measure lebesgue S + e"
proof (cases "S = {}")
case True
with that ‹e > 0› show ?thesis by force
next
case False
then have frS: "frontier S ≠ {}"
using ‹bounded S› frontier_eq_empty not_bounded_UNIV by blast
have "S ∈ lmeasurable"
by (simp add: ‹bounded S› measurable_Jordan neg)
have null: "(frontier S) ∈ null_sets lebesgue"
by (metis neg negligible_iff_null_sets)
have "frontier S ∈ lmeasurable" and mS0: "measure lebesgue (frontier S) = 0"
using neg negligible_imp_measurable negligible_iff_measure by blast+
with ‹e > 0› sets_lebesgue_outer_open
obtain U where "open U"
and U: "frontier S ⊆ U" "U - frontier S ∈ lmeasurable" "emeasure lebesgue (U - frontier S) < e"
by (metis fmeasurableD)
with null have "U ∈ lmeasurable"
by (metis borel_open measurable_Diff_null_set sets_completionI_sets sets_lborel)
have "measure lebesgue (U - frontier S) = measure lebesgue U"
using mS0 by (simp add: ‹U ∈ lmeasurable› fmeasurableD measure_Diff_null_set null)
with U have mU: "measure lebesgue U < e"
by (simp add: emeasure_eq_measure2 ennreal_less_iff)
show ?thesis
proof
have "- U ≠ {}"
using ‹U ∈ lmeasurable›
by (metis boolean_algebra.compl_zero double_complement not_measurable_UNIV)
with ‹open U› ‹frontier S ⊆ U› show "setdist (frontier S) (- U) > 0"
by (auto simp: ‹bounded S› open_closed compact_frontier_bounded setdist_gt_0_compact_closed frS)
fix T
assume "T ∈ lmeasurable"
and T: "⋀t. t ∈ T ⟹ ∃y. y ∈ S ∧ dist y t < setdist (frontier S) (- U)"
then have "measure lebesgue T - measure lebesgue S ≤ measure lebesgue (T - S)"
by (simp add: ‹S ∈ lmeasurable› measure_diff_le_measure_setdiff)
also have "… ≤ measure lebesgue U"
proof -
have "T - S ⊆ U"
proof clarify
fix x
assume "x ∈ T" and "x ∉ S"
then obtain y where "y ∈ S" and y: "dist y x < setdist (frontier S) (- U)"
using T by blast
have "closed_segment x y ∩ frontier S ≠ {}"
using connected_Int_frontier ‹x ∉ S› ‹y ∈ S› by blast
then obtain z where z: "z ∈ closed_segment x y" "z ∈ frontier S"
by auto
with y have "dist z x < setdist(frontier S) (- U)"
by (auto simp: dist_commute dest!: dist_in_closed_segment)
with z have False if "x ∈ -U"
using setdist_le_dist [OF ‹z ∈ frontier S› that] by auto
then show "x ∈ U"
by blast
qed
then show ?thesis
by (simp add: ‹S ∈ lmeasurable› ‹T ∈ lmeasurable› ‹U ∈ lmeasurable› fmeasurableD measure_mono_fmeasurable sets.Diff)
qed
finally have "measure lebesgue T - measure lebesgue S ≤ measure lebesgue U" .
with mU show "measure lebesgue T < measure lebesgue S + e"
by linarith
qed
qed
proposition
fixes f :: "'a::euclidean_space ⇒ 'a"
assumes S: "S ∈ lmeasurable"
and deriv: "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x within S)"
and int: "(λx. ¦eucl.det (f' x)¦) integrable_on S"
and bounded: "⋀x. x ∈ S ⟹ ¦eucl.det (f' x)¦ ≤ B"
shows measurable_bounded_differentiable_image:
"f ` S ∈ lmeasurable"
and measure_bounded_differentiable_image:
"measure lebesgue (f ` S) ≤ B * measure lebesgue S" (is "?M")
proof -
have "f ` S ∈ lmeasurable ∧ measure lebesgue (f ` S) ≤ B * measure lebesgue S"
proof (cases "B < 0")
case True
then have "S = {}"
by (meson abs_ge_zero bounded empty_iff equalityI less_le_trans linorder_not_less subsetI)
then show ?thesis
by auto
next
case False
then have "B ≥ 0"
by arith
let ?μ = "measure lebesgue"
have f_diff: "f differentiable_on S"
using deriv by (auto simp: differentiable_on_def differentiable_def)
have eps: "f ` S ∈ lmeasurable" "?μ (f ` S) ≤ (B+e) * ?μ S" (is "?ME")
if "e > 0" for e
proof -
have eps_d: "f ` S ∈ lmeasurable" "?μ (f ` S) ≤ (B+e) * (?μ S + d)" (is "?MD")
if "d > 0" for d
proof -
obtain T where T: "open T" "S ⊆ T" and TS: "(T-S) ∈ lmeasurable" and "emeasure lebesgue (T-S) < ennreal d"
using S ‹d > 0› sets_lebesgue_outer_open by blast
then have "?μ (T-S) < d"
by (metis emeasure_eq_measure2 ennreal_leI not_less)
with S T TS have "T ∈ lmeasurable" and Tless: "?μ T < ?μ S + d"
by (auto simp: measurable_measure_Diff dest!: fmeasurable_Diff_D)
have "∃r. 0 < r ∧ r < d ∧ ball x r ⊆ T ∧ f ` (S ∩ ball x r) ∈ lmeasurable ∧
?μ (f ` (S ∩ ball x r)) ≤ (B + e) * ?μ (ball x r)"
if "x ∈ S" "d > 0" for x d
proof -
have lin: "linear (f' x)"
and lim0: "((λy. (f y - (f x + f' x (y - x))) /⇩R norm(y - x)) ⤏ 0) (at x within S)"
using deriv ‹x ∈ S› by (auto simp: has_derivative_within bounded_linear.linear field_simps)
have bo: "bounded (f' x ` ball 0 1)"
by (simp add: bounded_linear_image linear_linear lin)
have neg: "negligible (frontier (f' x ` ball 0 1))"
using deriv has_derivative_linear ‹x ∈ S›
by (auto intro!: negligible_convex_frontier [OF convex_linear_image])
let ?unit_vol = "Henstock_Kurzweil_Integration.content (ball (0 :: 'a) 1)"
have 0: "0 < e * ?unit_vol"
using ‹e > 0› by (simp add: content_ball_pos)
obtain k where "k > 0" and k:
"⋀U. ⟦U ∈ lmeasurable; ⋀y. y ∈ U ⟹ ∃z. z ∈ f' x ` ball 0 1 ∧ dist z y < k⟧
⟹ ?μ U < ?μ (f' x ` ball 0 1) + e * ?unit_vol"
using measure_semicontinuous_with_hausdist_explicit [OF bo neg 0] by blast
obtain l where "l > 0" and l: "ball x l ⊆ T"
using ‹x ∈ S› ‹open T› ‹S ⊆ T› openE by blast
obtain ζ where "0 < ζ"
and ζ: "⋀y. ⟦y ∈ S; y ≠ x; dist y x < ζ⟧
⟹ norm (f y - (f x + f' x (y - x))) / norm (y - x) < k"
using lim0 ‹k > 0› by (simp add: Lim_within) (auto simp add: field_simps)
define r where "r ≡ min (min l (ζ/2)) (min 1 (d/2))"
show ?thesis
proof (intro exI conjI)
show "r > 0" "r < d"
using ‹l > 0› ‹ζ > 0› ‹d > 0› by (auto simp: r_def)
have "r ≤ l"
by (auto simp: r_def)
with l show "ball x r ⊆ T"
by auto
have ex_lessK: "∃x' ∈ ball 0 1. dist (f' x x') ((f y - f x) /⇩R r) < k"
if "y ∈ S" and "dist x y < r" for y
proof (cases "y = x")
case True
with lin linear_0 ‹k > 0› that show ?thesis
by (rule_tac x=0 in bexI) (auto simp: linear_0)
next
case False
then show ?thesis
proof (rule_tac x="(y - x) /⇩R r" in bexI)
have "f' x ((y - x) /⇩R r) = f' x (y - x) /⇩R r"
by (simp add: lin linear_scale)
then have "dist (f' x ((y - x) /⇩R r)) ((f y - f x) /⇩R r) = norm (f' x (y - x) /⇩R r - (f y - f x) /⇩R r)"
by (simp add: dist_norm)
also have "… = norm (f' x (y - x) - (f y - f x)) / r"
using ‹r > 0› by (simp add: divide_simps scale_right_diff_distrib [symmetric])
also have "… ≤ norm (f y - (f x + f' x (y - x))) / norm (y - x)"
using that ‹r > 0› False by (simp add: field_split_simps dist_norm norm_minus_commute mult_right_mono)
also have "… < k"
using that ‹0 < ζ› by (simp add: dist_commute r_def ζ [OF ‹y ∈ S› False])
finally show "dist (f' x ((y - x) /⇩R r)) ((f y - f x) /⇩R r) < k" .
show "(y - x) /⇩R r ∈ ball 0 1"
using that ‹r > 0› by (simp add: dist_norm divide_simps norm_minus_commute)
qed
qed
let ?rfs = "(λx. x /⇩R r) ` (+) (- f x) ` f ` (S ∩ ball x r)"
have rfs_mble: "?rfs ∈ lmeasurable"
proof (rule bounded_set_imp_lmeasurable)
have "f differentiable_on S ∩ ball x r"
using f_diff by (auto simp: fmeasurableD differentiable_on_subset)
with S show "?rfs ∈ sets lebesgue"
by (auto simp: sets.Int intro!: lebesgue_sets_translation differentiable_image_in_sets_lebesgue)
let ?B = "(λ(x, y). x + y) ` (f' x ` ball 0 1 × ball 0 k)"
have "bounded ?B"
by (simp add: bounded_plus [OF bo])
moreover have "?rfs ⊆ ?B"
apply (clarsimp simp: dist_norm image_iff dest!: ex_lessK)
by (metis add.commute diff_add_cancel dist_commute dist_norm ex_lessK mem_ball_0)
ultimately show "bounded (?rfs)"
by (rule bounded_subset)
qed
then have "(λx. r *⇩R x) ` ?rfs ∈ lmeasurable"
by (simp add: measurable_linear_image)
with ‹r > 0› have "(+) (- f x) ` f ` (S ∩ ball x r) ∈ lmeasurable"
by (simp add: image_comp o_def)
then have "(+) (f x) ` (+) (- f x) ` f ` (S ∩ ball x r) ∈ lmeasurable"
using measurable_translation by blast
then show fsb: "f ` (S ∩ ball x r) ∈ lmeasurable"
by (simp add: image_comp o_def)
have "?μ (f ` (S ∩ ball x r)) = ?μ (?rfs) * r ^ DIM('a)"
using ‹r > 0› fsb
by (simp add: measure_linear_image measure_translation_subtract measurable_translation_subtract eucl.det_scale' field_simps cong: image_cong_simp)
also have "… ≤ (¦eucl.det (f' x)¦ * ?unit_vol + e * ?unit_vol) * r ^ DIM('a)"
proof -
have "?μ (?rfs) < ?μ (f' x ` ball 0 1) + e * ?unit_vol"
using rfs_mble by (force intro: k dest!: ex_lessK)
then have "?μ (?rfs) < ¦eucl.det (f' x)¦ * ?unit_vol + e * ?unit_vol"
by (simp add: lin measure_linear_image [of "f' x"])
with ‹r > 0› show ?thesis
by auto
qed
also have "… ≤ (B + e) * ?μ (ball x r)"
using bounded [OF ‹x ∈ S›] ‹r > 0›
by (simp add: algebra_simps content_ball_conv_unit_ball[of r] content_ball_pos)
finally show "?μ (f ` (S ∩ ball x r)) ≤ (B + e) * ?μ (ball x r)" .
qed
qed
then obtain r where
r0d: "⋀x d. ⟦x ∈ S; d > 0⟧ ⟹ 0 < r x d ∧ r x d < d"
and rT: "⋀x d. ⟦x ∈ S; d > 0⟧ ⟹ ball x (r x d) ⊆ T"
and r: "⋀x d. ⟦x ∈ S; d > 0⟧ ⟹
(f ` (S ∩ ball x (r x d))) ∈ lmeasurable ∧
?μ (f ` (S ∩ ball x (r x d))) ≤ (B + e) * ?μ (ball x (r x d))"
by metis
obtain C where "countable C" and Csub: "C ⊆ {(x,r x t) |x t. x ∈ S ∧ 0 < t}"
and pwC: "pairwise (λi j. disjnt (ball (fst i) (snd i)) (ball (fst j) (snd j))) C"
and negC: "negligible(S - (⋃i ∈ C. ball (fst i) (snd i)))"
apply (rule Vitali_covering_theorem_balls [of S "{(x,r x t) |x t. x ∈ S ∧ 0 < t}" fst snd])
apply auto
by (metis dist_eq_0_iff r0d)
let ?UB = "(⋃(x,s) ∈ C. ball x s)"
have eq: "f ` (S ∩ ?UB) = (⋃(x,s) ∈ C. f ` (S ∩ ball x s))"
by auto
have mle: "?μ (⋃(x,s) ∈ K. f ` (S ∩ ball x s)) ≤ (B + e) * (?μ S + d)" (is "?l ≤ ?r")
if "K ⊆ C" and "finite K" for K
proof -
have gt0: "b > 0" if "(a, b) ∈ K" for a b
using Csub that ‹K ⊆ C› r0d by auto
have inj: "inj_on (λ(x, y). ball x y) K"
by (force simp: inj_on_def ball_eq_ball_iff dest: gt0)
have disjnt: "disjoint ((λ(x, y). ball x y) ` K)"
using pwC that pairwise_image pairwise_mono by fastforce
have "?l ≤ (∑i∈K. ?μ (case i of (x, s) ⇒ f ` (S ∩ ball x s)))"
proof (rule measure_UNION_le [OF ‹finite K›], clarify)
qed (meson Int_lower1 S differentiable_on_subset f_diff fmeasurableD
lmeasurable_ball order_refl sets.Int differentiable_image_in_sets_lebesgue)
also have "… ≤ (∑(x,s) ∈ K. (B + e) * ?μ (ball x s))"
using Csub r ‹K ⊆ C› by (intro sum_mono) auto
also have "… = (B + e) * (∑(x,s) ∈ K. ?μ (ball x s))"
by (simp add: prod.case_distrib sum_distrib_left)
also have "… = (B + e) * sum ?μ ((λ(x, y). ball x y) ` K)"
using ‹B ≥ 0› ‹e > 0› by (simp add: inj sum.reindex prod.case_distrib)
also have "… = (B + e) * ?μ (⋃(x,s) ∈ K. ball x s)"
using ‹B ≥ 0› ‹e > 0› that
by (subst measure_Union') (auto simp: disjnt measure_Union')
also have "… ≤ (B + e) * ?μ T"
using ‹B ≥ 0› ‹e > 0› that
using measure_mono_fmeasurable [OF _ _ ‹T ∈ lmeasurable›] Csub rT
apply simp
by (smt (verit) SUP_least measure_nonneg measure_notin_sets mem_Collect_eq old.prod.case subset_iff)
also have "… ≤ (B + e) * (?μ S + d)"
using ‹B ≥ 0› ‹e > 0› Tless by simp
finally show ?thesis .
qed
have fSUB_mble: "(f ` (S ∩ ?UB)) ∈ lmeasurable"
unfolding eq using Csub r False ‹e > 0› that
by (auto simp: intro!: fmeasurable_UN_bound [OF ‹countable C› _ mle])
have fSUB_meas: "?μ (f ` (S ∩ ?UB)) ≤ (B + e) * (?μ S + d)" (is "?MUB")
unfolding eq using Csub r False ‹e > 0› that
by (auto simp: intro!: measure_UN_bound [OF ‹countable C› _ mle])
have neg: "negligible ((f ` (S ∩ ?UB) - f ` S) ∪ (f ` S - f ` (S ∩ ?UB)))"
proof (rule negligible_subset [OF negligible_differentiable_image_negligible [OF order_refl negC, where f=f]])
show "f differentiable_on S - (⋃i∈C. ball (fst i) (snd i))"
by (meson DiffE differentiable_on_subset subsetI f_diff)
qed force
show "f ` S ∈ lmeasurable"
by (rule lmeasurable_negligible_symdiff [OF fSUB_mble neg])
show ?MD
using fSUB_meas measure_negligible_symdiff [OF fSUB_mble neg] by simp
qed
show "f ` S ∈ lmeasurable"
using eps_d [of 1] by simp
show ?ME
proof (rule field_le_epsilon)
fix δ :: real
assume "0 < δ"
then show "?μ (f ` S) ≤ (B + e) * ?μ S + δ"
using eps_d [of "δ / (B+e)"] ‹e > 0› ‹B ≥ 0› by (auto simp: divide_simps mult_ac)
qed
qed
show ?thesis
proof (cases "?μ S = 0")
case True
with eps have "?μ (f ` S) = 0"
by (metis mult_zero_right not_le zero_less_measure_iff)
then show ?thesis
using eps [of 1] by (simp add: True)
next
case False
have "?μ (f ` S) ≤ B * ?μ S"
proof (rule field_le_epsilon)
fix e :: real
assume "e > 0"
then show "?μ (f ` S) ≤ B * ?μ S + e"
using eps [of "e / ?μ S"] False by (auto simp: algebra_simps zero_less_measure_iff)
qed
with eps [of 1] show ?thesis by auto
qed
qed
then show "f ` S ∈ lmeasurable" ?M by blast+
qed
lemma m_diff_image_weak:
fixes f :: "'a::euclidean_space ⇒ 'a"
assumes S: "S ∈ lmeasurable"
and deriv: "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x within S)"
and int: "(λx. ¦eucl.det (f' x)¦) integrable_on S"
shows "f ` S ∈ lmeasurable ∧ measure lebesgue (f ` S) ≤ integral S (λx. ¦eucl.det (f' x)¦)"
proof -
let ?μ = "measure lebesgue"
have aint_S: "(λx. ¦eucl.det (f' x)¦) absolutely_integrable_on S"
using int unfolding absolutely_integrable_on_def by auto
define m where "m ≡ integral S (λx. ¦eucl.det (f' x)¦)"
have *: "f ` S ∈ lmeasurable" "?μ (f ` S) ≤ m + e * ?μ S"
if "e > 0" for e
proof -
define Sn where "Sn ≡ λn. {x ∈ S. real n * e ≤ ¦eucl.det (f' x)¦ ∧ ¦eucl.det (f' x)¦ < real (Suc n) * e}"
have Sn_sub: "Sn n ⊆ S" for n
by (auto simp: Sn_def)
have S_eq: "S = (⋃n. Sn n)"
proof (intro equalityI subsetI)
fix x assume "x ∈ S"
define n where "n = nat ⌊¦eucl.det (f' x)¦ / e⌋"
have "real_of_int ⌊¦eucl.det (f' x)¦ / e⌋ * e ≤ ¦eucl.det (f' x)¦"
using floor_divide_lower ‹e > 0› by blast
moreover have "¦eucl.det (f' x)¦ < (real_of_int ⌊¦eucl.det (f' x)¦ / e⌋ + 1) * e"
using floor_divide_upper ‹e > 0› by blast
moreover have "⌊¦eucl.det (f' x)¦ / e⌋ ≥ 0"
using ‹e > 0› by (simp add: floor_divide_lower)
ultimately have "x ∈ Sn n"
using ‹x ∈ S› by (auto simp: Sn_def n_def of_nat_nat nat_add_distrib algebra_simps)
then show "x ∈ (⋃n. Sn n)" by auto
qed (auto simp: Sn_def)
have Sn_mble: "Sn n ∈ lmeasurable" for n
proof -
have meas: "(λx. ¦eucl.det (f' x)¦) ∈ borel_measurable (lebesgue_on S)"
using integrable_imp_measurable[OF int] .
have 1: "{x ∈ S. real n * e ≤ ¦eucl.det (f' x)¦} ∈ sets (lebesgue_on S)"
using borel_measurable_le[OF _ meas] by simp
have 2: "{x ∈ S. ¦eucl.det (f' x)¦ < real (Suc n) * e} ∈ sets (lebesgue_on S)"
using borel_measurable_less[OF meas] by simp
have "{x ∈ S. real n * e ≤ ¦eucl.det (f' x)¦ ∧ ¦eucl.det (f' x)¦ < real (Suc n) * e} ∈ sets (lebesgue_on S)"
using sets.Int[OF 1 2] by (metis Collect_conj_eq2)
then have "Sn n ∈ sets lebesgue"
using S sets_restrict_space_iff[of S lebesgue] Sn_def by blast
then show ?thesis
using fmeasurableI2[OF S Sn_sub] by blast
qed
have Sn_deriv: "(f has_derivative f' x) (at x within Sn n)" if "x ∈ Sn n" for x n
by (meson Sn_sub deriv has_derivative_subset subsetD that)
have Sn_int: "(λx. ¦eucl.det (f' x)¦) integrable_on Sn n" for n
by (metis Sn_mble Sn_sub aint_S fmeasurableD set_integrable_subset
set_lebesgue_integral_eq_integral(1))
have Sn_bdd: "¦eucl.det (f' x)¦ ≤ real (Suc n) * e" if "x ∈ Sn n" for x n
using that by (auto simp: Sn_def less_imp_le)
have fSn_mble: "f ` Sn n ∈ lmeasurable" for n
using measurable_bounded_differentiable_image [OF Sn_mble Sn_deriv Sn_int Sn_bdd] .
have fSn_meas: "?μ (f ` Sn n) ≤ real (Suc n) * e * ?μ (Sn n)" for n
using measure_bounded_differentiable_image [OF Sn_mble Sn_deriv Sn_int Sn_bdd] .
have fSn_meas2: "?μ (f ` Sn n) ≤ integral (Sn n) (λx. ¦eucl.det (f' x)¦) + e * ?μ (Sn n)" for n
proof -
have "real (Suc n) * e * ?μ (Sn n) = real n * e * ?μ (Sn n) + e * ?μ (Sn n)"
by (simp add: algebra_simps)
also have "real n * e * ?μ (Sn n) ≤ integral (Sn n) (λx. ¦eucl.det (f' x)¦)"
proof -
have "real n * e * ?μ (Sn n) = integral (Sn n) (λx. real n * e)"
using lmeasure_integral[OF Sn_mble] integral_mult_right[of "Sn n" "real n * e"]
by (metis (no_types, lifting) Henstock_Kurzweil_Integration.integral_cong lambda_one mult_commute_abs)
also have "… ≤ integral (Sn n) (λx. ¦eucl.det (f' x)¦)"
using integral_le[OF integrable_on_const[OF Sn_mble] Sn_int] Sn_def by blast
finally show ?thesis .
qed
finally show ?thesis using fSn_meas [of n] by linarith
qed
have "f ` S = (⋃n. f ` Sn n)"
using S_eq by auto
have disj: "disjoint_family_on Sn {..n}" for n
unfolding disjoint_family_on_def Sn_def
using mult_strict_right_mono[OF _ ‹e > 0›]
apply (simp add: set_eq_iff)
by (smt (verit, best) nat_le_real_less of_nat_eq_iff of_nat_mono)
have bound: "?μ (⋃ ((λk. f ` Sn k) ` {..n})) ≤ m + e * ?μ S" for n
proof -
have "?μ (⋃ ((λk. f ` Sn k) ` {..n})) ≤ (∑k≤n. ?μ (f ` Sn k))"
by (intro measure_UNION_le) (auto intro: fSn_mble fmeasurableD)
also have "… ≤ (∑k≤n. integral (Sn k) (λx. ¦eucl.det (f' x)¦) + e * ?μ (Sn k))"
by (intro sum_mono) (use fSn_meas2 in auto)
also have "… = (∑k≤n. integral (Sn k) (λx. ¦eucl.det (f' x)¦)) + e * (∑k≤n. ?μ (Sn k))"
by (simp add: sum.distrib sum_distrib_left)
also have "… ≤ m + e * ?μ S"
proof (intro add_mono mult_left_mono)
show "(∑k≤n. integral (Sn k) (λx. ¦eucl.det (f' x)¦)) ≤ m"
proof -
have pw: "pairwise (λi i'. negligible (Sn i ∩ Sn i')) {..n}"
using disj unfolding disjoint_family_on_def pairwise_def
by auto
have hi: "((λx. ¦eucl.det (f' x)¦) has_integral (∑k≤n. integral (Sn k) (λx. ¦eucl.det (f' x)¦))) (⋃k≤n. Sn k)"
by (intro has_integral_UN[OF _ _ pw]) (auto intro: integrable_integral Sn_int)
have sum_eq: "(∑k≤n. integral (Sn k) (λx. ¦eucl.det (f' x)¦)) = integral (⋃k≤n. Sn k) (λx. ¦eucl.det (f' x)¦)"
using integral_unique[OF hi] by simp
also have "… ≤ integral S (λx. ¦eucl.det (f' x)¦)"
by (metis Sn_sub UN_least abs_ge_zero hi int integrable_on_def
integral_subset_le)
finally show ?thesis by (simp add: m_def)
qed
show "(∑k≤n. ?μ (Sn k)) ≤ ?μ S"
proof -
have "(∑k≤n. ?μ (Sn k)) = ?μ (⋃k≤n. Sn k)"
by (intro measure_finite_Union[symmetric])
(auto intro: disj fmeasurableD[OF Sn_mble]
simp: emeasure_eq_measure2[OF Sn_mble])
also have "… ≤ ?μ S"
by (metis S Sn_sub UN_least measure_mono_fmeasurable measure_nonneg
measure_notin_sets)
finally show ?thesis .
qed
show "0 ≤ e" using ‹e > 0› by linarith
qed
finally show ?thesis .
qed
have fS_mble: "f ` S ∈ lmeasurable"
using fmeasurable_countable_Union[OF fSn_mble bound] ‹f ` S = (⋃n. f ` Sn n)›
by (metis (no_types))
have fS_meas: "?μ (f ` S) ≤ m + e * ?μ S"
using measure_countable_Union_le[OF fSn_mble bound] ‹f ` S = (⋃n. f ` Sn n)›
by (metis (no_types) atMost_atLeast0 image_comp)
show "f ` S ∈ lmeasurable" "?μ (f ` S) ≤ m + e * ?μ S"
using fS_mble fS_meas by auto
qed
let ?x = "m - ?μ (f ` S)"
have False if "?μ (f ` S) > integral S (λx. ¦eucl.det (f' x)¦)"
proof -
have ml: "m < ?μ (f ` S)"
using m_def that by blast
then have "?μ S ≠ 0"
using "*"(2) bgauge_existence_lemma by fastforce
with ml have 0: "0 < - (m - ?μ (f ` S))/2 / ?μ S"
using that zero_less_measure_iff by force
then show ?thesis
using * [OF 0] that by (auto simp: field_split_simps m_def split: if_split_asm)
qed
then show ?thesis
by (meson "*"(1) gt_ex linorder_not_le)
qed
theorem
fixes f :: "'a::euclidean_space ⇒ 'a"
assumes S: "S ∈ sets lebesgue"
and deriv: "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x within S)"
and int: "(λx. ¦eucl.det (f' x)¦) integrable_on S"
shows measurable_differentiable_image: "f ` S ∈ lmeasurable"
and measure_differentiable_image:
"measure lebesgue (f ` S) ≤ integral S (λx. ¦eucl.det (f' x)¦)" (is "?M")
proof -
let ?One = "∑i∈Basis. i :: 'a"
let ?I = "λn::nat. cbox (- real n *⇩R ?One) (real n *⇩R ?One) ∩ S"
let ?μ = "measure lebesgue"
have "⋀x. x ∈ S ⟹ ∃xa. ∀i∈Basis. - real xa ≤ x ∙ i ∧ x ∙ i ≤ real xa"
by (meson abs_le_iff minus_le_iff norm_bound_Basis_le real_arch_simple)
then have Seq: "S = (⋃n. ?I n)"
by (auto simp: mem_box)
have fIn: "f ` ?I n ∈ lmeasurable"
and mfIn: "?μ (f ` ?I n) ≤ integral S (λx. ¦eucl.det (f' x)¦)" (is ?MN) for n
proof -
have In_mble: "?I n ∈ lmeasurable"
by (simp add: S fmeasurable_Int_fmeasurable)
have In_deriv: "(f has_derivative f' x) (at x within ?I n)" if "x ∈ ?I n" for x
by (meson IntD2 deriv has_derivative_subset inf_le2 that)
have In_int: "(λx. ¦eucl.det (f' x)¦) integrable_on ?I n"
using int integrable_on_subcbox
by (metis (lifting) Int_commute integrable_altD(1) integrable_restrict_Int)
have res: "f ` ?I n ∈ lmeasurable ∧ ?μ (f ` ?I n) ≤ integral (?I n) (λx. ¦eucl.det (f' x)¦)"
by (rule m_diff_image_weak [OF In_mble In_deriv In_int])
then show "f ` ?I n ∈ lmeasurable" by blast
have "integral (?I n) (λx. ¦eucl.det (f' x)¦) ≤ integral S (λx. ¦eucl.det (f' x)¦)"
by (rule integral_subset_le [OF _ In_int int]) auto
with res show ?MN by linarith
qed
have "(⋃k≤n. f ` ?I k) = f ` ?I n" for n
by (fastforce simp: mem_box)
with mfIn have "?μ (⋃k≤n. f ` ?I k) ≤ integral S (λx. ¦eucl.det (f' x)¦)" for n
by simp
then have "(⋃n. f ` ?I n) ∈ lmeasurable" "?μ (⋃n. f ` ?I n) ≤ integral S (λx. ¦eucl.det (f' x)¦)"
by (rule fmeasurable_countable_Union [OF fIn] measure_countable_Union_le [OF fIn])+
then show "f ` S ∈ lmeasurable" ?M
by (metis Seq image_UN)+
qed
subsection‹Borel measurable Jacobian determinant›
proposition linear_rational_approximation:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes "linear f" "e > 0"
obtains g where "linear g" "⋀i j. i ∈ Basis ⟹ j ∈ Basis ⟹ g i ∙ j ∈ ℚ"
"onorm (f - g) < e"
proof -
define d where "d = e / (2 * DIM('a) * DIM('b))"
have "d > 0" using assms by (simp add: d_def)
have "∀i ∈ Basis. ∀j ∈ Basis. ∃q ∈ ℚ. ¦q - f i ∙ j¦ < d"
using ‹d > 0› by (force intro: rational_approximation)
then obtain q where qrat: "⋀i j. i ∈ Basis ⟹ j ∈ Basis ⟹ q i j ∈ ℚ"
and qclo: "⋀i j. i ∈ Basis ⟹ j ∈ Basis ⟹ ¦q i j - f i ∙ j¦ < d"
by (metis (mono_tags))
define G where "G = blinfun_of_matrix (λi j. q j i)"
define g where "g = blinfun_apply G"
have lin_g: "linear g"
unfolding g_def using blinfun.bounded_linear_right linear_conv_bounded_linear by blast
have g_eq: "⋀x. g x = (∑i∈Basis. (∑j∈Basis. (x ∙ j * q j i)) *⇩R i)"
unfolding g_def G_def blinfun_of_matrix_apply
by (simp add: scale_sum_left[symmetric])
have g_basis: "⋀k m. k ∈ Basis ⟹ m ∈ Basis ⟹ g k ∙ m = q k m"
proof -
fix k :: 'a and m :: 'b assume km: "k ∈ Basis" "m ∈ Basis"
have "g k ∙ m = (∑i∈Basis. (∑j∈Basis. (k ∙ j * q j i)) *⇩R i) ∙ m"
by (simp add: g_eq)
also have "… = (∑j∈Basis. k ∙ j * q j m)"
using km by (simp add: inner_sum_left_Basis)
also have "… = q k m"
proof -
have "(∑j∈Basis. k ∙ j * q j m) = (∑j∈Basis. if k = j then q j m else 0)"
by (intro sum.cong) (auto simp: km inner_Basis)
also have "… = q k m"
using km by (simp add: sum.delta')
finally show ?thesis .
qed
finally show "g k ∙ m = q k m" .
qed
show thesis
proof (rule that[OF lin_g])
show "⋀i j. i ∈ Basis ⟹ j ∈ Basis ⟹ g i ∙ j ∈ ℚ"
using g_basis qrat by simp
next
have bl_fg: "bounded_linear (λx. f x - g x)"
using assms(1) lin_g linear_conv_bounded_linear by (intro bounded_linear_sub) blast+
have "onorm (f - g) ≤ (∑i∈Basis. norm ((f - g) i))"
using onorm_componentwise[OF bl_fg] by (simp add: fun_diff_def)
also have "… ≤ (∑i∈(Basis::'a set). (∑j∈(Basis::'b set). ¦(f - g) i ∙ j¦))"
by (intro sum_mono norm_le_l1)
also have "… = (∑i∈(Basis::'a set). (∑j∈(Basis::'b set). ¦f i ∙ j - q i j¦))"
by (simp add: inner_diff_left g_basis)
also have "… < (∑i∈(Basis::'a set). (∑j∈(Basis::'b set). d))"
by (intro sum_strict_mono finite_Basis) (use qclo abs_minus_commute in force)+
also have "… = DIM('a) * DIM('b) * d"
by simp
also have "… = e / 2"
unfolding d_def by simp
also have "… < e" using assms by simp
finally show "onorm (f - g) < e" .
qed
qed
proposition orthogonal_transformation_exists:
fixes a b :: "'a::euclidean_space"
assumes "norm a = norm b"
obtains T where "orthogonal_transformation T" "T a = b"
proof -
let ?a' = "eucl_to_vec a :: real ^ 'a basis"
let ?b' = "eucl_to_vec b :: real ^ 'a basis"
have norm_eq: "norm ?a' = norm ?b'"
using assms
by (metis (mono_tags) eucl_of_vec_to_vec transfer_eucl_norm rel_funD eucl_vec_rel_altdef)
then obtain T' :: "real ^ 'a basis ⇒ real ^ 'a basis"
where T': "orthogonal_transformation T'" "T' ?a' = ?b'"
using orthogonal_transformation_exists by metis
define T where "T = eucl_of_vec ∘ T' ∘ eucl_to_vec"
have inner_eq: "T v ∙ T w = v ∙ w" for v w
proof -
have "T v ∙ T w = T' (eucl_to_vec v) ∙ T' (eucl_to_vec w)"
unfolding T_def comp_def
by (metis (mono_tags) transfer_eucl_vec_inner rel_funD eucl_vec_rel_def)
also have "… = eucl_to_vec v ∙ eucl_to_vec w"
using T'(1) by (simp add: orthogonal_transformation_def)
also have "… = v ∙ w"
by (metis (mono_tags) eucl_vec_rel_altdef rel_funD transfer_eucl_vec_inner)
finally show ?thesis .
qed
have "linear T"
proof (rule linearI)
fix x y :: 'a
show "T (x + y) = T x + T y"
by (smt (verit) inner_eq vector_eq inner_commute inner_right_distrib)
next
fix c x
show "T (c *⇩R x) = c *⇩R T x"
by (simp add: inner_eq vector_eq)
qed
then have "orthogonal_transformation T"
using inner_eq by (simp add: orthogonal_transformation_def)
moreover have "T a = b"
unfolding T_def comp_def using T'(2) by simp
ultimately show thesis
using that by blast
qed
lemma lemma_partial_derivatives0:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes "linear f" and lim0: "((λx. f x /⇩R norm x) ⤏ 0) (at 0 within S)"
and lb: "⋀v. v ≠ 0 ⟹ (∃k>0. ∀e>0. ∃x. x ∈ S - {0} ∧ norm x < e ∧ k * norm x ≤ ¦v ∙ x¦)"
shows "f x = 0"
proof -
interpret linear f by fact
have "dim {x. f x = 0} ≤ DIM('a)"
by (rule dim_subset_UNIV)
moreover have False if less: "dim {x. f x = 0} < DIM('a)"
proof -
obtain d where "d ≠ 0" and d: "⋀y. f y = 0 ⟹ d ∙ y = 0"
using orthogonal_to_subspace_exists [OF less] orthogonal_def
by (metis (mono_tags, lifting) mem_Collect_eq span_base)
then obtain k where "k > 0"
and k: "⋀e. e > 0 ⟹ ∃y. y ∈ S - {0} ∧ norm y < e ∧ k * norm y ≤ ¦d ∙ y¦"
using lb by blast
have "∃h. ∀n. ((h n ∈ S ∧ h n ≠ 0 ∧ k * norm (h n) ≤ ¦d ∙ h n¦) ∧ norm (h n) < 1 / real (Suc n)) ∧
norm (h (Suc n)) < norm (h n)"
proof (rule dependent_nat_choice)
show "∃y. (y ∈ S ∧ y ≠ 0 ∧ k * norm y ≤ ¦d ∙ y¦) ∧ norm y < 1 / real (Suc 0)"
by simp (metis DiffE insertCI k not_less not_one_le_zero)
qed (use k [of "min (norm x) (1/(Suc n + 1))" for x n] in auto)
then obtain α where α: "⋀n. α n ∈ S - {0}" and kd: "⋀n. k * norm(α n) ≤ ¦d ∙ α n¦"
and norm_lt: "⋀n. norm(α n) < 1/(Suc n)"
by force
let ?β = "λn. α n /⇩R norm (α n)"
have com: "⋀g. (∀n. g n ∈ sphere (0::'a) 1)
⟹ ∃l ∈ sphere 0 1. ∃ρ::nat⇒nat. strict_mono ρ ∧ (g ∘ ρ) ⇢ l"
using compact_sphere compact_def by metis
moreover have "∀n. ?β n ∈ sphere 0 1"
using α by auto
ultimately obtain l::'a and ρ::"nat⇒nat"
where l: "l ∈ sphere 0 1" and "strict_mono ρ" and to_l: "(?β ∘ ρ) ⇢ l"
by meson
moreover have "continuous (at l) (λx. (¦d ∙ x¦ - k))"
by (intro continuous_intros)
ultimately have lim_dl: "((λx. (¦d ∙ x¦ - k)) ∘ (?β ∘ ρ)) ⇢ (¦d ∙ l¦ - k)"
by (meson continuous_imp_tendsto)
have "∀⇩F i in sequentially. 0 ≤ ((λx. ¦d ∙ x¦ - k) ∘ ((λn. α n /⇩R norm (α n)) ∘ ρ)) i"
using α kd by (auto simp: field_split_simps)
then have "k ≤ ¦d ∙ l¦"
using tendsto_lowerbound [OF lim_dl, of 0] by auto
moreover have "d ∙ l = 0"
proof (rule d)
show "f l = 0"
proof (rule LIMSEQ_unique [of "f ∘ ?β ∘ ρ"])
have "isCont f l"
using ‹linear f› linear_continuous_at linear_conv_bounded_linear by blast
then show "(f ∘ (λn. α n /⇩R norm (α n)) ∘ ρ) ⇢ f l"
unfolding comp_assoc
using to_l continuous_imp_tendsto by blast
have "α ⇢ 0"
using norm_lt LIMSEQ_norm_0 by metis
with ‹strict_mono ρ› have "(α ∘ ρ) ⇢ 0"
by (metis LIMSEQ_subseq_LIMSEQ)
with lim0 α have "((λx. f x /⇩R norm x) ∘ (α ∘ ρ)) ⇢ 0"
by (force simp: tendsto_at_iff_sequentially)
then show "(f ∘ (λn. α n /⇩R norm (α n)) ∘ ρ) ⇢ 0"
by (simp add: o_def scale)
qed
qed
ultimately show False
using ‹k > 0› by auto
qed
ultimately have dim: "dim {x. f x = 0} = DIM('a)"
by force
then show ?thesis
by (metis (mono_tags, lifting) dim_eq_full UNIV_I eq_0_on_span mem_Collect_eq span_raw_def)
qed
lemma lemma_partial_derivatives:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes "linear f" and lim: "((λx. f (x - a) /⇩R norm (x - a)) ⤏ 0) (at a within S)"
and lb: "⋀v. v ≠ 0 ⟹ (∃k>0. ∀e>0. ∃x ∈ S - {a}. norm(a - x) < e ∧ k * norm(a - x) ≤ ¦v ∙ (x - a)¦)"
shows "f x = 0"
proof -
have "((λx. f x /⇩R norm x) ⤏ 0) (at 0 within (λx. x-a) ` S)"
using lim by (simp add: Lim_within dist_norm)
then show ?thesis
proof (rule lemma_partial_derivatives0 [OF ‹linear f›])
fix v :: "'a"
assume v: "v ≠ 0"
show "∃k>0. ∀e>0. ∃x. x ∈ (λx. x - a) ` S - {0} ∧ norm x < e ∧ k * norm x ≤ ¦v ∙ x¦"
using lb [OF v] by (force simp: norm_minus_commute)
qed
qed
definition "All_Rat ≡ λA. (∀i∈Basis. ∀j∈Basis. A i ∙ j ∈ ℚ)"
lemma countable_rational_linear_maps:
"countable {A. linear A ∧ All_Rat A}"
proof -
have inj: "inj_on (λA. restrict A Basis)
{A :: 'a ⇒ 'b. linear A ∧ All_Rat A}"
using linear_eq_stdbasis
by (smt (verit, ccfv_SIG) inj_onI mem_Collect_eq restrict_apply')
have "countable {g :: 'a ⇒ 'b. (∀i. i ∉ Basis ⟶ g i = undefined) ∧ All_Rat g}"
proof (rule countable_subset)
let ?V = "{w :: 'b. ∀j∈Basis. w ∙ j ∈ ℚ}"
have cV: "countable ?V"
proof -
have inj: "inj_on (λw. restrict (λj. w ∙ j) Basis) ?V"
by (metis (mono_tags, lifting) euclidean_eq_iff inj_on_def restrict_apply')
moreover have "(λw. restrict (λj. w ∙ j) Basis) ` ?V ⊆ PiE Basis (λ_. ℚ)"
by (auto simp: PiE_def Pi_def extensional_def restrict_def)
moreover have "countable (PiE Basis (λ_. ℚ))"
by (intro countable_PiE finite_Basis) (auto simp: countable_rat)
ultimately show ?thesis
by (metis (mono_tags, lifting) countable_image_inj_on countable_subset)
qed
show "countable (Basis →⇩E ?V)"
by (intro countable_PiE finite_Basis) (auto simp: cV)
qed (auto simp: All_Rat_def)
moreover have "(λA:: 'a ⇒ 'b. restrict A Basis) `
{A. linear A ∧ All_Rat A} ⊆ {g. (∀i. i ∉ Basis ⟶ g i = undefined) ∧ All_Rat g}"
by (auto simp: All_Rat_def restrict_def)
ultimately show ?thesis
by (metis (no_types, lifting) inj countable_image_inj_on countable_subset)
qed
lemma negligible_thin_direction:
fixes S :: "'a::euclidean_space set"
shows "negligible {x ∈ S. ∃v. v ≠ 0 ∧
(∀ξ>0. ∃e>0. ∀y ∈ S-{x}. norm (x - y) < e ⟶ ¦v ∙ (y - x)¦ < ξ * norm (x - y))}"
(is "negligible ?N")
proof -
define Θ where "Θ ≡ λx v. ∀ξ>0. ∃e>0. ∀y ∈ S-{x}. norm (x - y) < e ⟶ ¦v ∙ (y - x)¦ < ξ * norm (x - y)"
have "?N = {x ∈ S. ∃v≠0. Θ x v}"
by (auto simp: Θ_def)
also have "negligible …"
unfolding negligible_eq_zero_density
proof clarsimp
fix x v and r e :: "real"
assume "x ∈ S" "v ≠ 0" "r > 0" "e > 0"
and Theta: "Θ x v"
moreover have "(norm v * e / 2) / DIM('a) ^ DIM('a) > 0"
using ‹v ≠ 0› ‹e > 0›
by (auto simp add: zero_less_divide_iff zero_less_mult_iff)
ultimately obtain d where "d > 0"
and dless: "⋀y. ⟦y ∈ S - {x}; norm (x - y) < d⟧ ⟹
¦v ∙ (y - x)¦ < ((norm v * e / 2) / DIM('a) ^ DIM('a)) * norm (x - y)"
by (metis Θ_def)
let ?W = "ball x (min d r) ∩ {y. ¦v ∙ (y - x)¦ < (norm v * e/2 * min d r) / DIM('a) ^ DIM('a)}"
have "open {x. ¦v ∙ (x - a)¦ < b}" for a b
by (intro open_Collect_less continuous_intros)
show "∃d>0. d ≤ r ∧
(∃U. {x' ∈ S. ∃v≠0. Θ x' v} ∩ ball x d ⊆ U ∧
U ∈ lmeasurable ∧ measure lebesgue U < e * content (ball x d))"
proof (intro exI conjI)
show "0 < min d r" "min d r ≤ r"
using ‹r > 0› ‹d > 0› by auto
show "{x' ∈ S. ∃v. v ≠ 0 ∧ Θ x' v} ∩ ball x (min d r) ⊆ ?W"
proof (clarsimp simp: dist_norm norm_minus_commute)
fix y w
assume "y ∈ S" "w ≠ 0"
and d: "norm (y - x) < d" and r: "norm (y - x) < r"
show "¦v ∙ (y - x)¦ < norm v * e * min d r / (2 * real DIM('a) ^ DIM('a))"
proof (cases "y = x")
case True
with ‹r > 0› ‹d > 0› ‹e > 0› ‹v ≠ 0› show ?thesis
by (auto simp: divide_simps)
next
case False
have "¦v ∙ (y - x)¦ < norm v * e / 2 / real (DIM('a) ^ DIM('a)) * norm (x - y)"
by (metis Diff_iff False ‹y ∈ S› d dless empty_iff insert_iff norm_minus_commute)
also have "… ≤ norm v * e * min d r / (2 * real DIM('a) ^ DIM('a))"
using d r ‹e > 0› by (simp add: divide_simps norm_minus_commute mult_left_mono)
finally show ?thesis .
qed
qed
show "?W ∈ lmeasurable"
by (simp add: fmeasurable_Int_fmeasurable borel_open)
obtain e_k :: 'a where ek: "e_k ∈ Basis"
using nonempty_Basis by blast
obtain T where T: "orthogonal_transformation T" and v: "v = T (norm v *⇩R e_k)"
using orthogonal_transformation_exists[of "norm v *⇩R e_k" v] that
by (metis abs_norm_cancel ek mult.right_neutral norm_Basis norm_scaleR)
define b where "b ≡ norm v"
have "b > 0"
using ‹v ≠ 0› by (auto simp: b_def)
have eqb: "inv T v = b *⇩R e_k"
using T v b_def orthogonal_transformation_bij bij_betw_inv_into_left
by (metis UNIV_I orthogonal_transformation_inj inv_f_f)
have "inj T" "bij T" and invT: "orthogonal_transformation (inv T)"
using T orthogonal_transformation_inj orthogonal_transformation_bij orthogonal_transformation_inv
by auto
let ?v = "∑i∈Basis. (min d r / DIM('a)) *⇩R i"
let ?v' = "∑i∈Basis. (if i = e_k then (e/2 * min d r) / DIM('a) ^ DIM('a) else min d r) *⇩R i"
let ?x' = "inv T x"
let ?W' = "(ball ?x' (min d r) ∩ {y. ¦(y - ?x') ∙ e_k¦ < e * min d r / (2 * DIM('a) ^ DIM('a))})"
have abs: "x - e ≤ y ∧ y ≤ x + e ⟷ abs(y - x) ≤ e" for x y e::real
by auto
have "?W = T ` ?W'"
proof -
have 1: "T ` (ball (inv T x) (min d r)) = ball x (min d r)"
by (simp add: T image_orthogonal_transformation_ball orthogonal_transformation_surj surj_f_inv_f)
have 2: "{y. ¦v ∙ (y - x)¦ < b * e * min d r / (2 * real DIM('a) ^ DIM('a))} =
T ` {y. ¦(y - ?x') ∙ e_k¦ < e * min d r / (2 * real DIM('a) ^ DIM('a))}"
proof -
have *: "¦T (b *⇩R e_k) ∙ (y - x)¦ = b * ¦(inv T y - ?x') ∙ e_k¦" for y
proof -
have "¦T (b *⇩R e_k) ∙ (y - x)¦ = ¦(b *⇩R e_k) ∙ inv T (y - x)¦"
using T invT by (metis orthogonal_transformation_def eqb v b_def)
also have "… = b * ¦e_k ∙ inv T (y - x)¦"
using ‹b > 0› by (simp add: abs_mult)
also have "… = b * ¦(inv T y - ?x') ∙ e_k¦"
using orthogonal_transformation_linear [OF invT]
by (simp add: linear_diff inner_commute)
finally show ?thesis
by simp
qed
show ?thesis
using v b_def [symmetric]
using ‹b > 0› by (simp add: * bij_image_Collect_eq [OF ‹bij T›] mult_less_cancel_left_pos times_divide_eq_right [symmetric] del: times_divide_eq_right)
qed
show ?thesis
using 1 2 b_def by (simp add: image_Int [OF ‹inj T›])
qed
moreover have "?W' ∈ lmeasurable"
by (auto intro: fmeasurable_Int_fmeasurable)
moreover have "¦eucl.det T¦ = 1"
proof -
note [transfer_rule] = transfer_measure_bij_rules transfer_eucl_bij_rules
have "orthogonal_transformation f ⟹ ¦eucl.det f¦ = 1" for f :: "'a ⇒ 'a"
using orthogonal_transformation_det[unfolded orthogonal_transformation_def,
where ?'n = "'a basis", untransferred]
by (simp add: orthogonal_transformation_def)
then show ?thesis using T by blast
qed
ultimately have "measure lebesgue ?W = measure lebesgue ?W'"
using measure_orthogonal_image [OF T] by simp
also have "… ≤ measure lebesgue (cbox (?x' - ?v') (?x' + ?v'))"
proof (rule measure_mono_fmeasurable)
show "?W' ⊆ cbox (?x' - ?v') (?x' + ?v')"
proof (intro subsetI)
fix y assume "y ∈ ?W'"
then have ball: "dist ?x' y < min d r"
and ek_bound: "¦(y - ?x') ∙ e_k¦ < e * min d r / (2 * real DIM('a) ^ DIM('a))"
by auto
then have dist: "norm (y - ?x') < min d r"
using ball by (simp add: dist_commute dist_norm)
then have "⋀i. i ∈ Basis ⟹ y ∙ i ≤ min d r + inv T x ∙ i"
by (smt (verit, ccfv_SIG) Basis_le_norm dist inner_diff_left)
then show "y ∈ cbox (?x' - ?v') (?x' + ?v')"
using ek_bound
apply (auto simp add: mem_box algebra_simps)
apply (metis abs dist inner_diff_left norm_bound_Basis_le norm_minus_commute
order_less_imp_le)
done
qed
qed auto
also have "… ≤ e/2 * measure lebesgue (cbox (?x' - ?v) (?x' + ?v))"
proof -
have "cbox (?x' - ?v) (?x' + ?v) ≠ {}"
using ‹r > 0› ‹d > 0› by (auto simp: box_ne_empty algebra_simps divide_less_0_iff)
with ‹r > 0› ‹d > 0› ‹e > 0› ek show ?thesis
apply (simp add: content_cbox_if mem_box prod_nonneg algebra_simps)
apply (simp add: abs if_distrib prod.delta_remove field_simps power_diff split: if_split_asm)
done
qed
also have "… ≤ e/2 * measure lebesgue (cball ?x' (min d r))"
proof (rule mult_left_mono [OF measure_mono_fmeasurable])
have *: "norm (?x' - y) ≤ min d r"
if y: "⋀i. i ∈ Basis ⟹ ¦(?x' - y) ∙ i¦ ≤ min d r / real DIM('a)" for y
proof -
have "norm (?x' - y) ≤ (∑i∈Basis. ¦(?x' - y) ∙ i¦)"
by (rule norm_le_l1)
also have "… ≤ real DIM('a) * (min d r / real DIM('a))"
by (rule sum_bounded_above) (use y in auto)
finally show ?thesis
by simp
qed
show "cbox (?x' - ?v) (?x' + ?v) ⊆ cball ?x' (min d r)"
apply (clarsimp simp only: mem_box dist_norm mem_cball intro!: *)
apply (simp add: abs_diff_le_iff algebra_simps)
done
qed (use ‹e > 0› in auto)
also have "… < e * content (cball ?x' (min d r))"
using ‹r > 0› ‹d > 0› ‹e > 0› by (auto intro: content_cball_pos)
also have "… = e * content (ball x (min d r))"
using ‹r > 0› ‹d > 0› content_ball_conv_unit_ball[of "min d r" "inv T x"]
content_ball_conv_unit_ball[of "min d r" x]
by (simp add: content_cball_conv_ball)
finally show "measure lebesgue ?W < e * content (ball x (min d r))" .
qed
qed
finally show ?thesis .
qed
lemma lebesgue_derivative_bound_set:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes S: "S ∈ sets lebesgue" and "linear A" and contf: "continuous_on S f"
shows "S ∩ (⋂y∈S. {x ∈ S. norm(y - x) < d ⟶ norm(f y - f x - A(y - x)) ≤ e * norm(y - x)}) ∈ sets lebesgue"
proof (rule lebesgue_closedin [OF _ S])
have *: "⟦U ≠ {} ⟹ closedin (top_of_set S) (S ∩ ⋂ U)⟧
⟹ closedin (top_of_set S) (S ∩ ⋂ U)" for U
by fastforce
show "closedin (top_of_set S) (S ∩ (⋂y∈S. {x ∈ S. norm(y - x) < d ⟶ norm(f y - f x - A(y - x)) ≤ e * norm(y - x)}))"
proof (rule *)
let ?C = "λy. {x ∈ S. norm(y - x) < d ⟶ norm(f y - f x - A(y - x)) ≤ e * norm(y - x)}"
assume ne: "(λy. ?C y) ` S ≠ {}"
then have Sne: "S ≠ {}" by blast
have sub: "(⋂y∈S. ?C y) ⊆ S"
using Sne by (auto intro: INF_lower2)
have eq: "S ∩ (⋂y∈S. ?C y) = (⋂y∈S. ?C y)"
using sub by (rule Int_absorb1)
show "closedin (top_of_set S) (S ∩ (⋂y∈S. ?C y))"
unfolding eq
proof (rule closedin_INT [OF Sne])
fix y assume "y ∈ S"
have "closedin (top_of_set S)
({x ∈ S. d ≤ norm (y - x)} ∪ {x ∈ S. norm (f y - f x - A (y - x)) ≤ e * norm (y - x)})"
proof (intro closedin_Un)
show "closedin (top_of_set S) {x ∈ S. d ≤ norm (y - x)}"
proof -
have "continuous_on S (λx. norm (y - x))"
by (intro continuous_on_norm continuous_on_diff continuous_on_const continuous_on_id)
then have "closedin (top_of_set S) (S ∩ (λx. norm (y - x)) -` {d..})"
by (intro continuous_closedin_preimage closed_atLeast)
moreover have "{x ∈ S. d ≤ norm (y - x)} = S ∩ (λx. norm (y - x)) -` {d..}"
by auto
ultimately show ?thesis by simp
qed
show "closedin (top_of_set S) {x ∈ S. norm (f y - f x - A (y - x)) ≤ e * norm (y - x)}"
proof -
have contAcomp: "continuous_on S (λx. A (y - x))"
by (simp add: ‹linear A› continuous_on_op_minus linear_continuous_on_compose)
have "continuous_on S (λx. norm (f y - f x - A (y - x)) - e * norm (y - x))"
by (intro continuous_intros contf contAcomp)
then have "closedin (top_of_set S) (S ∩ (λx. norm (f y - f x - A (y - x)) - e * norm (y - x)) -` {..0})"
by (intro continuous_closedin_preimage closed_atMost)
moreover have "{x ∈ S. norm (f y - f x - A (y - x)) ≤ e * norm (y - x)}
= S ∩ (λx. norm (f y - f x - A (y - x)) - e * norm (y - x)) -` {..0}"
by auto
ultimately show ?thesis by simp
qed
qed
moreover have "?C y
= {x ∈ S. d ≤ norm (y - x)} ∪ {x ∈ S. norm (f y - f x - A (y - x)) ≤ e * norm (y - x)}"
by (auto simp: not_less)
ultimately show "closedin (top_of_set S) (?C y)"
by simp
qed
qed
qed
lemma lebesgue_rational_linear_approx_set:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes S: "S ∈ sets lebesgue"
and contf: "continuous_on S f"
shows "{x ∈ S. ∀e>0. ∃d>0. ∃A. linear A ∧ A u ∙ v < b ∧ All_Rat A ∧
(∀y ∈ S. norm(y - x) < d ⟶ norm(f y - f x - A (y - x)) ≤ e * norm(y - x))}
∈ sets lebesgue"
proof -
let ?C = "λe A d y. {x ∈ S. norm(y - x) < d ⟶ norm(f y - f x - A (y - x)) ≤ e * norm(y - x)}"
let ?L = "{A. linear A ∧ A u ∙ v < b ∧ All_Rat A}"
let ?E = "{e ∈ ℚ. (0::real) < e}"
let ?D = "{d ∈ ℚ. (0::real) < d}"
let ?T = "{x ∈ S. ∀e>0. ∃d>0. ∃A. linear A ∧ A u ∙ v < b ∧ All_Rat A ∧
(∀y ∈ S. x ∈ ?C e A d y)}"
let ?U = "S ∩ (⋂e ∈ ?E. ⋃A ∈ ?L. ⋃d ∈ ?D. S ∩ (⋂y ∈ S. ?C e A d y))"
have "?T = ?U"
proof (intro set_eqI iffI ; clarsimp)
fix s :: 'a and q :: real and r :: real
assume "s ∈ S"
and "∀e>0. ∃d>0. ∃A. linear A ∧ A u ∙ v < b ∧ All_Rat A ∧ (∀y∈S. norm (y - s) < d ⟶ norm (f y - f s - A (y - s)) ≤ e * norm (y - s))"
and q: "q ∈ ℚ" "0 < q" and r: "r ∈ ℚ" "0 < r"
show "∃xa. linear xa ∧ xa u ∙ v < b ∧ All_Rat xa ∧ (∃xc. xc ∈ ℚ ∧ 0 < xc ∧ (∀xd∈S. norm (xd - s) < xc ⟶ norm (f xd - f s - xa (xd - s)) ≤ r * norm (xd - s)))"
proof -
obtain d A where linA: "linear A" and dpos: "d > 0" and Ab: "A u ∙ v < b" and AQ: "All_Rat A"
and norm: "∀y∈S. norm (y - s) < d ⟶ norm (f y - f s - A (y - s)) ≤ r * norm (y - s)"
using ‹∀e>0. _› ‹0 < r› by blast
obtain xc where xcQ: "xc ∈ ℚ" and xc_close: "¦xc - d/2¦ < d/2"
using rational_approximation [of "d/2"] dpos by auto
have "0 < xc" "xc < d"
using xc_close dpos by linarith+
then show ?thesis
using linA Ab AQ norm xcQ by (meson order.strict_trans)
qed
next
fix x :: 'a
and e :: real
assume "x ∈ S"
and xif: "x ∈ (if ∀x. (x::real) ∈ ℚ ⟶ ¬ 0 < x then UNIV else S ∩ (⋂x∈?E. ⋃xa∈?L. ⋃xb∈?D. ⋂y∈S. ?C x xa xb y))"
and "0 < e"
show "∃d>0. ∃A. linear A ∧ A u ∙ v < b ∧ All_Rat A ∧ (∀y∈S. norm (y - x) < d ⟶ norm (f y - f x - A (y - x)) ≤ e * norm (y - x))"
proof -
have nif: "¬ (∀x::real. x ∈ ℚ ⟶ ¬ 0 < x)"
using Rats_1 zero_less_one by blast
obtain q::real where qQ: "q ∈ ℚ" and q0: "0 < q" and qe: "q < e"
using ‹0 < e› Rats_dense_in_real by blast
from xif nif
have xmem: "x ∈ S ∩ (⋂x∈?E. ⋃xa∈?L. ⋃xb∈?D. ⋂y∈S. ?C x xa xb y)"
by (auto split: if_splits)
then have "x ∈ (⋃xa∈?L. ⋃xb∈?D. ⋂y∈S. ?C q xa xb y)"
using qQ q0 by blast
then obtain A d where linA: "linear A" and Ab: "A u ∙ v < b" and AQ: "All_Rat A"
and dQ: "d ∈ ℚ" and d0: "0 < d"
and norm: "∀y∈S. x ∈ S ∧ (norm (y - x) < d ⟶ norm (f y - f x - A (y - x)) ≤ q * norm (y - x))"
by auto
moreover have "q * norm (y - x) ≤ e * norm (y - x)" for y
using qe by (simp add: mult_right_mono)
ultimately show ?thesis
by (meson le_less order.trans)
qed
qed
moreover have "?U ∈ sets lebesgue"
proof -
have coE: "countable ?E"
using countable_Collect countable_rat by blast
have ne: "?E ≠ {}"
using zero_less_one Rats_1 by blast
have coA: "countable ?L"
by (rule countable_subset [OF _ countable_rational_linear_maps]) blast
have sets: "S ∩ (⋂y∈S. ?C e A d y) ∈ sets lebesgue" if "linear A" for e A d
using lebesgue_derivative_bound_set [OF S that contf] .
have coD: "countable ?D"
using countable_Collect countable_rat by blast
show ?thesis
proof (cases "S = {}")
case True
then show ?thesis by auto
next
case Sne: False
show ?thesis
unfolding INT_extend_simps if_not_P [OF ne] if_not_P [OF Sne]
apply (intro sets.Int sets.countable_INT' [OF coE ne] image_subsetI
sets.countable_UN' [OF coA] sets.countable_UN' [OF coD])
subgoal by (rule S)
subgoal for e A d
using sets [of A d e] Sne by auto
done
qed
qed
ultimately have "?T ∈ sets lebesgue"
by simp
moreover have "?T = {x ∈ S. ∀e>0. ∃d>0. ∃A. linear A ∧ A u ∙ v < b ∧ All_Rat A ∧
(∀y ∈ S. norm(y - x) < d ⟶ norm(f y - f x - A (y - x)) ≤ e * norm(y - x))}"
by auto
ultimately show ?thesis
by simp
qed
lemma rational_linear_approx_witness:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
and f' :: "'a ⇒ 'b"
assumes deriv: "(f has_derivative f') (at x within S)"
and b: "f' u ∙ v ≤ b"
and "e > 0"
and [simp]: "u ≠ 0" "v ≠ 0" "norm u = 1" "norm v = 1"
shows "∃d>0. ∃A. linear A ∧ A u ∙ v < b ∧ All_Rat A ∧
(∀y∈S. norm (y - x) < d ⟶ norm (f y - f x - A (y - x)) ≤ e * norm (y - x))"
proof -
have linf': "linear f'"
using deriv has_derivative_linear by blast
obtain d where "d>0"
and d: "⋀y. y∈S ⟹ 0 < dist y x ∧ dist y x < d ⟶ norm (f y - f x - f' (y - x)) / (norm (y - x))
< e/2"
using deriv ‹e > 0›
by (simp add: Deriv.has_derivative_at_within Lim_within)
(auto simp add: field_simps dest: spec [of _ "e/2"])
define P where "P ≡ λw. ((e / (4 * (u ∙ u) * (v ∙ v))) * (w ∙ u)) *⇩R v"
have linP: "linear P"
unfolding P_def by (intro linearI) (auto simp: inner_left_distrib scaleR_add_left scaleR_left_distrib algebra_simps add_divide_distrib)
have Puv: "P u ∙ v = e / 4"
using P_def by force
have onormP: "onorm P ≤ e / 4"
proof (rule onorm_bound)
fix w :: 'a
have "norm (P w) = ¦e / (4 * (u ∙ u) * (v ∙ v))¦ * ¦w ∙ u¦ * norm v"
unfolding P_def by (simp add: norm_scaleR abs_mult)
also have "… = e / 4 * ¦w ∙ u¦"
using ‹e > 0› by (simp add: dot_square_norm power2_eq_square)
also have "… ≤ e / 4 * norm w"
using ‹e > 0› Cauchy_Schwarz_ineq2 [of w u]
by (intro mult_left_mono) auto
finally show "norm (P w) ≤ e / 4 * norm w" .
next
show "0 ≤ e / 4" using ‹e > 0› by simp
qed
let ?A = "f' - P"
have blP: "bounded_linear P"
using linP linear_conv_bounded_linear by blast
have linA': "linear ?A"
by (simp add: fun_diff_def linP linear_compose_sub linf')
obtain B where linB: "linear B"
and BRats: "⋀i j. i ∈ Basis ⟹ j ∈ Basis ⟹ B i ∙ j ∈ ℚ"
and Bo_e6: "onorm (?A - B) < e/6"
by (metis ‹0 < e› divide_pos_pos linA' linear_rational_approximation zero_less_numeral)
show ?thesis
proof (intro exI conjI ballI impI)
show "d>0"
by (rule ‹d>0›)
show "linear B"
by (rule linB)
have bl: "bounded_linear (?A - B)"
using linA' linB
by (metis (no_types, lifting) ext linear_compose_sub linear_linear minus_apply)
show "B u ∙ v < b"
proof -
have "¦(?A - B) u ∙ v¦ ≤ onorm (?A - B) * norm u * norm v"
by (meson Cauchy_Schwarz_ineq2 bl mult_right_mono norm_imp_pos_and_ge onorm order_trans)
also have "… < e/6 * norm u * norm v"
using Bo_e6 by simp
finally have *: "¦(?A - B) u ∙ v¦ < e/6 * norm u * norm v" .
have "B u ∙ v ≤ ?A u ∙ v + e/6 * norm u * norm v"
by (smt (verit) "*" fun_diff_def inner_diff_left)
also have "?A u ∙ v = f' u ∙ v - e/4"
by (simp add: inner_diff_left Puv)
finally have "B u ∙ v ≤ f' u ∙ v - e / 12"
by simp
then show "B u ∙ v < b"
using b ‹e > 0› by linarith
qed
show "All_Rat B"
using BRats by (auto simp: All_Rat_def)
show "norm (f y - f x - B (y - x)) ≤ e * norm (y - x)"
if "y ∈ S" and y: "norm (y - x) < d" for y
proof (cases "y = x")
case True then show ?thesis
using linB linear_0 by simp
next
case False
have *: "norm(d' - d) ≤ e/2 ⟹ norm(y - (x + d')) < e/2 ⟹ norm(y - x - d) ≤ e" for d d' e and x y::"'b"
using norm_triangle_le [of "d' - d" "y - (x + d')"] by simp
show ?thesis
proof (rule *)
have split246: "⟦norm y ≤ e / 6; norm(x - y) ≤ e / 4⟧ ⟹ norm x ≤ e/2" if "e > 0" for e and x y :: "'b"
using norm_triangle_le [of y "x-y" "e/2"] ‹e > 0› by simp
have "norm (f' (y - x) - B (y - x)) = norm ((f' - B) (y - x))"
by (simp add: linear_diff [OF linf'] linear_diff [OF linB])
also have "… ≤ (e * norm (y - x)) / 2"
proof (rule split246)
have blAB: "bounded_linear (λw. ?A w - B w)"
using bounded_linear_sub linA' linB linear_linear by blast
have "norm ((?A - B) (y - x)) / norm (y - x) < e / 6"
using bl le_onorm Bo_e6 le_less_trans by blast
then show onAB: "norm ((?A - B) (y - x)) ≤ e * norm (y - x) / 6"
by (simp add: field_split_simps False)
have "(f' - B) (y - x) - (?A - B) (y - x) = P (y - x)"
by (simp add: algebra_simps)
then have "norm ((f' - B) (y - x) - (?A - B) (y - x)) ≤ onorm P * norm (y - x)"
using linP linear_conv_bounded_linear onorm by auto
also have "… ≤ (e/4) * norm (y - x)"
using onormP by (intro mult_right_mono) auto
finally show "norm ((f' - B) (y - x) - (?A - B) (y - x)) ≤ e * norm (y - x) / 4"
by simp
show "0 < e * norm (y - x)"
by (simp add: False ‹e > 0›)
qed
finally show "norm (f' (y - x) - B (y - x)) ≤ (e * norm (y - x)) / 2" .
show "norm (f y - (f x + f' (y - x))) < (e * norm (y - x)) / 2"
using False d [OF ‹y ∈ S›] y by (simp add: dist_norm field_simps)
qed
qed
qed
qed
lemma lebesgue_halfspace_derivative_le:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes S: "S ∈ sets lebesgue"
and f: "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x within S)"
and [simp]: "u ≠ 0" "v ≠ 0" "norm u = 1" "norm v = 1"
shows "{x ∈ S. f' x u ∙ v ≤ b} ∈ sets lebesgue"
proof -
have lin: "linear (f' x)" if "x ∈ S" for x
using f[OF that] has_derivative_linear by blast
have contf: "continuous_on S f"
using continuous_on_eq_continuous_within f has_derivative_continuous by blast
show ?thesis
proof (rule sets_negligible_symdiff)
define C where "C ≡ λe A d x y. norm(y - x) < d ⟶ norm(f y - f x - A (y - x)) ≤ e * norm(y - x)"
let ?T = "{x ∈ S. ∀e>0. ∃d>0. ∃A. linear A ∧ A u ∙ v < b ∧ All_Rat A ∧
(∀y ∈ S. C e A d x y)}"
show "?T ∈ sets lebesgue"
using lebesgue_rational_linear_approx_set [OF S contf]
proof -
have "?T = {x ∈ S. ∀e>0. ∃d>0. ∃A. linear A ∧ A u ∙ v < b ∧ All_Rat A ∧
(∀y ∈ S. norm(y - x) < d ⟶ norm(f y - f x - A (y - x)) ≤ e * norm(y - x))}"
by (auto simp: C_def)
then show ?thesis
using lebesgue_rational_linear_approx_set [OF S contf] by simp
qed
define M where "M ≡ (?T - {x ∈ S. f' x u ∙ v ≤ b} ∪ ({x ∈ S. f' x u ∙ v ≤ b} - ?T))"
define Θ where "Θ ≡ λx v. ∀ξ>0. ∃e>0. ∀y ∈ S-{x}. norm (x - y) < e ⟶ ¦v ∙ (y - x)¦ < ξ * norm (x - y)"
have nN: "negligible {x ∈ S. ∃v≠0. Θ x v}"
using negligible_thin_direction[of S] by (simp add: Θ_def)
have *: "(⋀x. (x ∉ S) ⟹ (x ∈ T ⟷ x ∈ U)) ⟹ (T - U) ∪ (U - T) ⊆ S" for S T U :: "'a set"
by blast
have MN: "M ⊆ {x ∈ S. ∃v≠0. Θ x v}"
unfolding M_def
proof (rule *)
fix x
assume x: "x ∉ {x ∈ S. ∃v≠0. Θ x v}"
show "(x ∈ ?T) ⟷ (x ∈ {x ∈ S. f' x u ∙ v ≤ b})"
proof (cases "x ∈ S")
case True
then have notPhi: "¬ Θ x v" if "v ≠ 0" for v
using x that by force
show ?thesis
proof (rule iffI; clarsimp)
assume b: "∀e>0. ∃d>0. ∃A. linear A ∧ A u ∙ v < b ∧ All_Rat A ∧
(∀y∈S. C e A d x y)"
(is "∀e>0. ∃d>0. ∃A. ?Φ e d A")
then have "∀k. ∃d>0. ∃A. ?Φ (1 / Suc k) d A"
by (metis (no_types, opaque_lifting) less_Suc_eq_0_disj of_nat_0_less_iff zero_less_divide_1_iff)
then obtain δ A where δ: "⋀k. δ k > 0"
and Ab: "⋀k. A k u ∙ v < b"
and A: "⋀k y. y ∈ S ⟹ C (1 / real (Suc k)) (A k) (δ k) x y"
and linA: "⋀k. linear (A k)"
by metis
have A_to_a: "∃a. (λn. A n i ∙ j) ⇢ a" for i j
proof -
define CA where "CA ≡ {x. Cauchy (λn. A n x)}"
have "∃l. (λn. A n 0) ⇢ l"
using A True δ by (fastforce simp: C_def)
moreover have "∃l. (λn. A n (x + y)) ⇢ l"
if "(λn. A n x) ⇢ l" and "(λn. A n y) ⇢ l'"
for x :: 'a and l :: 'b and y :: 'a and l' :: 'b
using that linA
by (intro exI [where x="l+l'"]) (simp add: Real_Vector_Spaces.linear_iff tendsto_add)
moreover have "∃l. (λn. A n (c *⇩R x)) ⇢ l" if "(λn. A n x) ⇢ l" for c x l
using that linA
by (intro exI [where x="c *⇩R l"]) (simp add: Real_Vector_Spaces.linear_iff tendsto_scaleR)
ultimately have "subspace CA"
by (auto simp: CA_def subspace_def convergent_eq_Cauchy [symmetric])
then have CA_eq: "CA = span CA"
by (metis span_eq_iff)
also have "… = UNIV"
proof -
have "dim CA ≤ DIM('a)"
using dim_subset_UNIV[of CA] by auto
moreover have "False" if less: "dim CA < DIM('a)"
proof -
obtain d where "d ≠ 0" and d: "⋀y. y ∈ span CA ⟹ orthogonal d y"
using less by (force intro: orthogonal_to_subspace_exists [of CA])
with notPhi [OF ‹d ≠ 0›] obtain ξ where "ξ > 0"
and ξ: "⋀e. e > 0 ⟹ ∃y ∈ S - {x}. norm (x - y) < e ∧ ξ * norm (x - y) ≤ ¦d ∙ (y - x)¦"
by (metis Θ_def linorder_not_less)
obtain γ z where γSx: "⋀i. γ i ∈ S - {x}"
and γle: "⋀i. ξ * norm(γ i - x) ≤ ¦d ∙ (γ i - x)¦"
and γx: "γ ⇢ x"
and z: "(λn. (γ n - x) /⇩R norm (γ n - x)) ⇢ z"
proof -
have "∃γ. (∀i. (γ i ∈ S - {x} ∧
ξ * norm(γ i - x) ≤ ¦d ∙ (γ i - x)¦ ∧ norm(γ i - x) < 1/Suc i) ∧
norm(γ(Suc i) - x) < norm(γ i - x))"
proof (rule dependent_nat_choice)
show "∃y. y ∈ S - {x} ∧ ξ * norm (y - x) ≤ ¦d ∙ (y - x)¦ ∧ norm (y - x) < 1 / Suc 0"
using ξ [of 1] by (auto simp: dist_norm norm_minus_commute)
next
fix y i
assume "y ∈ S - {x} ∧ ξ * norm (y - x) ≤ ¦d ∙ (y - x)¦ ∧ norm (y - x) < 1/Suc i"
then have "min (norm(y - x)) (1/((Suc i) + 1)) > 0"
by auto
then obtain y' where "y' ∈ S - {x}" and y': "norm (x - y') < min (norm (y - x)) (1/((Suc i) + 1))"
"ξ * norm (x - y') ≤ ¦d ∙ (y' - x)¦"
using ξ by metis
with ξ show "∃y'. (y' ∈ S - {x} ∧ ξ * norm (y' - x) ≤ ¦d ∙ (y' - x)¦ ∧
norm (y' - x) < 1/(Suc (Suc i))) ∧ norm (y' - x) < norm (y - x)"
by (auto simp: dist_norm norm_minus_commute)
qed
then obtain γ where γSx: "⋀i. γ i ∈ S - {x}"
and γle: "⋀i. ξ * norm(γ i - x) ≤ ¦d ∙ (γ i - x)¦"
and γconv: "⋀i. norm(γ i - x) < 1/(Suc i)"
by blast
let ?f = "λi. (γ i - x) /⇩R norm (γ i - x)"
have "?f i ∈ sphere 0 1" for i
using γSx by auto
then obtain l ρ where "l ∈ sphere 0 1" "strict_mono ρ" and l: "(?f ∘ ρ) ⇢ l"
using compact_sphere [of "0" 1] unfolding compact_def by meson
show thesis
proof
show "(γ ∘ ρ) i ∈ S - {x}" "ξ * norm ((γ ∘ ρ) i - x) ≤ ¦d ∙ ((γ ∘ ρ) i - x)¦" for i
using γSx γle by auto
have "γ ⇢ x"
proof (clarsimp simp add: LIMSEQ_def dist_norm)
fix r :: "real"
assume "r > 0"
with real_arch_invD obtain no where "no ≠ 0" "real no > 1/r"
by (metis divide_less_0_1_iff not_less_iff_gr_or_eq of_nat_0_eq_iff reals_Archimedean2)
with γconv show "∃no. ∀n≥no. norm (γ n - x) < r"
by (metis ‹r > 0› add.commute divide_inverse inverse_inverse_eq inverse_less_imp_less less_trans mult.left_neutral nat_le_real_less of_nat_Suc)
qed
with ‹strict_mono ρ› show "(γ ∘ ρ) ⇢ x"
by (metis LIMSEQ_subseq_LIMSEQ)
show "(λn. ((γ ∘ ρ) n - x) /⇩R norm ((γ ∘ ρ) n - x)) ⇢ l"
using l by (auto simp: o_def)
qed
qed
have "isCont (λx. (¦d ∙ x¦ - ξ)) z"
by (intro continuous_intros)
from isCont_tendsto_compose [OF this z]
have lim: "(λy. ¦d ∙ ((γ y - x) /⇩R norm (γ y - x))¦ - ξ) ⇢ ¦d ∙ z¦ - ξ"
by auto
moreover have "∀⇩F i in sequentially. 0 ≤ ¦d ∙ ((γ i - x) /⇩R norm (γ i - x))¦ - ξ"
proof (rule eventuallyI)
fix n
show "0 ≤ ¦d ∙ ((γ n - x) /⇩R norm (γ n - x))¦ - ξ"
using γle [of n] γSx by (auto simp: abs_mult divide_simps)
qed
ultimately have "ξ ≤ ¦d ∙ z¦"
using tendsto_lowerbound [where a=0] by fastforce
have "Cauchy (λn. A n z)"
proof (clarsimp simp add: Cauchy_def)
fix ε :: "real"
assume "0 < ε"
then obtain N::nat where "N > 0" and N: "ε/2 > 1/N"
by (metis half_gt_zero inverse_eq_divide neq0_conv real_arch_inverse)
show "∃M. ∀m≥M. ∀n≥M. dist (A m z) (A n z) < ε"
proof (intro exI allI impI)
fix i j
assume ij: "N ≤ i" "N ≤ j"
let ?V = "λi k. A i ((γ k - x) /⇩R norm (γ k - x))"
have "∀⇩F k in sequentially. dist (γ k) x < min (δ i) (δ j)"
using γx [unfolded tendsto_iff] by (meson min_less_iff_conj δ)
then have even: "∀⇩F k in sequentially. norm (?V i k - ?V j k) - 2 / N ≤ 0"
proof (rule eventually_mono, clarsimp)
fix p
assume p: "dist (γ p) x < δ i" "dist (γ p) x < δ j"
define g where "g ≡ λk. f (γ p) - f x - A k (γ p - x)"
have "norm ((A i - A j) (γ p - x)) = norm (g j - g i)"
by (simp add: g_def algebra_simps)
also have "… ≤ norm (g j) + norm (g i)"
using norm_triangle_ineq4 by blast
also have "… ≤ 1/(Suc j) * norm (γ p - x) + 1/(Suc i) * norm (γ p - x)"
using A γSx p by (simp add: g_def C_def add_mono dist_norm)
also have "… ≤ 1/N * norm (γ p - x) + 1/N * norm (γ p - x)"
using ij ‹N > 0› by (intro add_mono mult_right_mono) (auto simp: field_simps)
also have "… = 2 / N * norm (γ p - x)"
by simp
finally have no_le: "norm ((A i - A j) (γ p - x)) ≤ 2 / N * norm (γ p - x)" .
have "norm (?V i p - ?V j p) =
norm ((A i - A j) ((γ p - x) /⇩R norm (γ p - x)))"
by (simp add: algebra_simps)
also have "… = norm ((A i - A j) (γ p - x)) / norm (γ p - x)"
using linA[of i] linA[of j] norm_scaleR real_norm_def divide_inverse norm_inverse
by (smt (verit, del_insts) Real_Vector_Spaces.linear_iff abs_norm_cancel fun_diff_def
mult.commute scaleR_right_diff_distrib)
also have "… ≤ 2 / N"
using no_le by (auto simp: field_split_simps)
finally show "norm (?V i p - ?V j p) ≤ 2 / N" .
qed
have "isCont (λw. (norm(A i w - A j w) - 2 / N)) z"
by (simp add: continuous_intros linA linear_continuous_within linear_linear)
from isCont_tendsto_compose [OF this z]
have lim: "(λw. norm (A i ((γ w - x) /⇩R norm (γ w - x)) -
A j ((γ w - x) /⇩R norm (γ w - x))) - 2 / N)
⇢ norm (A i z - A j z) - 2 / N"
by auto
have "dist (A i z) (A j z) ≤ 2 / N"
using tendsto_upperbound [OF lim even] by (auto simp: dist_norm)
with N show "dist (A i z) (A j z) < ε"
by linarith
qed
qed
then have "d ∙ z = 0"
using CA_eq d by (auto simp: orthogonal_def CA_def)
then show False
using ‹0 < ξ› ‹ξ ≤ ¦d ∙ z¦› by auto
qed
ultimately show ?thesis
using dim_eq_full by fastforce
qed
finally have CA: "CA = UNIV" .
then have "Cauchy (λn. A n i)"
by (auto simp: CA_def)
then show "∃a. (λn. A n i ∙ j) ⇢ a"
using tendsto_inner[of "λn. A n i"] convergent_eq_Cauchy by blast
qed
have conv: "convergent (λn. A n i)" for i
proof -
obtain a where a: "⋀j. (λn. A n i ∙ j) ⇢ a j"
using A_to_a by metis
have "(λn. ∑j∈Basis. (A n i ∙ j) *⇩R j) ⇢ (∑j∈Basis. a j *⇩R j)"
by (intro tendsto_intros a)
moreover have "A n i = (∑j∈Basis. (A n i ∙ j) *⇩R j)" for n
by (rule euclidean_representation [symmetric])
ultimately show ?thesis
by (auto simp: convergent_def)
qed
define B where "B ≡ λi. lim (λn. A n i)"
have Blim: "(λn. A n i) ⇢ B i" for i
using conv unfolding B_def by (simp add: convergent_LIMSEQ_iff)
have linB: "linear B"
unfolding Real_Vector_Spaces.linear_iff
proof (intro conjI allI)
fix x y
have "(λn. A n (x + y)) ⇢ B (x + y)" by (rule Blim)
moreover have "(λn. A n x + A n y) ⇢ B x + B y"
by (intro tendsto_intros Blim)
moreover have "A n (x + y) = A n x + A n y" for n
using linA[of n] by (simp add: Real_Vector_Spaces.linear_iff)
ultimately show "B (x + y) = B x + B y"
by (simp add: LIMSEQ_unique)
next
fix c x
have "(λn. A n (c *⇩R x)) ⇢ B (c *⇩R x)" by (rule Blim)
moreover have "(λn. c *⇩R A n x) ⇢ c *⇩R B x"
by (intro tendsto_intros Blim)
moreover have "A n (c *⇩R x) = c *⇩R A n x" for n
using linA[of n] by (simp add: Real_Vector_Spaces.linear_iff)
ultimately show "B (c *⇩R x) = c *⇩R B x"
by (simp add: LIMSEQ_unique)
qed
have B: "(λn. A n i ∙ j) ⇢ B i ∙ j" for i j
using Blim[of i] by (intro tendsto_intros)
have lin_df: "linear (f' x)"
and lim_df: "((λy. (1 / norm (y - x)) *⇩R (f y - (f x + f' x (y - x)))) ⤏ 0) (at x within S)"
using ‹x ∈ S› f by (auto simp: has_derivative_within linear_linear)
moreover
interpret linear "f' x" by fact
have "(f' x - B) w = 0" for w
proof (rule lemma_partial_derivatives [of "f' x - B"])
show "linear (f' x - B)"
by (simp add: linB fun_diff_def linear_axioms linear_compose_sub)
have "((λy. ((f x + f' x (y - x)) - f y) /⇩R norm (y - x)) ⤏ 0) (at x within S)"
using tendsto_minus [OF lim_df] by (simp add: field_split_simps)
then show "((λy. (f' x - B) (y - x) /⇩R norm (y - x)) ⤏ 0) (at x within S)"
proof (rule Lim_transform)
have "((λy. ((f y + B x - (f x + B y)) /⇩R norm (y - x))) ⤏ 0) (at x within S)"
proof (clarsimp simp add: Lim_within dist_norm)
fix e :: "real"
assume "e > 0"
then obtain q::nat where "q ≠ 0" and qe2: "1/q < e/2"
by (metis divide_pos_pos inverse_eq_divide real_arch_inverse zero_less_numeral)
let ?g = "λp. sum (λi. sum (λj. abs((A p - B) i ∙ j)) Basis) Basis"
have blAB: "bounded_linear (A k - B)" for k
using linA linB by (simp add: linear_conv_bounded_linear fun_diff_def bounded_linear_sub)
have "(λk. onorm (A k - B)) ⇢ 0"
proof (rule Lim_null_comparison)
show "∀⇩F k in sequentially. norm (onorm (A k - B)) ≤ ?g k"
proof (rule eventually_sequentiallyI)
fix k :: "nat"
assume "0 ≤ k"
have "0 ≤ onorm (A k - B)"
using blAB by (rule onorm_pos_le)
moreover have "onorm (A k - B) ≤ (∑i∈Basis. ∑j∈Basis. ¦(A k - B) i ∙ j¦)"
proof (rule onorm_componentwise_le [OF blAB])
show "(∑i∈Basis. norm ((A k - B) i)) ≤ (∑i∈Basis. ∑j∈Basis. ¦(A k - B) i ∙ j¦)"
by (rule sum_mono [OF norm_le_l1])
qed
ultimately show "norm (onorm (A k - B)) ≤ (∑i∈Basis. ∑j∈Basis. ¦(A k - B) i ∙ j¦)"
by simp
qed
next
show "?g ⇢ 0"
proof (rule tendsto_null_sum)
fix i :: 'a
assume "i ∈ Basis"
show "(λp. ∑j∈Basis. ¦(A p - B) i ∙ j¦) ⇢ 0"
proof (rule tendsto_null_sum)
fix j :: 'b
assume "j ∈ Basis"
have "(λn. A n i ∙ j - B i ∙ j) ⇢ 0"
using B Lim_null by fastforce
moreover have "(A p - B) i ∙ j = A p i ∙ j - B i ∙ j" for p
by (simp add: inner_diff_left)
ultimately show "(λp. ¦(A p - B) i ∙ j¦) ⇢ 0"
using tendsto_rabs_zero_iff by force
qed
qed
qed
with ‹e > 0› obtain p where "⋀n. n ≥ p ⟹ ¦onorm (A n - B)¦ < e/2"
unfolding lim_sequentially by (metis diff_zero dist_real_def divide_pos_pos zero_less_numeral)
then have pqe2: "¦onorm (A (p + q) - B)¦ < e/2"
using le_add1 by blast
show "∃d>0. ∀y∈S. y ≠ x ∧ norm (y - x) < d ⟶
inverse (norm (y - x)) * norm (f y + B x - (f x + B y)) < e"
proof (intro exI, safe)
show "0 < δ(p + q)"
by (simp add: δ)
next
fix y
assume y: "y ∈ S" "norm (y - x) < δ(p + q)" and "y ≠ x"
have *: "⟦norm(b - c) < e - d; norm(y - x - b) ≤ d⟧ ⟹ norm(y - x - c) < e"
for b c d e x and y:: "'b"
using norm_triangle_ineq2 [of "y - x - c" "y - x - b"] by simp
have "norm (f y - f x - B (y - x)) < e * norm (y - x)"
proof (rule *)
show "norm (f y - f x - A (p + q) (y - x)) ≤ norm (y - x) / (Suc (p + q))"
using A y by (force simp: C_def)
have "norm (A (p + q) (y - x) - B (y - x)) ≤ onorm (A (p + q) - B) * norm(y - x)"
by (metis blAB minus_apply onorm)
also have "… < (e/2) * norm (y - x)"
using ‹y ≠ x› pqe2 by auto
also have "… ≤ (e - 1 / (Suc (p + q))) * norm (y - x)"
proof (rule mult_right_mono)
have "1 / Suc (p + q) ≤ 1 / q"
using ‹q ≠ 0› by (auto simp: field_split_simps)
also have "… < e/2"
using qe2 by auto
finally show "e / 2 ≤ e - 1 / real (Suc (p + q))"
by linarith
qed auto
finally show "norm (A (p + q) (y - x) - B (y - x)) < e * norm (y - x) - norm (y - x) / real (Suc (p + q))"
by (simp add: algebra_simps)
qed
then show "inverse (norm (y - x)) * norm (f y + B x - (f x + B y)) < e"
using ‹y ≠ x› linear_diff [OF linB]
by (simp add: field_split_simps algebra_simps)
qed
qed
then show "((λy. (f' x - B) (y - x) /⇩R
norm (y - x) - (f x + f' x (y - x) - f y) /⇩R norm (y - x)) ⤏ 0)
(at x within S)"
by (simp add: algebra_simps diff linear_diff [OF linB] lin_df)
qed
show "⋀v. v ≠ 0 ⟹
∃k>0. ∀e>0. ∃xa∈S - {x}. norm (x - xa) < e ∧ k * norm (x - xa) ≤ ¦v ∙ (xa - x)¦"
using x by (meson Θ_def linorder_not_le notPhi)
qed
ultimately have "f' x = B"
by (force simp: algebra_simps)
show "f' x u ∙ v ≤ b"
proof (rule tendsto_upperbound [of "λi. (A i u ∙ v)" _ sequentially])
show "(λi. A i u ∙ v) ⇢ f' x u ∙ v"
by (simp add: B ‹f' x = B›)
show "∀⇩F i in sequentially. A i u ∙ v ≤ b"
by (simp add: Ab less_eq_real_def)
qed auto
next
fix e :: "real"
assume "x ∈ S" and b: "f' x u ∙ v ≤ b" and "e > 0"
then show "∃d>0. ∃A. linear A ∧ A u ∙ v < b ∧ All_Rat A ∧ (∀y∈S. C e A d x y)"
unfolding C_def
by (intro rational_linear_approx_witness [OF f]) simp_all
qed
qed auto
qed
show "negligible M"
using negligible_subset [OF nN MN] .
qed
qed
proposition borel_measurable_partial_derivatives:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes S: "S ∈ sets lebesgue"
and f: "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x within S)"
and uB: "u ∈ Basis" and vB: "v ∈ Basis"
shows "(λx. f' x u ∙ v) ∈ borel_measurable (lebesgue_on S)"
proof -
have "{x ∈ S. f' x u ∙ v ≤ b} ∈ sets lebesgue" for b
by (rule lebesgue_halfspace_derivative_le [OF S f]) (use uB vB in ‹auto simp: norm_Basis›)
then show ?thesis
by (simp add: borel_measurable_vimage_halfspace_component_le sets_restrict_space_iff S)
qed
theorem borel_measurable_det_Jacobian:
fixes f :: "'a::euclidean_space ⇒ 'a"
assumes S: "S ∈ sets lebesgue" and f: "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x within S)"
shows "(λx. eucl.det (f' x)) ∈ borel_measurable (lebesgue_on S)"
unfolding eucl_det_def
by (intro borel_measurable_sum borel_measurable_prod borel_measurable_times
borel_measurable_const borel_measurable_partial_derivatives [OF S])
(auto intro: f elim: permutes_in_funpow_image[where n=1, simplified] simp: permutes_image [symmetric])
text‹The localisation wrt S uses the same argument for many similar results.›
theorem borel_measurable_lebesgue_on_preimage_borel:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes "S ∈ sets lebesgue"
shows "f ∈ borel_measurable (lebesgue_on S) ⟷
(∀T. T ∈ sets borel ⟶ {x ∈ S. f x ∈ T} ∈ sets lebesgue)"
proof -
have "{x. (if x ∈ S then f x else 0) ∈ T} ∈ sets lebesgue ⟷ {x ∈ S. f x ∈ T} ∈ sets lebesgue"
if "T ∈ sets borel" for T
proof (cases "0 ∈ T")
case True
then have "{x ∈ S. f x ∈ T} = {x. (if x ∈ S then f x else 0) ∈ T} ∩ S"
"{x. (if x ∈ S then f x else 0) ∈ T} = {x ∈ S. f x ∈ T} ∪ -S"
by auto
then show ?thesis
by (metis (no_types, lifting) Compl_in_sets_lebesgue assms sets.Int sets.Un)
next
case False
then have "{x. (if x ∈ S then f x else 0) ∈ T} = {x ∈ S. f x ∈ T}"
by auto
then show ?thesis
by auto
qed
then show ?thesis
unfolding borel_measurable_lebesgue_preimage_borel borel_measurable_if [OF assms, symmetric]
by blast
qed
lemma sets_lebesgue_almost_borel:
assumes "S ∈ sets lebesgue"
obtains B N where "B ∈ sets borel" "negligible N" "B ∪ N = S"
by (metis assms negligible_iff_null_sets negligible_subset null_sets_completionI sets_completionE sets_lborel)
lemma double_lebesgue_sets:
assumes S: "S ∈ sets lebesgue" and T: "T ∈ sets lebesgue" and fim: "f ` S ⊆ T"
shows "(∀U. U ∈ sets lebesgue ∧ U ⊆ T ⟶ {x ∈ S. f x ∈ U} ∈ sets lebesgue) ⟷
f ∈ borel_measurable (lebesgue_on S) ∧
(∀U. negligible U ∧ U ⊆ T ⟶ {x ∈ S. f x ∈ U} ∈ sets lebesgue)"
(is "?lhs ⟷ _ ∧ ?rhs")
unfolding borel_measurable_lebesgue_on_preimage_borel [OF S]
proof (intro iffI allI conjI impI, safe)
fix V :: "'b set"
assume *: "∀U. U ∈ sets lebesgue ∧ U ⊆ T ⟶ {x ∈ S. f x ∈ U} ∈ sets lebesgue"
and "V ∈ sets borel"
then have V: "V ∈ sets lebesgue"
by simp
have "{x ∈ S. f x ∈ V} = {x ∈ S. f x ∈ T ∩ V}"
using fim by blast
also have "{x ∈ S. f x ∈ T ∩ V} ∈ sets lebesgue"
using T V * le_inf_iff by blast
finally show "{x ∈ S. f x ∈ V} ∈ sets lebesgue" .
next
fix U :: "'b set"
assume "∀U. U ∈ sets lebesgue ∧ U ⊆ T ⟶ {x ∈ S. f x ∈ U} ∈ sets lebesgue"
"negligible U" "U ⊆ T"
then show "{x ∈ S. f x ∈ U} ∈ sets lebesgue"
using negligible_imp_sets by blast
next
fix U :: "'b set"
assume 1 [rule_format]: "(∀T. T ∈ sets borel ⟶ {x ∈ S. f x ∈ T} ∈ sets lebesgue)"
and 2 [rule_format]: "∀U. negligible U ∧ U ⊆ T ⟶ {x ∈ S. f x ∈ U} ∈ sets lebesgue"
and "U ∈ sets lebesgue" "U ⊆ T"
then obtain C N where C: "C ∈ sets borel ∧ negligible N ∧ C ∪ N = U"
using sets_lebesgue_almost_borel by metis
then have "{x ∈ S. f x ∈ C} ∈ sets lebesgue"
by (blast intro: 1)
moreover have "{x ∈ S. f x ∈ N} ∈ sets lebesgue"
using C ‹U ⊆ T› by (blast intro: 2)
moreover have "{x ∈ S. f x ∈ C ∪ N} = {x ∈ S. f x ∈ C} ∪ {x ∈ S. f x ∈ N}"
by auto
ultimately show "{x ∈ S. f x ∈ U} ∈ sets lebesgue"
using C by auto
qed
subsection‹Simplest case of Sard's theorem (we don't need continuity of derivative)›
lemma Sard_lemma00:
fixes P :: "'b::euclidean_space set"
assumes "a ≥ 0" and a: "a *⇩R i ≠ 0" and i: "i ∈ Basis"
and P: "P ⊆ {x. a *⇩R i ∙ x = 0}"
and "0 ≤ m" "0 ≤ e"
obtains S where "S ∈ lmeasurable"
and "{z. norm z ≤ m ∧ (∃t ∈ P. norm(z - t) ≤ e)} ⊆ S"
and "measure lebesgue S ≤ (2 * e) * (2 * m) ^ (DIM('b) - 1)"
proof -
have "a > 0"
using assms by simp
let ?v = "(∑j∈Basis. (if j = i then e else m) *⇩R j)"
show thesis
proof
have "- e ≤ x ∙ i" "x ∙ i ≤ e"
if "t ∈ P" "norm (x - t) ≤ e" for x t
using ‹a > 0› that Basis_le_norm [of i "x-t"] P i
by (auto simp: inner_commute algebra_simps)
moreover have "- m ≤ x ∙ j" "x ∙ j ≤ m"
if "norm x ≤ m" "t ∈ P" "norm (x - t) ≤ e" "j ∈ Basis" and "j ≠ i"
for x t j
using that Basis_le_norm [of j x] by auto
ultimately
show "{z. norm z ≤ m ∧ (∃t∈P. norm (z - t) ≤ e)} ⊆ cbox (-?v) ?v"
by (auto simp: mem_box)
have *: "∀k∈Basis. - ?v ∙ k ≤ ?v ∙ k"
using ‹0 ≤ m› ‹0 ≤ e› by (auto simp: inner_Basis)
have 2: "2 ^ DIM('b) = 2 * 2 ^ (DIM('b) - Suc 0)"
by (metis DIM_positive Suc_pred power_Suc)
show "measure lebesgue (cbox (-?v) ?v) ≤ 2 * e * (2 * m) ^ (DIM('b) - 1)"
using ‹i ∈ Basis›
by (simp add: content_cbox [OF *] prod.distrib prod.If_cases Diff_eq [symmetric] 2)
qed blast
qed
text‹As above, but reorienting the vector (HOL Light's @text{GEOM\_BASIS\_MULTIPLE\_TAC})›
lemma Sard_lemma0:
fixes P :: "'a::euclidean_space set"
assumes "a ≠ 0"
and P: "P ⊆ {x. a ∙ x = 0}" and "0 ≤ m" "0 ≤ e"
obtains S where "S ∈ lmeasurable"
and "{z. norm z ≤ m ∧ (∃t ∈ P. norm(z - t) ≤ e)} ⊆ S"
and "measure lebesgue S ≤ (2 * e) * (2 * m) ^ (DIM('a) - 1)"
proof -
obtain i :: 'a where i: "i ∈ Basis"
using nonempty_Basis by blast
have ni: "norm (norm a *⇩R i) = norm a"
using norm_Basis[OF i] by simp
then obtain T where T: "orthogonal_transformation T" and a: "T (norm a *⇩R i) = a"
using orthogonal_transformation_exists by metis
have Tinv [simp]: "T (inv T x) = x" for x
by (simp add: T orthogonal_transformation_surj surj_f_inv_f)
obtain S where S: "S ∈ lmeasurable"
and subS: "{z. norm z ≤ m ∧ (∃t ∈ T-`P. norm(z - t) ≤ e)} ⊆ S"
and mS: "measure lebesgue S ≤ (2 * e) * (2 * m) ^ (DIM('a) - 1)"
proof (rule Sard_lemma00 [of "norm a" i "T-`P" m e])
have "norm a *⇩R i ∙ x = 0" if "T x ∈ P" for x
proof -
have "norm a *⇩R i ∙ x = T (norm a *⇩R i) ∙ T x"
using T by (simp add: orthogonal_transformation_def)
also have "… = a ∙ T x"
by (simp add: a)
also have "… = 0"
using P that by auto
finally show ?thesis .
qed
then show "T -` P ⊆ {x. norm a *⇩R i ∙ x = 0}"
by auto
qed (use assms T i in auto)
show thesis
proof
show "T ` S ∈ lmeasurable"
using S measurable_orthogonal_image T by blast
have "{z. norm z ≤ m ∧ (∃t∈P. norm (z - t) ≤ e)} ⊆ T ` {z. norm z ≤ m ∧ (∃t∈T -` P. norm (z - t) ≤ e)}"
proof clarsimp
fix x t
assume §: "norm x ≤ m" "t ∈ P" "norm (x - t) ≤ e"
then have "norm (inv T x) ≤ m"
using orthogonal_transformation_inv [OF T] by (simp add: orthogonal_transformation_norm)
moreover have "∃t∈T -` P. norm (inv T x - t) ≤ e"
proof -
have "inv T t ∈ T -` P"
using ‹t ∈ P› by (simp add: vimage_def)
moreover have "norm (inv T x - inv T t) ≤ e"
proof -
have "inv T x - inv T t = inv T (x - t)"
using orthogonal_transformation_inv [OF T]
by (simp add: linear_diff orthogonal_transformation_linear)
also have "norm … = norm (x - t)"
using orthogonal_transformation_inv [OF T] by (simp add: orthogonal_transformation_norm)
finally show ?thesis
using §(3) by simp
qed
ultimately show ?thesis by auto
qed
ultimately show "x ∈ T ` {z. norm z ≤ m ∧ (∃t∈T -` P. norm (z - t) ≤ e)}"
by force
qed
then show "{z. norm z ≤ m ∧ (∃t∈P. norm (z - t) ≤ e)} ⊆ T ` S"
using image_mono [OF subS] by (rule order_trans)
show "measure lebesgue (T ` S) ≤ 2 * e * (2 * m) ^ (DIM('a) - 1)"
proof -
have linT: "linear T" and linTi: "linear (inv T)"
using T orthogonal_transformation_inv [OF T]
by (auto simp: orthogonal_transformation_linear)
have "T ∘ inv T = id"
using T orthogonal_transformation_surj surj_f_inv_f by fastforce
then have "eucl.det T * eucl.det (inv T) = 1"
using eucl.det_compose [OF linT linTi] by simp
have "¦eucl.det T¦ = 1"
proof -
note [transfer_rule] = transfer_measure_bij_rules transfer_eucl_bij_rules
have "orthogonal_transformation f ⟹ ¦eucl.det f¦ = 1" for f :: "'a ⇒ 'a"
using orthogonal_transformation_det[unfolded orthogonal_transformation_def,
where ?'n = "'a basis", untransferred]
by (simp add: orthogonal_transformation_def)
then show ?thesis using T by blast
qed
then have "measure lebesgue (T ` S) = measure lebesgue S"
using measure_orthogonal_image [OF T S] by simp
then show ?thesis using mS by simp
qed
qed
qed
text‹As above, but translating the sets (HOL Light's @text{GEN\_GEOM\_ORIGIN\_TAC})›
lemma Sard_lemma1:
fixes P :: "'a::euclidean_space set"
assumes P: "dim P < DIM('a)" and "0 ≤ m" "0 ≤ e"
obtains S where "S ∈ lmeasurable"
and "{z. norm(z - w) ≤ m ∧ (∃t ∈ P. norm(z - w - t) ≤ e)} ⊆ S"
and "measure lebesgue S ≤ (2 * e) * (2 * m) ^ (DIM('a) - 1)"
proof -
obtain a where "a ≠ 0" "P ⊆ {x. a ∙ x = 0}"
using lowdim_subset_hyperplane [of P] P span_base by auto
then obtain S where S: "S ∈ lmeasurable"
and subS: "{z. norm z ≤ m ∧ (∃t ∈ P. norm(z - t) ≤ e)} ⊆ S"
and mS: "measure lebesgue S ≤ (2 * e) * (2 * m) ^ (DIM('a) - 1)"
by (rule Sard_lemma0 [OF _ _ ‹0 ≤ m› ‹0 ≤ e›])
show thesis
proof
show "(+)w ` S ∈ lmeasurable"
by (metis measurable_translation S)
show "{z. norm (z - w) ≤ m ∧ (∃t∈P. norm (z - w - t) ≤ e)} ⊆ (+)w ` S"
using subS by force
show "measure lebesgue ((+)w ` S) ≤ 2 * e * (2 * m) ^ (DIM('a) - 1)"
by (metis measure_translation mS)
qed
qed
lemma Sard_lemma2:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes mlen: "DIM('a) ≤ DIM('b)" (is "?m ≤ ?n")
and "B > 0" "bounded S"
and derS: "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x within S)"
and rank: "⋀x. x ∈ S ⟹ dim (f' x ` UNIV) < DIM('b)"
and B: "⋀x. x ∈ S ⟹ onorm(f' x) ≤ B"
shows "negligible(f ` S)"
proof -
have lin_f': "⋀x. x ∈ S ⟹ linear(f' x)"
using derS has_derivative_linear by blast
show ?thesis
proof (clarsimp simp add: negligible_outer_le)
fix e :: "real"
assume "e > 0"
obtain b where b: "⋀x. x ∈ S ⟹ norm x ≤ b"
using ‹bounded S› by (auto simp: bounded_iff)
let ?One = "∑i∈Basis. i :: 'a"
obtain c where csub: "S ⊆ cbox (- c *⇩R ?One) (c *⇩R ?One)" and "c > 0"
proof
show "S ⊆ cbox (- (¦b¦ + 1) *⇩R ?One) ((¦b¦ + 1) *⇩R ?One)"
using norm_bound_Basis_le b
by (fastforce simp: mem_box inner_sum_right inner_Basis)
qed auto
then have box_cc: "box (- c *⇩R ?One) (c *⇩R ?One) ≠ {}" and cbox_cc: "cbox (- c *⇩R ?One) (c *⇩R ?One) ≠ {}"
using ‹c > 0› by (auto simp: box_ne_empty inner_sum_right inner_Basis)
obtain d where "d > 0" "d ≤ B"
and d: "(d * 2) * (4 * B) ^ (?n - 1) ≤ e / (2*c) ^ ?m / ?m ^ ?m"
apply (rule that [of "min B (e / (2*c) ^ ?m / ?m ^ ?m / (4 * B) ^ (?n - 1) / 2)"])
using ‹B > 0› ‹c > 0› ‹e > 0›
by (simp_all add: divide_simps min_mult_distrib_right)
have "∃r. 0 < r ∧ r ≤ 1/2 ∧
(x ∈ S
⟶ (∀y. y ∈ S ∧ norm(y - x) < r
⟶ norm(f y - f x - f' x (y - x)) ≤ d * norm(y - x)))" for x
proof (cases "x ∈ S")
case True
then obtain r where "r > 0"
and "⋀y. ⟦y ∈ S; norm (y - x) < r⟧
⟹ norm (f y - f x - f' x (y - x)) ≤ d * norm (y - x)"
using derS ‹d > 0› by (force simp: has_derivative_within_alt)
then show ?thesis
by (rule_tac x="min r (1/2)" in exI) simp
next
case False
then show ?thesis
by (rule_tac x="1/2" in exI) simp
qed
then obtain r where r12: "⋀x. 0 < r x ∧ r x ≤ 1/2"
and r: "⋀x y. ⟦x ∈ S; y ∈ S; norm(y - x) < r x⟧
⟹ norm(f y - f x - f' x (y - x)) ≤ d * norm(y - x)"
by metis
then have ga: "gauge (λx. ball x (r x))"
by (auto simp: gauge_def)
obtain 𝒟 where 𝒟: "countable 𝒟" and sub_cc: "⋃𝒟 ⊆ cbox (- c *⇩R ?One) (c *⇩R ?One)"
and cbox: "⋀K. K ∈ 𝒟 ⟹ interior K ≠ {} ∧ (∃u v. K = cbox u v)"
and djointish: "pairwise (λA B. interior A ∩ interior B = {}) 𝒟"
and covered: "⋀K. K ∈ 𝒟 ⟹ ∃x ∈ S ∩ K. K ⊆ ball x (r x)"
and close: "⋀u v. cbox u v ∈ 𝒟 ⟹ ∃n. ∀i∈Basis. v ∙ i - u ∙ i = 2*c / 2^n"
and covers: "S ⊆ ⋃𝒟"
apply (rule covering_lemma [OF csub box_cc ga])
apply (simp add: inner_sum_right inner_Basis)
done
let ?μ = "measure lebesgue"
have "∃T. T ∈ lmeasurable ∧ f ` (K ∩ S) ⊆ T ∧ ?μ T ≤ e / (2*c) ^ ?m * ?μ K"
if "K ∈ 𝒟" for K
proof -
obtain u v where uv: "K = cbox u v"
using cbox ‹K ∈ 𝒟› by blast
then have uv_ne: "cbox u v ≠ {}"
using cbox that by fastforce
obtain x where x: "x ∈ S ∩ cbox u v" "cbox u v ⊆ ball x (r x)"
using ‹K ∈ 𝒟› covered uv by blast
then have "dim (range (f' x)) < ?n"
by (simp add: rank)
then obtain T where T: "T ∈ lmeasurable"
and subT: "{z. norm(z - f x) ≤ (2 * B) * norm(v - u) ∧ (∃t ∈ range (f' x). norm(z - f x - t) ≤ d * norm(v - u))} ⊆ T"
and measT: "?μ T ≤ (2 * (d * norm(v - u))) * (2 * ((2 * B) * norm(v - u))) ^ (?n - 1)"
(is "_ ≤ ?DVU")
using Sard_lemma1 [of "range (f' x)" "(2 * B) * norm(v - u)" "d * norm(v - u)"]
using ‹B > 0› ‹d > 0› by auto
show ?thesis
proof (intro exI conjI)
have "f ` (K ∩ S) ⊆ {z. norm(z - f x) ≤ (2 * B) * norm(v - u) ∧ (∃t ∈ range (f' x). norm(z - f x - t) ≤ d * norm(v - u))}"
unfolding uv
proof (clarsimp simp: mult.assoc, intro conjI)
fix y
assume y: "y ∈ cbox u v" and "y ∈ S"
then have "norm (y - x) < r x"
by (metis dist_norm mem_ball norm_minus_commute subsetCE x(2))
then have le_dyx: "norm (f y - f x - f' x (y - x)) ≤ d * norm (y - x)"
using r [of x y] x ‹y ∈ S› by blast
have yx_le: "norm (y - x) ≤ norm (v - u)"
proof -
have comp: "¦(y - x) ∙ b¦ ≤ ¦(v - u) ∙ b¦" if "b ∈ Basis" for b
proof -
have "u ∙ b ≤ y ∙ b" "y ∙ b ≤ v ∙ b" "u ∙ b ≤ x ∙ b" "x ∙ b ≤ v ∙ b"
using x y that by (auto simp: mem_box)
then show ?thesis
by (simp add: inner_diff_left abs_le_iff)
qed
have "(y - x) ∙ (y - x) ≤ (v - u) ∙ (v - u)"
using comp norm_le norm_le_componentwise by blast
then show ?thesis
by (simp add: norm_eq_sqrt_inner real_sqrt_le_iff)
qed
have *: "⟦norm(y - x - z) ≤ d; norm z ≤ B; d ≤ B⟧ ⟹ norm(y - x) ≤ 2 * B"
for x y z :: 'b and d B
using norm_triangle_ineq2 [of "y - x" z] by auto
show "norm (f y - f x) ≤ 2 * (B * norm (v - u))"
proof (rule * [OF le_dyx])
have "norm (f' x (y - x)) ≤ onorm (f' x) * norm (y - x)"
using onorm [of "f' x" "y-x"] by (meson IntE lin_f' linear_linear x(1))
also have "… ≤ B * norm (v - u)"
by (meson B IntE lin_f' linear_linear mult_mono' norm_ge_zero onorm_pos_le x(1) yx_le)
finally show "norm (f' x (y - x)) ≤ B * norm (v - u)" .
show "d * norm (y - x) ≤ B * norm (v - u)"
using ‹B > 0› by (auto intro: mult_mono [OF ‹d ≤ B› yx_le])
qed
show "∃t. norm (f y - f x - f' x t) ≤ d * norm (v - u)"
by (smt (verit, best) ‹0 < d› le_dyx mult_le_cancel_left_pos yx_le)
qed
with subT show "f ` (K ∩ S) ⊆ T" by blast
show "?μ T ≤ e / (2*c) ^ ?m * ?μ K"
proof (rule order_trans [OF measT])
have "?DVU = (d * 2 * (4 * B) ^ (?n - 1)) * norm (v - u)^?n"
using ‹c > 0›
apply (simp add: algebra_simps)
by (metis Suc_pred power_Suc DIM_positive)
also have "… ≤ (e / (2*c) ^ ?m / (?m ^ ?m)) * norm(v - u) ^ ?n"
by (rule mult_right_mono [OF d]) auto
also have "… ≤ e / (2*c) ^ ?m * ?μ K"
proof -
have "u ∈ ball (x) (r x)" "v ∈ ball x (r x)"
using box_ne_empty(1) contra_subsetD [OF x(2)] mem_box(2) uv_ne by fastforce+
moreover have "r x ≤ 1/2"
using r12 by auto
ultimately have "norm (v - u) ≤ 1"
using norm_triangle_half_r [of x u 1 v]
by (metis (no_types, opaque_lifting) dist_commute dist_norm less_eq_real_def less_le_trans mem_ball)
then have "norm (v - u) ^ ?n ≤ norm (v - u) ^ ?m"
by (simp add: power_decreasing [OF mlen])
also have "… ≤ ?μ K * real (?m ^ ?m)"
proof -
obtain n where n: "⋀i. i ∈ Basis ⟹ v ∙ i - u ∙ i = 2 * c / 2^n"
using close [of u v] ‹K ∈ 𝒟› uv by blast
have "norm (v - u) ^ ?m ≤ (∑i∈Basis. ¦(v - u) ∙ i¦) ^ ?m"
by (intro power_mono norm_le_l1) auto
also have "… ≤ (∏i∈Basis. v ∙ i - u ∙ i) * real ?m ^ ?m"
by (simp add: n inner_diff_left field_simps ‹c > 0› less_eq_real_def)
also have "… = ?μ K * real (?m ^ ?m)"
by (simp add: uv uv_ne content_cbox')
finally show ?thesis .
qed
finally have *: "1 / real (?m ^ ?m) * norm (v - u) ^ ?n ≤ ?μ K"
by (simp add: field_split_simps)
show ?thesis
using mult_left_mono [OF *, of "e / (2*c) ^ ?m"] ‹c > 0› ‹e > 0› by auto
qed
finally show "?DVU ≤ e / (2*c) ^ ?m * ?μ K" .
qed
qed (use T in auto)
qed
then obtain g where meas_g: "⋀K. K ∈ 𝒟 ⟹ g K ∈ lmeasurable"
and sub_g: "⋀K. K ∈ 𝒟 ⟹ f ` (K ∩ S) ⊆ g K"
and le_g: "⋀K. K ∈ 𝒟 ⟹ ?μ (g K) ≤ e / (2*c)^?m * ?μ K"
by metis
have le_e: "?μ (⋃i∈ℱ. g i) ≤ e"
if "ℱ ⊆ 𝒟" "finite ℱ" for ℱ
proof -
have "?μ (⋃i∈ℱ. g i) ≤ (∑i∈ℱ. ?μ (g i))"
using meas_g ‹ℱ ⊆ 𝒟› by (auto intro: measure_UNION_le [OF ‹finite ℱ›])
also have "… ≤ (∑K∈ℱ. e / (2*c) ^ ?m * ?μ K)"
using ‹ℱ ⊆ 𝒟› sum_mono [OF le_g] by (meson le_g subsetCE sum_mono)
also have "… = e / (2*c) ^ ?m * (∑K∈ℱ. ?μ K)"
by (simp add: sum_distrib_left)
also have "… ≤ e"
proof -
have "ℱ division_of ⋃ℱ"
proof (rule division_ofI)
show "K ⊆ ⋃ℱ" "K ≠ {}" "∃a b. K = cbox a b" if "K ∈ ℱ" for K
using ‹K ∈ ℱ› covered cbox ‹ℱ ⊆ 𝒟› by (auto simp: Union_upper)
show "interior K ∩ interior L = {}" if "K ∈ ℱ" and "L ∈ ℱ" and "K ≠ L" for K L
by (metis (mono_tags, lifting) ‹ℱ ⊆ 𝒟› pairwiseD djointish pairwise_subset that)
qed (use that in auto)
then have "sum ?μ ℱ ≤ ?μ (⋃ℱ)"
by (simp add: content_division)
also have "… ≤ ?μ (cbox (- c *⇩R ?One) (c *⇩R ?One))"
proof (rule measure_mono_fmeasurable)
show "⋃ℱ ⊆ cbox (- c *⇩R ?One) (c *⇩R ?One)"
using sub_cc that(1) by force
qed (use ‹ℱ division_of ⋃ℱ› lmeasurable_division in auto)
also have "… = content (cbox (- c *⇩R ?One) (c *⇩R ?One))"
by simp
also have "… ≤ (2 ^ ?m * c ^ ?m)"
using ‹c > 0› by (simp add: content_cbox_if mem_box inner_sum_left inner_Basis)
finally have "sum ?μ ℱ ≤ (2 ^ ?m * c ^ ?m)" .
then show ?thesis
using ‹e > 0› ‹c > 0› by (auto simp: field_split_simps)
qed
finally show ?thesis .
qed
show "∃T. f ` S ⊆ T ∧ T ∈ lmeasurable ∧ ?μ T ≤ e"
proof (intro exI conjI)
show "f ` S ⊆ ⋃ (g ` 𝒟)"
using covers sub_g by force
show "⋃ (g ` 𝒟) ∈ lmeasurable"
by (rule fmeasurable_UN_bound [OF ‹countable 𝒟› meas_g le_e])
show "?μ (⋃ (g ` 𝒟)) ≤ e"
by (rule measure_UN_bound [OF ‹countable 𝒟› meas_g le_e])
qed
qed
qed
theorem baby_Sard:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes mlen: "DIM('a) ≤ DIM('b)"
and der: "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x within S)"
and rank: "⋀x. x ∈ S ⟹ dim (f' x ` UNIV) < DIM('b)"
shows "negligible(f ` S)"
proof -
let ?U = "λn. {x ∈ S. norm(x) ≤ n ∧ onorm(f' x) ≤ real n}"
have "⋀x. x ∈ S ⟹ ∃n. norm x ≤ real n ∧ onorm (f' x) ≤ real n"
by (meson linear order_trans real_arch_simple)
then have eq: "S = (⋃n. ?U n)"
by auto
have "negligible (f ` ?U n)" for n
proof (rule Sard_lemma2 [OF mlen])
show "0 < real n + 1"
by auto
show "bounded (?U n)"
using bounded_iff by blast
show "(f has_derivative f' x) (at x within ?U n)" if "x ∈ ?U n" for x
using der that by (force intro: has_derivative_subset)
qed (use rank in auto)
then show ?thesis
by (subst eq) (simp add: image_Union negligible_Union_nat)
qed
lemma borel_measurable_simple_function_limit_increasing:
fixes f :: "'a::euclidean_space ⇒ real"
shows "(f ∈ borel_measurable lebesgue ∧ (∀x. 0 ≤ f x)) ⟷
(∃g. (∀n x. 0 ≤ g n x ∧ g n x ≤ f x) ∧ (∀n x. g n x ≤ (g(Suc n) x)) ∧
(∀n. g n ∈ borel_measurable lebesgue) ∧ (∀n. finite(range (g n))) ∧
(∀x. (λn. g n x) ⇢ f x))"
(is "?lhs = ?rhs")
proof
assume f: ?lhs
have leb_f: "{x. a ≤ f x ∧ f x < b} ∈ sets lebesgue" for a b
proof -
have "{x. a ≤ f x ∧ f x < b} = {x. f x < b} - {x. f x < a}"
by auto
also have "… ∈ sets lebesgue"
using borel_measurable_vimage_halfspace_component_lt [of f UNIV] f by auto
finally show ?thesis .
qed
have "g n x ≤ f x"
if inc_g: "⋀n x. 0 ≤ g n x ∧ g n x ≤ g (Suc n) x"
and meas_g: "⋀n. g n ∈ borel_measurable lebesgue"
and fin: "⋀n. finite(range (g n))" and lim: "⋀x. (λn. g n x) ⇢ f x" for g n x
proof -
have "∃r>0. ∀N. ∃n≥N. dist (g n x) (f x) ≥ r" if "g n x > f x"
proof -
have g: "g n x ≤ g (N + n) x" for N
by (rule transitive_stepwise_le) (use inc_g in auto)
have "∃m≥N. g n x - f x ≤ dist (g m x) (f x)" for N
proof
show "N ≤ N + n ∧ g n x - f x ≤ dist (g (N + n) x) (f x)"
using g [of N] by (auto simp: dist_norm)
qed
with that show ?thesis
using diff_gt_0_iff_gt by blast
qed
with lim show ?thesis
unfolding lim_sequentially
by (meson less_le_not_le not_le_imp_less)
qed
moreover
let ?Ω = "λn k. indicator {y. k/2^n ≤ f y ∧ f y < (k+1)/2^n}"
let ?g = "λn x. (∑k::real | k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2*n). k/2^n * ?Ω n k x)"
have "∃g. (∀n x. 0 ≤ g n x ∧ g n x ≤ (g(Suc n) x)) ∧
(∀n. g n ∈ borel_measurable lebesgue) ∧ (∀n. finite(range (g n))) ∧(∀x. (λn. g n x) ⇢ f x)"
proof (intro exI allI conjI)
show "0 ≤ ?g n x" for n x
proof (clarify intro!: ordered_comm_monoid_add_class.sum_nonneg)
fix k::real
assume "k ∈ ℤ" and k: "¦k¦ ≤ 2 ^ (2*n)"
show "0 ≤ k/2^n * ?Ω n k x"
using f ‹k ∈ ℤ› apply (clarsimp simp: indicator_def field_split_simps Ints_def)
by (smt (verit) int_less_real_le mult_nonneg_nonneg of_int_0 zero_le_power)
qed
show "?g n x ≤ ?g (Suc n) x" for n x
proof -
have "?g n x =
(∑k | k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2*n).
k/2^n * (indicator {y. k/2^n ≤ f y ∧ f y < (k+1/2)/2^n} x +
indicator {y. (k+1/2)/2^n ≤ f y ∧ f y < (k+1)/2^n} x))"
by (rule sum.cong [OF refl]) (simp add: indicator_def field_split_simps)
also have "… = (∑k | k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2*n). k/2^n * indicator {y. k/2^n ≤ f y ∧ f y < (k+1/2)/2^n} x) +
(∑k | k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2*n). k/2^n * indicator {y. (k+1/2)/2^n ≤ f y ∧ f y < (k+1)/2^n} x)"
by (simp add: comm_monoid_add_class.sum.distrib algebra_simps)
also have "… = (∑k | k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2*n). (2 * k)/2 ^ Suc n * indicator {y. (2 * k)/2 ^ Suc n ≤ f y ∧ f y < (2 * k+1)/2 ^ Suc n} x) +
(∑k | k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2*n). (2 * k)/2 ^ Suc n * indicator {y. (2 * k+1)/2 ^ Suc n ≤ f y ∧ f y < ((2 * k+1) + 1)/2 ^ Suc n} x)"
by (force simp: field_simps indicator_def intro: sum.cong)
also have "… ≤ (∑k | k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2 * Suc n). k/2 ^ Suc n * (indicator {y. k/2 ^ Suc n ≤ f y ∧ f y < (k+1)/2 ^ Suc n} x))"
(is "?a + _ ≤ ?b")
proof -
have *: "⟦sum f I ≤ sum h I; a + sum h I ≤ b⟧ ⟹ a + sum f I ≤ b" for I a b f and h :: "real⇒real"
by linarith
let ?h = "λk. (2*k+1)/2 ^ Suc n *
(indicator {y. (2 * k+1)/2 ^ Suc n ≤ f y ∧ f y < ((2*k+1) + 1)/2 ^ Suc n} x)"
show ?thesis
proof (rule *)
show "(∑k | k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2*n).
2 * k/2 ^ Suc n * indicator {y. (2 * k+1)/2 ^ Suc n ≤ f y ∧ f y < (2 * k+1 + 1)/2 ^ Suc n} x)
≤ sum ?h {k ∈ ℤ. ¦k¦ ≤ 2 ^ (2*n)}"
by (rule sum_mono) (simp add: indicator_def field_split_simps)
next
have α: "?a = (∑k ∈ (*)2 ` {k ∈ ℤ. ¦k¦ ≤ 2 ^ (2*n)}.
k/2 ^ Suc n * indicator {y. k/2 ^ Suc n ≤ f y ∧ f y < (k+1)/2 ^ Suc n} x)"
by (auto simp: inj_on_def field_simps comm_monoid_add_class.sum.reindex)
have β: "sum ?h {k ∈ ℤ. ¦k¦ ≤ 2 ^ (2*n)}
= (∑k ∈ (λx. 2*x + 1) ` {k ∈ ℤ. ¦k¦ ≤ 2 ^ (2*n)}.
k/2 ^ Suc n * indicator {y. k/2 ^ Suc n ≤ f y ∧ f y < (k+1)/2 ^ Suc n} x)"
by (auto simp: inj_on_def field_simps comm_monoid_add_class.sum.reindex)
have 0: "(*) 2 ` {k ∈ ℤ. P k} ∩ (λx. 2 * x + 1) ` {k ∈ ℤ. P k} = {}" for P :: "real ⇒ bool"
proof -
have "2 * i ≠ 2 * j + 1" for i j :: int by arith
thus ?thesis
unfolding Ints_def by auto (use of_int_eq_iff in fastforce)
qed
have "?a + sum ?h {k ∈ ℤ. ¦k¦ ≤ 2 ^ (2*n)}
= (∑k ∈ (*)2 ` {k ∈ ℤ. ¦k¦ ≤ 2 ^ (2*n)} ∪ (λx. 2*x + 1) ` {k ∈ ℤ. ¦k¦ ≤ 2 ^ (2*n)}.
k/2 ^ Suc n * indicator {y. k/2 ^ Suc n ≤ f y ∧ f y < (k+1)/2 ^ Suc n} x)"
unfolding α β
using finite_abs_int_segment [of "2 ^ (2*n)"]
by (subst sum_Un) (auto simp: 0)
also have "… ≤ ?b"
proof (rule sum_mono2)
show "finite {k::real. k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2 * Suc n)}"
by (rule finite_abs_int_segment)
show "(*) 2 ` {k::real. k ∈ ℤ ∧ ¦k¦ ≤ 2^(2*n)} ∪ (λx. 2*x + 1) ` {k ∈ ℤ. ¦k¦ ≤ 2^(2*n)} ⊆ {k ∈ ℤ. ¦k¦ ≤ 2 ^ (2 * Suc n)}"
apply (clarsimp simp: image_subset_iff)
using one_le_power [of "2::real" "2*n"] by linarith
have *: "⟦x ∈ (S ∪ T) - U; ⋀x. x ∈ S ⟹ x ∈ U; ⋀x. x ∈ T ⟹ x ∈ U⟧ ⟹ P x" for S T U P
by blast
have "0 ≤ b" if "b ∈ ℤ" "f x * (2 * 2^n) < b + 1" for b
by (smt (verit, ccfv_SIG) Ints_cases f int_le_real_less mult_nonneg_nonneg of_int_add one_le_power that)
then show "0 ≤ b/2 ^ Suc n * indicator {y. b/2 ^ Suc n ≤ f y ∧ f y < (b + 1)/2 ^ Suc n} x"
if "b ∈ {k ∈ ℤ. ¦k¦ ≤ 2 ^ (2 * Suc n)} -
((*) 2 ` {k ∈ ℤ. ¦k¦ ≤ 2 ^ (2*n)} ∪ (λx. 2*x + 1) ` {k ∈ ℤ. ¦k¦ ≤ 2 ^ (2*n)})" for b
using that by (simp add: indicator_def divide_simps)
qed
finally show "?a + sum ?h {k ∈ ℤ. ¦k¦ ≤ 2 ^ (2*n)} ≤ ?b" .
qed
qed
finally show ?thesis .
qed
show "?g n ∈ borel_measurable lebesgue" for n
apply (intro borel_measurable_indicator borel_measurable_times borel_measurable_sum)
using leb_f sets_restrict_UNIV by auto
show "finite (range (?g n))" for n
proof -
have "(∑k | k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2*n). k/2^n * ?Ω n k x)
∈ (λk. k/2^n) ` {k ∈ ℤ. ¦k¦ ≤ 2 ^ (2*n)}" for x
proof (cases "∃k. k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2*n) ∧ k/2^n ≤ f x ∧ f x < (k+1)/2^n")
case True
then show ?thesis
by (blast intro: indicator_sum_eq)
next
case False
then have "(∑k | k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2*n). k/2^n * ?Ω n k x) = 0"
by auto
then show ?thesis by force
qed
then have "range (?g n) ⊆ ((λk. (k/2^n)) ` {k. k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2*n)})"
by auto
moreover have "finite ((λk::real. (k/2^n)) ` {k ∈ ℤ. ¦k¦ ≤ 2 ^ (2*n)})"
by (intro finite_imageI finite_abs_int_segment)
ultimately show ?thesis
by (rule finite_subset)
qed
show "(λn. ?g n x) ⇢ f x" for x
proof (clarsimp simp add: lim_sequentially)
fix e::real
assume "e > 0"
obtain N1 where N1: "2 ^ N1 > ¦f x¦"
using arch_pow[of 2] by auto
obtain N2 where N2: "(1/2) ^ N2 < e"
using ‹0 < e› arch_pow_inv by fastforce
have "dist (∑k | k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2*n). k/2^n * ?Ω n k x) (f x) < e" if "N1 + N2 ≤ n" for n
proof -
let ?m = "real_of_int ⌊2^n * f x⌋"
have "¦?m¦ ≤ 2^n * 2^N1"
using N1 apply (simp add: f)
by (meson floor_mono le_floor_iff less_le_not_le mult_le_cancel_left_pos zero_less_numeral zero_less_power)
also have "… ≤ 2 ^ (2*n)"
by (metis that add_leD1 add_le_cancel_left mult.commute mult_2_right one_less_numeral_iff
power_add power_increasing_iff semiring_norm(76))
finally have m_le: "¦?m¦ ≤ 2 ^ (2*n)" .
have "?m/2^n ≤ f x" "f x < (?m + 1)/2^n"
by (auto simp: mult.commute pos_divide_le_eq mult_imp_less_div_pos)
then have eq: "dist (∑k | k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2*n). k/2^n * ?Ω n k x) (f x)
= dist (?m/2^n) (f x)"
by (subst indicator_sum_eq [of ?m]) (auto simp: m_le)
have "¦2^n¦ * ¦?m/2^n - f x¦ = ¦2^n * (?m/2^n - f x)¦"
by (simp add: abs_mult)
also have "… < 2 ^ N2 * e"
using N2 by (simp add: divide_simps mult.commute) linarith
also have "… ≤ ¦2^n¦ * e"
using that ‹e > 0› by auto
finally show ?thesis
using eq by (simp add: dist_real_def)
qed
then show "∃no. ∀n≥no. dist (∑k | k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2*n). k * ?Ω n k x/2^n) (f x) < e"
by force
qed
qed
ultimately show ?rhs
by metis
next
assume RHS: ?rhs
with borel_measurable_simple_function_limit [of f UNIV, unfolded lebesgue_on_UNIV_eq]
show ?lhs
by (blast intro: order_trans)
qed
subsection‹A one-way version of change-of-variables not assuming injectivity. ›
lemma integral_on_image_ubound_weak:
fixes f :: "'a::euclidean_space ⇒ real"
assumes S: "S ∈ sets lebesgue"
and f: "f ∈ borel_measurable (lebesgue_on (g ` S))"
and nonneg_fg: "⋀x. x ∈ S ⟹ 0 ≤ f(g x)"
and der_g: "⋀x. x ∈ S ⟹ (g has_derivative g' x) (at x within S)"
and det_int_fg: "(λx. ¦eucl.det (g' x)¦ * f(g x)) integrable_on S"
and meas_gim: "⋀T. ⟦T ⊆ g ` S; T ∈ sets lebesgue⟧ ⟹ {x ∈ S. g x ∈ T} ∈ sets lebesgue"
shows "f integrable_on (g ` S) ∧
integral (g ` S) f ≤ integral S (λx. ¦eucl.det (g' x)¦ * f(g x))"
(is "_ ∧ _ ≤ ?b")
proof -
let ?D = "λx. ¦eucl.det (g' x)¦"
have cont_g: "continuous_on S g"
using der_g has_derivative_continuous_on by blast
have [simp]: "space (lebesgue_on S) = S"
by (simp add: S)
have gS_in_sets_leb: "g ` S ∈ sets lebesgue"
apply (rule differentiable_image_in_sets_lebesgue)
using der_g by (auto simp: S differentiable_def differentiable_on_def)
obtain h where nonneg_h: "⋀n x. 0 ≤ h n x"
and h_le_f: "⋀n x. x ∈ S ⟹ h n (g x) ≤ f (g x)"
and h_inc: "⋀n x. h n x ≤ h (Suc n) x"
and h_meas: "⋀n. h n ∈ borel_measurable lebesgue"
and fin_R: "⋀n. finite(range (h n))"
and lim: "⋀x. x ∈ g ` S ⟹ (λn. h n x) ⇢ f x"
proof -
let ?f = "λx. if x ∈ g ` S then f x else 0"
have "?f ∈ borel_measurable lebesgue ∧ (∀x. 0 ≤ ?f x)"
by (auto simp: gS_in_sets_leb f nonneg_fg measurable_restrict_space_iff [symmetric])
then show ?thesis
apply (clarsimp simp add: borel_measurable_simple_function_limit_increasing)
subgoal for h
by (rule_tac h=h in that) (auto split: if_split_asm)
done
qed
have h_lmeas: "{t. h n (g t) = y} ∩ S ∈ sets lebesgue" for y n
proof -
have "space (lebesgue_on (UNIV::'a set)) = UNIV"
by simp
then have "((h n) -`{y} ∩ g ` S) ∈ sets (lebesgue_on (g ` S))"
by (metis Int_commute borel_measurable_vimage h_meas image_eqI inf_top.right_neutral sets_restrict_space space_borel space_completion space_lborel)
then have "({u. h n u = y} ∩ g ` S) ∈ sets lebesgue"
using gS_in_sets_leb
by (simp add: integral_indicator fmeasurableI2 sets_restrict_space_iff vimage_def)
then have "{x ∈ S. g x ∈ ({u. h n u = y} ∩ g ` S)} ∈ sets lebesgue"
using meas_gim[of "({u. h n u = y} ∩ g ` S)"] by force
moreover have "{t. h n (g t) = y} ∩ S = {x ∈ S. g x ∈ ({u. h n u = y} ∩ g ` S)}"
by blast
ultimately show ?thesis
by auto
qed
have hint: "h n integrable_on g ` S ∧ integral (g ` S) (h n) ≤ integral S (λx. ?D x * h n (g x))"
(is "?INT ∧ ?lhs ≤ ?rhs") for n
proof -
let ?R = "range (h n)"
have hn_eq: "h n = (λx. ∑y∈?R. y * indicat_real {x. h n x = y} x)"
by (simp add: indicator_def if_distrib fin_R cong: if_cong)
have yind: "(λt. y * indicator{x. h n x = y} t) integrable_on (g ` S) ∧
(integral (g ` S) (λt. y * indicator {x. h n x = y} t))
≤ integral S (λt. ¦eucl.det (g' t)¦ * y * indicator {x. h n x = y} (g t))"
if y: "y ∈ ?R" for y::real
proof (cases "y=0")
case True
then show ?thesis using gS_in_sets_leb integrable_0 by force
next
case False
with that have "y > 0"
using less_eq_real_def nonneg_h by fastforce
have "(λx. if x ∈ {t. h n (g t) = y} then ?D x else 0) integrable_on S"
proof (rule measurable_bounded_by_integrable_imp_integrable)
have "(λx. ?D x) ∈ borel_measurable (lebesgue_on ({t. h n (g t) = y} ∩ S))"
proof -
have "(λv. eucl.det (g' v)) ∈ borel_measurable (lebesgue_on (S ∩ {v. h n (g v) = y}))"
by (metis Int_lower1 S assms(4) borel_measurable_det_Jacobian measurable_restrict_mono)
then show ?thesis
by (simp add: Int_commute)
qed
then have "(λx. if x ∈ {t. h n (g t) = y} ∩ S then ?D x else 0) ∈ borel_measurable lebesgue"
by (rule borel_measurable_if_I [OF _ h_lmeas])
then show "(λx. if x ∈ {t. h n (g t) = y} then ?D x else 0) ∈ borel_measurable (lebesgue_on S)"
by (simp add: if_if_eq_conj Int_commute borel_measurable_if [OF S, symmetric])
show "(λx. ?D x *⇩R f (g x) /⇩R y) integrable_on S"
by (rule integrable_cmul) (use det_int_fg in auto)
show "norm (if x ∈ {t. h n (g t) = y} then ?D x else 0) ≤ ?D x *⇩R f (g x) /⇩R y"
if "x ∈ S" for x
using nonneg_h [of n x] ‹y > 0› nonneg_fg [of x] h_le_f [of x n] that
by (auto simp: divide_simps mult_left_mono)
qed (use S in auto)
then have int_det: "(λt. ¦eucl.det (g' t)¦) integrable_on ({t. h n (g t) = y} ∩ S)"
using integrable_restrict_Int by force
have "(g ` ({t. h n (g t) = y} ∩ S)) ∈ lmeasurable"
by (blast intro: has_derivative_subset [OF der_g] measurable_differentiable_image [OF h_lmeas] int_det)
moreover have "g ` ({t. h n (g t) = y} ∩ S) = {x. h n x = y} ∩ g ` S"
by blast
moreover have "measure lebesgue (g ` ({t. h n (g t) = y} ∩ S))
≤ integral ({t. h n (g t) = y} ∩ S) (λt. ¦eucl.det (g' t)¦)"
by (blast intro: has_derivative_subset [OF der_g] measure_differentiable_image [OF h_lmeas _ int_det])
ultimately show ?thesis
using ‹y > 0› integral_restrict_Int [of S "{t. h n (g t) = y}" "λt. ¦eucl.det (g' t)¦ * y"]
apply (simp add: integrable_on_indicator integral_indicator)
apply (simp add: indicator_def of_bool_def if_distrib cong: if_cong)
done
qed
show ?thesis
proof
show "h n integrable_on g ` S"
apply (subst hn_eq)
using yind by (force intro: integrable_sum [OF fin_R])
have "?lhs = integral (g ` S) (λx. ∑y∈range (h n). y * indicat_real {x. h n x = y} x)"
by (metis hn_eq)
also have "… = (∑y∈range (h n). integral (g ` S) (λx. y * indicat_real {x. h n x = y} x))"
by (rule integral_sum [OF fin_R]) (use yind in blast)
also have "… ≤ (∑y∈range (h n). integral S (λu. ¦eucl.det (g' u)¦ * y * indicat_real {x. h n x = y} (g u)))"
using yind by (force intro: sum_mono)
also have "… = integral S (λu. ∑y∈range (h n). ¦eucl.det (g' u)¦ * y * indicat_real {x. h n x = y} (g u))"
proof (rule integral_sum [OF fin_R, symmetric])
fix y assume y: "y ∈ ?R"
with nonneg_h have "y ≥ 0"
by auto
show "(λu. ¦eucl.det (g' u)¦ * y * indicat_real {x. h n x = y} (g u)) integrable_on S"
proof (rule measurable_bounded_by_integrable_imp_integrable)
have "(λx. indicat_real {x. h n x = y} (g x)) ∈ borel_measurable (lebesgue_on S)"
using h_lmeas S
by (auto simp: indicator_vimage [symmetric] borel_measurable_indicator_iff sets_restrict_space_iff)
then show "(λu. ¦eucl.det (g' u)¦ * y * indicat_real {x. h n x = y} (g u)) ∈ borel_measurable (lebesgue_on S)"
by (intro borel_measurable_times borel_measurable_abs borel_measurable_const borel_measurable_det_Jacobian [OF S der_g])
next
fix x
assume "x ∈ S"
then have "y * indicat_real {x. h n x = y} (g x) ≤ f (g x)"
using h_le_f nonneg_fg
by (smt (verit, best) indicator_times_eq_if(1) mem_Collect_eq mult.commute
vector_space_over_itself.scale_eq_0_iff)
with ‹y ≥ 0› show "norm (?D x * y * indicat_real {x. h n x = y} (g x)) ≤ ?D x * f(g x)"
by (simp add: abs_mult mult.assoc mult_left_mono)
qed (use S det_int_fg in auto)
qed
also have "… = integral S (λT. ¦eucl.det (g' T)¦ *
(∑y∈range (h n). y * indicat_real {x. h n x = y} (g T)))"
by (simp add: sum_distrib_left mult.assoc)
also have "… = ?rhs"
by (metis hn_eq)
finally show "integral (g ` S) (h n) ≤ ?rhs" .
qed
qed
have le: "integral S (λT. ¦eucl.det (g' T)¦ * h n (g T)) ≤ ?b" for n
proof (rule integral_le)
show "(λT. ¦eucl.det (g' T)¦ * h n (g T)) integrable_on S"
proof (rule measurable_bounded_by_integrable_imp_integrable)
have "(λT. ¦eucl.det (g' T)¦ *⇩R h n (g T)) ∈ borel_measurable (lebesgue_on S)"
proof (intro borel_measurable_scaleR borel_measurable_abs borel_measurable_det_Jacobian ‹S ∈ sets lebesgue›)
have eq: "{x ∈ S. f x ≤ a} = (⋃b ∈ (f ` S) ∩ atMost a. {x. f x = b} ∩ S)" for f and a::real
by auto
have "finite ((λx. h n (g x)) ` S ∩ {..a})" for a
by (force intro: finite_subset [OF _ fin_R])
with h_lmeas [of n] show "(λx. h n (g x)) ∈ borel_measurable (lebesgue_on S)"
apply (simp add: borel_measurable_vimage_halfspace_component_le ‹S ∈ sets lebesgue› sets_restrict_space_iff eq)
by (metis (mono_tags) SUP_inf sets.finite_UN)
qed (use der_g in blast)
then show "(λT. ¦eucl.det (g' T)¦ * h n (g T)) ∈ borel_measurable (lebesgue_on S)"
by simp
show "norm (?D x * h n (g x)) ≤ ?D x *⇩R f (g x)"
if "x ∈ S" for x
by (simp add: h_le_f mult_left_mono nonneg_h that)
qed (use S det_int_fg in auto)
show "?D x * h n (g x) ≤ ?D x * f (g x)" if "x ∈ S" for x
by (simp add: ‹x ∈ S› h_le_f mult_left_mono)
show "(λx. ?D x * f (g x)) integrable_on S"
using det_int_fg by blast
qed
have "f integrable_on g ` S ∧ (λk. integral (g ` S) (h k)) ⇢ integral (g ` S) f"
proof (rule monotone_convergence_increasing)
have "¦integral (g ` S) (h n)¦ ≤ integral S (λx. ?D x * f (g x))" for n
proof -
have "¦integral (g ` S) (h n)¦ = integral (g ` S) (h n)"
using hint by (simp add: integral_nonneg nonneg_h)
also have "… ≤ integral S (λx. ?D x * f (g x))"
using hint le by (meson order_trans)
finally show ?thesis .
qed
then show "bounded (range (λk. integral (g ` S) (h k)))"
by (force simp: bounded_iff)
qed (use h_inc lim hint in auto)
moreover have "integral (g ` S) (h n) ≤ integral S (λx. ?D x * f (g x))" for n
using hint by (blast intro: le order_trans)
ultimately show ?thesis
by (auto intro: Lim_bounded)
qed
lemma integral_on_image_ubound_nonneg:
fixes f :: "'a::euclidean_space ⇒ real"
assumes nonneg_fg: "⋀x. x ∈ S ⟹ 0 ≤ f(g x)"
and der_g: "⋀x. x ∈ S ⟹ (g has_derivative g' x) (at x within S)"
and intS: "(λx. ¦eucl.det (g' x)¦ * f(g x)) integrable_on S"
shows "f integrable_on (g ` S) ∧ integral (g ` S) f ≤ integral S (λx. ¦eucl.det (g' x)¦ * f(g x))"
(is "_ ∧ _ ≤ ?b")
proof -
let ?D = "λx. eucl.det (g' x)"
define S' where "S' ≡ {x ∈ S. ?D x * f(g x) ≠ 0}"
then have der_gS': "⋀x. x ∈ S' ⟹ (g has_derivative g' x) (at x within S')"
by (metis (mono_tags, lifting) der_g has_derivative_subset mem_Collect_eq subset_iff)
have "(λx. if x ∈ S then ¦?D x¦ * f (g x) else 0) integrable_on UNIV"
by (simp add: integrable_restrict_UNIV intS)
then have Df_borel: "(λx. if x ∈ S then ¦?D x¦ * f (g x) else 0) ∈ borel_measurable lebesgue"
using integrable_imp_measurable lebesgue_on_UNIV_eq by force
have S': "S' ∈ sets lebesgue"
proof -
from Df_borel borel_measurable_vimage_open [of _ UNIV]
have "{x. (if x ∈ S then ¦?D x¦ * f (g x) else 0) ∈ T} ∈ sets lebesgue"
if "open T" for T
using that unfolding lebesgue_on_UNIV_eq
by (fastforce simp add: dest!: spec)
then have "{x. (if x ∈ S then ¦?D x¦ * f (g x) else 0) ∈ -{0}} ∈ sets lebesgue"
using open_Compl by blast
then show ?thesis
by (simp add: S'_def conj_ac split: if_split_asm cong: conj_cong)
qed
then have gS': "g ` S' ∈ sets lebesgue"
proof (rule differentiable_image_in_sets_lebesgue)
show "g differentiable_on S'"
using der_g unfolding S'_def differentiable_def differentiable_on_def
by (blast intro: has_derivative_subset)
qed auto
have f: "f ∈ borel_measurable (lebesgue_on (g ` S'))"
proof (clarsimp simp add: borel_measurable_vimage_open)
fix T :: "real set"
assume "open T"
have "{x ∈ g ` S'. f x ∈ T} = g ` {x ∈ S'. f(g x) ∈ T}"
by blast
moreover have "g ` {x ∈ S'. f(g x) ∈ T} ∈ sets lebesgue"
proof (rule differentiable_image_in_sets_lebesgue)
let ?h = "λx. ¦?D x¦ * f (g x) /⇩R ¦?D x¦"
have "(λx. if x ∈ S' then ¦?D x¦ * f (g x) else 0) = (λx. if x ∈ S then ¦?D x¦ * f (g x) else 0)"
by (auto simp: S'_def)
also have "… ∈ borel_measurable lebesgue"
by (rule Df_borel)
finally have *: "(λx. ¦?D x¦ * f (g x)) ∈ borel_measurable (lebesgue_on S')"
by (simp add: borel_measurable_if_D)
have "(λv. eucl.det (g' v)) ∈ borel_measurable (lebesgue_on S')"
using S' borel_measurable_det_Jacobian der_gS' by blast
then have "?h ∈ borel_measurable (lebesgue_on S')"
using "*" borel_measurable_abs borel_measurable_inverse borel_measurable_scaleR by blast
moreover have "?h x = f(g x)" if "x ∈ S'" for x
using that by (auto simp: S'_def)
ultimately have "(λx. f(g x)) ∈ borel_measurable (lebesgue_on S')"
by (metis (no_types, lifting) measurable_lebesgue_cong)
then show "{x ∈ S'. f (g x) ∈ T} ∈ sets lebesgue"
by (simp add: ‹S' ∈ sets lebesgue› ‹open T› borel_measurable_vimage_open sets_restrict_space_iff)
show "g differentiable_on {x ∈ S'. f (g x) ∈ T}"
using der_g unfolding S'_def differentiable_def differentiable_on_def
by (blast intro: has_derivative_subset)
qed auto
ultimately have "{x ∈ g ` S'. f x ∈ T} ∈ sets lebesgue"
by metis
then show "{x ∈ g ` S'. f x ∈ T} ∈ sets (lebesgue_on (g ` S'))"
by (simp add: ‹g ` S' ∈ sets lebesgue› sets_restrict_space_iff)
qed
have intS': "(λx. ¦?D x¦ * f (g x)) integrable_on S'"
using intS
by (rule integrable_spike_set) (auto simp: S'_def intro: empty_imp_negligible)
have lebS': "{x ∈ S'. g x ∈ T} ∈ sets lebesgue" if "T ⊆ g ` S'" "T ∈ sets lebesgue" for T
proof -
have "g ∈ borel_measurable (lebesgue_on S')"
using der_gS' has_derivative_continuous_on S'
by (blast intro: continuous_imp_measurable_on_sets_lebesgue)
moreover have "{x ∈ S'. g x ∈ U} ∈ sets lebesgue" if "negligible U" "U ⊆ g ` S'" for U
proof (intro negligible_imp_sets negligible_differentiable_vimage that)
fix x
assume x: "x ∈ S'"
then have "linear (g' x)"
using der_gS' has_derivative_linear by blast
with x show "inj (g' x)"
using eucl.det_eq_0_iff by (auto simp: S'_def)
qed (use der_gS' in auto)
ultimately show ?thesis
using double_lebesgue_sets [OF S' gS' order_refl] that by blast
qed
have int_gS': "f integrable_on g ` S' ∧ integral (g ` S') f ≤ integral S' (λx. ¦?D x¦ * f(g x))"
using integral_on_image_ubound_weak [OF S' f nonneg_fg der_gS' intS' lebS'] S'_def by blast
have neg_det: "negligible (g ` {x ∈ S. eucl.det (g' x) = 0})"
proof (rule baby_Sard [OF order_refl], simp_all)
fix x
assume x: "x ∈ S ∧ eucl.det (g' x) = 0"
then show "(g has_derivative g' x) (at x within {x ∈ S. eucl.det (g' x) = 0})"
by (metis (no_types, lifting) der_g has_derivative_subset mem_Collect_eq subsetI)
have "linear (g' x)"
using ‹(g has_derivative g' x) _› has_derivative_linear by blast
then have "¬ inj (g' x)"
using x eucl.det_eq_0_iff by auto
then have "¬ surj (g' x)"
using ‹linear (g' x)› eucl.linear_surjective_imp_injective by auto
then have "g' x ` UNIV ≠ UNIV"
by (simp add: surj_def)
moreover have "subspace (g' x ` UNIV)"
using ‹linear (g' x)› linear_subspace_image subspace_UNIV by blast
ultimately show "dim (g' x ` UNIV) < DIM('a)"
using eucl.subspace_dim_equal [of "g' x ` UNIV" UNIV] subspace_UNIV eucl.dim_UNIV
by (metis eucl.dim_subset le_neq_implies_less subset_UNIV)
qed
then have negg: "negligible (g ` S - g ` {x ∈ S. ?D x ≠ 0})"
by (rule negligible_subset) (auto simp: S'_def)
have null: "g ` {x ∈ S. ?D x ≠ 0} - g ` S = {}"
by (auto simp: S'_def)
let ?F = "{x ∈ S. f (g x) ≠ 0}"
have eq: "g ` S' = g ` ?F ∩ g ` {x ∈ S. ?D x ≠ 0}"
by (auto simp: S'_def image_iff)
show ?thesis
proof
have "((λx. if x ∈ g ` ?F then f x else 0) integrable_on g ` {x ∈ S. ?D x ≠ 0})"
using int_gS' eq integrable_restrict_Int [where f=f]
by simp
then have "f integrable_on g ` {x ∈ S. ?D x ≠ 0}"
by (auto simp: image_iff elim!: integrable_eq)
then show "f integrable_on g ` S"
using negg null
by (auto intro: integrable_spike_set [OF _ empty_imp_negligible negligible_subset])
have "integral (g ` S) f = integral (g ` {x ∈ S. ?D x ≠ 0}) f"
using negg by (auto intro: negligible_subset integral_spike_set)
also have "… = integral (g ` {x ∈ S. ?D x ≠ 0}) (λx. if x ∈ g ` ?F then f x else 0)"
by (auto simp: image_iff intro!: integral_cong)
also have "… = integral (g ` S') f"
using eq integral_restrict_Int by simp
also have "… ≤ integral S' (λx. ¦?D x¦ * f(g x))"
by (metis int_gS')
also have "… ≤ ?b"
by (rule integral_subset_le [OF _ intS' intS]) (use nonneg_fg S'_def in auto)
finally show "integral (g ` S) f ≤ ?b" .
qed
qed
lemma absolutely_integrable_on_image_real:
fixes f :: "'a::euclidean_space ⇒ real" and g :: "'a ⇒ 'a"
assumes der_g: "⋀x. x ∈ S ⟹ (g has_derivative g' x) (at x within S)"
and intS: "(λx. ¦eucl.det (g' x)¦ * f(g x)) absolutely_integrable_on S"
shows "f absolutely_integrable_on (g ` S)"
proof -
let ?D = "λx. ¦eucl.det (g' x)¦ * f (g x)"
let ?N = "{x ∈ S. f (g x) < 0}" and ?P = "{x ∈ S. f (g x) > 0}"
have eq: "{x. (if x ∈ S then ?D x else 0) > 0} = {x ∈ S. ?D x > 0}"
"{x. (if x ∈ S then ?D x else 0) < 0} = {x ∈ S. ?D x < 0}"
by auto
have "?D integrable_on S"
using intS absolutely_integrable_on_def by blast
then have "(λx. if x ∈ S then ?D x else 0) integrable_on UNIV"
by (simp add: integrable_restrict_UNIV)
then have D_borel: "(λx. if x ∈ S then ?D x else 0) ∈ borel_measurable (lebesgue_on UNIV)"
using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
then have Dlt: "{x ∈ S. ?D x < 0} ∈ sets lebesgue"
unfolding borel_measurable_vimage_halfspace_component_lt
by (drule_tac x=0 in spec) (auto simp: eq)
from D_borel have Dgt: "{x ∈ S. ?D x > 0} ∈ sets lebesgue"
unfolding borel_measurable_vimage_halfspace_component_gt
by (drule_tac x=0 in spec) (auto simp: eq)
have dfgbm: "?D ∈ borel_measurable (lebesgue_on S)"
using intS absolutely_integrable_on_def integrable_imp_measurable by blast
have der_gN: "(g has_derivative g' x) (at x within ?N)" if "x ∈ ?N" for x
using der_g has_derivative_subset that by force
have "(λx. - f x) integrable_on g ` ?N ∧
integral (g ` ?N) (λx. - f x) ≤ integral ?N (λx. ¦eucl.det (g' x)¦ * - f (g x))"
proof (rule integral_on_image_ubound_nonneg [OF _ der_gN])
have 1: "?D integrable_on {x ∈ S. ?D x < 0}"
using Dlt
by (auto intro: set_lebesgue_integral_eq_integral [OF set_integrable_subset] intS)
have "uminus ∘ (λx. ¦eucl.det (g' x)¦ * - f (g x)) integrable_on ?N"
by (simp add: o_def mult_less_0_iff empty_imp_negligible integrable_spike_set [OF 1])
then show "(λx. ¦eucl.det (g' x)¦ * - f (g x)) integrable_on ?N"
by (simp add: integrable_neg_iff o_def)
qed auto
then have "f integrable_on g ` ?N"
by (simp add: integrable_neg_iff)
moreover have "g ` ?N = {y ∈ g ` S. f y < 0}"
by auto
ultimately have "f integrable_on {y ∈ g ` S. f y < 0}"
by simp
then have N: "f absolutely_integrable_on {y ∈ g ` S. f y < 0}"
by (rule absolutely_integrable_absolutely_integrable_ubound) auto
have der_gP: "(g has_derivative g' x) (at x within ?P)" if "x ∈ ?P" for x
using der_g has_derivative_subset that by force
have "f integrable_on g ` ?P ∧ integral (g ` ?P) f ≤ integral ?P ?D"
proof (rule integral_on_image_ubound_nonneg [OF _ der_gP])
show "?D integrable_on ?P"
proof (rule integrable_spike_set)
show "?D integrable_on {x ∈ S. 0 < ?D x}"
using Dgt
by (auto intro: set_lebesgue_integral_eq_integral [OF set_integrable_subset] intS)
qed (auto simp: zero_less_mult_iff empty_imp_negligible)
qed auto
then have "f integrable_on g ` ?P"
by metis
moreover have "g ` ?P = {y ∈ g ` S. f y > 0}"
by auto
ultimately have "f integrable_on {y ∈ g ` S. f y > 0}"
by simp
then have P: "f absolutely_integrable_on {y ∈ g ` S. f y > 0}"
by (rule absolutely_integrable_absolutely_integrable_lbound) auto
have "(λx. if x ∈ g ` S ∧ f x < 0 ∨ x ∈ g ` S ∧ 0 < f x then f x else 0) = (λx. if x ∈ g ` S then f x else 0)"
by auto
then show ?thesis
using absolutely_integrable_Un [OF N P] absolutely_integrable_restrict_UNIV [symmetric, where f=f]
by simp
qed
proposition absolutely_integrable_on_image:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" and g :: "'a ⇒ 'a"
assumes der_g: "⋀x. x ∈ S ⟹ (g has_derivative g' x) (at x within S)"
and intS: "(λx. ¦eucl.det (g' x)¦ *⇩R f(g x)) absolutely_integrable_on S"
shows "f absolutely_integrable_on (g ` S)"
proof (rule absolutely_integrable_componentwise)
fix b :: 'b assume "b ∈ Basis"
have "(λx. ¦eucl.det (g' x)¦ * (f (g x) ∙ b)) absolutely_integrable_on S"
using absolutely_integrable_component [OF intS, of b]
by auto
then show "(λx. f x ∙ b) absolutely_integrable_on g ` S"
by (auto intro: absolutely_integrable_on_image_real der_g)
qed
proposition integral_on_image_ubound:
fixes f :: "'a::euclidean_space ⇒ real" and g :: "'a ⇒ 'a"
assumes "⋀x. x ∈ S ⟹ 0 ≤ f(g x)"
and "⋀x. x ∈ S ⟹ (g has_derivative g' x) (at x within S)"
and "(λx. ¦eucl.det (g' x)¦ * f(g x)) integrable_on S"
shows "integral (g ` S) f ≤ integral S (λx. ¦eucl.det (g' x)¦ * f(g x))"
using integral_on_image_ubound_nonneg [OF assms] by simp
subsection‹Change-of-variables theorem›
text‹The classic change-of-variables theorem. We have two versions with quite general hypotheses,
the first that the transforming function has a continuous inverse, the second that the base set is
Lebesgue measurable.›
lemma cov_invertible_nonneg_le:
fixes f :: "'a::euclidean_space ⇒ real" and g :: "'a ⇒ 'a"
assumes der_g: "⋀x. x ∈ S ⟹ (g has_derivative g' x) (at x within S)"
and der_h: "⋀y. y ∈ T ⟹ (h has_derivative h' y) (at y within T)"
and f0: "⋀y. y ∈ T ⟹ 0 ≤ f y"
and hg: "⋀x. x ∈ S ⟹ g x ∈ T ∧ h(g x) = x"
and gh: "⋀y. y ∈ T ⟹ h y ∈ S ∧ g(h y) = y"
and id: "⋀y. y ∈ T ⟹ h' y ∘ g'(h y) = id"
shows "f integrable_on T ∧ (integral T f) ≤ b ⟷
(λx. ¦eucl.det (g' x)¦ * f(g x)) integrable_on S ∧
integral S (λx. ¦eucl.det (g' x)¦ * f(g x)) ≤ b"
(is "?lhs = ?rhs")
proof -
have Teq: "T = g`S" and Seq: "S = h`T"
using hg gh image_iff by fastforce+
have gS: "g differentiable_on S"
by (meson der_g differentiable_def differentiable_on_def)
let ?D = "λx. ¦eucl.det (g' x)¦ * f (g x)"
show ?thesis
proof
assume ?lhs
then have fT: "f integrable_on T" and intf: "integral T f ≤ b"
by blast+
show ?rhs
proof
let ?fgh = "λx. ¦eucl.det (h' x)¦ * (¦eucl.det (g' (h x))¦ * f (g (h x)))"
have ddf: "?fgh x = f x"
if "x ∈ T" for x
proof -
have lin_h: "linear (h' x)" and lin_g: "linear (g' (h x))"
using der_h that gh der_g has_derivative_linear by blast+
have "h' x ∘ g'(h x) = id"
using id that by blast
then have "eucl.det (h' x ∘ g' (h x)) = 1"
by auto
then have "eucl.det (h' x) * eucl.det (g' (h x)) = 1"
by (simp add: eucl.det_compose [OF lin_h lin_g])
then have "¦eucl.det (h' x)¦ * ¦eucl.det (g' (h x))¦ = 1"
by (metis abs_1 abs_mult)
then show ?thesis
by (simp add: gh that)
qed
have "?D integrable_on (h ` T)"
proof (intro set_lebesgue_integral_eq_integral absolutely_integrable_on_image_real)
show "(λx. ?fgh x) absolutely_integrable_on T"
by (smt (verit, del_insts) abs_absolutely_integrableI_1 ddf f0 fT integrable_eq)
qed (use der_h in auto)
with Seq show "(λx. ?D x) integrable_on S"
by simp
have "integral S (λx. ?D x) ≤ integral T (λx. ?fgh x)"
unfolding Seq
proof (rule integral_on_image_ubound)
show "(λx. ?fgh x) integrable_on T"
using ddf fT integrable_eq by force
qed (use f0 gh der_h in auto)
also have "… = integral T f"
by (force simp: ddf intro: integral_cong)
finally show "integral S (λx. ?D x) ≤ b"
using intf by linarith
qed
next
assume R: ?rhs
then have "f integrable_on g ` S"
by (metis (full_types) der_g f0 hg integral_on_image_ubound_nonneg)
moreover have "integral (g ` S) f ≤ integral S (λx. ?D x)"
by (rule integral_on_image_ubound [OF f0 der_g]) (use R Teq in auto)
ultimately show ?lhs
using R by (simp add: Teq)
qed
qed
lemma cov_invertible_nonneg_eq:
fixes f :: "'a::euclidean_space ⇒ real" and g :: "'a ⇒ 'a"
assumes "⋀x. x ∈ S ⟹ (g has_derivative g' x) (at x within S)"
and "⋀y. y ∈ T ⟹ (h has_derivative h' y) (at y within T)"
and "⋀y. y ∈ T ⟹ 0 ≤ f y"
and "⋀x. x ∈ S ⟹ g x ∈ T ∧ h(g x) = x"
and "⋀y. y ∈ T ⟹ h y ∈ S ∧ g(h y) = y"
and "⋀y. y ∈ T ⟹ h' y ∘ g'(h y) = id"
shows "((λx. ¦eucl.det (g' x)¦ * f(g x)) has_integral b) S ⟷ (f has_integral b) T"
using cov_invertible_nonneg_le [OF assms]
by (simp add: has_integral_iff) (meson eq_iff)
lemma cov_invertible_real:
fixes f :: "'a::euclidean_space ⇒ real" and g :: "'a ⇒ 'a"
assumes der_g: "⋀x. x ∈ S ⟹ (g has_derivative g' x) (at x within S)"
and der_h: "⋀y. y ∈ T ⟹ (h has_derivative h' y) (at y within T)"
and hg: "⋀x. x ∈ S ⟹ g x ∈ T ∧ h(g x) = x"
and gh: "⋀y. y ∈ T ⟹ h y ∈ S ∧ g(h y) = y"
and id: "⋀y. y ∈ T ⟹ h' y ∘ g'(h y) = id"
shows "(λx. ¦eucl.det(g' x)¦ * f(g x)) absolutely_integrable_on S ∧
integral S (λx. ¦eucl.det(g' x)¦ * f(g x)) = b ⟷
f absolutely_integrable_on T ∧ integral T f = b"
(is "?lhs = ?rhs")
proof -
have Teq: "T = g`S" and Seq: "S = h`T"
using hg gh image_iff by fastforce+
let ?DP = "λx. ¦eucl.det(g' x)¦ * f(g x)" and ?DN = "λx. ¦eucl.det(g' x)¦ * -f(g x)"
have "+": "(?DP has_integral b) {x ∈ S. f (g x) > 0} ⟷ (f has_integral b) {y ∈ T. f y > 0}" for b
proof (rule cov_invertible_nonneg_eq)
have *: "(λx. f (g x)) -` Y ∩ {x ∈ S. f (g x) > 0}
= ((λx. f (g x)) -` Y ∩ S) ∩ {x ∈ S. f (g x) > 0}" for Y
by auto
show "(g has_derivative g' x) (at x within {x ∈ S. f (g x) > 0})" if "x ∈ {x ∈ S. f (g x) > 0}" for x
using that der_g has_derivative_subset by fastforce
show "(h has_derivative h' y) (at y within {y ∈ T. f y > 0})" if "y ∈ {y ∈ T. f y > 0}" for y
using that der_h has_derivative_subset by fastforce
qed (use gh hg id in auto)
have "-": "(?DN has_integral b) {x ∈ S. f (g x) < 0} ⟷ ((λx. - f x) has_integral b) {y ∈ T. f y < 0}" for b
proof (rule cov_invertible_nonneg_eq)
have *: "(λx. - f (g x)) -` y ∩ {x ∈ S. f (g x) < 0}
= ((λx. f (g x)) -` uminus ` y ∩ S) ∩ {x ∈ S. f (g x) < 0}" for y
using image_iff by fastforce
show "(g has_derivative g' x) (at x within {x ∈ S. f (g x) < 0})" if "x ∈ {x ∈ S. f (g x) < 0}" for x
using that der_g has_derivative_subset by fastforce
show "(h has_derivative h' y) (at y within {y ∈ T. f y < 0})" if "y ∈ {y ∈ T. f y < 0}" for y
using that der_h has_derivative_subset by fastforce
qed (use gh hg id in auto)
show ?thesis
proof
assume LHS: ?lhs
have eq: "{x. (if x ∈ S then ?DP x else 0) > 0} = {x ∈ S. ?DP x > 0}"
"{x. (if x ∈ S then ?DP x else 0) < 0} = {x ∈ S. ?DP x < 0}"
by auto
have "?DP integrable_on S"
using LHS absolutely_integrable_on_def by blast
then have "(λx. if x ∈ S then ?DP x else 0) integrable_on UNIV"
by (simp add: integrable_restrict_UNIV)
then have D_borel: "(λx. if x ∈ S then ?DP x else 0) ∈ borel_measurable (lebesgue_on UNIV)"
using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
then have SN: "{x ∈ S. ?DP x < 0} ∈ sets lebesgue"
unfolding borel_measurable_vimage_halfspace_component_lt
by (drule_tac x=0 in spec) (auto simp: eq)
from D_borel have SP: "{x ∈ S. ?DP x > 0} ∈ sets lebesgue"
unfolding borel_measurable_vimage_halfspace_component_gt
by (drule_tac x=0 in spec) (auto simp: eq)
have "?DP absolutely_integrable_on {x ∈ S. ?DP x > 0}"
using LHS by (fast intro!: set_integrable_subset [OF _, of _ S] SP)
then have aP: "?DP absolutely_integrable_on {x ∈ S. f (g x) > 0}"
by (rule absolutely_integrable_spike_set) (auto simp: zero_less_mult_iff empty_imp_negligible)
have "?DP absolutely_integrable_on {x ∈ S. ?DP x < 0}"
using LHS by (fast intro!: set_integrable_subset [OF _, of _ S] SN)
then have aN: "?DP absolutely_integrable_on {x ∈ S. f (g x) < 0}"
by (rule absolutely_integrable_spike_set) (auto simp: mult_less_0_iff empty_imp_negligible)
have fN: "f integrable_on {y ∈ T. f y < 0}"
"integral {y ∈ T. f y < 0} f = integral {x ∈ S. f (g x) < 0} ?DP"
using "-" [of "integral {x ∈ S. f(g x) < 0} ?DN"] aN
by (auto simp: set_lebesgue_integral_eq_integral has_integral_iff integrable_neg_iff)
have faN: "f absolutely_integrable_on {y ∈ T. f y < 0}"
proof (rule absolutely_integrable_integrable_bound)
show "(λx. - f x) integrable_on {y ∈ T. f y < 0}"
using fN by (auto simp: integrable_neg_iff)
qed (use fN in auto)
have fP: "f integrable_on {y ∈ T. f y > 0}"
"integral {y ∈ T. f y > 0} f = integral {x ∈ S. f (g x) > 0} ?DP"
using "+" [of "integral {x ∈ S. f(g x) > 0} ?DP"] aP
by (auto simp: set_lebesgue_integral_eq_integral has_integral_iff integrable_neg_iff)
have faP: "f absolutely_integrable_on {y ∈ T. f y > 0}"
using fP(1) nonnegative_absolutely_integrable_1 by fastforce
have fa: "f absolutely_integrable_on ({y ∈ T. f y < 0} ∪ {y ∈ T. f y > 0})"
by (rule absolutely_integrable_Un [OF faN faP])
show ?rhs
proof
have eq: "((if x ∈ T ∧ f x < 0 ∨ x ∈ T ∧ 0 < f x then 1 else 0) * f x)
= (if x ∈ T then 1 else 0) * f x" for x
by auto
show "f absolutely_integrable_on T"
using fa by (simp add: indicator_def of_bool_def set_integrable_def eq)
have [simp]: "{y ∈ T. f y < 0} ∩ {y ∈ T. 0 < f y} = {}" for T and f :: "'a ⇒ real"
by auto
have "integral T f = integral ({y ∈ T. f y < 0} ∪ {y ∈ T. f y > 0}) f"
by (intro empty_imp_negligible integral_spike_set) (auto simp: eq)
also have "… = integral {y ∈ T. f y < 0} f + integral {y ∈ T. f y > 0} f"
using fN fP by simp
also have "… = integral {x ∈ S. f (g x) < 0} ?DP + integral {x ∈ S. 0 < f (g x)} ?DP"
by (simp add: fN fP)
also have "… = integral ({x ∈ S. f (g x) < 0} ∪ {x ∈ S. 0 < f (g x)}) ?DP"
using aP aN by (simp add: set_lebesgue_integral_eq_integral)
also have "… = integral S ?DP"
by (intro empty_imp_negligible integral_spike_set) auto
also have "… = b"
using LHS by simp
finally show "integral T f = b" .
qed
next
assume RHS: ?rhs
have eq: "{x. (if x ∈ T then f x else 0) > 0} = {x ∈ T. f x > 0}"
"{x. (if x ∈ T then f x else 0) < 0} = {x ∈ T. f x < 0}"
by auto
have "f integrable_on T"
using RHS absolutely_integrable_on_def by blast
then have "(λx. if x ∈ T then f x else 0) integrable_on UNIV"
by (simp add: integrable_restrict_UNIV)
then have D_borel: "(λx. if x ∈ T then f x else 0) ∈ borel_measurable (lebesgue_on UNIV)"
using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
then have TN: "{x ∈ T. f x < 0} ∈ sets lebesgue"
unfolding borel_measurable_vimage_halfspace_component_lt
by (drule_tac x=0 in spec) (auto simp: eq)
from D_borel have TP: "{x ∈ T. f x > 0} ∈ sets lebesgue"
unfolding borel_measurable_vimage_halfspace_component_gt
by (drule_tac x=0 in spec) (auto simp: eq)
have aint: "f absolutely_integrable_on {y. y ∈ T ∧ 0 < (f y)}"
"f absolutely_integrable_on {y. y ∈ T ∧ (f y) < 0}"
and intT: "integral T f = b"
using set_integrable_subset [of _ T] TP TN RHS by blast+
show ?lhs
proof
have fN: "f integrable_on {v ∈ T. f v < 0}"
using absolutely_integrable_on_def aint by blast
then have DN: "(?DN has_integral integral {y ∈ T. f y < 0} (λx. - f x)) {x ∈ S. f (g x) < 0}"
using "-" [of "integral {y ∈ T. f y < 0} (λx. - f x)"]
by (simp add: has_integral_neg_iff integrable_integral)
have aDN: "?DP absolutely_integrable_on {x ∈ S. f (g x) < 0}"
apply (rule absolutely_integrable_integrable_bound [where g = ?DN])
using DN hg by (fastforce simp: abs_mult integrable_neg_iff)+
have fP: "f integrable_on {v ∈ T. f v > 0}"
using absolutely_integrable_on_def aint by blast
then have DP: "(?DP has_integral integral {y ∈ T. f y > 0} f) {x ∈ S. f (g x) > 0}"
using "+" [of "integral {y ∈ T. f y > 0} f"]
by (simp add: has_integral_neg_iff integrable_integral)
have aDP: "?DP absolutely_integrable_on {x ∈ S. f (g x) > 0}"
apply (rule absolutely_integrable_integrable_bound [where g = ?DP])
using DP hg by (fastforce simp: integrable_neg_iff)+
have eq: "(if x ∈ S then 1 else 0) * ?DP x = (if x ∈ S ∧ f (g x) < 0 ∨ x ∈ S ∧ f (g x) > 0 then 1 else 0) * ?DP x" for x
by force
have "?DP absolutely_integrable_on ({x ∈ S. f (g x) < 0} ∪ {x ∈ S. f (g x) > 0})"
by (rule absolutely_integrable_Un [OF aDN aDP])
then show I: "?DP absolutely_integrable_on S"
by (simp add: indicator_def of_bool_def eq set_integrable_def)
have [simp]: "{y ∈ S. f y < 0} ∩ {y ∈ S. 0 < f y} = {}" for S and f :: "'a ⇒ real"
by auto
have "integral S ?DP = integral ({x ∈ S. f (g x) < 0} ∪ {x ∈ S. f (g x) > 0}) ?DP"
by (intro empty_imp_negligible integral_spike_set) auto
also have "… = integral {x ∈ S. f (g x) < 0} ?DP + integral {x ∈ S. 0 < f (g x)} ?DP"
using aDN aDP by (simp add: set_lebesgue_integral_eq_integral)
also have "… = - integral {y ∈ T. f y < 0} (λx. - f x) + integral {y ∈ T. f y > 0} f"
using DN DP by (auto simp: has_integral_iff)
also have "… = integral ({x ∈ T. f x < 0} ∪ {x ∈ T. 0 < f x}) f"
by (simp add: fN fP)
also have "… = integral T f"
by (intro empty_imp_negligible integral_spike_set) auto
also have "… = b"
using intT by simp
finally show "integral S ?DP = b" .
qed
qed
qed
lemma cv_inv_version3:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" and g :: "'a ⇒ 'a"
assumes der_g: "⋀x. x ∈ S ⟹ (g has_derivative g' x) (at x within S)"
and der_h: "⋀y. y ∈ T ⟹ (h has_derivative h' y) (at y within T)"
and hg: "⋀x. x ∈ S ⟹ g x ∈ T ∧ h(g x) = x"
and gh: "⋀y. y ∈ T ⟹ h y ∈ S ∧ g(h y) = y"
and id: "⋀y. y ∈ T ⟹ h' y ∘ g'(h y) = id"
shows "(λx. ¦eucl.det(g' x)¦ *⇩R f(g x)) absolutely_integrable_on S ∧
integral S (λx. ¦eucl.det(g' x)¦ *⇩R f(g x)) = b
⟷ f absolutely_integrable_on T ∧ integral T f = b"
proof -
let ?D = "λx. ¦eucl.det(g' x)¦ *⇩R f(g x)"
have "((λx. ¦eucl.det(g' x)¦ * (f(g x) ∙ i)) absolutely_integrable_on S ∧ integral S (λx. ¦eucl.det(g' x)¦ * (f(g x) ∙ i)) = b ∙ i) ⟷
((λx. f x ∙ i) absolutely_integrable_on T ∧ integral T (λx. f x ∙ i) = b ∙ i)" for i
by (rule cov_invertible_real [OF der_g der_h hg gh id])
then have "?D absolutely_integrable_on S ∧ (?D has_integral b) S ⟷
f absolutely_integrable_on T ∧ (f has_integral b) T"
unfolding absolutely_integrable_componentwise_iff [where f=f] has_integral_componentwise_iff [of f]
absolutely_integrable_componentwise_iff [where f="?D"] has_integral_componentwise_iff [of ?D]
by (auto simp: all_conj_distrib has_integral_iff set_lebesgue_integral_eq_integral dest: absolutely_integrable_on_def [THEN iffD1, THEN conjunct1])
then show ?thesis
using absolutely_integrable_on_def by blast
qed
lemma cv_inv_version4:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" and g :: "'a ⇒ 'a"
assumes der_g: "⋀x. x ∈ S ⟹ (g has_derivative g' x) (at x within S) ∧ eucl.det(g' x) ≠ 0"
and hg: "⋀x. x ∈ S ⟹ continuous_on (g ` S) h ∧ h(g x) = x"
shows "(λx. ¦eucl.det(g' x)¦ *⇩R f(g x)) absolutely_integrable_on S ∧
integral S (λx. ¦eucl.det(g' x)¦ *⇩R f(g x)) = b
⟷ f absolutely_integrable_on (g ` S) ∧ integral (g ` S) f = b"
proof -
have "∃h'. x ∈ S
⟶ (g has_derivative g' x) (at x within S) ∧ linear h' ∧ g' x ∘ h' = id ∧ h' ∘ g' x = id" for x
proof (cases "x ∈ S")
case True
then have "linear (g' x)" "inj (g' x)" "(g has_derivative g' x) (at x within S)"
using der_g has_derivative_linear eucl.det_eq_0_iff by blast+
then have "linear (inv (g' x))" "g' x ∘ inv (g' x) = id" "inv (g' x) ∘ g' x = id"
using eucl.inj_linear_imp_inv_linear inv_o_cancel surj_iff eucl.linear_inj_imp_surj
by blast+
then show ?thesis
using ‹(g has_derivative g' x) (at x within S)› by blast
qed auto
then obtain h' where h':
"⋀x. x ∈ S
⟹ (g has_derivative g' x) (at x within S) ∧
linear (h' x) ∧ g' x ∘ (h' x) = id ∧ (h' x) ∘ g' x = id"
by metis
show ?thesis
proof (rule cv_inv_version3)
show "⋀y. y ∈ g ` S ⟹ (h has_derivative h' (h y)) (at y within g ` S)"
using h' hg
by (force simp: continuous_on_eq_continuous_within intro!: has_derivative_inverse_within)
qed (use h' hg in auto)
qed
theorem has_absolute_integral_change_of_variables_invertible:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" and g :: "'a ⇒ 'a"
assumes der_g: "⋀x. x ∈ S ⟹ (g has_derivative g' x) (at x within S)"
and hg: "⋀x. x ∈ S ⟹ h(g x) = x"
and conth: "continuous_on (g ` S) h"
shows "(λx. ¦eucl.det(g' x)¦ *⇩R f(g x)) absolutely_integrable_on S ∧ integral S (λx. ¦eucl.det(g' x)¦ *⇩R f(g x)) = b ⟷
f absolutely_integrable_on (g ` S) ∧ integral (g ` S) f = b"
(is "?lhs = ?rhs")
proof -
let ?S = "{x ∈ S. eucl.det(g' x) ≠ 0}" and ?D = "λx. ¦eucl.det(g' x)¦ *⇩R f(g x)"
have *: "?D absolutely_integrable_on ?S ∧ integral ?S ?D = b
⟷ f absolutely_integrable_on (g ` ?S) ∧ integral (g ` ?S) f = b"
proof (rule cv_inv_version4)
show "(g has_derivative g' x) (at x within ?S) ∧ eucl.det(g' x) ≠ 0"
if "x ∈ ?S" for x
using der_g that has_derivative_subset that by fastforce
show "continuous_on (g ` ?S) h ∧ h (g x) = x"
if "x ∈ ?S" for x
using that continuous_on_subset [OF conth] by (simp add: hg image_mono)
qed
have "negligible (g ` {x ∈ S. eucl.det(g' x) = 0})"
proof (rule baby_Sard [OF order_refl], simp_all)
fix x
assume x: "x ∈ S ∧ eucl.det (g' x) = 0"
then show "(g has_derivative g' x) (at x within {x ∈ S. eucl.det (g' x) = 0})"
by (metis (no_types, lifting) der_g has_derivative_subset mem_Collect_eq subsetI)
have "linear (g' x)"
using ‹(g has_derivative g' x) _› has_derivative_linear by blast
then have "g' x ` UNIV ≠ UNIV"
using det_eq_0_iff linear_surj_imp_inj x by blast
moreover have "subspace (g' x ` UNIV)"
using ‹linear (g' x)› linear_subspace_image subspace_UNIV by blast
ultimately show "dim (g' x ` UNIV) < DIM('a)"
using eucl.subspace_dim_equal [of "g' x ` UNIV" UNIV] subspace_UNIV eucl.dim_UNIV
by (metis eucl.dim_subset le_neq_implies_less subset_UNIV)
qed
then have neg: "negligible {x ∈ g ` S. x ∉ g ` ?S ∧ f x ≠ 0}"
by (auto intro: negligible_subset)
have [simp]: "{x ∈ g ` ?S. x ∉ g ` S ∧ f x ≠ 0} = {}"
by auto
have "?D absolutely_integrable_on ?S ∧ integral ?S ?D = b
⟷ ?D absolutely_integrable_on S ∧ integral S ?D = b"
by (intro conj_cong absolutely_integrable_spike_set_eq)
(auto simp: integral_spike_set empty_imp_negligible neg)
moreover
have "f absolutely_integrable_on (g ` ?S) ∧ integral (g ` ?S) f = b
⟷ f absolutely_integrable_on (g ` S) ∧ integral (g ` S) f = b"
by (auto intro!: conj_cong absolutely_integrable_spike_set_eq integral_spike_set neg)
ultimately show ?thesis
using "*" by blast
qed
theorem has_absolute_integral_change_of_variables_compact:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" and g :: "'a ⇒ 'a"
assumes "compact S"
and der_g: "⋀x. x ∈ S ⟹ (g has_derivative g' x) (at x within S)"
and inj: "inj_on g S"
shows "((λx. ¦eucl.det(g' x)¦ *⇩R f(g x)) absolutely_integrable_on S ∧
integral S (λx. ¦eucl.det(g' x)¦ *⇩R f(g x)) = b
⟷ f absolutely_integrable_on (g ` S) ∧ integral (g ` S) f = b)"
proof -
obtain h where hg: "⋀x. x ∈ S ⟹ h(g x) = x"
using inj by (metis the_inv_into_f_f)
have conth: "continuous_on (g ` S) h"
by (metis ‹compact S› continuous_on_inv der_g has_derivative_continuous_on hg)
show ?thesis
by (rule has_absolute_integral_change_of_variables_invertible [OF der_g hg conth])
qed
lemma integral_countable_UN:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
and s :: "nat ⇒ 'a set"
assumes f: "f absolutely_integrable_on (⋃ (range s))"
and s: "⋀m. s m ∈ sets lebesgue"
shows ai: "f absolutely_integrable_on (⋃ (s ` {..n}))"
and "(λn. integral (⋃ (s ` {..n})) f) ⇢ integral (⋃ (range s)) f" (is "?F ⇢ ?I")
proof -
show fU: "f absolutely_integrable_on (⋃m≤n. s m)" for n
using assms by (blast intro: set_integrable_subset [OF f])
have fint: "f integrable_on (⋃ (range s))"
using absolutely_integrable_on_def f by blast
let ?h = "λx. if x ∈ ⋃(s ` UNIV) then norm(f x) else 0"
have "(λn. integral UNIV (λx. if x ∈ (⋃m≤n. s m) then f x else 0))
⇢ integral UNIV (λx. if x ∈ ⋃(s ` UNIV) then f x else 0)"
proof (rule dominated_convergence)
show "(λx. if x ∈ (⋃m≤n. s m) then f x else 0) integrable_on UNIV" for n
unfolding integrable_restrict_UNIV
using fU absolutely_integrable_on_def by blast
show "(λx. if x ∈ ⋃(s ` UNIV) then norm(f x) else 0) integrable_on UNIV"
by (metis (no_types) absolutely_integrable_on_def f integrable_restrict_UNIV)
show "⋀x. (λn. if x ∈ (⋃m≤n. s m) then f x else 0)
⇢ (if x ∈ ⋃(s ` UNIV) then f x else 0)"
by (force intro: tendsto_eventually eventually_sequentiallyI)
qed auto
then show "?F ⇢ ?I"
by (simp only: integral_restrict_UNIV)
qed
lemma has_absolute_integral_change_of_variables_compact_family:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" and g :: "'a ⇒ 'a"
assumes compact: "⋀n::nat. compact (F n)"
and der_g: "⋀x. x ∈ (⋃n. F n) ⟹ (g has_derivative g' x) (at x within (⋃n. F n))"
and inj: "inj_on g (⋃n. F n)"
shows "((λx. ¦eucl.det(g' x)¦ *⇩R f(g x)) absolutely_integrable_on (⋃n. F n) ∧
integral (⋃n. F n) (λx. ¦eucl.det(g' x)¦ *⇩R f(g x)) = b
⟷ f absolutely_integrable_on (g ` (⋃n. F n)) ∧ integral (g ` (⋃n. F n)) f = b)"
proof -
let ?D = "λx. ¦eucl.det(g' x)¦ *⇩R f (g x)"
let ?U = "λn. ⋃m≤n. F m"
let ?lift = "vec::real⇒real^1"
have F_leb: "F m ∈ sets lebesgue" for m
by (simp add: compact borel_compact)
have iff: "(λx. ¦eucl.det(g' x)¦ *⇩R f (g x)) absolutely_integrable_on (?U n) ∧
integral (?U n) (λx. ¦eucl.det(g' x)¦ *⇩R f (g x)) = b
⟷ f absolutely_integrable_on (g ` (?U n)) ∧ integral (g ` (?U n)) f = b" for n b and f :: "'a ⇒ 'c::euclidean_space"
proof (rule has_absolute_integral_change_of_variables_compact)
show "compact (?U n)"
by (simp add: compact compact_UN)
show "(g has_derivative g' x) (at x within (?U n))"
if "x ∈ ?U n" for x
using that by (blast intro!: has_derivative_subset [OF der_g])
show "inj_on g (?U n)"
using inj by (auto simp: inj_on_def)
qed
show ?thesis
unfolding image_UN
proof safe
assume DS: "?D absolutely_integrable_on (⋃n. F n)"
and b: "b = integral (⋃n. F n) ?D"
have DU: "⋀n. ?D absolutely_integrable_on (?U n)"
"(λn. integral (?U n) ?D) ⇢ integral (⋃n. F n) ?D"
using integral_countable_UN [where s=F and f="?D"] DS F_leb by auto
with iff have fag: "f absolutely_integrable_on g ` (?U n)"
and fg_int: "integral (⋃m≤n. g ` F m) f = integral (?U n) ?D" for n
by (auto simp: image_UN)
let ?h = "λx. if x ∈ (⋃m. g ` F m) then norm(f x) else 0"
have "(λx. if x ∈ (⋃m. g ` F m) then f x else 0) absolutely_integrable_on UNIV"
proof (rule dominated_convergence_absolutely_integrable)
show "(λx. if x ∈ (⋃m≤k. g ` F m) then f x else 0) absolutely_integrable_on UNIV" for k
unfolding absolutely_integrable_restrict_UNIV
using fag by (simp add: image_UN)
let ?nf = "λn x. if x ∈ (⋃m≤n. g ` F m) then norm(f x) else 0"
show "?h integrable_on UNIV"
proof (rule monotone_convergence_increasing [THEN conjunct1])
show "?nf k integrable_on UNIV" for k
using fag
unfolding integrable_restrict_UNIV absolutely_integrable_on_def by (simp add: image_UN)
{ fix n
have "(norm ∘ ?D) absolutely_integrable_on ?U n"
by (intro absolutely_integrable_norm DU)
then have "integral (g ` ?U n) (norm ∘ f) = integral (?U n) (norm ∘ ?D)"
using iff [of n "norm ∘ f" "integral (?U n) (λx. ¦eucl.det(g' x)¦ * norm (f (g x)))"]
by (auto simp: o_def)
}
moreover have "bounded (range (λk. integral (?U k) (norm ∘ ?D)))"
unfolding bounded_iff
proof (rule exI, clarify)
fix k
show "norm (integral (?U k) (norm ∘ ?D)) ≤ integral (⋃n. F n) (norm ∘ ?D)"
unfolding integral_restrict_UNIV [of _ "norm ∘ ?D", symmetric]
proof (rule integral_norm_bound_integral)
show "(λx. if x ∈ ⋃ (F ` {..k}) then (norm ∘ ?D) x else 0) integrable_on UNIV"
"(λx. if x ∈ (⋃n. F n) then (norm ∘ ?D) x else 0) integrable_on UNIV"
using DU(1) DS
unfolding absolutely_integrable_on_def o_def integrable_restrict_UNIV by auto
qed auto
qed
ultimately show "bounded (range (λk. integral UNIV (?nf k)))"
by (simp add: integral_restrict_UNIV image_UN [symmetric] o_def)
next
show "(λk. if x ∈ (⋃m≤k. g ` F m) then norm (f x) else 0)
⇢ (if x ∈ (⋃m. g ` F m) then norm (f x) else 0)" for x
by (force intro: tendsto_eventually eventually_sequentiallyI)
qed auto
next
show "(λk. if x ∈ (⋃m≤k. g ` F m) then f x else 0)
⇢ (if x ∈ (⋃m. g ` F m) then f x else 0)" for x
proof clarsimp
fix m y
assume "y ∈ F m"
show "(λk. if ∃x∈{..k}. g y ∈ g ` F x then f (g y) else 0) ⇢ f (g y)"
using ‹y ∈ F m› by (force intro: tendsto_eventually eventually_sequentiallyI [of m])
qed
qed auto
then show fai: "f absolutely_integrable_on (⋃m. g ` F m)"
using absolutely_integrable_restrict_UNIV by blast
show "integral ((⋃x. g ` F x)) f = integral (⋃n. F n) ?D"
proof (rule LIMSEQ_unique)
show "(λn. integral (?U n) ?D) ⇢ integral (⋃x. g ` F x) f"
unfolding fg_int [symmetric]
proof (rule integral_countable_UN [OF fai])
show "g ` F m ∈ sets lebesgue" for m
proof (rule differentiable_image_in_sets_lebesgue [OF F_leb])
show "g differentiable_on F m"
by (meson der_g differentiableI UnionI differentiable_on_def differentiable_on_subset rangeI subsetI)
qed auto
qed
qed (use DU in metis)
next
assume fs: "f absolutely_integrable_on (⋃x. g ` F x)"
and b: "b = integral ((⋃x. g ` F x)) f"
have gF_leb: "g ` F m ∈ sets lebesgue" for m
proof (rule differentiable_image_in_sets_lebesgue [OF F_leb])
show "g differentiable_on F m"
using der_g unfolding differentiable_def differentiable_on_def
by (meson Sup_upper UNIV_I UnionI has_derivative_subset image_eqI)
qed auto
have fgU: "⋀n. f absolutely_integrable_on (⋃m≤n. g ` F m)"
"(λn. integral (⋃m≤n. g ` F m) f) ⇢ integral (⋃m. g ` F m) f"
using integral_countable_UN [OF fs gF_leb] by auto
with iff have DUn: "?D absolutely_integrable_on ?U n"
and D_int: "integral (?U n) ?D = integral (⋃m≤n. g ` F m) f" for n
by (auto simp: image_UN)
let ?h = "λx. if x ∈ (⋃n. F n) then norm(?D x) else 0"
have "(λx. if x ∈ (⋃n. F n) then ?D x else 0) absolutely_integrable_on UNIV"
proof (rule dominated_convergence_absolutely_integrable)
show "(λx. if x ∈ ?U k then ?D x else 0) absolutely_integrable_on UNIV" for k
unfolding absolutely_integrable_restrict_UNIV using DUn by simp
let ?nD = "λn x. if x ∈ ?U n then norm(?D x) else 0"
show "?h integrable_on UNIV"
proof (rule monotone_convergence_increasing [THEN conjunct1])
show "?nD k integrable_on UNIV" for k
using DUn
unfolding integrable_restrict_UNIV absolutely_integrable_on_def by (simp add: image_UN)
{ fix n::nat
have "(norm ∘ f) absolutely_integrable_on (⋃m≤n. g ` F m)"
using absolutely_integrable_norm fgU by blast
then have "integral (?U n) (norm ∘ ?D) = integral (g ` ?U n) (norm ∘ f)"
using iff [of n "norm ∘ f" "integral (g ` ?U n) (norm ∘ f)"]
unfolding image_UN by (auto simp: o_def)
}
moreover have "bounded (range (λk. integral (g ` ?U k) (norm ∘ f)))"
unfolding bounded_iff
proof (intro exI, clarify)
fix k
show "norm (integral (g ` ?U k) (norm ∘ f)) ≤ integral (g ` (⋃n. F n)) (norm ∘ f)"
unfolding integral_restrict_UNIV [of _ "norm ∘ f", symmetric]
proof (rule integral_norm_bound_integral)
show "(λx. if x ∈ g ` ?U k then (norm ∘ f) x else 0) integrable_on UNIV"
"(λx. if x ∈ g ` (⋃n. F n) then (norm ∘ f) x else 0) integrable_on UNIV"
using fgU fs
unfolding absolutely_integrable_on_def o_def integrable_restrict_UNIV
by (auto simp: image_UN)
qed auto
qed
ultimately show "bounded (range (λk. integral UNIV (?nD k)))"
unfolding integral_restrict_UNIV image_UN [symmetric] o_def by simp
next
show "(λk. if x ∈ ?U k then norm (?D x) else 0) ⇢ (if x ∈ (⋃n. F n) then norm (?D x) else 0)" for x
by (force intro: tendsto_eventually eventually_sequentiallyI)
qed auto
next
show "(λk. if x ∈ ?U k then ?D x else 0) ⇢ (if x ∈ (⋃n. F n) then ?D x else 0)" for x
proof clarsimp
fix n
assume "x ∈ F n"
then show "(λm. if ∃j∈{..m}. x ∈ F j then ?D x else 0) ⇢ ?D x"
by (auto intro!: tendsto_eventually eventually_sequentiallyI [of n])
qed
qed auto
then show Dai: "?D absolutely_integrable_on (⋃n. F n)"
unfolding absolutely_integrable_restrict_UNIV by simp
show "integral (⋃n. F n) ?D = integral ((⋃x. g ` F x)) f"
proof (rule LIMSEQ_unique)
show "(λn. integral (⋃m≤n. g ` F m) f) ⇢ integral (⋃n. F n) ?D"
unfolding D_int [symmetric] by (rule integral_countable_UN [OF Dai F_leb])
qed (use fgU in metis)
qed
qed
theorem has_absolute_integral_change_of_variables:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" and g :: "'a ⇒ 'a"
assumes S: "S ∈ sets lebesgue"
and der_g: "⋀x. x ∈ S ⟹ (g has_derivative g' x) (at x within S)"
and inj: "inj_on g S"
shows "(λx. ¦eucl.det(g' x)¦ *⇩R f(g x)) absolutely_integrable_on S ∧
integral S (λx. ¦eucl.det(g' x)¦ *⇩R f(g x)) = b
⟷ f absolutely_integrable_on (g ` S) ∧ integral (g ` S) f = b"
proof -
obtain C N where "fsigma C" and N: "N ∈ null_sets lebesgue" and CNS: "C ∪ N = S" and "disjnt C N"
using lebesgue_set_almost_fsigma [OF S] .
then obtain F :: "nat ⇒ ('a) set"
where F: "range F ⊆ Collect compact" and Ceq: "C = Union(range F)"
using fsigma_Union_compact by metis
have "negligible N"
using N by (simp add: negligible_iff_null_sets)
have "g differentiable_on N"
by (metis CNS der_g differentiable_def differentiable_on_def differentiable_on_subset sup_ge2)
with ‹negligible N›
have neg_gN: "negligible (g ` N)"
by (blast intro: negligible_differentiable_image_negligible)
have neg: "negligible {x ∈ g ` C - g ` S. f x ≠ 0}" "negligible {x ∈ g ` S - g ` C. f x ≠ 0}"
using CNS by (blast intro: negligible_subset [OF neg_gN])+
let ?D = "λx. ¦eucl.det(g' x)¦ *⇩R f (g x)"
have "?D absolutely_integrable_on C ∧ integral C ?D = b
⟷ f absolutely_integrable_on (g ` C) ∧ integral (g ` C) f = b"
unfolding Ceq
proof (rule has_absolute_integral_change_of_variables_compact_family)
fix n x
assume "x ∈ ⋃(F ` UNIV)"
then show "(g has_derivative g' x) (at x within ⋃(F ` UNIV))"
using Ceq ‹C ∪ N = S› der_g has_derivative_subset by blast
next
show "inj_on g (⋃(F ` UNIV))"
using CNS Ceq inj inj_on_subset by blast
qed (use F in auto)
moreover
have "?D absolutely_integrable_on C ∧ integral C ?D = b
⟷ ?D absolutely_integrable_on S ∧ integral S ?D = b"
proof (rule conj_cong)
have neg: "negligible {x ∈ C - S. ?D x ≠ 0}" "negligible {x ∈ S - C. ?D x ≠ 0}"
using CNS by (blast intro: negligible_subset [OF ‹negligible N›])+
then show "(?D absolutely_integrable_on C) = (?D absolutely_integrable_on S)"
by (rule absolutely_integrable_spike_set_eq)
show "(integral C ?D = b) ⟷ (integral S ?D = b)"
using integral_spike_set [OF neg] by simp
qed
moreover
have "f absolutely_integrable_on (g ` C) ∧ integral (g ` C) f = b
⟷ f absolutely_integrable_on (g ` S) ∧ integral (g ` S) f = b"
using absolutely_integrable_spike_set_eq integral_spike_set neg by blast
ultimately show ?thesis
by simp
qed
corollary absolutely_integrable_change_of_variables:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" and g :: "'a ⇒ 'a"
assumes "S ∈ sets lebesgue"
and "⋀x. x ∈ S ⟹ (g has_derivative g' x) (at x within S)"
and "inj_on g S"
shows "f absolutely_integrable_on (g ` S)
⟷ (λx. ¦eucl.det(g' x)¦ *⇩R f(g x)) absolutely_integrable_on S"
using assms has_absolute_integral_change_of_variables by blast
corollary integral_change_of_variables:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" and g :: "'a ⇒ 'a"
assumes S: "S ∈ sets lebesgue"
and der_g: "⋀x. x ∈ S ⟹ (g has_derivative g' x) (at x within S)"
and inj: "inj_on g S"
and disj: "(f absolutely_integrable_on (g ` S) ∨
(λx. ¦eucl.det(g' x)¦ *⇩R f(g x)) absolutely_integrable_on S)"
shows "integral (g ` S) f = integral S (λx. ¦eucl.det(g' x)¦ *⇩R f(g x))"
using has_absolute_integral_change_of_variables [OF S der_g inj] disj
by blast
lemma has_absolute_integral_change_of_variables_1:
fixes f :: "real ⇒ 'b::euclidean_space" and g :: "real ⇒ real"
assumes S: "S ∈ sets lebesgue"
and der_g: "⋀x. x ∈ S ⟹ (g has_vector_derivative g' x) (at x within S)"
and inj: "inj_on g S"
shows "(λx. ¦g' x¦ *⇩R f(g x)) absolutely_integrable_on S ∧
integral S (λx. ¦g' x¦ *⇩R f(g x)) = b
⟷ f absolutely_integrable_on (g ` S) ∧ integral (g ` S) f = b"
proof -
have "(λx. ¦eucl.det((*) (g' x))¦ *⇩R f(g x)) absolutely_integrable_on S ∧
integral S (λx. ¦eucl.det((*) (g' x))¦ *⇩R f(g x)) = b
⟷ f absolutely_integrable_on (g ` S) ∧ integral (g ` S) f = b"
by (rule has_absolute_integral_change_of_variables [OF S _ inj])
(use der_g in ‹auto simp: has_vector_derivative_def mult.commute›)
then show ?thesis
by auto
qed
corollary absolutely_integrable_change_of_variables_1:
fixes f :: "real ⇒ 'b::euclidean_space" and g :: "real ⇒ real"
assumes S: "S ∈ sets lebesgue"
and der_g: "⋀x. x ∈ S ⟹ (g has_vector_derivative g' x) (at x within S)"
and inj: "inj_on g S"
shows "(f absolutely_integrable_on g ` S ⟷
(λx. ¦g' x¦ *⇩R f(g x)) absolutely_integrable_on S)"
using has_absolute_integral_change_of_variables_1 [OF assms] by auto
text ‹when @{term "n=1"}›
lemma has_absolute_integral_change_of_variables_1':
fixes f :: "real ⇒ real" and g :: "real ⇒ real"
assumes S: "S ∈ sets lebesgue"
and der_g: "⋀x. x ∈ S ⟹ (g has_field_derivative g' x) (at x within S)"
and inj: "inj_on g S"
shows "(λx. ¦g' x¦ * f(g x)) absolutely_integrable_on S ∧
integral S (λx. ¦g' x¦ * f (g x)) = b
⟷ f absolutely_integrable_on (g ` S) ∧ integral (g ` S) f = b"
proof -
have "(λx. ¦g' x¦ *⇩R vec (f(g x)) :: real ^ 1) absolutely_integrable_on S ∧
integral S (λx. ¦g' x¦ *⇩R vec (f(g x))) = (vec b :: real ^ 1)
⟷ (λx. vec (f x) :: real ^ 1) absolutely_integrable_on (g ` S) ∧
integral (g ` S) (λx. vec (f x)) = (vec b :: real ^ 1)"
using assms unfolding has_real_derivative_iff_has_vector_derivative
by (intro has_absolute_integral_change_of_variables_1 assms) auto
thus ?thesis
by (simp add: absolutely_integrable_on_1_iff integral_on_1_eq)
qed
lemma has_absolute_integral_reflect_real:
fixes f :: "real ⇒ real"
assumes "uminus ` A ⊆ B" "uminus ` B ⊆ A" "A ∈ sets lebesgue"
shows "(λx. f (-x)) absolutely_integrable_on A ∧ integral A (λx. f (-x)) = b ⟷
f absolutely_integrable_on B ∧ integral B f = b"
proof -
have bij: "bij_betw uminus A B"
by (rule bij_betwI[of _ _ _ uminus]) (use assms in auto)
have "((λx. ¦-1¦ * f (-x)) absolutely_integrable_on A ∧
integral A (λx. ¦-1¦ * f (-x)) = b) ⟷
(f absolutely_integrable_on uminus ` A ∧ integral (uminus ` A) f = b)"
using assms
by (intro has_absolute_integral_change_of_variables_1') (auto intro!: derivative_eq_intros)
also have "uminus ` A = B"
using bij by (simp add: bij_betw_def)
finally show ?thesis
by simp
qed
subsection‹Change of variables for integrals: special case of linear function›
lemma has_absolute_integral_change_of_variables_linear:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" and g :: "'a ⇒ 'a"
assumes "linear g"
shows "(λx. ¦eucl.det g¦ *⇩R f(g x)) absolutely_integrable_on S ∧
integral S (λx. ¦eucl.det g¦ *⇩R f(g x)) = b
⟷ f absolutely_integrable_on (g ` S) ∧ integral (g ` S) f = b"
proof (cases "eucl.det g = 0")
case True
then have "negligible(g ` S)"
using assms eucl.det_eq_0_iff negligible_linear_singular_image by blast
with True show ?thesis
by (auto simp: absolutely_integrable_on_def integrable_negligible integral_negligible)
next
case False
then have "inj g"
using assms eucl.det_eq_0_iff by blast
then have h: "⋀x. x ∈ S ⟹ inv g (g x) = x" "linear (inv g)"
using inv_f_f eucl.inj_linear_imp_inv_linear assms by auto
show ?thesis
proof (rule has_absolute_integral_change_of_variables_invertible)
show "(g has_derivative g) (at x within S)" for x
by (simp add: assms linear_imp_has_derivative)
show "continuous_on (g ` S) (inv g)"
using continuous_on_eq_continuous_within has_derivative_continuous linear_imp_has_derivative h by blast
qed (use h in auto)
qed
lemma absolutely_integrable_change_of_variables_linear:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" and g :: "'a ⇒ 'a"
assumes "linear g"
shows "(λx. ¦eucl.det g¦ *⇩R f(g x)) absolutely_integrable_on S
⟷ f absolutely_integrable_on (g ` S)"
using assms has_absolute_integral_change_of_variables_linear by blast
lemma absolutely_integrable_on_linear_image:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" and g :: "'a ⇒ 'a"
assumes "linear g"
shows "f absolutely_integrable_on (g ` S)
⟷ (f ∘ g) absolutely_integrable_on S ∨ eucl.det g = 0"
unfolding assms absolutely_integrable_change_of_variables_linear [OF assms, symmetric] absolutely_integrable_on_scaleR_iff
by (auto simp: set_integrable_def)
lemma integral_change_of_variables_linear:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" and g :: "'a ⇒ 'a"
assumes "linear g"
and "f absolutely_integrable_on (g ` S) ∨ (f ∘ g) absolutely_integrable_on S"
shows "integral (g ` S) f = ¦eucl.det g¦ *⇩R integral S (f ∘ g)"
unfolding o_def
by (metis absolutely_integrable_on_linear_image assms
has_absolute_integral_change_of_variables_linear integral_cmul)
lemma absolutely_integrable_change_of_variables_1':
fixes f :: "real ⇒ real" and g :: "real ⇒ real"
assumes "S ∈ sets lebesgue"
assumes "⋀x. x ∈ S ⟹ (g has_field_derivative h x) (at x within S)"
assumes "inj_on g S"
shows "f absolutely_integrable_on g ` S ⟷ (λx. ¦h x¦ * f (g x)) absolutely_integrable_on S"
using has_absolute_integral_change_of_variables_1'[of S g h f] assms by auto
lemma absolutely_integrable_change_of_variables_real:
fixes f :: "real ⇒ 'a :: euclidean_space" and g :: "real ⇒ real"
assumes "S ∈ sets lebesgue"
assumes "⋀x. x ∈ S ⟹ (g has_field_derivative h x) (at x within S)"
assumes "inj_on g S"
shows "f absolutely_integrable_on g ` S ⟷ (λx. ¦h x¦ *⇩R f (g x)) absolutely_integrable_on S"
using absolutely_integrable_change_of_variables_1 assms
has_real_derivative_iff_has_vector_derivative by blast
lemma has_absolute_integral_change_of_variables_real:
fixes f :: "real ⇒ 'a :: euclidean_space" and g :: "real ⇒ real"
assumes "S ∈ sets lebesgue"
assumes "⋀x. x ∈ S ⟹ (g has_field_derivative h x) (at x within S)"
assumes "inj_on g S"
shows "(λx. ¦h x¦ *⇩R f (g x)) absolutely_integrable_on S ∧ integral S (λx. ¦h x¦ *⇩R f (g x)) = b
⟷ f absolutely_integrable_on g ` S ∧ integral (g ` S) f = b"
proof (intro conj_cong)
show iff: "(λx. ¦h x¦ *⇩R f (g x)) absolutely_integrable_on S ⟷
f absolutely_integrable_on g ` S"
using absolutely_integrable_change_of_variables_real assms by blast
assume "f absolutely_integrable_on g ` S"
hence integrable: "f integrable_on g ` S" "(λx. ¦h x¦ *⇩R f (g x)) integrable_on S"
using set_lebesgue_integral_eq_integral(1) iff by metis+
have "(λx. ¦h x¦ *⇩R f (g x)) absolutely_integrable_on S ∧
(integral S (λx. ¦h x¦ *⇩R f (g x)) = b) ⟷
(∀a∈Basis. (λx. (¦h x¦ *⇩R f (g x)) ∙ a) absolutely_integrable_on S ∧
(integral S (λx. (¦h x¦ *⇩R f (g x)) ∙ a) = b ∙ a))"
by (subst absolutely_integrable_componentwise_iff, subst integral_eq_iff_componentwise)
(use integrable in auto)
also have "… ⟷ (∀a∈Basis. (λx. ¦h x¦ * (f (g x) ∙ a)) absolutely_integrable_on S ∧
(integral S (λx. ¦h x¦ * (f (g x) ∙ a)) = b ∙ a))"
by simp
also have "… ⟷ (∀a∈Basis. (λx. f x ∙ a) absolutely_integrable_on g ` S ∧
(integral (g ` S) (λx. f x ∙ a) = b ∙ a))"
by (intro ball_cong has_absolute_integral_change_of_variables_1' assms refl)
also have "… ⟷ f absolutely_integrable_on g ` S ∧ integral (g ` S) f = b"
by (simp add: ‹f absolutely_integrable_on g ` S› absolutely_integrable_component
integrable(1) integral_eq_iff_componentwise)
finally show "(integral S (λx. ¦h x¦ *⇩R f (g x)) = b) = (integral (g ` S) f = b)"
using ‹f absolutely_integrable_on g ` S› iff by blast
qed
subsection‹Change of variable for measure›
lemma has_measure_differentiable_image:
fixes f :: "'a::euclidean_space ⇒ 'a"
assumes "S ∈ sets lebesgue"
and "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x within S)"
and "inj_on f S"
shows "f ` S ∈ lmeasurable ∧ measure lebesgue (f ` S) = m
⟷ ((λx. ¦eucl.det (f' x)¦) has_integral m) S"
using has_absolute_integral_change_of_variables [OF assms, of "λx. (1::real^1)" "vec m"]
unfolding absolutely_integrable_on_1_iff integral_on_1_eq integrable_on_1_iff absolutely_integrable_on_def
by (auto simp: has_integral_iff lmeasurable_iff_integrable_on lmeasure_integral)
lemma measurable_differentiable_image_eq:
fixes f :: "'a::euclidean_space ⇒ 'a::euclidean_space"
assumes "S ∈ sets lebesgue"
and "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x within S)"
and "inj_on f S"
shows "f ` S ∈ lmeasurable ⟷ (λx. ¦eucl.det (f' x)¦) integrable_on S"
using has_measure_differentiable_image [OF assms]
by blast
lemma measurable_differentiable_image_alt:
fixes f :: "'a::euclidean_space ⇒ 'a"
assumes "S ∈ sets lebesgue"
and "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x within S)"
and "inj_on f S"
shows "f ` S ∈ lmeasurable ⟷ (λx. ¦eucl.det (f' x)¦) absolutely_integrable_on S"
using measurable_differentiable_image_eq [OF assms]
by (simp only: absolutely_integrable_on_iff_nonneg)
lemma measure_differentiable_image_eq:
fixes f :: "'a::euclidean_space ⇒ 'a"
assumes S: "S ∈ sets lebesgue"
and der_f: "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x within S)"
and inj: "inj_on f S"
and intS: "(λx. ¦eucl.det (f' x)¦) integrable_on S"
shows "measure lebesgue (f ` S) = integral S (λx. ¦eucl.det (f' x)¦)"
using measurable_differentiable_image_eq [OF S der_f inj]
assms has_measure_differentiable_image by blast
proposition measure_lebesgue_linear_transformation:
fixes A :: "'a::euclidean_space set"
fixes f :: "_ ⇒ 'a"
assumes "bounded A" "A ∈ sets lebesgue" "linear f"
shows "measure lebesgue (f ` A) = ¦det f¦ * measure lebesgue A"
proof -
from assms have [intro]: "A ∈ lmeasurable"
by (intro bounded_set_imp_lmeasurable) auto
hence [intro]: "f ` A ∈ lmeasurable"
by (intro lmeasure_integral measurable_linear_image assms)
have "measure lebesgue (f ` A) = integral (f ` A) (λ_. 1)"
by (intro lmeasure_integral measurable_linear_image assms) auto
also have "… = integral (f ` A) (λ_. 1 :: real ^ 1) $ 0"
by (subst integral_component_eq_cart [symmetric]) (auto intro: integrable_on_const)
also have "… = ¦det f¦ * integral A (λx. 1 :: real ^ 1) $ 0"
using assms
by (subst integral_change_of_variables_linear)
(auto simp: o_def absolutely_integrable_on_def intro: integrable_on_const)
also have "integral A (λx. 1 :: real ^ 1) $ 0 = integral A (λx. 1)"
by (subst integral_component_eq_cart [symmetric]) (auto intro: integrable_on_const)
also have "… = measure lebesgue A"
by (intro lmeasure_integral [symmetric]) auto
finally show ?thesis .
qed
end