# Theory Library_Complements

(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr License: BSD *) section ‹Additions to the library› theory Library_Complements imports "HOL-Analysis.Analysis" "HOL-Cardinals.Cardinal_Order_Relation" begin subsection ‹Mono intros› text ‹We have a lot of (large) inequalities to prove. It is very convenient to have a set of introduction rules for this purpose (a lot should be added to it, I have put here all the ones I needed). The typical use case is when one wants to prove some inequality, say $ \exp (x*x) \leq y + \exp(1 + z * z + y)$, assuming $y \geq 0$ and $0 \leq x \leq z$. One would write it has \begin{verbatim} have "0 + \exp(0 + x * x + 0) < = y + \exp(1 + z * z + y)" using `y > = 0` `x < = z` by (intro mono_intros) \end{verbatim} When the left and right hand terms are written in completely analogous ways as above, then the introduction rules (that contain monotonicity of addition, of the exponential, and so on) reduce this to comparison of elementary terms in the formula. This is a very naive strategy, that fails in many situations, but that is very efficient when used correctly. › named_theorems mono_intros "structural introduction rules to prove inequalities" declare le_imp_neg_le [mono_intros] declare add_left_mono [mono_intros] declare add_right_mono [mono_intros] declare add_strict_left_mono [mono_intros] declare add_strict_right_mono [mono_intros] declare add_mono [mono_intros] declare add_less_le_mono [mono_intros] declare diff_right_mono [mono_intros] declare diff_left_mono [mono_intros] declare diff_mono [mono_intros] declare mult_left_mono [mono_intros] declare mult_right_mono [mono_intros] declare mult_mono [mono_intros] declare max.mono [mono_intros] declare min.mono [mono_intros] declare power_mono [mono_intros] declare ln_ge_zero [mono_intros] declare ln_le_minus_one [mono_intros] declare ennreal_minus_mono [mono_intros] declare ennreal_leI [mono_intros] declare e2ennreal_mono [mono_intros] declare enn2ereal_nonneg [mono_intros] declare zero_le [mono_intros] declare top_greatest [mono_intros] declare bot_least [mono_intros] declare dist_triangle [mono_intros] declare dist_triangle2 [mono_intros] declare dist_triangle3 [mono_intros] declare exp_ge_add_one_self [mono_intros] declare exp_gt_one [mono_intros] declare exp_less_mono [mono_intros] declare dist_triangle [mono_intros] declare abs_triangle_ineq [mono_intros] declare abs_triangle_ineq2 [mono_intros] declare abs_triangle_ineq2_sym [mono_intros] declare abs_triangle_ineq3 [mono_intros] declare abs_triangle_ineq4 [mono_intros] declare Liminf_le_Limsup [mono_intros] declare ereal_liminf_add_mono [mono_intros] declare le_of_int_ceiling [mono_intros] declare ereal_minus_mono [mono_intros] declare infdist_triangle [mono_intros] declare divide_right_mono [mono_intros] declare self_le_power [mono_intros] lemma ln_le_cancelI [mono_intros]: assumes "(0::real) < x" "x ≤ y" shows "ln x ≤ ln y" using assms by auto lemma exp_le_cancelI [mono_intros]: assumes "x ≤ (y::real)" shows "exp x ≤ exp y" using assms by simp lemma mult_ge1_mono [mono_intros]: assumes "a ≥ (0::'a::linordered_idom)" "b ≥ 1" shows "a ≤ a * b" "a ≤ b * a" using assms mult_le_cancel_left1 mult_le_cancel_right1 by force+ text ‹A few convexity inequalities we will need later on.› lemma xy_le_uxx_vyy [mono_intros]: assumes "u > 0" "u * v = (1::real)" shows "x * y ≤ u * x^2/2 + v * y^2/2" proof - have "v > 0" using assms by (metis (full_types) dual_order.strict_implies_order le_less_linear mult_nonneg_nonpos not_one_le_zero) then have *: "sqrt u * sqrt v = 1" using assms by (metis real_sqrt_mult real_sqrt_one) have "(sqrt u * x - sqrt v * y)^2 ≥ 0" by auto then have "u * x^2 + v * y^2 - 2 * 1 * x * y ≥ 0" unfolding power2_eq_square *[symmetric] using ‹u > 0› ‹v > 0› by (auto simp add: algebra_simps) then show ?thesis by (auto simp add: algebra_simps divide_simps) qed lemma xy_le_xx_yy [mono_intros]: "x * y ≤ x^2/2 + y^2/2" for x y::real using xy_le_uxx_vyy[of 1 1] by auto lemma ln_squared_bound [mono_intros]: "(ln x)^2 ≤ 2 * x - 2" if "x ≥ 1" for x::real proof - define f where "f = (λx::real. 2 * x - 2 - ln x * ln x)" have *: "DERIV f x :> 2 - 2 * ln x / x" if "x > 0" for x::real unfolding f_def using that by (auto intro!: derivative_eq_intros) have "f 1 ≤ f x" if "x ≥ 1" for x proof (rule DERIV_nonneg_imp_nondecreasing[OF that]) fix t::real assume "t ≥ 1" show "∃y. (f has_real_derivative y) (at t) ∧ 0 ≤ y" apply (rule exI[of _ "2 - 2 * ln t / t"]) using *[of t] ‹t ≥ 1› by (auto simp add: divide_simps ln_bound) qed then show ?thesis unfolding f_def power2_eq_square using that by auto qed text ‹In the next lemma, the assumptions are too strong (negative numbers less than $-1$ also work well to have a square larger than $1$), but in practice one proves inequalities with nonnegative numbers, so this version is really the useful one for \verb+mono_intros+.› lemma mult_ge1_powers [mono_intros]: assumes "a ≥ (1::'a::linordered_idom)" shows "1 ≤ a * a" "1 ≤ a * a * a" "1 ≤ a * a * a * a" using assms by (meson assms dual_order.trans mult_ge1_mono(1) zero_le_one)+ lemmas [mono_intros] = ln_bound lemma mono_cSup: fixes f :: "'a::conditionally_complete_lattice ⇒ 'b::conditionally_complete_lattice" assumes "bdd_above A" "A ≠ {}" "mono f" shows "Sup (f`A) ≤ f (Sup A)" by (metis assms(1) assms(2) assms(3) cSUP_least cSup_upper mono_def) lemma mono_cSup_bij: fixes f :: "'a::conditionally_complete_linorder ⇒ 'b::conditionally_complete_linorder" assumes "bdd_above A" "A ≠ {}" "mono f" "bij f" shows "Sup (f`A) = f(Sup A)" proof - have "Sup ((inv f)`(f`A)) ≤ (inv f) (Sup (f`A))" apply (rule mono_cSup) using mono_inv[OF assms(3) assms(4)] assms(2) bdd_above_image_mono[OF assms(3) assms(1)] by auto then have "f (Sup ((inv f)`(f`A))) ≤ Sup (f`A)" using assms mono_def by (metis (no_types, hide_lams) bij_betw_imp_surj_on surj_f_inv_f) moreover have "f (Sup ((inv f)`(f`A))) = f(Sup A)" using assms by (simp add: bij_is_inj) ultimately show ?thesis using mono_cSup[OF assms(1) assms(2) assms(3)] by auto qed subsection ‹More topology› text ‹In situations of interest to us later on, convergence is well controlled only for sequences living in some dense subset of the space (but the limit can be anywhere). This is enough to establish continuity of the function, if the target space is well enough separated. The statement we give below is very general, as we do not assume that the function is continuous inside the original set $S$, it will typically only be continuous at a set $T$ contained in the closure of $S$. In many applications, $T$ will be the closure of $S$, but we are also thinking of the case where one constructs an extension of a function inside a space, to its boundary, and the behaviour at the boundary is better than inside the space. The example we have in mind is the extension of a quasi-isometry to the boundary of a Gromov hyperbolic space. In the following criterion, we assume that if $u_n$ inside $S$ converges to a point at the boundary $T$, then $f(u_n)$ converges (where $f$ is some function inside). Then, we can extend the function $f$ at the boundary, by picking the limit value of $f(u_n)$ for some sequence converging to $u_n$. Then the lemma asserts that $f$ is continuous at every point $b$ on the boundary. The proof is done in two steps: \begin{enumerate} \item First, if $v_n$ is another inside sequence tending to the same point $b$ on the boundary, then $f(v_n)$ converges to the same value as $f(u_n)$: this is proved by considering the sequence $w$ equal to $u$ at even times and to $v$ at odd times, and saying that $f(w_n)$ converges. Its limit is equal to the limit of $f(u_n)$ and of $f(v_n)$, so they have to coincide. \item Now, consider a general sequence $v$ (in the space or the boundary) converging to $b$. We want to show that $f(v_n)$ tends to $f(b)$. If $v_n$ is inside $S$, we have already done it in the first step. If it is on the boundary, on the other hand, we can approximate it by an inside point $w_n$ for which $f(w_n)$ is very close to $f(v_n)$. Then $w_n$ is an inside sequence converging to $b$, hence $f(w_n)$ converges to $f(b)$ by the first step, and then $f(v_n)$ also converges to $f(b)$. The precise argument is more conveniently written by contradiction. It requires good separation properties of the target space. \end{enumerate}› text ‹First, we introduce the material to interpolate between two sequences, one at even times and the other one at odd times.› definition even_odd_interpolate::"(nat ⇒ 'a) ⇒ (nat ⇒ 'a) ⇒ (nat ⇒ 'a)" where "even_odd_interpolate u v n = (if even n then u (n div 2) else v (n div 2))" lemma even_odd_interpolate_compose: "even_odd_interpolate (f o u) (f o v) = f o (even_odd_interpolate u v)" unfolding even_odd_interpolate_def comp_def by auto lemma even_odd_interpolate_filterlim: "filterlim u F sequentially ∧ filterlim v F sequentially ⟷ filterlim (even_odd_interpolate u v) F sequentially" proof (auto) assume H: "filterlim (even_odd_interpolate u v) F sequentially" define r::"nat ⇒ nat" where "r = (λn. 2 * n)" have "strict_mono r" unfolding r_def strict_mono_def by auto then have "filterlim r sequentially sequentially" by (simp add: filterlim_subseq) have "filterlim (λn. (even_odd_interpolate u v) (r n)) F sequentially" by (rule filterlim_compose[OF H filterlim_subseq[OF ‹strict_mono r›]]) moreover have "even_odd_interpolate u v (r n) = u n" for n unfolding r_def even_odd_interpolate_def by auto ultimately show "filterlim u F sequentially" by auto define r::"nat ⇒ nat" where "r = (λn. 2 * n + 1)" have "strict_mono r" unfolding r_def strict_mono_def by auto then have "filterlim r sequentially sequentially" by (simp add: filterlim_subseq) have "filterlim (λn. (even_odd_interpolate u v) (r n)) F sequentially" by (rule filterlim_compose[OF H filterlim_subseq[OF ‹strict_mono r›]]) moreover have "even_odd_interpolate u v (r n) = v n" for n unfolding r_def even_odd_interpolate_def by auto ultimately show "filterlim v F sequentially" by auto next assume H: "filterlim u F sequentially" "filterlim v F sequentially" show "filterlim (even_odd_interpolate u v) F sequentially" unfolding filterlim_iff eventually_sequentially proof (auto) fix P assume *: "eventually P F" obtain N1 where N1: "⋀n. n ≥ N1 ⟹ P (u n)" using H(1) unfolding filterlim_iff eventually_sequentially using * by auto obtain N2 where N2: "⋀n. n ≥ N2 ⟹ P (v n)" using H(2) unfolding filterlim_iff eventually_sequentially using * by auto have "P (even_odd_interpolate u v n)" if "n ≥ 2 * N1 + 2 * N2" for n proof (cases "even n") case True have "n div 2 ≥ N1" using that by auto then show ?thesis unfolding even_odd_interpolate_def using True N1 by auto next case False have "n div 2 ≥ N2" using that by auto then show ?thesis unfolding even_odd_interpolate_def using False N2 by auto qed then show "∃N. ∀n ≥ N. P (even_odd_interpolate u v n)" by auto qed qed text ‹Then, we prove the continuity criterion for extensions of functions to the boundary $T$ of a set $S$. The first assumption is that $f(u_n)$ converges when $f$ converges to the boundary, and the second one that the extension of $f$ to the boundary has been defined using the limit along some sequence tending to the point under consideration. The following criterion is the most general one, but this is not the version that is most commonly applied so we use a prime in its name.› lemma continuous_at_extension_sequentially': fixes f :: "'a::{first_countable_topology, t2_space} ⇒ 'b::t3_space" assumes "b ∈ T" "⋀u b. (∀n. u n ∈ S) ⟹ b ∈ T ⟹ u ⇢ b ⟹ convergent (λn. f (u n))" "⋀b. b ∈ T ⟹ ∃u. (∀n. u n ∈ S) ∧ u ⇢ b ∧ ((λn. f (u n)) ⇢ f b)" shows "continuous (at b within (S ∪ T)) f" proof - have first_step: "(λn. f (u n)) ⇢ f c" if "⋀n. u n ∈ S" "u ⇢ c" "c ∈ T" for u c proof - obtain v where v: "⋀n. v n ∈ S" "v ⇢ c" "(λn. f (v n)) ⇢ f c" using assms(3)[OF ‹c ∈ T›] by blast then have A: "even_odd_interpolate u v ⇢ c" unfolding even_odd_interpolate_filterlim[symmetric] using ‹u ⇢ c› by auto moreover have B: "∀n. even_odd_interpolate u v n ∈ S" using ‹⋀n. u n ∈ S› ‹⋀n. v n ∈ S› unfolding even_odd_interpolate_def by auto have "convergent (λn. f (even_odd_interpolate u v n))" by (rule assms(2)[OF B ‹c ∈ T› A]) then obtain m where "(λn. f (even_odd_interpolate u v n)) ⇢ m" unfolding convergent_def by auto then have "even_odd_interpolate (f o u) (f o v) ⇢ m" unfolding even_odd_interpolate_compose unfolding comp_def by auto then have "(f o u) ⇢ m" "(f o v) ⇢ m" unfolding even_odd_interpolate_filterlim[symmetric] by auto then have "m = f c" using v(3) unfolding comp_def using LIMSEQ_unique by auto then show ?thesis using ‹(f o u) ⇢ m› unfolding comp_def by auto qed show "continuous (at b within (S ∪ T)) f" proof (rule ccontr) assume "¬ ?thesis" then obtain U where U: "open U" "f b ∈ U" "¬(∀⇩_{F}x in at b within S ∪ T. f x ∈ U)" unfolding continuous_within tendsto_def[where l = "f b"] using sequentially_imp_eventually_nhds_within by auto have "∃V W. open V ∧ open W ∧ f b ∈ V ∧ (UNIV - U) ⊆ W ∧ V ∩ W = {}" apply (rule t3_space) using U by auto then obtain V W where VW: "open V" "open W" "f b ∈ V" "UNIV - U ⊆ W" "V ∩ W = {}" by auto obtain A :: "nat ⇒ 'a set" where *: "⋀i. open (A i)" "⋀i. b ∈ A i" "⋀F. ∀n. F n ∈ A n ⟹ F ⇢ b" by (rule first_countable_topology_class.countable_basis) blast with * U(3) have "∃F. ∀n. F n ∈ S ∪ T ∧ F n ∈ A n ∧ ¬ (f(F n) ∈ U)" unfolding at_within_def eventually_inf_principal eventually_nhds by (intro choice) (meson DiffE) then obtain F where F: "⋀n. F n ∈ S ∪ T" "⋀n. F n ∈ A n" "⋀n. f(F n) ∉ U" by auto have "∃y. y ∈ S ∧ y ∈ A n ∧ f y ∈ W" for n proof (cases "F n ∈ S") case True show ?thesis apply (rule exI[of _ "F n"]) using F VW True by auto next case False then have "F n ∈ T" using ‹F n ∈ S ∪ T› by auto obtain u where u: "⋀p. u p ∈ S" "u ⇢ F n" "(λp. f (u p)) ⇢ f(F n)" using assms(3)[OF ‹F n ∈ T›] by auto moreover have "f(F n) ∈ W" using F VW by auto ultimately have "eventually (λp. f (u p) ∈ W) sequentially" using ‹open W› by (simp add: tendsto_def) moreover have "eventually (λp. u p ∈ A n) sequentially" using ‹F n ∈ A n› u ‹open (A n)› by (simp add: tendsto_def) ultimately have "∃p. f(u p) ∈ W ∧ u p ∈ A n" using eventually_False_sequentially eventually_elim2 by blast then show ?thesis using u(1) by auto qed then have "∃u. ∀n. u n ∈ S ∧ u n ∈ A n ∧ f (u n) ∈ W" by (auto intro: choice) then obtain u where u: "⋀n. u n ∈ S" "⋀n. u n ∈ A n" "⋀n. f (u n) ∈ W" by blast then have "u ⇢ b" using *(3) by auto then have "(λn. f (u n)) ⇢ f b" using first_step assms u by auto then have "eventually (λn. f (u n) ∈ V) sequentially" using VW by (simp add: tendsto_def) then have "∃n. f (u n) ∈ V" using eventually_False_sequentially eventually_elim2 by blast then show False using u(3) ‹V ∩ W = {}› by auto qed qed text ‹We can specialize the previous statement to the common case where one already knows the sequential continuity of $f$ along sequences in $S$ converging to a point in $T$. This will be the case in most --but not all-- applications. This is a straightforward application of the above criterion.› proposition continuous_at_extension_sequentially: fixes f :: "'a::{first_countable_topology, t2_space} ⇒ 'b::t3_space" assumes "a ∈ T" "T ⊆ closure S" "⋀u b. (∀n. u n ∈ S) ⟹ b ∈ T ⟹ u ⇢ b ⟹ (λn. f (u n)) ⇢ f b" shows "continuous (at a within (S ∪ T)) f" apply (rule continuous_at_extension_sequentially'[OF ‹a ∈ T›]) using assms(3) convergent_def apply blast by (metis assms(2) assms(3) closure_sequential subset_iff) text ‹We also give global versions. We can only express the continuity on $T$, so this is slightly weaker than the previous statements since we are not saying anything on inside sequences tending to $T$ -- but in cases where $T$ contains $S$ these statements contain all the information.› lemma continuous_on_extension_sequentially': fixes f :: "'a::{first_countable_topology, t2_space} ⇒ 'b::t3_space" assumes "⋀u b. (∀n. u n ∈ S) ⟹ b ∈ T ⟹ u ⇢ b ⟹ convergent (λn. f (u n))" "⋀b. b ∈ T ⟹ ∃u. (∀n. u n ∈ S) ∧ u ⇢ b ∧ ((λn. f (u n)) ⇢ f b)" shows "continuous_on T f" unfolding continuous_on_eq_continuous_within apply (auto intro!: continuous_within_subset[of _ "S ∪ T" f T]) by (intro continuous_at_extension_sequentially'[OF _ assms], auto) lemma continuous_on_extension_sequentially: fixes f :: "'a::{first_countable_topology, t2_space} ⇒ 'b::t3_space" assumes "T ⊆ closure S" "⋀u b. (∀n. u n ∈ S) ⟹ b ∈ T ⟹ u ⇢ b ⟹ (λn. f (u n)) ⇢ f b" shows "continuous_on T f" unfolding continuous_on_eq_continuous_within apply (auto intro!: continuous_within_subset[of _ "S ∪ T" f T]) by (intro continuous_at_extension_sequentially[OF _ assms], auto) subsubsection ‹Homeomorphisms› text ‹A variant around the notion of homeomorphism, which is only expressed in terms of the function and not of its inverse.› definition homeomorphism_on::"'a set ⇒ ('a::topological_space ⇒ 'b::topological_space) ⇒ bool" where "homeomorphism_on S f = (∃g. homeomorphism S (f`S) f g)" lemma homeomorphism_on_continuous: assumes "homeomorphism_on S f" shows "continuous_on S f" using assms unfolding homeomorphism_on_def homeomorphism_def by auto lemma homeomorphism_on_bij: assumes "homeomorphism_on S f" shows "bij_betw f S (f`S)" using assms unfolding homeomorphism_on_def homeomorphism_def by auto (metis inj_on_def inj_on_imp_bij_betw) lemma homeomorphism_on_homeomorphic: assumes "homeomorphism_on S f" shows "S homeomorphic (f`S)" using assms unfolding homeomorphism_on_def homeomorphic_def by auto lemma homeomorphism_on_compact: fixes f::"'a::topological_space ⇒ 'b::t2_space" assumes "continuous_on S f" "compact S" "inj_on f S" shows "homeomorphism_on S f" unfolding homeomorphism_on_def using homeomorphism_compact[OF assms(2) assms(1) _ assms(3)] by auto lemma homeomorphism_on_subset: assumes "homeomorphism_on S f" "T ⊆ S" shows "homeomorphism_on T f" using assms homeomorphism_of_subsets unfolding homeomorphism_on_def by blast lemma homeomorphism_on_empty [simp]: "homeomorphism_on {} f" unfolding homeomorphism_on_def using homeomorphism_empty[of f] by auto lemma homeomorphism_on_cong: assumes "homeomorphism_on X f" "X' = X" "⋀x. x ∈ X ⟹ f' x = f x" shows "homeomorphism_on X' f'" proof - obtain g where g:"homeomorphism X (f`X) f g" using assms unfolding homeomorphism_on_def by auto have "homeomorphism X' (f'`X') f' g" apply (rule homeomorphism_cong[OF g]) using assms by (auto simp add: rev_image_eqI) then show ?thesis unfolding homeomorphism_on_def by auto qed lemma homeomorphism_on_inverse: fixes f::"'a::topological_space ⇒ 'b::topological_space" assumes "homeomorphism_on X f" shows "homeomorphism_on (f`X) (inv_into X f)" proof - obtain g where g: "homeomorphism X (f`X) f g" using assms unfolding homeomorphism_on_def by auto then have "g`f`X = X" by (simp add: homeomorphism_def) then have "homeomorphism_on (f`X) g" unfolding homeomorphism_on_def using homeomorphism_symD[OF g] by auto moreover have "g x = inv_into X f x" if "x ∈ f`X" for x using g that unfolding homeomorphism_def by (auto, metis f_inv_into_f inv_into_into that) ultimately show ?thesis using homeomorphism_on_cong by force qed text ‹Characterization of homeomorphisms in terms of sequences: a map is a homeomorphism if and only if it respects convergent sequences.› lemma homeomorphism_on_compose: assumes "homeomorphism_on S f" "x ∈ S" "eventually (λn. u n ∈ S) F" shows "(u ⤏ x) F ⟷ ((λn. f (u n)) ⤏ f x) F" proof assume "(u ⤏ x) F" then show "((λn. f (u n)) ⤏ f x) F" using continuous_on_tendsto_compose[OF homeomorphism_on_continuous[OF assms(1)] _ assms(2) assms(3)] by simp next assume *: "((λn. f (u n)) ⤏ f x) F" have I: "inv_into S f (f y) = y" if "y ∈ S" for y using homeomorphism_on_bij[OF assms(1)] by (meson bij_betw_inv_into_left that) then have A: "eventually (λn. u n = inv_into S f (f (u n))) F" using assms eventually_mono by force have "((λn. (inv_into S f) (f (u n))) ⤏ (inv_into S f) (f x)) F" apply (rule continuous_on_tendsto_compose[OF homeomorphism_on_continuous[OF homeomorphism_on_inverse[OF assms(1)]] *]) using assms eventually_mono by (auto) fastforce then show "(u ⤏ x) F" unfolding tendsto_cong[OF A] I[OF ‹x ∈ S›] by simp qed lemma homeomorphism_on_sequentially: fixes f::"'a::{first_countable_topology, t2_space} ⇒ 'b::{first_countable_topology, t2_space}" assumes "⋀x u. x ∈ S ⟹ (∀n. u n ∈ S) ⟹ u ⇢ x ⟷ (λn. f (u n)) ⇢ f x" shows "homeomorphism_on S f" proof - have "x = y" if "f x = f y" "x ∈ S" "y ∈ S" for x y proof - have "(λn. f x) ⇢ f y" using that by auto then have "(λn. x) ⇢ y" using assms(1) that by auto then show "x = y" using LIMSEQ_unique by auto qed then have "inj_on f S" by (simp add: inj_on_def) have Cf: "continuous_on S f" apply (rule continuous_on_sequentiallyI) using assms by auto define g where "g = inv_into S f" have Cg: "continuous_on (f`S) g" proof (rule continuous_on_sequentiallyI) fix v b assume H: "∀n. v n ∈ f ` S" "b ∈ f ` S" "v ⇢ b" define u where "u = (λn. g (v n))" define a where "a = g b" have "u n ∈ S" "f (u n) = v n" for n unfolding u_def g_def using H(1) by (auto simp add: inv_into_into f_inv_into_f) have "a ∈ S" "f a = b" unfolding a_def g_def using H(2) by (auto simp add: inv_into_into f_inv_into_f) show "(λn. g(v n)) ⇢ g b" unfolding u_def[symmetric] a_def[symmetric] apply (rule iffD2[OF assms]) using ‹⋀n. u n ∈ S› ‹a ∈ S› ‹v ⇢ b› unfolding ‹⋀n. f (u n) = v n› ‹f a = b› by auto qed have "homeomorphism S (f`S) f g" apply (rule homeomorphismI[OF Cf Cg]) unfolding g_def using ‹inj_on f S› by auto then show ?thesis unfolding homeomorphism_on_def by auto qed lemma homeomorphism_on_UNIV_sequentially: fixes f::"'a::{first_countable_topology, t2_space} ⇒ 'b::{first_countable_topology, t2_space}" assumes "⋀x u. u ⇢ x ⟷ (λn. f (u n)) ⇢ f x" shows "homeomorphism_on UNIV f" using assms by (auto intro!: homeomorphism_on_sequentially) text ‹Now, we give similar characterizations in terms of sequences living in a dense subset. As in the sequential continuity criteria above, we first give a very general criterion, where the map does not have to be continuous on the approximating set $S$, only on the limit set $T$, without any a priori identification of the limit. Then, we specialize this statement to a less general but often more usable version.› lemma homeomorphism_on_extension_sequentially_precise: fixes f::"'a::{first_countable_topology, t3_space} ⇒ 'b::{first_countable_topology, t3_space}" assumes "⋀u b. (∀n. u n ∈ S) ⟹ b ∈ T ⟹ u ⇢ b ⟹ convergent (λn. f (u n))" "⋀u c. (∀n. u n ∈ S) ⟹ c ∈ f`T ⟹ (λn. f (u n)) ⇢ c ⟹ convergent u" "⋀b. b ∈ T ⟹ ∃u. (∀n. u n ∈ S) ∧ u ⇢ b ∧ ((λn. f (u n)) ⇢ f b)" "⋀n. u n ∈ S ∪ T" "l ∈ T" shows "u ⇢ l ⟷ (λn. f (u n)) ⇢ f l" proof assume H: "u ⇢ l" have "continuous (at l within (S ∪ T)) f" apply (rule continuous_at_extension_sequentially'[OF ‹l ∈ T›]) using assms(1) assms(3) by auto then show "(λn. f (u n)) ⇢ f l" apply (rule continuous_within_tendsto_compose) using H assms(4) by auto next text ‹For the reverse implication, we would like to use the continuity criterion \verb+ continuous_at_extension_sequentially'+ applied to the inverse of $f$. Unfortunately, this inverse is only well defined on $T$, while our sequence takes values in $S \cup T$. So, instead, we redo by hand the proof of the continuity criterion, but in the opposite direction.› assume H: "(λn. f (u n)) ⇢ f l" show "u ⇢ l" proof (rule ccontr) assume "¬ ?thesis" then obtain U where U: "open U" "l ∈ U" "¬(∀⇩_{F}n in sequentially. u n ∈ U)" unfolding continuous_within tendsto_def[where l = l] using sequentially_imp_eventually_nhds_within by auto obtain A :: "nat ⇒ 'b set" where *: "⋀i. open (A i)" "⋀i. f l ∈ A i" "⋀F. ∀n. F n ∈ A n ⟹ F ⇢ f l" by (rule first_countable_topology_class.countable_basis) blast have B: "eventually (λn. f (u n) ∈ A i) sequentially" for i using ‹open (A i)› ‹f l ∈ A i› H topological_tendstoD by fastforce have M: "∃r. r ≥ N ∧ (u r ∉ U) ∧ f (u r) ∈ A i" for N i using U(3) B[of i] unfolding eventually_sequentially by (meson dual_order.trans le_cases) have "∃r. ∀n. (u (r n) ∉ U ∧ f (u (r n)) ∈ A n) ∧ r (Suc n) ≥ r n + 1" apply (rule dependent_nat_choice) using M by auto then obtain r where r: "⋀n. u (r n) ∉ U" "⋀n. f (u (r n)) ∈ A n" "⋀n. r (Suc n) ≥ r n + 1" by auto then have "strict_mono r" by (metis Suc_eq_plus1 Suc_le_lessD strict_monoI_Suc) have "∃V W. open V ∧ open W ∧ l ∈ V ∧ (UNIV - U) ⊆ W ∧ V ∩ W = {}" apply (rule t3_space) using U by auto then obtain V W where VW: "open V" "open W" "l ∈ V" "UNIV - U ⊆ W" "V ∩ W = {}" by auto have "∃z. z ∈ S ∧ f z ∈ A n ∧ z ∈ W" for n proof - define z where "z = u (r n)" have "f z ∈ A n" unfolding z_def using r(2) by auto have "z ∈ S ∪ T" "z ∉ U" unfolding z_def using r(1) assms(4) by auto then have "z ∈ W" using VW by auto show ?thesis proof (cases "z ∈ T") case True obtain u::"nat ⇒ 'a" where u: "⋀p. u p ∈ S" "u ⇢ z" "(λp. f (u p)) ⇢ f z" using assms(3)[OF ‹z ∈ T›] by auto then have "eventually (λp. f (u p) ∈ A n) sequentially" using ‹open (A n)› ‹f z ∈ A n› unfolding tendsto_def by simp moreover have "eventually (λp. u p ∈ W) sequentially" using ‹open W› ‹z ∈ W› u unfolding tendsto_def by simp ultimately have "∃p. u p ∈ W ∧ f (u p) ∈ A n" using eventually_False_sequentially eventually_elim2 by blast then show ?thesis using u(1) by auto next case False then have "z ∈ S" using ‹z ∈ S ∪ T› by auto then show ?thesis using ‹f z ∈ A n› ‹z ∈ W› by auto qed qed then have "∃v. ∀n. v n ∈ S ∧ f (v n) ∈ A n ∧ v n ∈ W" by (auto intro: choice) then obtain v where v: "⋀n. v n ∈ S" "⋀n. f (v n) ∈ A n" "⋀n. v n ∈ W" by blast then have I: "(λn. f (v n)) ⇢ f l" using *(3) by auto obtain w where w: "⋀n. w n ∈ S" "w ⇢ l" "((λn. f (w n)) ⇢ f l)" using assms(3)[OF ‹l ∈ T›] by auto have "even_odd_interpolate (f o v) (f o w) ⇢ f l" unfolding even_odd_interpolate_filterlim[symmetric] comp_def using v w I by auto then have *: "(λn. f (even_odd_interpolate v w n)) ⇢ f l" unfolding even_odd_interpolate_compose unfolding comp_def by auto have "convergent (even_odd_interpolate v w)" apply (rule assms(2)[OF _ _ *]) unfolding even_odd_interpolate_def using v(1) w(1) ‹l ∈ T› by auto then obtain z where "even_odd_interpolate v w ⇢ z" unfolding convergent_def by auto then have *: "v ⇢ z" "w ⇢ z" unfolding even_odd_interpolate_filterlim[symmetric] by auto then have "z = l" using v(2) w(2) LIMSEQ_unique by auto then have "v ⇢ l" using * by simp then have "eventually (λn. v n ∈ V) sequentially" using VW by (simp add: tendsto_def) then have "∃n. v n ∈ V" using eventually_False_sequentially eventually_elim2 by blast then show False using v(3) ‹V ∩ W = {}› by auto qed qed lemma homeomorphism_on_extension_sequentially': fixes f::"'a::{first_countable_topology, t3_space} ⇒ 'b::{first_countable_topology, t3_space}" assumes "⋀u b. (∀n. u n ∈ S) ⟹ b ∈ T ⟹ u ⇢ b ⟹ convergent (λn. f (u n))" "⋀u c. (∀n. u n ∈ S) ⟹ c ∈ f`T ⟹ (λn. f (u n)) ⇢ c ⟹ convergent u" "⋀b. b ∈ T ⟹ ∃u. (∀n. u n ∈ S) ∧ u ⇢ b ∧ ((λn. f (u n)) ⇢ f b)" shows "homeomorphism_on T f" apply (rule homeomorphism_on_sequentially, rule homeomorphism_on_extension_sequentially_precise[of S T]) using assms by auto proposition homeomorphism_on_extension_sequentially: fixes f::"'a::{first_countable_topology, t3_space} ⇒ 'b::{first_countable_topology, t3_space}" assumes "⋀u b. (∀n. u n ∈ S) ⟹ u ⇢ b ⟷ (λn. f (u n)) ⇢ f b" "T ⊆ closure S" shows "homeomorphism_on T f" apply (rule homeomorphism_on_extension_sequentially'[of S]) using assms(1) convergent_def apply fastforce using assms(1) convergent_def apply blast by (metis assms(1) assms(2) closure_sequential subsetCE) lemma homeomorphism_on_UNIV_extension_sequentially: fixes f::"'a::{first_countable_topology, t3_space} ⇒ 'b::{first_countable_topology, t3_space}" assumes "⋀u b. (∀n. u n ∈ S) ⟹ u ⇢ b ⟷ (λn. f (u n)) ⇢ f b" "closure S = UNIV" shows "homeomorphism_on UNIV f" apply (rule homeomorphism_on_extension_sequentially[of S]) using assms by auto subsubsection ‹Proper spaces› text ‹Proper spaces, i.e., spaces in which every closed ball is compact -- or, equivalently, any closed bounded set is compact.› definition proper::"('a::metric_space) set ⇒ bool" where "proper S ≡ (∀ x r. compact (cball x r ∩ S))" lemma properI: assumes "⋀x r. compact (cball x r ∩ S)" shows "proper S" using assms unfolding proper_def by auto lemma proper_compact_cball: assumes "proper (UNIV::'a::metric_space set)" shows "compact (cball (x::'a) r)" using assms unfolding proper_def by auto lemma proper_compact_bounded_closed: assumes "proper (UNIV::'a::metric_space set)" "closed (S::'a set)" "bounded S" shows "compact S" proof - obtain x r where "S ⊆ cball x r" using ‹bounded S› bounded_subset_cball by blast then have *: "S = S ∩ cball x r" by auto show ?thesis apply (subst *, rule closed_Int_compact) using assms unfolding proper_def by auto qed lemma proper_real [simp]: "proper (UNIV::real set)" unfolding proper_def by auto lemma complete_of_proper: assumes "proper S" shows "complete S" proof - have "∃l∈S. u ⇢ l" if "Cauchy u" "⋀n. u n ∈ S" for u proof - have "bounded (range u)" using ‹Cauchy u› cauchy_imp_bounded by auto then obtain x r where *: "⋀n. dist x (u n) ≤ r" unfolding bounded_def by auto then have "u n ∈ (cball x r) ∩ S" for n using ‹u n ∈ S› by auto moreover have "complete ((cball x r) ∩ S)" apply (rule compact_imp_complete) using assms unfolding proper_def by auto ultimately show ?thesis unfolding complete_def using ‹Cauchy u› by auto qed then show ?thesis unfolding complete_def by auto qed lemma proper_of_compact: assumes "compact S" shows "proper S" using assms by (auto intro: properI) lemma proper_Un: assumes "proper A" "proper B" shows "proper (A ∪ B)" using assms unfolding proper_def by (auto simp add: compact_Un inf_sup_distrib1) subsubsection ‹Miscellaneous topology› text ‹When manipulating the triangle inequality, it is very frequent to deal with 4 points (and automation has trouble doing it automatically). Even sometimes with 5 points...› lemma dist_triangle4 [mono_intros]: "dist x t ≤ dist x y + dist y z + dist z t" using dist_triangle[of x z y] dist_triangle[of x t z] by auto lemma dist_triangle5 [mono_intros]: "dist x u ≤ dist x y + dist y z + dist z t + dist t u" using dist_triangle4[of x u y z] dist_triangle[of z u t] by auto text ‹A thickening of a compact set is closed.› lemma compact_has_closed_thickening: assumes "compact C" "continuous_on C f" shows "closed (⋃x∈C. cball x (f x))" proof (auto simp add: closed_sequential_limits) fix u l assume *: "∀n::nat. ∃x∈C. dist x (u n) ≤ f x" "u ⇢ l" have "∃x::nat⇒'a. ∀n. x n ∈ C ∧ dist (x n) (u n) ≤ f (x n)" apply (rule choice) using * by auto then obtain x::"nat ⇒ 'a" where x: "⋀n. x n ∈ C" "⋀n. dist (x n) (u n) ≤ f (x n)" by blast obtain r c where "strict_mono r" "c ∈ C" "(x o r) ⇢ c" using x(1) ‹compact C› by (meson compact_eq_seq_compact_metric seq_compact_def) then have "c ∈ C" using x(1) ‹compact C› by auto have lim: "(λn. f (x (r n)) - dist (x (r n)) (u (r n))) ⇢ f c - dist c l" apply (intro tendsto_intros, rule continuous_on_tendsto_compose[of C f]) using *(2) x(1) ‹(x o r) ⇢ c› ‹continuous_on C f› ‹c ∈ C› ‹strict_mono r› LIMSEQ_subseq_LIMSEQ unfolding comp_def by auto have "f c - dist c l ≥ 0" apply (rule LIMSEQ_le_const[OF lim]) using x(2) by auto then show "∃x∈C. dist x l ≤ f x" using ‹c ∈ C› by auto qed text ‹congruence rule for continuity. The assumption that $f y = g y$ is necessary since \verb+at x+ is the pointed neighborhood at $x$.› lemma continuous_within_cong: assumes "continuous (at y within S) f" "eventually (λx. f x = g x) (at y within S)" "f y = g y" shows "continuous (at y within S) g" using assms continuous_within filterlim_cong by fastforce text ‹A function which tends to infinity at infinity, on a proper set, realizes its infimum› lemma continuous_attains_inf_proper: fixes f :: "'a::metric_space ⇒ 'b::linorder_topology" assumes "proper s" "a ∈ s" "continuous_on s f" "⋀z. z ∈ s - cball a r ⟹ f z ≥ f a" shows "∃x∈s. ∀y∈s. f x ≤ f y" proof (cases "r ≥ 0") case True have "∃x∈cball a r ∩ s. ∀y ∈ cball a r ∩ s. f x ≤ f y" apply (rule continuous_attains_inf) using assms True unfolding proper_def apply (auto simp add: continuous_on_subset) using centre_in_cball by blast then obtain x where x: "x ∈ cball a r ∩ s" "⋀y. y ∈ cball a r ∩ s ⟹ f x ≤ f y" by auto have "f x ≤ f y" if "y ∈ s" for y proof (cases "y ∈ cball a r") case True then show ?thesis using x(2) that by auto next case False have "f x ≤ f a" apply (rule x(2)) using assms True by auto then show ?thesis using assms(4)[of y] that False by auto qed then show ?thesis using x(1) by auto next case False show ?thesis apply (rule bexI[of _ a]) using assms False by auto qed subsubsection ‹Measure of balls› text ‹The image of a ball by an affine map is still a ball, with explicit center and radius. (Now unused)› lemma affine_image_ball [simp]: "(λy. R *⇩_{R}y + x) ` cball 0 1 = cball (x::('a::real_normed_vector)) ¦R¦" proof have "dist x (R *⇩_{R}y + x) ≤ ¦R¦" if "dist 0 y ≤ 1" for y proof - have "dist x (R *⇩_{R}y + x) = norm ((R *⇩_{R}y + x) - x)" by (simp add: dist_norm) also have "... = ¦R¦ * norm y" by auto finally show ?thesis using that by (simp add: mult_left_le) qed then show "(λy. R *⇩_{R}y + x) ` cball 0 1 ⊆ cball x ¦R¦" by auto show "cball x ¦R¦ ⊆ (λy. R *⇩_{R}y + x) ` cball 0 1" proof (cases "¦R¦ = 0") case True then have "cball x ¦R¦ = {x}" by auto moreover have "x = R *⇩_{R}0 + x ∧ 0 ∈ cball 0 1" by auto ultimately show ?thesis by auto next case False have "z ∈ (λy. R *⇩_{R}y + x) ` cball 0 1" if "z ∈ cball x ¦R¦" for z proof - define y where "y = (z - x) /⇩_{R}R" have "R *⇩_{R}y + x = z" unfolding y_def using False by auto moreover have "y ∈ cball 0 1" using ‹z ∈ cball x ¦R¦› False unfolding y_def by (auto simp add: dist_norm[symmetric] divide_simps dist_commute) ultimately show ?thesis by auto qed then show ?thesis by auto qed qed text ‹From the rescaling properties of Lebesgue measure in a euclidean space, it follows that the measure of any ball can be expressed in terms of the measure of the unit ball.› lemma lebesgue_measure_ball: assumes "R ≥ 0" shows "measure lborel (cball (x::('a::euclidean_space)) R) = R^(DIM('a)) * measure lborel (cball (0::'a) 1)" "emeasure lborel (cball (x::('a::euclidean_space)) R) = R^(DIM('a)) * emeasure lborel (cball (0::'a) 1)" apply (simp add: assms content_cball) by (simp add: assms emeasure_cball ennreal_mult' ennreal_power mult.commute) text ‹We show that the unit ball has positive measure -- this is obvious, but useful. We could show it by arguing that it contains a box, whose measure can be computed, but instead we say that if the measure vanished then the measure of any ball would also vanish, contradicting the fact that the space has infinite measure. This avoids all computations.› lemma lebesgue_measure_ball_pos: "emeasure lborel (cball (0::'a::euclidean_space) 1) > 0" "measure lborel (cball (0::'a::euclidean_space) 1) > 0" proof - show "emeasure lborel (cball (0::'a::euclidean_space) 1) > 0" proof (rule ccontr) assume "¬(emeasure lborel (cball (0::'a::euclidean_space) 1) > 0)" then have "emeasure lborel (cball (0::'a) 1) = 0" by auto then have "emeasure lborel (cball (0::'a) n) = 0" for n::nat using lebesgue_measure_ball(2)[of "real n" 0] by (metis mult_zero_right of_nat_0_le_iff) then have "emeasure lborel (⋃n. cball (0::'a) (real n)) = 0" by (metis (mono_tags, lifting) borel_closed closed_cball emeasure_UN_eq_0 imageE sets_lborel subsetI) moreover have "(⋃n. cball (0::'a) (real n)) = UNIV" by (auto simp add: real_arch_simple) ultimately show False by simp qed moreover have "emeasure lborel (cball (0::'a::euclidean_space) 1) < ∞" by (rule emeasure_bounded_finite, auto) ultimately show "measure lborel (cball (0::'a::euclidean_space) 1) > 0" by (metis borel_closed closed_cball ennreal_0 has_integral_iff_emeasure_lborel has_integral_measure_lborel less_irrefl order_refl zero_less_measure_iff) qed subsubsection ‹infdist and closest point projection› text ‹The distance to a union of two sets is the minimum of the distance to the two sets.› lemma infdist_union_min [mono_intros]: assumes "A ≠ {}" "B ≠ {}" shows "infdist x (A ∪ B) = min (infdist x A) (infdist x B)" using assms by (simp add: infdist_def cINF_union inf_real_def) text ‹The distance to a set is non-increasing with the set.› lemma infdist_mono [mono_intros]: assumes "A ⊆ B" "A ≠ {}" shows "infdist x B ≤ infdist x A" by (simp add: assms infdist_eq_setdist setdist_subset_right) text ‹If a set is proper, then the infimum of the distances to this set is attained.› lemma infdist_proper_attained: assumes "proper C" "C ≠ {}" shows "∃c∈C. infdist x C = dist x c" proof - obtain a where "a ∈ C" using assms by auto have *: "dist x a ≤ dist x z" if "dist a z ≥ 2 * dist a x" for z proof - have "2 * dist a x ≤ dist a z" using that by simp also have "... ≤ dist a x + dist x z" by (intro mono_intros) finally show ?thesis by (simp add: dist_commute) qed have "∃c∈C. ∀d∈C. dist x c ≤ dist x d" apply (rule continuous_attains_inf_proper[OF assms(1) ‹a ∈ C›, of _ "2 * dist a x"]) using * by (auto intro: continuous_intros) then show ?thesis unfolding infdist_def using ‹C ≠ {}› by (metis antisym bdd_below_image_dist cINF_lower le_cINF_iff) qed lemma infdist_almost_attained: assumes "infdist x X < a" "X ≠ {}" shows "∃y∈X. dist x y < a" using assms using cInf_less_iff[of "(dist x)`X"] unfolding infdist_def by auto lemma infdist_triangle_abs [mono_intros]: "¦infdist x A - infdist y A¦ ≤ dist x y" by (metis (full_types) abs_diff_le_iff diff_le_eq dist_commute infdist_triangle) text ‹The next lemma is missing in the library, contrary to its cousin \verb+continuous_infdist+.› text ‹The infimum of the distance to a singleton set is simply the distance to the unique member of the set.› text ‹The closest point projection of $x$ on $A$. It is not unique, so we choose one point realizing the minimal distance. And if there is no such point, then we use $x$, to make some statements true without any assumption.› definition proj_set::"'a::metric_space ⇒ 'a set ⇒ 'a set" where "proj_set x A = {y ∈ A. dist x y = infdist x A}" definition distproj::"'a::metric_space ⇒ 'a set ⇒ 'a" where "distproj x A = (if proj_set x A ≠ {} then SOME y. y ∈ proj_set x A else x)" lemma proj_setD: assumes "y ∈ proj_set x A" shows "y ∈ A" "dist x y = infdist x A" using assms unfolding proj_set_def by auto lemma proj_setI: assumes "y ∈ A" "dist x y ≤ infdist x A" shows "y ∈ proj_set x A" using assms infdist_le[OF ‹y ∈ A›, of x] unfolding proj_set_def by auto lemma proj_setI': assumes "y ∈ A" "⋀z. z ∈ A ⟹ dist x y ≤ dist x z" shows "y ∈ proj_set x A" proof (rule proj_setI[OF ‹y ∈ A›]) show "dist x y ≤ infdist x A" apply (subst infdist_notempty) using assms by (auto intro!: cInf_greatest) qed lemma distproj_in_proj_set: assumes "proj_set x A ≠ {}" shows "distproj x A ∈ proj_set x A" "distproj x A ∈ A" "dist x (distproj x A) = infdist x A" proof - show "distproj x A ∈ proj_set x A" using assms unfolding distproj_def using some_in_eq by auto then show "distproj x A ∈ A" "dist x (distproj x A) = infdist x A" unfolding proj_set_def by auto qed lemma proj_set_nonempty_of_proper: assumes "proper A" "A ≠ {}" shows "proj_set x A ≠ {}" proof - have "∃y. y ∈ A ∧ dist x y = infdist x A" using infdist_proper_attained[OF assms, of x] by auto then show "proj_set x A ≠ {}" unfolding proj_set_def by auto qed lemma distproj_self [simp]: assumes "x ∈ A" shows "proj_set x A = {x}" "distproj x A = x" proof - show "proj_set x A = {x}" unfolding proj_set_def using assms by auto then show "distproj x A = x" unfolding distproj_def by auto qed lemma distproj_closure [simp]: assumes "x ∈ closure A" shows "distproj x A = x" proof (cases "proj_set x A ≠ {}") case True show ?thesis using distproj_in_proj_set(3)[OF True] assms by (metis closure_empty dist_eq_0_iff distproj_self(2) in_closure_iff_infdist_zero) next case False then show ?thesis unfolding distproj_def by auto qed lemma distproj_le: assumes "y ∈ A" shows "dist x (distproj x A) ≤ dist x y" proof (cases "proj_set x A ≠ {}") case True show ?thesis using distproj_in_proj_set(3)[OF True] infdist_le[OF assms] by auto next case False then show ?thesis unfolding distproj_def by auto qed lemma proj_set_dist_le: assumes "y ∈ A" "p ∈ proj_set x A" shows "dist x p ≤ dist x y" using assms infdist_le unfolding proj_set_def by auto subsection ‹Material on ereal and ennreal› text ‹We add the simp rules that we needed to make all computations become more or less automatic.› lemma ereal_of_real_of_ereal_iff [simp]: "ereal(real_of_ereal x) = x ⟷ x ≠ ∞ ∧ x ≠ - ∞" "x = ereal(real_of_ereal x) ⟷ x ≠ ∞ ∧ x ≠ - ∞" by (metis MInfty_neq_ereal(1) PInfty_neq_ereal(2) real_of_ereal.elims)+ declare ereal_inverse_eq_0 [simp] declare ereal_0_gt_inverse [simp] declare ereal_inverse_le_0_iff [simp] declare ereal_divide_eq_0_iff [simp] declare ereal_mult_le_0_iff [simp] declare ereal_zero_le_0_iff [simp] declare ereal_mult_less_0_iff [simp] declare ereal_zero_less_0_iff [simp] declare ereal_uminus_eq_reorder [simp] declare ereal_minus_le_iff [simp] lemma ereal_inverse_noteq_minus_infinity [simp]: "1/(x::ereal) ≠ -∞" by (simp add: divide_ereal_def) lemma ereal_inverse_positive_iff_nonneg_not_infinity [simp]: "0 < 1/(x::ereal) ⟷ (x ≥ 0 ∧ x ≠ ∞)" by (cases x, auto simp add: one_ereal_def) lemma ereal_inverse_negative_iff_nonpos_not_infinity' [simp]: "0 > inverse (x::ereal) ⟷ (x < 0 ∧ x ≠ -∞)" by (cases x, auto simp add: one_ereal_def) lemma ereal_divide_pos_iff [simp]: "0 < x/(y::ereal) ⟷ (y ≠ ∞ ∧ y ≠ -∞) ∧ ((x > 0 ∧ y > 0) ∨ (x < 0 ∧ y < 0) ∨ (y = 0 ∧ x > 0))" unfolding divide_ereal_def by auto lemma ereal_divide_neg_iff [simp]: "0 > x/(y::ereal) ⟷ (y ≠ ∞ ∧ y ≠ -∞) ∧ ((x > 0 ∧ y < 0) ∨ (x < 0 ∧ y > 0) ∨ (y = 0 ∧ x < 0))" unfolding divide_ereal_def by auto text ‹More additions to \verb+mono_intros+.› lemma ereal_leq_imp_neg_leq [mono_intros]: fixes x y::ereal assumes "x ≤ y" shows "-y ≤ -x" using assms by auto lemma ereal_le_imp_neg_le [mono_intros]: fixes x y::ereal assumes "x < y" shows "-y < -x" using assms by auto declare ereal_mult_left_mono [mono_intros] declare ereal_mult_right_mono [mono_intros] declare ereal_mult_strict_right_mono [mono_intros] declare ereal_mult_strict_left_mono [mono_intros] text ‹Monotonicity of basic inclusions.› lemma ennreal_mono': "mono ennreal" by (simp add: ennreal_leI monoI) lemma enn2ereal_mono': "mono enn2ereal" by (simp add: less_eq_ennreal.rep_eq mono_def) lemma e2ennreal_mono': "mono e2ennreal" by (simp add: e2ennreal_mono mono_def) lemma enn2ereal_mono [mono_intros]: assumes "x ≤ y" shows "enn2ereal x ≤ enn2ereal y" using assms less_eq_ennreal.rep_eq by auto lemma ereal_mono: "mono ereal" unfolding mono_def by auto lemma ereal_strict_mono: "strict_mono ereal" unfolding strict_mono_def by auto lemma ereal_mono2 [mono_intros]: assumes "x ≤ y" shows "ereal x ≤ ereal y" by (simp add: assms) lemma ereal_strict_mono2 [mono_intros]: assumes "x < y" shows "ereal x < ereal y" using assms by auto lemma enn2ereal_a_minus_b_plus_b [mono_intros]: "enn2ereal a ≤ enn2ereal (a - b) + enn2ereal b" by (metis diff_add_self_ennreal less_eq_ennreal.rep_eq linear plus_ennreal.rep_eq) text ‹The next lemma follows from the same assertion in ereals.› lemma enn2ereal_strict_mono [mono_intros]: assumes "x < y" shows "enn2ereal x < enn2ereal y" using assms less_ennreal.rep_eq by auto declare ennreal_mult_strict_left_mono [mono_intros] declare ennreal_mult_strict_right_mono [mono_intros] lemma ennreal_ge_0 [mono_intros]: assumes "0 < x" shows "0 < ennreal x" by (simp add: assms) text ‹The next lemma is true and useful in ereal. Note that variants such as $a + b \leq c + d$ implies $a-d \leq c -b$ are not true -- take $a = c = \infty$ and $b = d = 0$...› lemma ereal_minus_le_minus_plus [mono_intros]: fixes a b c::ereal assumes "a ≤ b + c" shows "-b ≤ -a + c" using assms apply (cases a, cases b, cases c, auto) using ereal_infty_less_eq2(2) ereal_plus_1(4) by fastforce lemma tendsto_ennreal_0 [tendsto_intros]: assumes "(u ⤏ 0) F" shows "((λn. ennreal(u n)) ⤏ 0) F" unfolding ennreal_0[symmetric] by (intro tendsto_intros assms) lemma tendsto_ennreal_1 [tendsto_intros]: assumes "(u ⤏ 1) F" shows "((λn. ennreal(u n)) ⤏ 1) F" unfolding ennreal_1[symmetric] by (intro tendsto_intros assms) subsection ‹Miscellaneous› lemma lim_ceiling_over_n [tendsto_intros]: assumes "(λn. u n/n) ⇢ l" shows "(λn. ceiling(u n)/n) ⇢ l" proof (rule tendsto_sandwich[of "λn. u n/n" _ _ "λn. u n/n + 1/n"]) show "∀⇩_{F}n in sequentially. u n / real n ≤ real_of_int ⌈u n⌉ / real n" unfolding eventually_sequentially by (rule exI[of _ 1], auto simp add: divide_simps) show "∀⇩_{F}n in sequentially. real_of_int ⌈u n⌉ / real n ≤ u n / real n + 1 / real n" unfolding eventually_sequentially by (rule exI[of _ 1], auto simp add: divide_simps) have "(λn. u n / real n + 1 / real n) ⇢ l + 0" by (intro tendsto_intros assms) then show "(λn. u n / real n + 1 / real n) ⇢ l" by auto qed (simp add: assms) subsubsection ‹Liminfs and Limsups› text ‹More facts on liminfs and limsups› lemma Limsup_obtain': fixes u::"'a ⇒ 'b::complete_linorder" assumes "Limsup F u > c" "eventually P F" shows "∃n. P n ∧ u n > c" proof - have *: "(INF P∈{P. eventually P F}. SUP x∈{x. P x}. u x) > c" using assms by (simp add: Limsup_def) have **: "c < (SUP x∈{x. P x}. u x)" using less_INF_D[OF *, of P] assms by auto then show ?thesis by (simp add: less_SUP_iff) qed lemma limsup_obtain: fixes u::"nat ⇒ 'a :: complete_linorder" assumes "limsup u > c" shows "∃n ≥ N. u n > c" using Limsup_obtain'[OF assms, of "λn. n ≥ N"] unfolding eventually_sequentially by auto lemma Liminf_obtain': fixes u::"'a ⇒ 'b::complete_linorder" assumes "Liminf F u < c" "eventually P F" shows "∃n. P n ∧ u n < c" proof - have *: "(SUP P∈{P. eventually P F}. INF x∈{x. P x}. u x) < c" using assms by (simp add: Liminf_def) have **: "(INF x∈{x. P x}. u x) < c" using SUP_lessD[OF *, of P] assms by auto then show ?thesis by (simp add: INF_less_iff) qed lemma liminf_obtain: fixes u::"nat ⇒ 'a :: complete_linorder" assumes "liminf u < c" shows "∃n ≥ N. u n < c" using Liminf_obtain'[OF assms, of "λn. n ≥ N"] unfolding eventually_sequentially by auto text ‹The Liminf of a minimum is the minimum of the Liminfs.› lemma Liminf_min_eq_min_Liminf: fixes u v::"nat ⇒ 'a::complete_linorder" shows "Liminf F (λn. min (u n) (v n)) = min (Liminf F u) (Liminf F v)" proof (rule order_antisym) show "Liminf F (λn. min (u n) (v n)) ≤ min (Liminf F u) (Liminf F v)" by (auto simp add: Liminf_mono) have "Liminf F (λn. min (u n) (v n)) > w" if H: "min (Liminf F u) (Liminf F v) > w" for w proof (cases "{w<..<min (Liminf F u) (Liminf F v)} = {}") case True have "eventually (λn. u n > w) F" "eventually (λn. v n > w) F" using H le_Liminf_iff by fastforce+ then have "eventually (λn. min (u n) (v n) > w) F" apply auto using eventually_elim2 by fastforce moreover have "z > w ⟹ z ≥ min (Liminf F u) (Liminf F v)" for z using H True not_le_imp_less by fastforce ultimately have "eventually (λn. min (u n) (v n) ≥ min (Liminf F u) (Liminf F v)) F" by (simp add: eventually_mono) then have "min (Liminf F u) (Liminf F v) ≤ Liminf F (λn. min (u n) (v n))" by (metis Liminf_bounded) then show ?thesis using H less_le_trans by blast next case False then obtain z where "z ∈ {w<..<min (Liminf F u) (Liminf F v)}" by blast then have H: "w < z" "z < min (Liminf F u) (Liminf F v)" by auto then have "eventually (λn. u n > z) F" "eventually (λn. v n > z) F" using le_Liminf_iff by fastforce+ then have "eventually (λn. min (u n) (v n) > z) F" apply auto using eventually_elim2 by fastforce then have "Liminf F (λn. min (u n) (v n)) ≥ z" by (simp add: Liminf_bounded eventually_mono less_imp_le) then show ?thesis using H(1) by auto qed then show "min (Liminf F u) (Liminf F v) ≤ Liminf F (λn. min (u n) (v n))" using not_le_imp_less by blast qed text ‹The Limsup of a maximum is the maximum of the Limsups.› lemma Limsup_max_eq_max_Limsup: fixes u::"'a ⇒ 'b::complete_linorder" shows "Limsup F (λn. max (u n) (v n)) = max (Limsup F u) (Limsup F v)" proof (rule order_antisym) show "max (Limsup F u) (Limsup F v) ≤ Limsup F (λn. max (u n) (v n))" by (auto intro: Limsup_mono) have "Limsup F (λn. max (u n) (v n)) < e" if "max (Limsup F u) (Limsup F v) < e" for e proof (cases "∃t. max (Limsup F u) (Limsup F v) < t ∧ t < e") case True then obtain t where t: "t < e" "max (Limsup F u) (Limsup F v) < t" by auto then have "Limsup F u < t" "Limsup F v < t" using that max_def by auto then have *: "eventually (λn. u n < t) F" "eventually (λn. v n < t) F" by (auto simp: Limsup_lessD) have "eventually (λn. max (u n) (v n) < t) F" using eventually_mono[OF eventually_conj[OF *]] by auto then have "Limsup F (λn. max (u n) (v n)) ≤ t" by (meson Limsup_obtain' not_le_imp_less order.asym) then show ?thesis using t by auto next case False have "Limsup F u < e" "Limsup F v < e" using that max_def by auto then have *: "eventually (λn. u n < e) F" "eventually (λn. v n < e) F" by (auto simp: Limsup_lessD) have "eventually (λn. max (u n) (v n) ≤ max (Limsup F u) (Limsup F v)) F" apply (rule eventually_mono[OF eventually_conj[OF *]]) using False not_le_imp_less by force then have "Limsup F (λn. max (u n) (v n)) ≤ max (Limsup F u) (Limsup F v)" by (meson Limsup_obtain' leD leI) then show ?thesis using that le_less_trans by blast qed then show "Limsup F (λn. max (u n) (v n)) ≤ max (Limsup F u) (Limsup F v)" using not_le_imp_less by blast qed subsubsection ‹Bounding the cardinality of a finite set› text ‹A variation with real bounds.› lemma finite_finite_subset_caract': fixes C::real assumes "⋀G. G ⊆ F ⟹ finite G ⟹ card G ≤ C" shows "finite F ∧ card F ≤ C" by (meson assms finite_if_finite_subsets_card_bdd le_nat_floor order_refl) text ‹To show that a set has cardinality at most one, it suffices to show that any two of its elements coincide.› lemma finite_at_most_singleton: assumes "⋀x y. x ∈ F ⟹ y ∈ F ⟹ x = y" shows "finite F ∧ card F ≤ 1" proof (cases "F = {}") case True then show ?thesis by auto next case False then obtain x where "x ∈ F" by auto then have "F = {x}" using assms by auto then show ?thesis by auto qed text ‹Bounded sets of integers are finite.› lemma finite_real_int_interval [simp]: "finite (range real_of_int ∩ {a..b})" proof - have "range real_of_int ∩ {a..b} ⊆ real_of_int`{floor a..ceiling b}" by (auto, metis atLeastAtMost_iff ceiling_mono ceiling_of_int floor_mono floor_of_int image_eqI) then show ?thesis using finite_subset by blast qed text ‹Well separated sets of real numbers are finite, with controlled cardinality.› lemma separated_in_real_card_bound: assumes "T ⊆ {a..(b::real)}" "d > 0" "⋀x y. x ∈ T ⟹ y ∈ T ⟹ y > x ⟹ y ≥ x + d" shows "finite T" "card T ≤ nat (floor ((b-a)/d) + 1)" proof - define f where "f = (λx. floor ((x-a) / d))" have "f`{a..b} ⊆ {0..floor ((b-a)/d)}" unfolding f_def using ‹d > 0› by (auto simp add: floor_mono frac_le) then have *: "f`T ⊆ {0..floor ((b-a)/d)}" using ‹T ⊆ {a..b}› by auto then have "finite (f`T)" by (rule finite_subset, auto) have "card (f`T) ≤ card {0..floor ((b-a)/d)}" apply (rule card_mono) using * by auto then have card_le: "card (f`T) ≤ nat (floor ((b-a)/d) + 1)" using card_atLeastAtMost_int by auto have *: "f x ≠ f y" if "y ≥ x + d" for x y proof - have "(y-a)/d ≥ (x-a)/d + 1" using ‹d > 0› that by (auto simp add: divide_simps) then show ?thesis unfolding f_def by linarith qed have "inj_on f T" unfolding inj_on_def using * assms(3) by (auto, metis not_less_iff_gr_or_eq) show "finite T" using ‹finite (f`T)› ‹inj_on f T› finite_image_iff by blast have "card T = card (f`T)" using ‹inj_on f T› by (simp add: card_image) then show "card T ≤ nat (floor ((b-a)/d) + 1)" using card_le by auto qed subsection ‹Manipulating finite ordered sets› text ‹We will need below to construct finite sets of real numbers with good properties expressed in terms of consecutive elements of the set. We introduce tools to manipulate such sets, expressing in particular the next and the previous element of the set and controlling how they evolve when one inserts a new element in the set. It works in fact in any linorder, and could also prove useful to construct sets of integer numbers. Manipulating the next and previous elements work well, except at the top (respectively bottom). In our constructions, these will be fixed and called $b$ and $a$.› text ‹Notations for the next and the previous elements.› definition next_in::"'a set ⇒ 'a ⇒ ('a::linorder)" where "next_in A u = Min (A ∩ {u<..})" definition prev_in::"'a set ⇒ 'a ⇒ ('a::linorder)" where "prev_in A u = Max (A ∩ {..<u})" context fixes A::"('a::linorder) set" and a b::'a assumes A: "finite A" "A ⊆ {a..b}" "a ∈ A" "b ∈ A" "a < b" begin text ‹Basic properties of the next element, when one starts from an element different from top.› lemma next_in_basics: assumes "u ∈ {a..<b}" shows "next_in A u ∈ A" "next_in A u > u" "A ∩ {u<..<next_in A u} = {}" proof - have next_in_A: "next_in A u ∈ A ∩ {u<..}" unfolding next_in_def apply (rule Min_in) using assms ‹finite A› ‹b ∈ A› by auto then show "next_in A u ∈ A" "next_in A u > u" by auto show "A ∩ {u<..<next_in A u} = {}" unfolding next_in_def using A by (auto simp add: leD) qed lemma next_inI: assumes "u ∈ {a..<b}" "v ∈ A" "v > u" "{u<..<v} ∩ A = {}" shows "next_in A u = v" using assms next_in_basics[OF ‹u ∈ {a..<b}›] by fastforce text ‹Basic properties of the previous element, when one starts from an element different from bottom.› lemma prev_in_basics: assumes "u ∈ {a<..b}" shows "prev_in A u ∈ A" "prev_in A u < u" "A ∩ {prev_in A u<..<u} = {}" proof - have prev_in_A: "prev_in A u ∈ A ∩ {..<u}" unfolding prev_in_def apply (rule Max_in) using assms ‹finite A› ‹a ∈ A› by auto then show "prev_in A u ∈ A" "prev_in A u < u" by auto show "A ∩ {prev_in A u<..<u} = {}" unfolding prev_in_def using A by (auto simp add: leD) qed lemma prev_inI: assumes "u ∈ {a<..b}" "v ∈ A" "v < u" "{v<..<u} ∩ A = {}" shows "prev_in A u = v" using assms prev_in_basics[OF ‹u ∈ {a<..b}›] by (meson disjoint_iff_not_equal greaterThanLessThan_iff less_linear) text ‹The interval $[a,b]$ is covered by the intervals between the consecutive elements of $A$.› lemma intervals_decomposition: "(⋃ U ∈ {{u..next_in A u} | u. u ∈ A - {b}}. U) = {a..b}" proof show "(⋃U∈{{u..next_in A u} |u. u ∈ A - {b}}. U) ⊆ {a..b}" using ‹A ⊆ {a..b}› next_in_basics(1) apply auto apply fastforce by (metis ‹A ⊆ {a..b}› atLeastAtMost_iff eq_iff le_less_trans less_eq_real_def not_less subset_eq subset_iff_psubset_eq) have "x ∈ (⋃U∈{{u..next_in A u} |u. u ∈ A - {b}}. U)" if "x ∈ {a..b}" for x proof - consider "x = b" | "x ∈ A - {b}" | "x ∉ A" by blast then show ?thesis proof(cases) case 1 define u where "u = prev_in A b" have "b ∈ {a<..b}" using ‹a < b› by simp have "u ∈ A - {b}" unfolding u_def using prev_in_basics[OF ‹b ∈ {a<..b}›] by simp then have "u ∈ {a..<b}" using ‹A ⊆ {a..b}› ‹a < b› by fastforce have "next_in A u = b" using prev_in_basics[OF ‹b ∈ {a<..b}›] next_in_basics[OF ‹u ∈ {a..<b}›] ‹A ⊆ {a..b}› unfolding u_def by force then have "x ∈ {u..next_in A u}" unfolding 1 using prev_in_basics[OF ‹b ∈ {a<..b}›] u_def by auto then show ?thesis using ‹u ∈ A - {b}› by auto next case 2 then have "x ∈ {a..<b}" using ‹A ⊆ {a..b}› ‹a < b› by fastforce have "x ∈ {x.. next_in A x}" using next_in_basics[OF ‹x ∈ {a..<b}›] by auto then show ?thesis using 2 by auto next case 3 then have "x ∈ {a<..b}" using that ‹a ∈ A› leI by fastforce define u where "u = prev_in A x" have "u ∈ A - {b}" unfolding u_def using prev_in_basics[OF ‹x ∈ {a<..b}›] that by auto then have "u ∈ {a..<b}" using ‹A ⊆ {a..b}› ‹a < b› by fastforce have "x ∈ {u..next_in A u}" using prev_in_basics[OF ‹x ∈ {a<..b}›] next_in_basics[OF ‹u ∈ {a..<b}›] unfolding u_def by auto then show ?thesis using ‹u ∈ A - {b}› by auto qed qed then show "{a..b} ⊆ (⋃U∈{{u..next_in A u} |u. u ∈ A - {b}}. U)" by auto qed end text ‹If one inserts an additional element, then next and previous elements are not modified, except at the location of the insertion.› lemma next_in_insert: assumes A: "finite A" "A ⊆ {a..b}" "a ∈ A" "b ∈ A" "a < b" and "x ∈ {a..b} - A" shows "⋀u. u ∈ A - {b, prev_in A x} ⟹ next_in (insert x A) u = next_in A u" "next_in (insert x A) x = next_in A x" "next_in (insert x A) (prev_in A x) = x" proof - define B where "B = insert x A" have B: "finite B" "B ⊆ {a..b}" "a ∈ B" "b ∈ B" "a < b" using assms unfolding B_def by auto have x: "x ∈ {a..<b}" "x ∈ {a<..b}" using assms leI by fastforce+ show "next_in B x = next_in A x" unfolding B_def by (auto simp add: next_in_def) show "next_in B (prev_in A x) = x" apply (rule next_inI[OF B]) unfolding B_def using prev_in_basics[OF A ‹x ∈ {a<..b}›] ‹A ⊆ {a..b}› x by auto fix u assume "u ∈ A - {b, prev_in A x}" then have "u ∈ {a..<b}" using assms by fastforce have "x ∉ {u<..<next_in A u}" proof (rule ccontr) assume "¬(x ∉ {u<..<next_in A u})" then have *: "x ∈ {u<..<next_in A u}" by auto have "prev_in A x = u" apply (rule prev_inI[OF A ‹x ∈ {a<..b}›]) using ‹u ∈ A - {b, prev_in A x}› * next_in_basics[OF A ‹u ∈ {a..<b}›] apply auto by (meson disjoint_iff_not_equal greaterThanLessThan_iff less_trans) then show False using ‹u ∈ A - {b, prev_in A x}› by auto qed show "next_in B u = next_in A u" apply (rule next_inI[OF B ‹u ∈ {a..<b}›]) unfolding B_def using next_in_basics[OF A ‹u ∈ {a..<b}›] ‹x ∉ {u<..<next_in A u}› by auto qed text ‹If consecutive elements are enough separated, this implies a simple bound on the cardinality of the set.› lemma separated_in_real_card_bound2: fixes A::"real set" assumes A: "finite A" "A ⊆ {a..b}" "a ∈ A" "b ∈ A" "a < b" and B: "⋀u. u ∈ A - {b} ⟹ next_in A u ≥ u + d" "d > 0" shows "card A ≤ nat (floor ((b-a)/d) + 1)" proof (rule separated_in_real_card_bound[OF ‹A ⊆ {a..b}› ‹d > 0›]) fix x y assume "x ∈ A" "y ∈ A" "y > x" then have "x ∈ A - {b}" "x ∈ {a..<b}" using ‹A ⊆ {a..b}› by auto have "y ≥ next_in A x" using next_in_basics[OF A ‹x ∈ {a..<b}›] ‹y ∈ A› ‹y > x› by auto then show "y ≥ x + d" using B(1)[OF ‹x ∈ A - {b}›] by auto qed subsection ‹Well-orders› text ‹In this subsection, we give additional lemmas on well-orders or cardinals or whatever, that would well belong to the library, and will be needed below.› lemma (in wo_rel) max2_underS [simp]: assumes "x ∈ underS z" "y ∈ underS z" shows "max2 x y ∈ underS z" using assms max2_def by auto lemma (in wo_rel) max2_underS' [simp]: assumes "x ∈ underS y" shows "max2 x y = y" "max2 y x = y" apply (simp add: underS_E assms max2_def) using assms max2_def ANTISYM antisym_def underS_E by fastforce lemma (in wo_rel) max2_xx [simp]: "max2 x x = x" using max2_def by auto declare underS_notIn [simp] text ‹The abbrevation $=o$ is used both in \verb+Set_Algebras+ and Cardinals. We disable the one from \verb+Set_Algebras+.› no_notation elt_set_eq (infix "=o" 50) lemma regularCard_ordIso: assumes "Card_order r" "regularCard r" "s =o r" shows "regularCard s" unfolding regularCard_def proof (auto) fix K assume K: "K ⊆ Field s" "cofinal K s" obtain f where f: "bij_betw f (Field s) (Field r)" "embed s r f" using ‹s =o r› unfolding ordIso_def iso_def by auto have "f`K ⊆ Field r" using K(1) f(1) bij_betw_imp_surj_on by blast have "cofinal (f`K) r" unfolding cofinal_def proof fix a assume "a ∈ Field r" then obtain a' where a: "a' ∈ Field s" "f a' = a" using f by (metis bij_betw_imp_surj_on imageE) then obtain b' where b: "b' ∈ K" "a' ≠ b' ∧ (a', b') ∈ s" using ‹cofinal K s› unfolding cofinal_def by auto have P1: "f b' ∈ f`K" using b(1) by auto have "a' ≠ b'" "a' ∈ Field s" "b' ∈ Field s" using a(1) b K(1) by auto then have P2: "a ≠ f b'" unfolding a(2)[symmetric] using f(1) unfolding bij_betw_def inj_on_def by auto have "(a', b') ∈ s" using b by auto then have P3: "(a, f b') ∈ r" unfolding a(2)[symmetric] using f by (meson FieldI1 FieldI2 Card_order_ordIso[OF assms(1) assms(3)] card_order_on_def iso_defs(1) iso_iff2) show "∃b∈f ` K. a ≠ b ∧ (a, b) ∈ r" using P1 P2 P3 by blast qed then have "|f`K| =o r" using ‹regularCard r› ‹f`K ⊆ Field r› unfolding regularCard_def by auto moreover have "|f`K| =o |K|" using f(1) K(1) by (meson bij_betw_subset card_of_ordIsoI ordIso_symmetric) ultimately show "|K| =o s" using ‹s =o r› by (meson ordIso_symmetric ordIso_transitive) qed lemma AboveS_not_empty_in_regularCard: assumes "|S| <o r" "S ⊆ Field r" assumes r: "Card_order r" "regularCard r" "¬finite (Field r)" shows "AboveS r S ≠ {}" proof - have "¬(cofinal S r)" using assms not_ordLess_ordIso unfolding regularCard_def by auto then obtain a where a: "a ∈ Field r" "∀b∈S. ¬(a ≠ b ∧ (a,b) ∈ r)" unfolding cofinal_def by auto have *: "a = b ∨ (b, a) ∈ r" if "b ∈ S" for b proof - have "a = b ∨ (a,b) ∉ r" using a that by auto then show ?thesis using ‹Card_order r› ‹a ∈ Field r› ‹b ∈ S› ‹S ⊆ Field r› unfolding card_order_on_def well_order_on_def linear_order_on_def total_on_def by auto qed obtain c where "c ∈ Field r" "c ≠ a" "(a, c) ∈ r" using a(1) r infinite_Card_order_limit by fastforce then have "c ∈ AboveS r S" unfolding AboveS_def apply simp using Card_order_trans[OF r(1)] by (metis *) then show ?thesis by auto qed lemma AboveS_not_empty_in_regularCard': assumes "|S| <o r" "f`S ⊆ Field r" "T ⊆ S" assumes r: "Card_order r" "regularCard r" "¬finite (Field r)" shows "AboveS r (f`T) ≠ {}" proof - have "|f`T| ≤o |T|" by simp moreover have "|T| ≤o |S|" using ‹T ⊆ S› by simp ultimately have *: "|f`T| <o r" using ‹|S| <o r› by (meson ordLeq_ordLess_trans) show ?thesis using AboveS_not_empty_in_regularCard[OF * _ r] ‹T ⊆ S› ‹f`S ⊆ Field r› by auto qed lemma Well_order_extend: assumes WELL: "well_order_on A r" and SUB: "A ⊆ B" shows "∃r'. well_order_on B r' ∧ r ⊆ r'" proof- have r: "Well_order r ∧ Field r = A" using WELL well_order_on_Well_order by blast let ?C = "B - A" obtain r'' where "well_order_on ?C r''" using well_order_on by blast then have r'': "Well_order r'' ∧ Field r'' = ?C" using well_order_on_Well_order by blast let ?r' = "r Osum r''" have "Field r Int Field r'' = {}" using r r'' by auto then have "r ≤o ?r'" using Osum_ordLeq[of r r''] r r'' by blast then have "Well_order ?r'" unfolding ordLeq_def by auto moreover have "Field ?r' = B" using r r'' SUB by (auto simp add: Field_Osum) ultimately have "well_order_on B ?r'" by auto moreover have "r ⊆ ?r'" by (simp add: Osum_def subrelI) ultimately show ?thesis by blast qed text ‹The next lemma shows that, if the range of a function is endowed with a wellorder, then one can pull back this wellorder by the function, and then extend it in the fibers of the function in order to keep the wellorder property. The proof is done by taking an arbitrary family of wellorders on each of the fibers, and using the lexicographic order: one has $x < y$ if $f x < f y$, or if $f x = f y$ and, in the corresponding fiber of $f$, one has $x < y$. To formalize it, it is however more efficient to use one single wellorder, and restrict it to each fiber.› lemma Well_order_pullback: assumes "Well_order r" shows "∃s. Well_order s ∧ Field s = UNIV ∧ (∀x y. (f x, f y) ∈ (r-Id) ⟶ (x, y) ∈ s)" proof - obtain r2 where r2: "Well_order r2" "Field r2 = UNIV" "r ⊆ r2" using Well_order_extend[OF assms, of UNIV] well_order_on_Well_order by auto obtain s2 where s2: "Well_order s2" "Field s2 = (UNIV::'b set)" by (meson well_ordering) have r2s2: "⋀x y z. (x, y) ∈ s2 ⟹ (y, z) ∈ s2 ⟹ (x, z) ∈ s2" "⋀x. (x, x) ∈ s2" "⋀x y. (x, y) ∈ s2 ∨ (y, x) ∈ s2" "⋀x y. (x, y) ∈ s2 ⟹ (y, x) ∈ s2 ⟹ x = y" "⋀x y z. (x, y) ∈ r2 ⟹ (y, z) ∈ r2 ⟹ (x, z) ∈ r2" "⋀x. (x, x) ∈ r2" "⋀x y. (x, y) ∈ r2 ∨ (y, x) ∈ r2" "⋀x y. (x, y) ∈ r2 ⟹ (y, x) ∈ r2 ⟹ x = y" using r2 s2 unfolding well_order_on_def linear_order_on_def partial_order_on_def total_on_def preorder_on_def antisym_def refl_on_def trans_def by (metis UNIV_I)+ define s where "s = {(x,y). (f x, f y) ∈ r2 ∧ (f x = f y ⟶ (x, y) ∈ s2)}" have "linear_order s" unfolding linear_order_on_def partial_order_on_def preorder_on_def proof (auto) show "total_on UNIV s" unfolding s_def apply (rule total_onI, auto) using r2s2 by metis+ show "refl_on UNIV s" unfolding s_def apply (rule refl_onI, auto) using r2s2 by blast+ show "trans s" unfolding s_def apply (rule transI, auto) using r2s2 by metis+ show "antisym s" unfolding s_def apply (rule antisymI, auto) using r2s2 by metis+ qed moreover have "wf (s - Id)" proof (rule wfI_min) fix x::'b and Q assume "x ∈ Q" obtain z' where z': "z' ∈ f`Q" "⋀y. (y, z') ∈ r2 - Id ⟶ y ∉ f`Q" proof (rule wfE_min[of "r2-Id" "f x" "f`Q"], auto) show "wf(r2-Id)" using ‹Well_order r2› unfolding well_order_on_def by auto show "f x ∈ f`Q" using ‹x ∈ Q› by auto qed define Q2 where "Q2 = Q ∩ f-`{z'}" obtain z where z: "z ∈ Q2" "⋀y. (y, z) ∈ s2 - Id ⟶ y ∉ Q2" proof (rule wfE_min'[of "s2-Id" "Q2"], auto) show "wf(s2-Id)" using ‹Well_order s2› unfolding well_order_on_def by auto assume "Q2 = {}" then show False unfolding Q2_def using ‹z' ∈ f`Q› by blast qed have "(y, z) ∈ (s-Id) ⟹ y ∉ Q" for y unfolding s_def using z' z Q2_def by auto then show "∃z∈Q. ∀y. (y, z) ∈ s - Id ⟶ y ∉ Q" using ‹z ∈ Q2› Q2_def by auto qed ultimately have "well_order_on UNIV s" unfolding well_order_on_def by simp moreover have "(f x, f y) ∈ (r-Id) ⟶ (x, y) ∈ s" for x y unfolding s_def using ‹r ⊆ r2› by auto ultimately show ?thesis using well_order_on_Well_order by metis qed end (*of theory Library_Complements*)

# Theory Eexp_Eln

(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr License: BSD *) section ‹The exponential on extended real numbers.› theory Eexp_Eln imports Library_Complements begin text ‹To define the distance on the Gromov completion of hyperbolic spaces, we need to use the exponential on extended real numbers. We can not use the symbol \verb+exp+, as this symbol is already used in Banach algebras, so we use \verb+ennexp+ instead. We prove its basic properties (together with properties of the logarithm) here. We also use it to define the square root on ennreal. Finally, we also define versions from ereal to ereal.› function ennexp::"ereal ⇒ ennreal" where "ennexp (ereal r) = ennreal (exp r)" | "ennexp (∞) = ∞" | "ennexp (-∞) = 0" by (auto intro: ereal_cases) termination by standard (rule wf_empty) lemma ennexp_0 [simp]: "ennexp 0 = 1" by (auto simp add: zero_ereal_def one_ennreal_def) function eln::"ennreal ⇒ ereal" where "eln (ennreal r) = (if r ≤ 0 then -∞ else ereal (ln r))" | "eln (∞) = ∞" by (auto intro: ennreal_cases, metis ennreal_eq_0_iff, simp add: ennreal_neg) termination by standard (rule wf_empty) lemma eln_simps [simp]: "eln 0 = -∞" "eln 1 = 0" "eln top = ∞" apply (simp only: eln.simps ennreal_0[symmetric], simp) apply (simp only: eln.simps ennreal_1[symmetric], simp) using eln.simps(2) by auto lemma eln_real_pos: assumes "r > 0" shows "eln (ennreal r) = ereal (ln r)" using eln.simps assms by auto lemma eln_ennexp [simp]: "eln (ennexp x) = x" apply (cases x) using eln.simps by auto lemma ennexp_eln [simp]: "ennexp (eln x) = x" apply (cases x) using eln.simps by auto lemma ennexp_strict_mono: "strict_mono ennexp" proof - have "ennexp x < ennexp y" if "x < y" for x y apply (cases x, cases y) using that apply (auto simp add: ennreal_less_iff) by (cases y, auto) then show ?thesis unfolding strict_mono_def by auto qed lemma ennexp_mono: "mono ennexp" using ennexp_strict_mono by (simp add: strict_mono_mono) lemma ennexp_strict_mono2 [mono_intros]: assumes "x < y" shows "ennexp x < ennexp y" using ennexp_strict_mono assms unfolding strict_mono_def by auto lemma ennexp_mono2 [mono_intros]: assumes "x ≤ y" shows "ennexp x ≤ ennexp y" using ennexp_mono assms unfolding mono_def by auto lemma ennexp_le1 [simp]: "ennexp x ≤ 1 ⟷ x ≤ 0" by (metis ennexp_0 ennexp_mono2 ennexp_strict_mono eq_iff le_cases strict_mono_eq) lemma ennexp_ge1 [simp]: "ennexp x ≥ 1 ⟷ x ≥ 0" by (metis ennexp_0 ennexp_mono2 ennexp_strict_mono eq_iff le_cases strict_mono_eq) lemma eln_strict_mono: "strict_mono eln" by (metis ennexp_eln strict_monoI ennexp_strict_mono strict_mono_less) lemma eln_mono: "mono eln" using eln_strict_mono by (simp add: strict_mono_mono) lemma eln_strict_mono2 [mono_intros]: assumes "x < y" shows "eln x < eln y" using eln_strict_mono assms unfolding strict_mono_def by auto lemma eln_mono2 [mono_intros]: assumes "x ≤ y" shows "eln x ≤ eln y" using eln_mono assms unfolding mono_def by auto lemma eln_le0 [simp]: "eln x ≤ 0 ⟷ x ≤ 1" by (metis ennexp_eln ennexp_le1) lemma eln_ge0 [simp]: "eln x ≥ 0 ⟷ x ≥ 1" by (metis ennexp_eln ennexp_ge1) lemma bij_ennexp: "bij ennexp" by (auto intro!: bij_betw_byWitness[of _ eln]) lemma bij_eln: "bij eln" by (auto intro!: bij_betw_byWitness[of _ ennexp]) lemma ennexp_continuous: "continuous_on UNIV ennexp" apply (rule continuous_onI_mono) using ennexp_mono unfolding mono_def by (auto simp add: bij_ennexp bij_is_surj) lemma ennexp_tendsto [tendsto_intros]: assumes "((λn. u n) ⤏ l) F" shows "((λn. ennexp(u n)) ⤏ ennexp l) F" using ennexp_continuous assms by (metis UNIV_I continuous_on tendsto_compose) lemma eln_continuous: "continuous_on UNIV eln" apply (rule continuous_onI_mono) using eln_mono unfolding mono_def by (auto simp add: bij_eln bij_is_surj) lemma eln_tendsto [tendsto_intros]: assumes "((λn. u n) ⤏ l) F" shows "((λn. eln(u n)) ⤏ eln l) F" using eln_continuous assms by (metis UNIV_I continuous_on tendsto_compose) lemma ennexp_special_values [simp]: "ennexp x = 0 ⟷ x = -∞" "ennexp x = 1 ⟷ x = 0" "ennexp x = ∞ ⟷ x = ∞" "ennexp x = top ⟷ x = ∞" by auto (metis eln_ennexp eln_simps)+ lemma eln_special_values [simp]: "eln x = -∞ ⟷ x = 0" "eln x = 0 ⟷ x = 1" "eln x = ∞ ⟷ x = ∞" apply auto apply (metis ennexp.simps ennexp_eln ennexp_0)+ by (metis ennexp.simps(2) ennexp_eln infinity_ennreal_def) lemma ennexp_add_mult: assumes "¬((a = ∞ ∧ b = -∞) ∨ (a = -∞ ∧ b = ∞))" shows "ennexp(a+b) = ennexp a * ennexp b" apply (cases a, cases b) using assms by (auto simp add: ennreal_mult'' exp_add ennreal_top_eq_mult_iff) lemma eln_mult_add: assumes "¬((a = ∞ ∧ b = 0) ∨ (a = 0 ∧ b = ∞))" shows "eln(a * b) = eln a + eln b" by (smt assms ennexp.simps(2) ennexp.simps(3) ennexp_add_mult ennexp_eln eln_ennexp) text ‹We can also define the square root on ennreal using the above exponential.› definition ennsqrt::"ennreal ⇒ ennreal" where "ennsqrt x = ennexp(eln x/2)" lemma ennsqrt_square [simp]: "(ennsqrt x) * (ennsqrt x) = x" proof - have "y/2 + y/2 = y" for y::ereal by (cases y, auto) then show ?thesis unfolding ennsqrt_def by (subst ennexp_add_mult[symmetric], auto) qed lemma ennsqrt_simps [simp]: "ennsqrt 0 = 0" "ennsqrt 1 = 1" "ennsqrt ∞ = ∞" "ennsqrt top = top" unfolding ennsqrt_def by auto lemma ennsqrt_mult: "ennsqrt(a * b) = ennsqrt a * ennsqrt b" proof - have [simp]: "z/ereal 2 = -∞ ⟷ z = -∞" for z by (auto simp add: ereal_divide_eq) consider "a = 0" | "b = 0" | "a > 0 ∧ b > 0" using zero_less_iff_neq_zero by auto then show ?thesis apply (cases, auto) apply (cases a, cases b, auto simp add: ennreal_mult_top ennreal_top_mult) unfolding ennsqrt_def apply (subst ennexp_add_mult[symmetric], auto) apply (subst eln_mult_add, auto) done qed lemma ennsqrt_square2 [simp]: "ennsqrt (x * x) = x" unfolding ennsqrt_mult by auto lemma ennsqrt_eq_iff_square: "ennsqrt x = y ⟷ x = y * y" by auto lemma ennsqrt_bij: "bij ennsqrt" by (rule bij_betw_byWitness[of _ "λx. x * x"], auto) lemma ennsqrt_strict_mono: "strict_mono ennsqrt" unfolding ennsqrt_def apply (rule strict_mono_compose[OF ennexp_strict_mono]) apply (rule strict_mono_compose[OF _ eln_strict_mono]) by (auto simp add: ereal_less_divide_pos ereal_mult_divide strict_mono_def) lemma ennsqrt_mono: "mono ennsqrt" using ennsqrt_strict_mono by (simp add: strict_mono_mono) lemma ennsqrt_mono2 [mono_intros]: assumes "x ≤ y" shows "ennsqrt x ≤ ennsqrt y" using ennsqrt_mono assms unfolding mono_def by auto lemma ennsqrt_continuous: "continuous_on UNIV ennsqrt" apply (rule continuous_onI_mono) using ennsqrt_mono unfolding mono_def by (auto simp add: ennsqrt_bij bij_is_surj) lemma ennsqrt_tendsto [tendsto_intros]: assumes "((λn. u n) ⤏ l) F" shows "((λn. ennsqrt(u n)) ⤏ ennsqrt l) F" using ennsqrt_continuous assms by (metis UNIV_I continuous_on tendsto_compose) lemma ennsqrt_ennreal_ennreal_sqrt [simp]: assumes "t ≥ (0::real)" shows "ennsqrt (ennreal t) = ennreal (sqrt t)" proof - have "ennreal t = ennreal (sqrt t) * ennreal(sqrt t)" apply (subst ennreal_mult[symmetric]) using assms by auto then show ?thesis by auto qed lemma ennreal_sqrt2: "ennreal (sqrt 2) = ennsqrt 2" using ennsqrt_ennreal_ennreal_sqrt[of 2] by auto lemma ennsqrt_4 [simp]: "ennsqrt 4 = 2" by (metis ennreal_numeral ennsqrt_ennreal_ennreal_sqrt real_sqrt_four zero_le_numeral) lemma ennsqrt_le [simp]: "ennsqrt x ≤ ennsqrt y ⟷ x ≤ y" proof assume "ennsqrt x ≤ ennsqrt y" then have "ennsqrt x * ennsqrt x ≤ ennsqrt y * ennsqrt y" by (intro mult_mono, auto) then show "x ≤ y" by auto qed (auto intro: mono_intros) text ‹We can also define the square root on ereal using the square root on ennreal, and $0$ for negative numbers.› definition esqrt::"ereal ⇒ ereal" where "esqrt x = enn2ereal(ennsqrt (e2ennreal x))" lemma esqrt_square [simp]: assumes "x ≥ 0" shows "(esqrt x) * (esqrt x) = x" unfolding esqrt_def times_ennreal.rep_eq[symmetric] ennsqrt_square[of "e2ennreal x"] using assms enn2ereal_e2ennreal by auto lemma esqrt_of_neg [simp]: assumes "x ≤ 0" shows "esqrt x = 0" unfolding esqrt_def e2ennreal_neg[OF assms] by (auto simp add: zero_ennreal.rep_eq) lemma esqrt_nonneg [simp]: "esqrt x ≥ 0" unfolding esqrt_def by auto lemma esqrt_eq_iff_square [simp]: assumes "x ≥ 0" "y ≥ 0" shows "esqrt x = y ⟷ x = y * y" using esqrt_def esqrt_square assms apply auto by (metis e2ennreal_enn2ereal ennsqrt_square2 eq_onp_same_args ereal_ennreal_cases leD times_ennreal.abs_eq) lemma esqrt_simps [simp]: "esqrt 0 = 0" "esqrt 1 = 1" "esqrt ∞ = ∞" "esqrt top = top" "esqrt (-∞) = 0" by (auto simp: top_ereal_def) lemma esqrt_mult: assumes "a ≥ 0" shows "esqrt(a * b) = esqrt a * esqrt b" proof (cases "b ≥ 0") case True show ?thesis unfolding esqrt_def apply (subst times_ennreal.rep_eq[symmetric]) apply (subst ennsqrt_mult[of "e2ennreal a" "e2ennreal b", symmetric]) apply (subst times_ennreal.abs_eq) using assms True by (auto simp add: eq_onp_same_args) next case False then have "a * b ≤ 0" using assms ereal_mult_le_0_iff by auto then have "esqrt(a * b) = 0" by auto moreover have "esqrt b = 0" using False by auto ultimately show ?thesis by auto qed lemma esqrt_square2 [simp]: "esqrt(x * x) = abs(x)" proof - have "esqrt(x * x) = esqrt(abs x * abs x)" by (metis (no_types, hide_lams) abs_ereal_ge0 ereal_abs_mult ereal_zero_le_0_iff linear) also have "... = abs x" by (auto simp add: esqrt_mult) finally show ?thesis by auto qed lemma esqrt_mono: "mono esqrt" unfolding esqrt_def mono_def by (auto intro: mono_intros) lemma esqrt_mono2 [mono_intros]: assumes "x ≤ y" shows "esqrt x ≤ esqrt y" using esqrt_mono assms unfolding mono_def by auto lemma esqrt_continuous: "continuous_on UNIV esqrt" unfolding esqrt_def apply (rule continuous_on_compose2[of UNIV enn2ereal], intro continuous_on_enn2ereal) by (rule continuous_on_compose2[of UNIV ennsqrt], auto intro!: ennsqrt_continuous continuous_on_e2ennreal) lemma esqrt_tendsto [tendsto_intros]: assumes "((λn. u n) ⤏ l) F" shows "((λn. esqrt(u n)) ⤏ esqrt l) F" using esqrt_continuous assms by (metis UNIV_I continuous_on tendsto_compose) lemma esqrt_ereal_ereal_sqrt [simp]: assumes "t ≥ (0::real)" shows "esqrt (ereal t) = ereal (sqrt t)" proof - have "ereal t = ereal (sqrt t) * ereal(sqrt t)" using assms by auto then show ?thesis using assms ereal_less_eq(5) esqrt_mult esqrt_square real_sqrt_ge_zero by presburger qed lemma ereal_sqrt2: "ereal (sqrt 2) = esqrt 2" using esqrt_ereal_ereal_sqrt[of 2] by auto lemma esqrt_4 [simp]: "esqrt 4 = 2" by auto lemma esqrt_le [simp]: "esqrt x ≤ esqrt y ⟷ (x ≤ 0 ∨ x ≤ y)" apply (auto simp add: esqrt_mono2) by (metis eq_iff ereal_zero_times esqrt_mono2 esqrt_square le_cases) text ‹Finally, we define eexp, as the composition of ennexp and the injection of ennreal in ereal.› definition eexp::"ereal ⇒ ereal" where "eexp x = enn2ereal (ennexp x)" lemma eexp_special_values [simp]: "eexp 0 = 1" "eexp (∞) = ∞" "eexp(-∞) = 0" unfolding eexp_def by (auto simp add: zero_ennreal.rep_eq one_ennreal.rep_eq) lemma eexp_strict_mono: "strict_mono eexp" unfolding eexp_def using ennexp_strict_mono unfolding strict_mono_def by (auto intro: mono_intros) lemma eexp_mono: "mono eexp" using eexp_strict_mono by (simp add: strict_mono_mono) lemma eexp_strict_mono2 [mono_intros]: assumes "x < y" shows "eexp x < eexp y" using eexp_strict_mono assms unfolding strict_mono_def by auto lemma eexp_mono2 [mono_intros]: assumes "x ≤ y" shows "eexp x ≤ eexp y" using eexp_mono assms unfolding mono_def by auto lemma eexp_le_eexp_iff_le: "eexp x ≤ eexp y ⟷ x ≤ y" using eexp_strict_mono2 not_le by (auto intro: mono_intros) lemma eexp_lt_eexp_iff_lt: "eexp x < eexp y ⟷ x < y" using eexp_mono2 not_le by (auto intro: mono_intros) lemma eexp_special_values_iff [simp]: "eexp x = 0 ⟷ x = -∞" "eexp x = 1 ⟷ x = 0" "eexp x = ∞ ⟷ x = ∞" "eexp x = top ⟷ x = ∞" unfolding eexp_def apply (auto simp add: zero_ennreal.rep_eq one_ennreal.rep_eq top_ereal_def) apply (metis e2ennreal_enn2ereal ennexp.simps(3) ennexp_strict_mono strict_mono_eq zero_ennreal_def) by (metis e2ennreal_enn2ereal eln_ennexp eln_simps(2) one_ennreal_def) lemma eexp_ineq_iff [simp]: "eexp x ≤ 1 ⟷ x ≤ 0" "eexp x ≥ 1 ⟷ x ≥ 0" "eexp x > 1 ⟷ x > 0" "eexp x < 1 ⟷ x < 0" "eexp x ≥ 0" "eexp x > 0 ⟷ x ≠ - ∞" "eexp x < ∞ ⟷ x ≠ ∞" apply (metis eexp_le_eexp_iff_le eexp_lt_eexp_iff_lt eexp_special_values)+ apply (simp add: eexp_def) using eexp_strict_mono2 apply (force) by simp lemma eexp_ineq [mono_intros]: "x ≤ 0 ⟹ eexp x ≤ 1" "x < 0 ⟹ eexp x < 1" "x ≥ 0 ⟹ eexp x ≥ 1" "x > 0 ⟹ eexp x > 1" "eexp x ≥ 0" "x > -∞ ⟹ eexp x > 0" "x < ∞ ⟹ eexp x < ∞" by auto lemma eexp_continuous: "continuous_on UNIV eexp" unfolding eexp_def by (rule continuous_on_compose2[of UNIV enn2ereal], auto simp: continuous_on_enn2ereal ennexp_continuous) lemma eexp_tendsto' [simp]: "((λn. eexp(u n)) ⤏ eexp l) F ⟷ ((λn. u n) ⤏ l) F" proof assume H: "((λn. eexp (u n)) ⤏ eexp l) F" have "((λn. eln (e2ennreal (eexp (u n)))) ⤏ eln (e2ennreal (eexp l))) F" by (intro tendsto_intros H) then show "(u ⤏ l) F" unfolding eexp_def by auto next assume "(u ⤏ l) F" then show "((λn. eexp(u n)) ⤏ eexp l) F" using eexp_continuous by (metis UNIV_I continuous_on tendsto_compose) qed lemma eexp_tendsto [tendsto_intros]: assumes "((λn. u n) ⤏ l) F" shows "((λn. eexp(u n)) ⤏ eexp l) F" using assms by auto lemma eexp_add_mult: assumes "¬((a = ∞ ∧ b = -∞) ∨ (a = -∞ ∧ b = ∞))" shows "eexp(a+b) = eexp a * eexp b" using ennexp_add_mult[OF assms] unfolding eexp_def by (simp add: times_ennreal.rep_eq) lemma eexp_ereal [simp]: "eexp(ereal x) = ereal(exp x)" by (simp add: eexp_def) end (*of theory Eexp_Eln*)

# Theory Hausdorff_Distance

(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr License: BSD *) section ‹Hausdorff distance› theory Hausdorff_Distance imports Library_Complements begin subsection ‹Preliminaries› subsection ‹Hausdorff distance› text ‹The Hausdorff distance between two subsets of a metric space is the minimal $M$ such that each set is included in the $M$-neighborhood of the other. For nonempty bounded sets, it satisfies the triangular inequality, it is symmetric, but it vanishes on sets that have the same closure. In particular, it defines a distance on closed bounded nonempty sets. We establish all these properties below.› definition hausdorff_distance::"('a::metric_space) set ⇒ 'a set ⇒ real" where "hausdorff_distance A B = (if A = {} ∨ B = {} ∨ (¬(bounded A)) ∨ (¬(bounded B)) then 0 else max (SUP x∈A. infdist x B) (SUP x∈B. infdist x A))" lemma hausdorff_distance_self [simp]: "hausdorff_distance A A = 0" unfolding hausdorff_distance_def by auto lemma hausdorff_distance_sym: "hausdorff_distance A B = hausdorff_distance B A" unfolding hausdorff_distance_def by auto lemma hausdorff_distance_points [simp]: "hausdorff_distance {x} {y} = dist x y" unfolding hausdorff_distance_def by (auto, metis dist_commute max.idem) text ‹The Hausdorff distance is expressed in terms of a supremum. To use it, one needs again and again to show that this is the supremum of a set which is bounded from above.› lemma bdd_above_infdist_aux: assumes "bounded A" "bounded B" shows "bdd_above ((λx. infdist x B)`A)" proof (cases "B = {}") case True then show ?thesis unfolding infdist_def by auto next case False then obtain y where "y ∈ B" by auto then have "infdist x B ≤ dist x y" if "x ∈ A" for x by (simp add: infdist_le) then show ?thesis unfolding bdd_above_def by (auto, metis assms(1) bounded_any_center dist_commute order_trans) qed lemma hausdorff_distance_nonneg [simp, mono_intros]: "hausdorff_distance A B ≥ 0" proof (cases "A = {} ∨ B = {} ∨ (¬(bounded A)) ∨ (¬(bounded B))") case True then show ?thesis unfolding hausdorff_distance_def by auto next case False then have "A ≠ {}" "B ≠ {}" "bounded A" "bounded B" by auto have "(SUP x∈A. infdist x B) ≥ 0" using bdd_above_infdist_aux[OF ‹bounded A› ‹bounded B›] infdist_nonneg by (metis ‹A ≠ {}› all_not_in_conv cSUP_upper2) moreover have "(SUP x∈B. infdist x A) ≥ 0" using bdd_above_infdist_aux[OF ‹bounded B› ‹bounded A›] infdist_nonneg by (metis ‹B ≠ {}› all_not_in_conv cSUP_upper2) ultimately show ?thesis unfolding hausdorff_distance_def by auto qed lemma hausdorff_distanceI: assumes "⋀x. x ∈ A ⟹ infdist x B ≤ D" "⋀x. x ∈ B ⟹ infdist x A ≤ D" "D ≥ 0" shows "hausdorff_distance A B ≤ D" proof (cases "A = {} ∨ B = {} ∨ (¬(bounded A)) ∨ (¬(bounded B))") case True then show ?thesis unfolding hausdorff_distance_def using ‹D ≥ 0› by auto next case False then have "A ≠ {}" "B ≠ {}" "bounded A" "bounded B" by auto have "(SUP x∈A. infdist x B) ≤ D" apply (rule cSUP_least, simp add: ‹A ≠ {}›) using assms(1) by blast moreover have "(SUP x∈B. infdist x A) ≤ D" apply (rule cSUP_least, simp add: ‹B ≠ {}›) using assms(2) by blast ultimately show ?thesis unfolding hausdorff_distance_def using False by auto qed lemma hausdorff_distanceI2: assumes "⋀x. x ∈ A ⟹ ∃y∈B. dist x y ≤ D" "⋀x. x ∈ B ⟹ ∃y∈A. dist x y ≤ D" "D ≥ 0" shows "hausdorff_distance A B ≤ D" proof (rule hausdorff_distanceI[OF _ _ ‹D ≥ 0›]) fix x assume "x ∈ A" show "infdist x B ≤ D" using assms(1)[OF ‹x ∈ A›] infdist_le2 by fastforce next fix x assume "x ∈ B" show "infdist x A ≤ D" using assms(2)[OF ‹x ∈ B›] infdist_le2 by fastforce qed lemma infdist_le_hausdorff_distance [mono_intros]: assumes "x ∈ A" "bounded A" "bounded B" shows "infdist x B ≤ hausdorff_distance A B" proof (cases "B = {}") case True then have "infdist x B = 0" unfolding infdist_def by auto then show ?thesis using hausdorff_distance_nonneg by auto next case False have "infdist x B ≤ (SUP y∈A. infdist y B)" using bdd_above_infdist_aux[OF ‹bounded A› ‹bounded B›] by (meson assms(1) cSUP_upper) then show ?thesis unfolding hausdorff_distance_def using assms False by auto qed lemma hausdorff_distance_infdist_triangle [mono_intros]: assumes "B ≠ {}" "bounded B" "bounded C" shows "infdist x C ≤ infdist x B + hausdorff_distance B C" proof (cases "C = {}") case True then have "infdist x C = 0" unfolding infdist_def by auto then show ?thesis using infdist_nonneg[of x B] hausdorff_distance_nonneg[of B C] by auto next case False have "infdist x C - hausdorff_distance B C ≤ dist x b" if "b ∈ B" for b proof - have "infdist x C ≤ infdist b C + dist x b" by (rule infdist_triangle) also have "... ≤ dist x b + hausdorff_distance B C" using infdist_le_hausdorff_distance[OF ‹b ∈ B› ‹bounded B› ‹bounded C›] by auto finally show ?thesis by auto qed then have "infdist x C - hausdorff_distance B C ≤ infdist x B" unfolding infdist_def using ‹B ≠ {}› by (simp add: le_cINF_iff) then show ?thesis by auto qed lemma hausdorff_distance_triangle [mono_intros]: assumes "B ≠ {}" "bounded B" shows "hausdorff_distance A C ≤ hausdorff_distance A B + hausdorff_distance B C" proof (cases "A = {} ∨ C = {} ∨ (¬(bounded A)) ∨ (¬(bounded C))") case True then have "hausdorff_distance A C = 0" unfolding hausdorff_distance_def by auto then show ?thesis using hausdorff_distance_nonneg[of A B] hausdorff_distance_nonneg[of B C] by auto next case False then have *: "A ≠ {}" "C ≠ {}" "bounded A" "bounded C" by auto define M where "M = hausdorff_distance A B + hausdorff_distance B C" have "infdist x C ≤ M" if "x ∈ A" for x using hausdorff_distance_infdist_triangle[OF ‹B ≠ {}› ‹bounded B › ‹bounded C›, of x] infdist_le_hausdorff_distance[OF ‹x ∈ A› ‹bounded A› ‹bounded B›] by (auto simp add: M_def) moreover have "infdist x A ≤ M" if "x ∈ C" for x using hausdorff_distance_infdist_triangle[OF ‹B ≠ {}› ‹bounded B › ‹bounded A›, of x] infdist_le_hausdorff_distance[OF ‹x ∈ C› ‹bounded C› ‹bounded B›] by (auto simp add: hausdorff_distance_sym M_def) ultimately have "hausdorff_distance A C ≤ M" unfolding hausdorff_distance_def using * bdd_above_infdist_aux by (auto simp add: cSUP_least) then show ?thesis unfolding M_def by auto qed lemma hausdorff_distance_subset: assumes "A ⊆ B" "A ≠ {}" "bounded B" shows "hausdorff_distance A B = (SUP x∈B. infdist x A)" proof - have H: "B ≠ {}" "bounded A" using assms bounded_subset by auto have "(SUP x∈A. infdist x B) = 0" using assms by (simp add: subset_eq) moreover have "(SUP x∈B. infdist x A) ≥ 0" using bdd_above_infdist_aux[OF ‹bounded B› ‹bounded A›] infdist_nonneg[of _ A] by (meson H(1) cSUP_upper2 ex_in_conv) ultimately show ?thesis unfolding hausdorff_distance_def using assms H by auto qed lemma hausdorff_distance_closure [simp]: "hausdorff_distance A (closure A) = 0" proof (cases "A = {} ∨ (¬(bounded A))") case True then show ?thesis unfolding hausdorff_distance_def by auto next case False then have "A ≠ {}" "bounded A" by auto then have "closure A ≠ {}" "bounded (closure A)" "A ⊆ closure A" using closure_subset by auto have "infdist x A = 0" if "x ∈ closure A" for x using in_closure_iff_infdist_zero[OF ‹A ≠ {}›] that by auto then have "(SUP x∈closure A. infdist x A) = 0" using ‹closure A ≠ {}› by auto then show ?thesis unfolding hausdorff_distance_subset[OF ‹A ⊆ closure A› ‹A ≠ {}› ‹bounded (closure A)›] by simp qed lemma hausdorff_distance_closures [simp]: "hausdorff_distance (closure A) (closure B) = hausdorff_distance A B" proof (cases "A = {} ∨ B = {} ∨ (¬(bounded A)) ∨ (¬(bounded B))") case True then have *: "hausdorff_distance A B = 0" unfolding hausdorff_distance_def by auto have "closure A = {} ∨ (¬(bounded (closure A))) ∨ closure B = {} ∨ (¬(bounded (closure B)))" using True bounded_subset closure_subset by auto then have "hausdorff_distance (closure A) (closure B) = 0" unfolding hausdorff_distance_def by auto then show ?thesis using * by simp next case False then have H: "A ≠ {}" "B ≠ {}" "bounded A" "bounded B" by auto then have H2: "closure A ≠ {}" "closure B ≠ {}" "bounded (closure A)" "bounded (closure B)" by auto have "hausdorff_distance A B ≤ hausdorff_distance A (closure A) + hausdorff_distance (closure A) B" apply (rule hausdorff_distance_triangle) using H H2 by auto also have "... = hausdorff_distance (closure A) B" using hausdorff_distance_closure by auto also have "... ≤ hausdorff_distance (closure A) (closure B) + hausdorff_distance (closure B) B" apply (rule hausdorff_distance_triangle) using H H2 by auto also have "... = hausdorff_distance (closure A) (closure B)" using hausdorff_distance_closure by (auto simp add: hausdorff_distance_sym) finally have *: "hausdorff_distance A B ≤ hausdorff_distance (closure A) (closure B)" by simp have "hausdorff_distance (closure A) (closure B) ≤ hausdorff_distance (closure A) A + hausdorff_distance A (closure B)" apply (rule hausdorff_distance_triangle) using H H2 by auto also have "... = hausdorff_distance A (closure B)" using hausdorff_distance_closure by (auto simp add: hausdorff_distance_sym) also have "... ≤ hausdorff_distance A B + hausdorff_distance B (closure B)" apply (rule hausdorff_distance_triangle) using H H2 by auto also have "... = hausdorff_distance A B" using hausdorff_distance_closure by (auto simp add: hausdorff_distance_sym) finally have "hausdorff_distance (closure A) (closure B) ≤ hausdorff_distance A B" by simp then show ?thesis using * by auto qed lemma hausdorff_distance_zero: assumes "A ≠ {}" "bounded A" "B ≠ {}" "bounded B" shows "hausdorff_distance A B = 0 ⟷ closure A = closure B" proof assume H: "hausdorff_distance A B = 0" have "A ⊆ closure B" proof fix x assume "x ∈ A" have "infdist x B = 0" using infdist_le_hausdorff_distance[OF ‹x ∈ A› ‹bounded A› ‹bounded B›] H infdist_nonneg[of x B] by auto then show "x ∈ closure B" using in_closure_iff_infdist_zero[OF ‹B ≠ {}›] by auto qed then have A: "closure A ⊆ closure B" by (simp add: closure_minimal) have "B ⊆ closure A" proof fix x assume "x ∈ B" have "infdist x A = 0" using infdist_le_hausdorff_distance[OF ‹x ∈ B› ‹bounded B› ‹bounded A›] H infdist_nonneg[of x A] by (auto simp add: hausdorff_distance_sym) then show "x ∈ closure A" using in_closure_iff_infdist_zero[OF ‹A ≠ {}›] by auto qed then have "closure B ⊆ closure A" by (simp add: closure_minimal) then show "closure A = closure B" using A by auto next assume "closure A = closure B" then show "hausdorff_distance A B = 0" using hausdorff_distance_closures[of A B] by auto qed lemma hausdorff_distance_vimage: assumes "⋀x. x ∈ A ⟹ dist (f x) (g x) ≤ C" "C ≥ 0" shows "hausdorff_distance (f`A) (g`A) ≤ C" apply (rule hausdorff_distanceI2[OF _ _ ‹C ≥ 0›]) using assms by (auto simp add: dist_commute, auto) lemma hausdorff_distance_union [mono_intros]: assumes "A ≠ {}" "B ≠ {}" "C ≠ {}" "D ≠ {}" shows "hausdorff_distance (A ∪ B) (C ∪ D) ≤ max (hausdorff_distance A C) (hausdorff_distance B D)" proof (cases "bounded A ∧ bounded B ∧ bounded C ∧ bounded D") case False then have "hausdorff_distance (A ∪ B) (C ∪ D) = 0" unfolding hausdorff_distance_def by auto then show ?thesis by (simp add: hausdorff_distance_nonneg le_max_iff_disj) next case True show ?thesis proof (rule hausdorff_distanceI, auto) fix x assume H: "x ∈ A" have "infdist x (C ∪ D) ≤ infdist x C" by (simp add: assms infdist_union_min) also have "... ≤ hausdorff_distance A C" apply (rule infdist_le_hausdorff_distance) using H True by auto also have "... ≤ max (hausdorff_distance A C) (hausdorff_distance B D)" by auto finally show "infdist x (C ∪ D) ≤ max (hausdorff_distance A C) (hausdorff_distance B D)" by simp next fix x assume H: "x ∈ B" have "infdist x (C ∪ D) ≤ infdist x D" by (simp add: assms infdist_union_min) also have "... ≤ hausdorff_distance B D" apply (rule infdist_le_hausdorff_distance) using H True by auto also have "... ≤ max (hausdorff_distance A C) (hausdorff_distance B D)" by auto finally show "infdist x (C ∪ D) ≤ max (hausdorff_distance A C) (hausdorff_distance B D)" by simp next fix x assume H: "x ∈ C" have "infdist x (A ∪ B) ≤ infdist x A" by (simp add: assms infdist_union_min) also have "... ≤ hausdorff_distance C A" apply (rule infdist_le_hausdorff_distance) using H True by auto also have "... ≤ max (hausdorff_distance A C) (hausdorff_distance B D)" using hausdorff_distance_sym[of A C] by auto finally show "infdist x (A ∪ B) ≤ max (hausdorff_distance A C) (hausdorff_distance B D)" by simp next fix x assume H: "x ∈ D" have "infdist x (A ∪ B) ≤ infdist x B" by (simp add: assms infdist_union_min) also have "... ≤ hausdorff_distance D B" apply (rule infdist_le_hausdorff_distance) using H True by auto also have "... ≤ max (hausdorff_distance A C) (hausdorff_distance B D)" using hausdorff_distance_sym[of B D] by auto finally show "infdist x (A ∪ B) ≤ max (hausdorff_distance A C) (hausdorff_distance B D)" by simp qed (simp add: le_max_iff_disj) qed end (*of theory Hausdorff_Distance*)

# Theory Isometries

(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr License: BSD *) section ‹Isometries› theory Isometries imports Library_Complements Hausdorff_Distance begin text ‹Isometries, i.e., functions that preserve distances, show up very often in mathematics. We introduce a dedicated definition, and show its basic properties.› definition isometry_on::"('a::metric_space) set ⇒ ('a ⇒ ('b::metric_space)) ⇒ bool" where "isometry_on X f = (∀x ∈ X. ∀y ∈ X. dist (f x) (f y) = dist x y)" definition isometry :: "('a::metric_space ⇒ 'b::metric_space) ⇒ bool" where "isometry f ≡ isometry_on UNIV f ∧ range f = UNIV" lemma isometry_on_subset: assumes "isometry_on X f" "Y ⊆ X" shows "isometry_on Y f" using assms unfolding isometry_on_def by auto lemma isometry_onI [intro?]: assumes "⋀x y. x ∈ X ⟹ y ∈ X ⟹ dist (f x) (f y) = dist x y" shows "isometry_on X f" using assms unfolding isometry_on_def by auto lemma isometry_onD: assumes "isometry_on X f" "x ∈ X" "y ∈ X" shows "dist (f x) (f y) = dist x y" using assms unfolding isometry_on_def by auto lemma isometryI [intro?]: assumes "⋀x y. dist (f x) (f y) = dist x y" "range f = UNIV" shows "isometry f" unfolding isometry_def isometry_on_def using assms by auto lemma assumes "isometry_on X f" shows isometry_on_lipschitz: "1-lipschitz_on X f" and isometry_on_uniformly_continuous: "uniformly_continuous_on X f" and isometry_on_continuous: "continuous_on X f" proof - show "1-lipschitz_on X f" apply (rule lipschitz_onI) using isometry_onD[OF assms] by auto then show "uniformly_continuous_on X f" "continuous_on X f" using lipschitz_on_uniformly_continuous lipschitz_on_continuous_on by auto qed lemma isometryD: assumes "isometry f" shows "isometry_on UNIV f" "dist (f x) (f y) = dist x y" "range f = UNIV" "1-lipschitz_on UNIV f" "uniformly_continuous_on UNIV f" "continuous_on UNIV f" using assms unfolding isometry_def isometry_on_def apply auto using isometry_on_lipschitz isometry_on_uniformly_continuous isometry_on_continuous assms unfolding isometry_def by blast+ lemma isometry_on_injective: assumes "isometry_on X f" shows "inj_on f X" using assms inj_on_def isometry_on_def by force lemma isometry_on_compose: assumes "isometry_on X f" "isometry_on (f`X) g" shows "isometry_on X (λx. g(f x))" using assms unfolding isometry_on_def by auto lemma isometry_on_cong: assumes "isometry_on X f" "⋀x. x ∈ X ⟹ g x = f x" shows "isometry_on X g" using assms unfolding isometry_on_def by auto lemma isometry_on_inverse: assumes "isometry_on X f" shows "isometry_on (f`X) (inv_into X f)" "⋀x. x ∈ X ⟹ (inv_into X f) (f x) = x" "⋀y. y ∈ f`X ⟹ f (inv_into X f y) = y" "bij_betw f X (f`X)" proof - show *: "bij_betw f X (f`X)" using assms unfolding bij_betw_def inj_on_def isometry_on_def by force show "isometry_on (f`X) (inv_into X f)" using assms unfolding isometry_on_def by (auto) (metis (mono_tags, lifting) dist_eq_0_iff inj_on_def inv_into_f_f) fix x assume "x ∈ X" then show "(inv_into X f) (f x) = x" using * by (simp add: bij_betw_def) next fix y assume "y ∈ f`X" then show "f (inv_into X f y) = y" by (simp add: f_inv_into_f) qed lemma isometry_inverse: assumes "isometry f" shows "isometry (inv f)" "bij f" using isometry_on_inverse[OF isometryD(1)[OF assms]] isometryD(3)[OF assms] unfolding isometry_def by (auto simp add: bij_imp_bij_inv bij_is_surj) lemma isometry_on_homeomorphism: assumes "isometry_on X f" shows "homeomorphism X (f`X) f (inv_into X f)" "homeomorphism_on X f" "X homeomorphic f`X" proof - show *: "homeomorphism X (f`X) f (inv_into X f)" apply (rule homeomorphismI) using uniformly_continuous_imp_continuous[OF isometry_on_uniformly_continuous] isometry_on_inverse[OF assms] assms by auto then show "X homeomorphic f`X" unfolding homeomorphic_def by auto show "homeomorphism_on X f" unfolding homeomorphism_on_def using * by auto qed lemma isometry_homeomorphism: fixes f::"('a::metric_space) ⇒ ('b::metric_space)" assumes "isometry f" shows "homeomorphism UNIV UNIV f (inv f)" "(UNIV::'a set) homeomorphic (UNIV::'b set)" using isometry_on_homeomorphism[OF isometryD(1)[OF assms]] isometryD(3)[OF assms] by auto lemma isometry_on_closure: assumes "isometry_on X f" "continuous_on (closure X) f" shows "isometry_on (closure X) f" proof (rule isometry_onI) fix x y assume "x ∈ closure X" "y ∈ closure X" obtain u v::"nat ⇒ 'a" where *: "⋀n. u n ∈ X" "u ⇢ x" "⋀n. v n ∈ X" "v ⇢ y" using ‹x ∈ closure X› ‹y ∈ closure X› unfolding closure_sequential by blast have "(λn. f (u n)) ⇢ f x" using *(1) *(2) ‹x ∈ closure X› ‹continuous_on (closure X) f› unfolding comp_def continuous_on_closure_sequentially[of X f] by auto moreover have "(λn. f (v n)) ⇢ f y" using *(3) *(4) ‹y ∈ closure X› ‹continuous_on (closure X) f› unfolding comp_def continuous_on_closure_sequentially[of X f] by auto ultimately have "(λn. dist (f (u n)) (f (v n))) ⇢ dist (f x) (f y)" by (simp add: tendsto_dist) then have "(λn. dist (u n) (v n)) ⇢ dist (f x) (f y)" using assms(1) *(1) *(3) unfolding isometry_on_def by auto moreover have "(λn. dist (u n) (v n)) ⇢ dist x y" using *(2) *(4) by (simp add: tendsto_dist) ultimately show "dist (f x) (f y) = dist x y" using LIMSEQ_unique by auto qed lemma isometry_extend_closure: fixes f::"('a::metric_space) ⇒ ('b::complete_space)" assumes "isometry_on X f" shows "∃g. isometry_on (closure X) g ∧ (∀x∈X. g x = f x)" proof - obtain g where g: "⋀x. x ∈ X ⟹ g x = f x" "uniformly_continuous_on (closure X) g" using uniformly_continuous_on_extension_on_closure[OF isometry_on_uniformly_continuous[OF assms]] by metis have "isometry_on (closure X) g" apply (rule isometry_on_closure, rule isometry_on_cong[OF assms]) using g uniformly_continuous_imp_continuous[OF g(2)] by auto then show ?thesis using g(1) by auto qed lemma isometry_on_complete_image: assumes "isometry_on X f" "complete X" shows "complete (f`X)" proof (rule completeI) fix u :: "nat ⇒ 'b" assume u: "∀n. u n ∈ f`X" "Cauchy u" define v where "v = (λn. inv_into X f (u n))" have "v n ∈ X" for n unfolding v_def by (simp add: inv_into_into u(1)) have "dist (v n) (v m) = dist (u n) (u m)" for m n using u(1) isometry_on_inverse[OF ‹isometry_on X f›] unfolding isometry_on_def v_def by (auto simp add: inv_into_into) then have "Cauchy v" using u(2) unfolding Cauchy_def by auto obtain l where "l ∈ X" "v ⇢ l" apply (rule completeE[OF ‹complete X› _ ‹Cauchy v›]) using ‹⋀n. v n ∈ X› by auto have "(λn. f (v n)) ⇢ f l" apply (rule continuous_on_tendsto_compose[OF isometry_on_continuous[OF ‹isometry_on X f›]]) using ‹⋀n. v n ∈ X› ‹l ∈ X› ‹v ⇢ l› by auto moreover have "f(v n) = u n" for n unfolding v_def by (simp add: f_inv_into_f u(1)) ultimately have "u ⇢ f l" by auto then show "∃m ∈ f`X. u ⇢ m" using ‹l ∈ X› by auto qed lemma isometry_on_id [simp]: "isometry_on A (λx. x)" "isometry_on A id" unfolding isometry_on_def by auto lemma isometry_on_add [simp]: "isometry_on A (λx. x + (t::'a::real_normed_vector))" unfolding isometry_on_def by auto lemma isometry_on_minus [simp]: "isometry_on A (λ(x::'a::real_normed_vector). -x)" unfolding isometry_on_def by (auto simp add: dist_minus) lemma isometry_on_diff [simp]: "isometry_on A (λx. (t::'a::real_normed_vector) - x)" unfolding isometry_on_def by (auto, metis add_uminus_conv_diff dist_add_cancel dist_minus) lemma isometry_preserves_bounded: assumes "isometry_on X f" "A ⊆ X" shows "bounded (f`A) ⟷ bounded A" unfolding bounded_two_points using assms(2) isometry_onD[OF assms(1)] by auto (metis assms(2) rev_subsetD)+ lemma isometry_preserves_infdist: "infdist (f x) (f`A) = infdist x A" if "isometry_on X f" "A ⊆ X" "x ∈ X" using that by (simp add: infdist_def image_comp isometry_on_def subset_iff) lemma isometry_preserves_hausdorff_distance: "hausdorff_distance (f`A) (f`B) = hausdorff_distance A B" if "isometry_on X f" "A ⊆ X" "B ⊆ X" using that isometry_preserves_infdist [OF that(1) that(2)] isometry_preserves_infdist [OF that(1) that(3)] isometry_preserves_bounded [OF that(1) that(2)] isometry_preserves_bounded [OF that(1) that(3)] by (simp add: hausdorff_distance_def image_comp subset_eq) lemma isometry_on_UNIV_iterates: fixes f::"('a::metric_space) ⇒ 'a" assumes "isometry_on UNIV f" shows "isometry_on UNIV (f^^n)" by (induction n, auto, rule isometry_on_compose[of _ _ f], auto intro: isometry_on_subset[OF assms]) lemma isometry_iterates: fixes f::"('a::metric_space) ⇒ 'a" assumes "isometry f" shows "isometry (f^^n)" using isometry_on_UNIV_iterates[OF isometryD(1)[OF assms], of n] bij_fn[OF isometry_inverse(2)[OF assms], of n] unfolding isometry_def by (simp add: bij_is_surj) section ‹Geodesic spaces› text ‹A geodesic space is a metric space in which any pair of points can be joined by a geodesic segment, i.e., an isometrically embedded copy of a segment in the real line. Most spaces in geometry are geodesic. We introduce in this section the corresponding class of metric spaces. First, we study properties of general geodesic segments in metric spaces.› subsection ‹Geodesic segments in general metric spaces› definition geodesic_segment_between::"('a::metric_space) set ⇒ 'a ⇒ 'a ⇒ bool" where "geodesic_segment_between G x y = (∃g::(real ⇒ 'a). g 0 = x ∧ g (dist x y) = y ∧ isometry_on {0..dist x y} g ∧ G = g`{0..dist x y})" definition geodesic_segment::"('a::metric_space) set ⇒ bool" where "geodesic_segment G = (∃x y. geodesic_segment_between G x y)" text ‹We also introduce the parametrization of a geodesic segment. It is convenient to use the following definition, which guarantees that the point is on $G$ even without checking that $G$ is a geodesic segment or that the parameter is in the reasonable range: this shortens some arguments below.› definition geodesic_segment_param::"('a::metric_space) set ⇒ 'a ⇒ real ⇒ 'a" where "geodesic_segment_param G x t = (if ∃w. w ∈ G ∧ dist x w = t then SOME w. w ∈ G ∧ dist x w = t else SOME w. w ∈ G)" lemma geodesic_segment_betweenI: assumes "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" shows "geodesic_segment_between G x y" unfolding geodesic_segment_between_def apply (rule exI[of _ g]) using assms by auto lemma geodesic_segmentI [intro, simp]: assumes "geodesic_segment_between G x y" shows "geodesic_segment G" unfolding geodesic_segment_def using assms by auto lemma geodesic_segmentI2 [intro]: assumes "isometry_on {a..b} g" "a ≤ (b::real)" shows "geodesic_segment_between (g`{a..b}) (g a) (g b)" "geodesic_segment (g`{a..b})" proof - define h where "h = (λt. g (t+a))" have *: "isometry_on {0..b-a} h" apply (rule isometry_onI) using ‹isometry_on {a..b} g› ‹a ≤ b› by (auto simp add: isometry_on_def h_def) have **: "dist (h 0) (h (b-a)) = b-a" using isometry_onD[OF ‹isometry_on {0..b-a} h›, of 0 "b-a"] ‹a ≤ b› unfolding dist_real_def by auto have "geodesic_segment_between (h`{0..b-a}) (h 0) (h (b-a))" unfolding geodesic_segment_between_def apply (rule exI[of _ h]) unfolding ** using * by auto moreover have "g`{a..b} = h`{0..b-a}" unfolding h_def apply (auto simp add: image_iff) by (metis add.commute atLeastAtMost_iff diff_ge_0_iff_ge diff_right_mono le_add_diff_inverse) moreover have "h 0 = g a" "h (b-a) = g b" unfolding h_def by auto ultimately show "geodesic_segment_between (g`{a..b}) (g a) (g b)" by auto then show "geodesic_segment (g`{a..b})" unfolding geodesic_segment_def by auto qed lemma geodesic_segmentD: assumes "geodesic_segment_between G x y" shows "∃g::(real ⇒ _). (g t = x ∧ g (t + dist x y) = y ∧ isometry_on {t..t+dist x y} g ∧ G = g`{t..t+dist x y})" proof - obtain h where h: "h 0 = x" "h (dist x y) = y" "isometry_on {0..dist x y} h" "G = h`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) have * [simp]: "(λx. x - t) ` {t..t + dist x y} = {0..dist x y}" by auto define g where "g = (λs. h (s - t))" have "g t = x" "g (t + dist x y) = y" using h assms(1) unfolding g_def by auto moreover have "isometry_on {t..t+dist x y} g" unfolding g_def apply (rule isometry_on_compose[of _ _ h]) by (simp add: dist_real_def isometry_on_def, simp add: h(3)) moreover have "g` {t..t + dist x y} = G" unfolding g_def h(4) using * by (metis image_image) ultimately show ?thesis by auto qed lemma geodesic_segment_endpoints [simp]: assumes "geodesic_segment_between G x y" shows "x ∈ G" "y ∈ G" "G ≠ {}" using assms unfolding geodesic_segment_between_def by (auto, metis atLeastAtMost_iff image_eqI less_eq_real_def zero_le_dist) lemma geodesic_segment_commute: assumes "geodesic_segment_between G x y" shows "geodesic_segment_between G y x" proof - obtain g::"real⇒'a" where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) define h::"real⇒'a" where "h = (λt. g(dist x y-t))" have "(λt. dist x y -t)`{0..dist x y} = {0..dist x y}" by auto then have "h`{0..dist x y} = G" unfolding g(4) h_def by (metis image_image) moreover have "h 0 = y" "h (dist x y) = x" unfolding h_def using g by auto moreover have "isometry_on {0..dist x y} h" unfolding h_def apply (rule isometry_on_compose[of _ _ g]) using g(3) by auto ultimately show ?thesis unfolding geodesic_segment_between_def by (auto simp add: dist_commute) qed lemma geodesic_segment_dist: assumes "geodesic_segment_between G x y" "a ∈ G" shows "dist x a + dist a y = dist x y" proof - obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) obtain t where t: "t ∈ {0..dist x y}" "a = g t" using g(4) assms by auto have "dist x a = t" using isometry_onD[OF g(3) _ t(1), of 0] unfolding g(1) dist_real_def t(2) using t(1) by auto moreover have "dist a y = dist x y - t" using isometry_onD[OF g(3) _ t(1), of "dist x y"] unfolding g(2) dist_real_def t(2) using t(1) by (auto simp add: dist_commute) ultimately show ?thesis by auto qed lemma geodesic_segment_dist_unique: assumes "geodesic_segment_between G x y" "a ∈ G" "b ∈ G" "dist x a = dist x b" shows "a = b" proof - obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) obtain ta where ta: "ta ∈ {0..dist x y}" "a = g ta" using g(4) assms by auto have *: "dist x a = ta" unfolding g(1)[symmetric] ta(2) using isometry_onD[OF g(3), of 0 ta] unfolding dist_real_def using ta(1) by auto obtain tb where tb: "tb ∈ {0..dist x y}" "b = g tb" using g(4) assms by auto have "dist x b = tb" unfolding g(1)[symmetric] tb(2) using isometry_onD[OF g(3), of 0 tb] unfolding dist_real_def using tb(1) by auto then have "ta = tb" using * ‹dist x a = dist x b› by auto then show "a = b" using ta(2) tb(2) by auto qed lemma geodesic_segment_union: assumes "dist x z = dist x y + dist y z" "geodesic_segment_between G x y" "geodesic_segment_between H y z" shows "geodesic_segment_between (G ∪ H) x z" "G ∩ H = {y}" proof - obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) obtain h where h: "h (dist x y) = y" "h (dist x z) = z" "isometry_on {dist x y..dist x z} h" "H = h`{dist x y..dist x z}" unfolding ‹dist x z = dist x y + dist y z› using geodesic_segmentD[OF ‹geodesic_segment_between H y z›, of "dist x y"] by auto define f where "f = (λt. if t ≤ dist x y then g t else h t)" have fg: "f t = g t" if "t ≤ dist x y" for t unfolding f_def using that by auto have fh: "f t = h t" if "t ≥ dist x y" for t unfolding f_def apply (cases "t > dist x y") using that g(2) h(1) by auto have "f 0 = x" "f (dist x z) = z" using fg fh g(1) h(2) assms(1) by auto have "f`{0..dist x z} = f`{0..dist x y} ∪ f`{dist x y..dist x z}" unfolding assms(1) image_Un[symmetric] by (simp add: ivl_disj_un_two_touch(4)) moreover have "f`{0..dist x y} = G" unfolding g(4) using fg image_cong by force moreover have "f`{dist x y..dist x z} = H" unfolding h(4) using fh image_cong by force ultimately have "f`{0..dist x z} = G ∪ H" by simp have Ifg: "dist (f s) (f t) = s-t" if "0 ≤ t" "t ≤ s" "s ≤ dist x y" for s t using that fg[of s] fg[of t] isometry_onD[OF g(3), of s t] unfolding dist_real_def by auto have Ifh: "dist (f s) (f t) = s-t" if "dist x y ≤ t" "t ≤ s" "s ≤ dist x z" for s t using that fh[of s] fh[of t] isometry_onD[OF h(3), of s t] unfolding dist_real_def by auto have I: "dist (f s) (f t) = s-t" if "0 ≤ t" "t ≤ s" "s ≤ dist x z" for s t proof - consider "t ≤ dist x y ∧ s ≥ dist x y" | "s ≤ dist x y" | "t ≥ dist x y" by fastforce then show ?thesis proof (cases) case 1 have "dist (f t) (f s) ≤ dist (f t) (f (dist x y)) + dist (f (dist x y)) (f s)" using dist_triangle by auto also have "... ≤ (dist x y - t) + (s - dist x y)" using that 1 Ifg[of t "dist x y"] Ifh[of "dist x y" s] by (auto simp add: dist_commute intro: mono_intros) finally have *: "dist (f t) (f s) ≤ s - t" by simp have "dist x z ≤ dist (f 0) (f t) + dist (f t) (f s) + dist (f s) (f (dist x z))" unfolding ‹f 0 = x› ‹f (dist x z) = z› using dist_triangle4 by auto also have "... ≤ t + dist (f t) (f s) + (dist x z - s)" using that 1 Ifg[of 0 t] Ifh[of s "dist x z"] by (auto simp add: dist_commute intro: mono_intros) finally have "s - t ≤ dist (f t) (f s)" by auto then show "dist (f s) (f t) = s-t" using * dist_commute by auto next case 2 then show ?thesis using Ifg that by auto next case 3 then show ?thesis using Ifh that by auto qed qed have "isometry_on {0..dist x z} f" unfolding isometry_on_def dist_real_def using I by (auto, metis abs_of_nonneg dist_commute dist_real_def le_cases zero_le_dist) then show "geodesic_segment_between (G ∪ H) x z" unfolding geodesic_segment_between_def using ‹f 0 = x› ‹f (dist x z) = z› ‹f`{0..dist x z} = G ∪ H› by auto have "G ∩ H ⊆ {y}" proof (auto) fix a assume a: "a ∈ G" "a ∈ H" obtain s where s: "s ∈ {0..dist x y}" "a = g s" using a g(4) by auto obtain t where t: "t ∈ {dist x y..dist x z}" "a = h t" using a h(4) by auto have "a = f s" using fg s by auto moreover have "a = f t" using fh t by auto ultimately have "s = t" using isometry_onD[OF ‹isometry_on {0..dist x z} f›, of s t] s(1) t(1) by auto then have "s = dist x y" using s t by auto then show "a = y" using s(2) g by auto qed then show "G ∩ H = {y}" using assms by auto qed lemma geodesic_segment_dist_le: assumes "geodesic_segment_between G x y" "a ∈ G" "b ∈ G" shows "dist a b ≤ dist x y" proof - obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) obtain s t where st: "s ∈ {0..dist x y}" "t ∈ {0..dist x y}" "a = g s" "b = g t" using g(4) assms by auto have "dist a b = abs(s-t)" using isometry_onD[OF g(3) st(1) st(2)] unfolding st(3) st(4) dist_real_def by simp then show "dist a b ≤ dist x y" using st(1) st(2) unfolding dist_real_def by auto qed lemma geodesic_segment_param [simp]: assumes "geodesic_segment_between G x y" shows "geodesic_segment_param G x 0 = x" "geodesic_segment_param G x (dist x y) = y" "t ∈ {0..dist x y} ⟹ geodesic_segment_param G x t ∈ G" "isometry_on {0..dist x y} (geodesic_segment_param G x)" "(geodesic_segment_param G x)`{0..dist x y} = G" "t ∈ {0..dist x y} ⟹ dist x (geodesic_segment_param G x t) = t" "s ∈ {0..dist x y} ⟹ t ∈ {0..dist x y} ⟹ dist (geodesic_segment_param G x s) (geodesic_segment_param G x t) = abs(s-t)" "z ∈ G ⟹ z = geodesic_segment_param G x (dist x z)" proof - obtain g::"real⇒'a" where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) have *: "g t ∈ G ∧ dist x (g t) = t" if "t ∈ {0..dist x y}" for t using isometry_onD[OF g(3), of 0 t] that g(1) g(4) unfolding dist_real_def by auto have G: "geodesic_segment_param G x t = g t" if "t ∈ {0..dist x y}" for t proof - have A: "geodesic_segment_param G x t ∈ G ∧ dist x (geodesic_segment_param G x t) = t" using *[OF that] unfolding geodesic_segment_param_def apply auto using *[OF that] by (metis (mono_tags, lifting) someI)+ obtain s where s: "geodesic_segment_param G x t = g s" "s ∈ {0..dist x y}" using A g(4) by auto have "s = t" using *[OF ‹s ∈ {0..dist x y}›] A unfolding s(1) by auto then show ?thesis using s by auto qed show "geodesic_segment_param G x 0 = x" "geodesic_segment_param G x (dist x y) = y" "t ∈ {0..dist x y} ⟹ geodesic_segment_param G x t ∈ G" "isometry_on {0..dist x y} (geodesic_segment_param G x)" "(geodesic_segment_param G x)`{0..dist x y} = G" "t ∈ {0..dist x y} ⟹ dist x (geodesic_segment_param G x t) = t" "s ∈ {0..dist x y} ⟹ t ∈ {0..dist x y} ⟹ dist (geodesic_segment_param G x s) (geodesic_segment_param G x t) = abs(s-t)" "z ∈ G ⟹ z = geodesic_segment_param G x (dist x z)" using G g apply (auto simp add: rev_image_eqI) using G isometry_on_cong * atLeastAtMost_iff apply blast using G isometry_on_cong * atLeastAtMost_iff apply blast by (auto simp add: * dist_real_def isometry_onD) qed lemma geodesic_segment_param_in_segment: assumes "G ≠ {}" shows "geodesic_segment_param G x t ∈ G" unfolding geodesic_segment_param_def apply (auto, metis (mono_tags, lifting) someI) using assms some_in_eq by fastforce lemma geodesic_segment_reverse_param: assumes "geodesic_segment_between G x y" "t ∈ {0..dist x y}" shows "geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t" proof - have * [simp]: "geodesic_segment_between G y x" using geodesic_segment_commute[OF assms(1)] by simp have "geodesic_segment_param G y (dist x y - t) ∈ G" apply (rule geodesic_segment_param(3)[of _ _ x]) using assms(2) by (auto simp add: dist_commute) moreover have "dist (geodesic_segment_param G y (dist x y - t)) x = t" using geodesic_segment_param(2)[OF *] geodesic_segment_param(7)[OF *, of "dist x y -t" "dist x y"] assms(2) by (auto simp add: dist_commute) moreover have "geodesic_segment_param G x t ∈ G" apply (rule geodesic_segment_param(3)[OF assms(1)]) using assms(2) by auto moreover have "dist (geodesic_segment_param G x t) x = t" using geodesic_segment_param(6)[OF assms] by (simp add: dist_commute) ultimately show ?thesis using geodesic_segment_dist_unique[OF assms(1)] by (simp add: dist_commute) qed lemma dist_along_geodesic_wrt_endpoint: assumes "geodesic_segment_between G x y" "u ∈ G" "v ∈ G" shows "dist u v = abs(dist u x - dist v x)" proof - have *: "u = geodesic_segment_param G x (dist x u)" "v = geodesic_segment_param G x (dist x v)" using assms by auto have "dist u v = dist (geodesic_segment_param G x (dist x u)) (geodesic_segment_param G x (dist x v))" using * by auto also have "... = abs(dist x u - dist x v)" apply (rule geodesic_segment_param(7)[OF assms(1)]) using assms apply auto using geodesic_segment_dist_le geodesic_segment_endpoints(1) by blast+ finally show ?thesis by (simp add: dist_commute) qed text ‹One often needs to restrict a geodesic segment to a subsegment. We introduce the tools to express this conveniently.› definition geodesic_subsegment::"('a::metric_space) set ⇒ 'a ⇒ real ⇒ real ⇒ 'a set" where "geodesic_subsegment G x s t = G ∩ {z. dist x z ≥ s ∧ dist x z ≤ t}" text ‹A subsegment is always contained in the original segment.› lemma geodesic_subsegment_subset: "geodesic_subsegment G x s t ⊆ G" unfolding geodesic_subsegment_def by simp text ‹A subsegment is indeed a geodesic segment, and its endpoints and parametrization can be expressed in terms of the original segment.› lemma geodesic_subsegment: assumes "geodesic_segment_between G x y" "0 ≤ s" "s ≤ t" "t ≤ dist x y" shows "geodesic_subsegment G x s t = (geodesic_segment_param G x)`{s..t}" "geodesic_segment_between (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (geodesic_segment_param G x t)" "⋀u. s ≤ u ⟹ u ≤ t ⟹ geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u" proof - show A: "geodesic_subsegment G x s t = (geodesic_segment_param G x)`{s..t}" proof (auto) fix y assume y: "y ∈ geodesic_subsegment G x s t" have "y = geodesic_segment_param G x (dist x y)" apply (rule geodesic_segment_param(8)[OF assms(1)]) using y geodesic_subsegment_subset by force moreover have "dist x y ≥ s ∧ dist x y ≤ t" using y unfolding geodesic_subsegment_def by auto ultimately show "y ∈ geodesic_segment_param G x ` {s..t}" by auto next fix u assume H: "s ≤ u" "u ≤ t" have *: "dist x (geodesic_segment_param G x u) = u" apply (rule geodesic_segment_param(6)[OF assms(1)]) using H assms by auto show "geodesic_segment_param G x u ∈ geodesic_subsegment G x s t" unfolding geodesic_subsegment_def using geodesic_segment_param_in_segment[OF geodesic_segment_endpoints(3)[OF assms(1)]] by (auto simp add: * H) qed have *: "isometry_on {s..t} (geodesic_segment_param G x)" by (rule isometry_on_subset[of "{0..dist x y}"]) (auto simp add: assms) show B: "geodesic_segment_between (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (geodesic_segment_param G x t)" unfolding A apply (rule geodesic_segmentI2) using * assms by auto fix u assume u: "s ≤ u" "u ≤ t" show "geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u" proof (rule geodesic_segment_dist_unique[OF B]) show "geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) ∈ geodesic_subsegment G x s t" by (rule geodesic_segment_param_in_segment[OF geodesic_segment_endpoints(3)[OF B]]) show "geodesic_segment_param G x u ∈ geodesic_subsegment G x s t" unfolding A using u by auto have "dist (geodesic_segment_param G x s) (geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s)) = u - s" using B assms u by auto moreover have "dist (geodesic_segment_param G x s) (geodesic_segment_param G x u) = u -s" using assms u by auto ultimately show "dist (geodesic_segment_param G x s) (geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s)) = dist (geodesic_segment_param G x s) (geodesic_segment_param G x u)" by simp qed qed text ‹The parameterizations of a segment and a subsegment sharing an endpoint coincide where defined.› lemma geodesic_segment_subparam: assumes "geodesic_segment_between G x z" "geodesic_segment_between H x y" "H ⊆ G" "t ∈ {0..dist x y}" shows "geodesic_segment_param G x t = geodesic_segment_param H x t" proof - have "geodesic_segment_param H x t ∈ G" using assms(3) geodesic_segment_param(3)[OF assms(2) assms(4)] by auto then have "geodesic_segment_param H x t = geodesic_segment_param G x (dist x (geodesic_segment_param H x t))" using geodesic_segment_param(8)[OF assms(1)] by auto then show ?thesis using geodesic_segment_param(6)[OF assms(2) assms(4)] by auto qed text ‹A segment contains a subsegment between any of its points› lemma geodesic_subsegment_exists: assumes "geodesic_segment G" "x ∈ G" "y ∈ G" shows "∃H. H ⊆ G ∧ geodesic_segment_between H x y" proof - obtain a0 b0 where Ga0b0: "geodesic_segment_between G a0 b0" using assms(1) unfolding geodesic_segment_def by auto text ‹Permuting the endpoints if necessary, we can ensure that the first endpoint $a$ is closer to $x$ than $y$.› have "∃ a b. geodesic_segment_between G a b ∧ dist x a ≤ dist y a" proof (cases "dist x a0 ≤ dist y a0") case True show ?thesis apply (rule exI[of _ a0], rule exI[of _ b0]) using True Ga0b0 by auto next case False show ?thesis apply (rule exI[of _ b0], rule exI[of _ a0]) using Ga0b0 geodesic_segment_commute geodesic_segment_dist[OF Ga0b0 ‹x ∈ G›] geodesic_segment_dist[OF Ga0b0 ‹y ∈ G›] False by (auto simp add: dist_commute) qed then obtain a b where Gab: "geodesic_segment_between G a b" "dist x a ≤ dist y a" by auto have *: "0 ≤ dist x a" "dist x a ≤ dist y a" "dist y a ≤ dist a b" using Gab assms by (meson geodesic_segment_dist_le geodesic_segment_endpoints(1) zero_le_dist)+ have **: "x = geodesic_segment_param G a (dist x a)" "y = geodesic_segment_param G a (dist y a)" using Gab ‹x ∈ G› ‹y ∈ G› by (metis dist_commute geodesic_segment_param(8))+ define H where "H = geodesic_subsegment G a (dist x a) (dist y a)" have "H ⊆ G" unfolding H_def by (rule geodesic_subsegment_subset) moreover have "geodesic_segment_between H x y" unfolding H_def using geodesic_subsegment(2)[OF Gab(1) *] ** by auto ultimately show ?thesis by auto qed text ‹A geodesic segment is homeomorphic to an interval.› lemma geodesic_segment_homeo_interval: assumes "geodesic_segment_between G x y" shows "{0..dist x y} homeomorphic G" proof - obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) show ?thesis using isometry_on_homeomorphism(3)[OF g(3)] unfolding g(4) by simp qed text ‹Just like an interval, a geodesic segment is compact, connected, path connected, bounded, closed, nonempty, and proper.› lemma geodesic_segment_topology: assumes "geodesic_segment G" shows "compact G" "connected G" "path_connected G" "bounded G" "closed G" "G ≠ {}" "proper G" proof - show "compact G" using assms geodesic_segment_homeo_interval homeomorphic_compactness unfolding geodesic_segment_def by force show "path_connected G" using assms is_interval_path_connected geodesic_segment_homeo_interval homeomorphic_path_connectedness unfolding geodesic_segment_def by (metis is_interval_cc) then show "connected G" using path_connected_imp_connected by auto show "bounded G" by (rule compact_imp_bounded, fact) show "closed G" by (rule compact_imp_closed, fact) show "G ≠ {}" using assms geodesic_segment_def geodesic_segment_endpoints(3) by auto show "proper G" using proper_of_compact ‹compact G› by auto qed lemma geodesic_segment_between_x_x [simp]: "geodesic_segment_between {x} x x" "geodesic_segment {x}" "geodesic_segment_between G x x ⟷ G = {x}" proof - show *: "geodesic_segment_between {x} x x" unfolding geodesic_segment_between_def apply (rule exI[of _ "λ_. x"]) unfolding isometry_on_def by auto then show "geodesic_segment {x}" by auto show "geodesic_segment_between G x x ⟷ G = {x}" using geodesic_segment_dist_le geodesic_segment_endpoints(2) * by fastforce qed lemma geodesic_segment_disconnection: assumes "geodesic_segment_between G x y" "z ∈ G" shows "(connected (G - {z})) = (z = x ∨ z = y)" proof - obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) obtain t where t: "t ∈ {0..dist x y}" "z = g t" using ‹z ∈ G› g(4) by auto have "({0..dist x y} - {t}) homeomorphic (G - {g t})" proof - have *: "isometry_on ({0..dist x y} - {t}) g" apply (rule isometry_on_subset[OF g(3)]) by auto have "({0..dist x y} - {t}) homeomorphic g`({0..dist x y} - {t})" by (rule isometry_on_homeomorphism(3)[OF *]) moreover have "g`({0..dist x y} - {t}) = G - {g t}" unfolding g(4) using isometry_on_injective[OF g(3)] t by (auto simp add: inj_onD) ultimately show ?thesis by auto qed moreover have "connected({0..dist x y} - {t}) = (t = 0 ∨ t = dist x y)" using t(1) by (auto simp add: connected_iff_interval, fastforce) ultimately have "connected (G - {z}) = (t = 0 ∨ t = dist x y)" unfolding ‹z = g t›[symmetric]using homeomorphic_connectedness by blast moreover have "(t = 0 ∨ t = dist x y) = (z = x ∨ z = y)" using t g apply auto by (metis atLeastAtMost_iff isometry_on_inverse(2) order_refl zero_le_dist)+ ultimately show ?thesis by auto qed lemma geodesic_segment_unique_endpoints: assumes "geodesic_segment_between G x y" "geodesic_segment_between G a b" shows "{x, y} = {a, b}" by (metis geodesic_segment_disconnection assms(1) assms(2) doubleton_eq_iff geodesic_segment_endpoints(1) geodesic_segment_endpoints(2)) lemma geodesic_segment_subsegment: assumes "geodesic_segment G" "H ⊆ G" "compact H" "connected H" "H ≠ {}" shows "geodesic_segment H" proof - obtain x y where "geodesic_segment_between G x y" using assms unfolding geodesic_segment_def by auto obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) define L where "L = (inv_into {0..dist x y} g)`H" have "L ⊆ {0..dist x y}" unfolding L_def using isometry_on_inverse[OF ‹isometry_on {0..dist x y} g›] assms(2) g(4) by auto have "isometry_on G (inv_into {0..dist x y} g)" using isometry_on_inverse[OF ‹isometry_on {0..dist x y} g›] g(4) by auto then have "isometry_on H (inv_into {0..dist x y} g)" using ‹H ⊆ G› isometry_on_subset by auto then have "H homeomorphic L" unfolding L_def using isometry_on_homeomorphism(3) by auto then have "compact L ∧ connected L" using assms homeomorphic_compactness homeomorphic_connectedness by blast then obtain a b where "L = {a..b}" using connected_compact_interval_1[of L] by auto have "a ≤ b" using ‹H ≠ {}› ‹L = {a..b}› unfolding L_def by auto then have "0 ≤ a" "b ≤ dist x y" using ‹L ⊆ {0..dist x y}› ‹L = {a..b}› by auto have *: "H = g`{a..b}" by (metis L_def ‹L = {a..b}› assms(2) g(4) image_inv_into_cancel) show "geodesic_segment H" unfolding * apply (rule geodesic_segmentI2[OF _ ‹a ≤ b›]) apply (rule isometry_on_subset[OF g(3)]) using ‹0 ≤ a› ‹b ≤ dist x y› by auto qed text ‹The image under an isometry of a geodesic segment is still obviously a geodesic segment.› lemma isometry_preserves_geodesic_segment_between: assumes "isometry_on X f" "G ⊆ X" "geodesic_segment_between G x y" shows "geodesic_segment_between (f`G) (f x) (f y)" proof - obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}" by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def) then have *: "f`G = (f o g) `{0..dist x y}" "f x = (f o g) 0" "f y = (f o g) (dist x y)" by auto show ?thesis unfolding * apply (intro geodesic_segmentI2(1)) unfolding comp_def apply (rule isometry_on_compose[of _ g]) using g(3) g(4) assms by (auto intro: isometry_on_subset) qed text ‹The sum of distances $d(w, x) + d(w, y)$ can be controlled using the distance from $w$ to a geodesic segment between $x$ and $y$.› lemma geodesic_segment_distance: assumes "geodesic_segment_between G x y" shows "dist w x + dist w y ≤ dist x y + 2 * infdist w G" proof - have "∃z ∈ G. infdist w G = dist w z" apply (rule infdist_proper_attained) using assms by (auto simp add: geodesic_segment_topology) then obtain z where z: "z ∈ G" "infdist w G = dist w z" by auto have "dist w x + dist w y ≤ (dist w z + dist z x) + (dist w z + dist z y)" by (intro mono_intros) also have "... = dist x z + dist z y + 2 * dist w z" by (auto simp add: dist_commute) also have "... = dist x y + 2 * infdist w G" using z(1) assms geodesic_segment_dist unfolding z(2) by auto finally show ?thesis by auto qed text ‹If a point $y$ is on a geodesic segment between $x$ and its closest projection $p$ on a set $A$, then $p$ is also a closest projection of $y$, and the closest projection set of $y$ is contained in that of $x$.› lemma proj_set_geodesic_same_basepoint: assumes "p ∈ proj_set x A" "geodesic_segment_between G p x" "y ∈ G" shows "p ∈ proj_set y A" proof (rule proj_setI) show "p ∈ A" using assms proj_setD by auto have *: "dist y p ≤ dist y q" if "q ∈ A" for q proof - have "dist p y + dist y x = dist p x" using assms geodesic_segment_dist by blast also have "... ≤ dist q x" using proj_set_dist_le[OF ‹q ∈ A› assms(1)] by (simp add: dist_commute) also have "... ≤ dist q y + dist y x" by (intro mono_intros) finally show ?thesis by (simp add: dist_commute) qed have "dist y p ≤ Inf (dist y ` A)" apply (rule cINF_greatest) using ‹p ∈ A› * by auto then show "dist y p ≤ infdist y A" unfolding infdist_def using ‹p ∈ A› by auto qed lemma proj_set_subset: assumes "p ∈ proj_set x A" "geodesic_segment_between G p x" "y ∈ G" shows "proj_set y A ⊆ proj_set x A" proof - have "z ∈ proj_set x A" if "z ∈ proj_set y A" for z proof (rule proj_setI) show "z ∈ A" using that proj_setD by auto have "dist x z ≤ dist x y + dist y z" by (intro mono_intros) also have "... ≤ dist x y + dist y p" using proj_set_dist_le[OF proj_setD(1)[OF ‹p ∈ proj_set x A›] that] by auto also have "... = dist x p" using assms geodesic_segment_commute geodesic_segment_dist by blast also have "... = infdist x A" using proj_setD(2)[OF assms(1)] by simp finally show "dist x z ≤ infdist x A" by simp qed then show ?thesis by auto qed lemma proj_set_thickening: assumes "p ∈ proj_set x Z" "0 ≤ D" "D ≤ dist p x" "geodesic_segment_between G p x" shows "geodesic_segment_param G p D ∈ proj_set x (⋃z∈Z. cball z D)" proof (rule proj_setI') have "dist p (geodesic_segment_param G p D) = D" using geodesic_segment_param(7)[OF assms(4), of 0 D] unfolding geodesic_segment_param(1)[OF assms(4)] using assms by simp then show "geodesic_segment_param G p D ∈ (⋃