Theory Ultrametric_Restriction_Spaces
section ‹Ultrametric Structure of restriction Spaces›
theory Ultrametric_Restriction_Spaces
imports Ultrametric_Restriction_Spaces_Locale
Restriction_Spaces Banach_Theorem_Extension
begin
text ‹This has only be proven with the sort constraint,
not inside the context of the class \<^class>‹metric_space› ...›
context metric_space begin
lemma LIMSEQ_def : ‹X ⇢ L ⟷ (∀r>0. ∃no. ∀n≥no. dist (X n) L < r)›
unfolding tendsto_iff eventually_sequentially ..
lemma LIMSEQ_iff_nz: ‹X ⇢ L ⟷ (∀r>0. ∃no>0. ∀n≥no. dist (X n) L < r)›
by (meson Suc_leD LIMSEQ_def zero_less_Suc)
lemma metric_LIMSEQ_I: ‹(⋀r. 0 < r ⟹ ∃no. ∀n≥no. dist (X n) L < r) ⟹ X ⇢ L›
by (simp add: LIMSEQ_def)
lemma metric_LIMSEQ_D: ‹X ⇢ L ⟹ 0 < r ⟹ ∃no. ∀n≥no. dist (X n) L < r›
by (simp add: LIMSEQ_def)
lemma LIMSEQ_dist_iff:
‹f ⇢ l ⟷ (λx. dist (f x) l) ⇢ 0›
proof (unfold LIMSEQ_def, rule iffI)
show ‹(λn. dist (f n) l) ⇢ 0 ⟹ (∀r>0. ∃no. ∀n≥no. dist (f n) l < r)›
by (metis (mono_tags, lifting) eventually_at_top_linorder order_tendstoD(2))
next
show ‹∀r>0. ∃no. ∀n≥no. dist (f n) l < r ⟹ (λn. dist (f n) l) ⇢ 0›
by (simp add: metric_space_class.LIMSEQ_def)
qed
lemma Cauchy_converges_subseq:
fixes u::"nat ⇒ 'a"
assumes "Cauchy u"
"strict_mono r"
"(u ∘ r) ⇢ l"
shows "u ⇢ l"
proof -
have *: "eventually (λn. dist (u n) l < e) sequentially" if "e > 0" for e
proof -
have "e/2 > 0" using that by auto
then obtain N1 where N1: "⋀m n. m ≥ N1 ⟹ n ≥ N1 ⟹ dist (u m) (u n) < e/2"
using ‹Cauchy u› unfolding Cauchy_def by blast
obtain N2 where N2: "⋀n. n ≥ N2 ⟹ dist ((u ∘ r) n) l < e / 2"
using order_tendstoD(2)[OF iffD1[OF LIMSEQ_dist_iff ‹(u ∘ r) ⇢ l›] ‹e/2 > 0›]
unfolding eventually_sequentially by auto
have "dist (u n) l < e" if "n ≥ max N1 N2" for n
proof -
have "dist (u n) l ≤ dist (u n) ((u ∘ r) n) + dist ((u ∘ r) n) l"
by (rule dist_triangle)
also have "… < e/2 + e/2"
proof (intro add_strict_mono)
show "dist (u n) ((u ∘ r) n) < e / 2"
using N1[of n "r n"] N2[of n] that unfolding comp_def
by (meson assms(2) le_trans max.bounded_iff strict_mono_imp_increasing)
show "dist ((u ∘ r) n) l < e / 2"
using N2 that by auto
qed
finally show ?thesis by simp
qed
then show ?thesis unfolding eventually_sequentially by blast
qed
have "(λn. dist (u n) l) ⇢ 0"
by (simp add: less_le_trans * order_tendstoI)
then show ?thesis using LIMSEQ_dist_iff by auto
qed
end
subsection ‹The Construction with Classes›
class restriction_σ = restriction_space +
fixes restriction_σ :: ‹'a itself ⇒ nat ⇒ real› (‹σ⇩↓›)
setup ‹Sign.add_const_constraint (\<^const_name>‹dist›, NONE)›
class non_decseq_restriction_space =
uniformity_dist + open_uniformity + restriction_σ +
assumes restriction_σ_tendsto_zero' : ‹σ⇩↓ TYPE('a) ⇢ 0›
and zero_less_restriction_σ' [simp] : ‹0 < σ⇩↓ TYPE('a) n›
and dist_restriction_is' : ‹dist x y = (INF n ∈ {n. x ↓ n = y ↓ n}. σ⇩↓ TYPE('a) n)›
begin
sublocale NonDecseqRestrictionSpace ‹(↓)› ‹(=)› ‹UNIV› ‹σ⇩↓ TYPE ('a)› dist
by unfold_locales (simp_all add: restriction_σ_tendsto_zero' dist_restriction_is')
end
setup ‹Sign.add_const_constraint (\<^const_name>‹dist›, SOME \<^typ>‹'a :: metric_space ⇒ 'a ⇒ real›)›
text ‹We hide duplicated facts
@{thm restriction_σ_tendsto_zero zero_less_restriction_σ dist_restriction_is}.›
hide_fact restriction_σ_tendsto_zero' zero_less_restriction_σ' dist_restriction_is'
context non_decseq_restriction_space begin
subclass ultrametric_space
proof unfold_locales
show ‹dist x y = 0 ⟷ x = y› for x y
by (simp add: "restriction_dist_eq_0_iff_related")
have dist_commute : ‹dist x y = dist y x› for x y
by (simp add: dist_restriction_is) metis
show ‹dist x y ≤ max (dist x z) (dist y z)› for x y z
proof -
consider ‹x ≠ y› and ‹y ≠ z› and ‹x ≠ z› | ‹x = y ∨ y = z ∨ x = z› by blast
thus ‹dist x y ≤ max (dist x z) (dist y z)›
proof cases
assume ‹x ≠ y› and ‹y ≠ z› and ‹x ≠ z›
from this(1)[THEN not_related_imp_dist_restriction_le_some_restriction_σ]
this(2, 3)[THEN not_related_imp_dist_restriction_is_some_restriction_σ]
obtain l m n
where * : ‹dist x y ≤ σ⇩↓ TYPE('a) l› ‹x ↓ Suc l ≠ y ↓ Suc l›
and ** : ‹dist y z = σ⇩↓ TYPE('a) m› ‹∀k≤m. y ↓ k = z ↓ k›
and *** : ‹dist x z = σ⇩↓ TYPE('a) n› ‹∀k≤n. x ↓ k = z ↓ k› by blast
have ‹min n m ≤ l›
proof (rule ccontr)
assume ‹¬ min n m ≤ l›
hence ‹Suc l ≤ n› and ‹Suc l ≤ m› by simp_all
with "**"(2) "***"(2) Suc_le_lessD
have ‹x ↓ Suc l = z ↓ Suc l› ‹y ↓ Suc l = z ↓ Suc l› by simp_all
hence ‹x ↓ Suc l = y ↓ Suc l› by simp
with ‹x ↓ Suc l ≠ y ↓ Suc l› show False ..
qed
have ‹dist x y ≤ σ⇩↓ TYPE('a) (min n m)›
by (rule restriction_space_Inf_properties(1))
(simp add: "**"(2) "***"(2))
also have ‹… ≤ max (dist x z) (dist y z)›
unfolding "**"(1) "***"(1) by linarith
finally show ‹dist x y ≤ max (dist x z) (dist y z)› .
next
show ‹x = y ∨ y = z ∨ x = z ⟹ dist x y ≤ max (dist x z) (dist y z)›
by (elim disjE, simp_all add: dist_commute)
(metis not_related_imp_dist_restriction_is_some_restriction_σ
restriction_dist_eq_0_iff_related zero_le_restriction_σ dual_order.refl)
qed
qed
qed
end
context non_decseq_restriction_space begin
lemma restriction_tendsto_self: ‹(λn. x ↓ n) ⇢ x›
proof -
have ‹(λn. dist (x ↓ n) x) ⇢ 0›
proof (rule real_tendsto_sandwich[OF _ ])
show ‹∀⇩F n in sequentially. 0 ≤ dist (x ↓ n) x› by simp
next
show ‹∀⇩F n in sequentially. dist (x ↓ n) x ≤ σ⇩↓ TYPE('a) n›
by (auto intro: eventually_sequentiallyI[OF restriction_space_Inf_properties(1)])
next
show ‹(λn. 0) ⇢ 0› by simp
next
show ‹σ⇩↓ TYPE('a) ⇢ 0› by (simp add: restriction_σ_tendsto_zero)
qed
thus ‹(λn. x ↓ n) ⇢ x›
by (subst tendsto_iff[of ‹(λn. x ↓ n)›], subst eventually_sequentially)
(simp add: LIMSEQ_iff)
qed
end
class decseq_restriction_space = non_decseq_restriction_space +
assumes decseq_restriction_σ' : ‹decseq (σ⇩↓ TYPE('a))›
begin
sublocale DecseqRestrictionSpace ‹(↓)› ‹(=)› ‹UNIV :: 'a set›
‹restriction_σ TYPE('a)› dist
by unfold_locales (simp add: decseq_restriction_σ')
lemmas dist_restriction_is_bis_simplified = dist_restriction_is_bis[simplified]
and not_eq_imp_dist_restriction_is_restriction_σ_Sup_restriction_eq_simplified =
not_eq_imp_dist_restriction_is_restriction_σ_Sup_restriction_eq[simplified]
end
text ‹We hide duplicated fact @{thm decseq_restriction_σ}.›
hide_fact decseq_restriction_σ'
class strict_decseq_restriction_space = non_decseq_restriction_space +
assumes strict_decseq_restriction_σ : ‹strict_decseq (σ⇩↓ TYPE('a))›
begin
subclass decseq_restriction_space
by unfold_locales
(fact strict_decseq_imp_decseq[OF strict_decseq_restriction_σ])
end
text ‹Generic Properties›
lemma (in metric_space) dist_sequences_tendsto_zero_imp_tendsto_iff :
‹(λn. dist (σ n) (ψ n)) ⇢ 0 ⟹ σ ⇢ Σ ⟷ ψ ⇢ Σ›
proof (rule iffI)
show ‹ψ ⇢ Σ› if ‹σ ⇢ Σ› and ‹(λn. dist (σ n) (ψ n)) ⇢ 0› for σ ψ
proof -
from that have * : ‹(λn. dist (σ n) (ψ n) + dist (σ n) Σ) ⇢ 0›
unfolding LIMSEQ_dist_iff using tendsto_add_zero by blast
have ‹(λn. dist (ψ n) Σ) ⇢ 0›
by (rule real_tendsto_sandwich
[of ‹λn. 0› ‹λn. dist (ψ n) Σ› _ ‹λn. dist (σ n) (ψ n) + dist (σ n) Σ›])
(simp_all add: "*" dist_triangle3)
with LIMSEQ_dist_iff show ‹ψ ⇢ Σ› by blast
qed
thus ‹(λn. dist (σ n) (ψ n)) ⇢ 0 ⟹ ψ ⇢ Σ ⟹ σ ⇢ Σ›
by (simp add: dist_commute)
qed
lemma (in non_decseq_restriction_space) restricted_sequence_tendsto_iff :
‹(λn. σ n ↓ n) ⇢ Σ ⟷ σ ⇢ Σ›
proof -
have ‹(λn. dist (σ n ↓ n) (σ n)) ⇢ 0›
proof (unfold metric_space_class.LIMSEQ_def, intro allI impI)
fix ε :: real assume ‹0 < ε›
from restriction_σ_tendsto_zero[unfolded metric_space_class.LIMSEQ_def, rule_format, OF ‹0 < ε›]
obtain no where ‹∀n≥no. σ⇩↓ TYPE('a) n < ε›
by (auto simp add: dist_real_def)
have ‹no ≤ n ⟹ dist (dist (σ n ↓ n) (σ n)) 0 < ε› for n
by (simp, rule le_less_trans[OF restriction_space_Inf_properties(1)[of ‹σ⇩↓ TYPE('a) n›]])
(simp, simp add: ‹∀n≥no. σ⇩↓ TYPE('a) n < ε›)
thus ‹∃no. ∀n≥no. dist (dist (σ n ↓ n) (σ n)) 0 < ε› by blast
qed
thus ‹(λn. σ n ↓ n) ⇢ Σ ⟷ σ ⇢ Σ›
by (simp add: dist_sequences_tendsto_zero_imp_tendsto_iff)
qed
lemma (in non_decseq_restriction_space) Cauchy_restriction_chain :
‹Cauchy σ› if ‹chain⇩↓ σ›
proof (rule metric_CauchyI)
fix ε :: real assume ‹0 < ε›
from LIMSEQ_D[OF restriction_σ_tendsto_zero ‹0 < ε›, simplified]
obtain M where ‹σ⇩↓ TYPE('a) M < ε› by blast
moreover have ‹M ≤ m ⟹ M ≤ n ⟹ dist (σ m) (σ n) ≤ σ⇩↓ TYPE('a) M› for m n
by (rule restriction_space_Inf_properties(1), simp add: image_iff)
(metis restriction_chain_def_ter ‹chain⇩↓ σ›)
ultimately have ‹∀m≥M. ∀n≥M. dist (σ m) (σ n) < ε›
by (meson dual_order.strict_trans2)
thus ‹∃M. ∀m≥M. ∀n≥M. dist (σ m) (σ n) < ε› ..
qed
lemma (in non_decseq_restriction_space) restriction_tendsto_imp_tendsto :
‹σ ⇢ Σ› if ‹σ ─↓→ Σ›
proof (rule metric_LIMSEQ_I)
fix ε :: real assume ‹0 < ε›
with restriction_σ_tendsto_zero[THEN LIMSEQ_D]
obtain n0 where ‹∀k≥n0. σ⇩↓ TYPE('a) k < ε› by auto
hence ‹σ⇩↓ TYPE('a) n0 < ε› by simp
from restriction_tendstoD[OF ‹σ ─↓→ Σ›]
obtain n1 where ‹∀k≥n1. Σ ↓ n0 = σ k ↓ n0› ..
hence ‹∀k≥n1. dist (σ k) Σ ≤ σ⇩↓ TYPE('a) n0›
by (simp add: restriction_space_Inf_properties(1))
with ‹σ⇩↓ TYPE('a) n0 < ε›
have ‹∀k≥n1. dist (σ k) Σ < ε› by (meson order_le_less_trans)
thus ‹∃n1. ∀k≥n1. dist (σ k) Σ < ε› ..
qed
text ‹In Decseq Restriction Space›
context decseq_restriction_space begin
lemma le_dist_to_restriction_eqE :
obtains k where ‹n ≤ k› ‹⋀x y :: 'a. dist x y ≤ σ⇩↓ TYPE('a) k ⟹ x ↓ n = y ↓ n›
proof -
have ‹∃k≥n. ∀x y :: 'a. dist x y ≤ σ⇩↓ TYPE('a) k ⟶ x ↓ n = y ↓ n›
proof (rule ccontr)
assume ‹¬ (∃k≥n. ∀x y :: 'a. dist x y ≤ σ⇩↓ TYPE('a) k ⟶ x ↓ n = y ↓ n)›
hence ‹∀k≥n. ∃x y :: 'a. dist x y ≤ σ⇩↓ TYPE('a) k ∧ x ↓ n ≠ y ↓ n› by simp
then obtain X Y :: ‹nat ⇒ 'a›
where * : ‹∀k≥n. dist (X k) (Y k) ≤ σ⇩↓ TYPE('a) k›
‹∀k≥n. X k ↓ n ≠ Y k ↓ n› by metis
moreover obtain n0 where ‹∀k≥n0. σ⇩↓ TYPE('a) k < σ⇩↓ TYPE('a) n›
by (metis LIMSEQ_D zero_less_restriction_σ abs_of_nonneg diff_zero
restriction_σ_tendsto_zero real_norm_def zero_le_restriction_σ)
ultimately have ‹∀k≥n+n0. dist (X k) (Y k) < σ⇩↓ TYPE('a) n›
by (metis dual_order.strict_trans2 add_leE)
moreover from "*"(2) have ‹∀k≥n. σ⇩↓ TYPE('a) n ≤ dist (X k) (Y k)›
by (simp add: dist_restriction_is_bis)
(metis (full_types) decseq_restriction_σ[THEN decseqD] linorder_linear
not_eq_imp_dist_restriction_is_restriction_σ_Sup_restriction_eq_simplified(2))
ultimately show False by (metis le_add1 linorder_not_le order_refl)
qed
thus ‹(⋀k. ⟦n ≤ k; ⋀x y :: 'a. dist x y ≤ σ⇩↓ TYPE('a) k ⟹ x ↓ n = y ↓ n⟧
⟹ thesis) ⟹ thesis› by blast
qed
theorem tendsto_iff_restriction_tendsto : ‹σ ⇢ Σ ⟷ σ ─↓→ Σ›
proof (rule iffI)
show ‹σ ─↓→ Σ ⟹ σ ⇢ Σ› by (fact restriction_tendsto_imp_tendsto)
next
show ‹σ ─↓→ Σ› if ‹σ ⇢ Σ›
proof (rule restriction_tendstoI)
fix n
obtain n0 where ‹dist x y ≤ σ⇩↓ TYPE('a) n0 ⟹ x ↓ n = y ↓ n› for x y :: 'a
by (metis le_dist_to_restriction_eqE)
moreover from metric_LIMSEQ_D[OF ‹σ ⇢ Σ› zero_less_restriction_σ]
obtain n1 where ‹∀k≥n1. dist (σ k) Σ < σ⇩↓ TYPE('a) n0› ..
ultimately have ‹∀k≥n1. Σ ↓ n = σ k ↓ n› by (metis dual_order.order_iff_strict)
thus ‹∃n1. ∀k≥n1. Σ ↓ n = σ k ↓ n› ..
qed
qed
corollary convergent_iff_restriction_convergent : ‹convergent σ ⟷ convergent⇩↓ σ›
by (simp add: convergent_def restriction_convergent_def tendsto_iff_restriction_tendsto)
theorem complete_iff_restriction_complete :
‹(∀σ. Cauchy σ ⟶ convergent σ) ⟷ (∀σ. chain⇩↓ σ ⟶ convergent⇩↓ σ)›
proof (intro iffI impI allI)
fix σ assume hyp : ‹∀σ. Cauchy σ ⟶ convergent σ› and ‹chain⇩↓ σ›
from Cauchy_restriction_chain ‹chain⇩↓ σ› have ‹Cauchy σ› by blast
hence ‹convergent σ› by (simp add: hyp)
thus ‹convergent⇩↓ σ› by (simp add: convergent_iff_restriction_convergent)
next
fix σ assume hyp : ‹∀σ. chain⇩↓ σ ⟶ convergent⇩↓ σ› and ‹Cauchy σ›
from ‹Cauchy σ› have * : ‹∀n. ∃k. ∀l≥k. σ l ↓ n = σ k ↓ n›
by (metis (mono_tags, opaque_lifting) Cauchy_altdef2 dual_order.order_iff_strict
le_dist_to_restriction_eqE zero_less_restriction_σ)
define f where ‹f ≡ rec_nat
(LEAST k. ∀l≥k. σ l ↓ 0 = σ k ↓ 0)
(λn k. LEAST l. k < l ∧ (∀m≥l. σ m ↓ Suc n = σ l ↓ Suc n))›
have f_Suc_def : ‹f (Suc n) = (LEAST l. f n < l ∧ (∀m≥l. σ m ↓ Suc n = σ l ↓ Suc n))›
(is ‹f (Suc n) = Least (?f_Suc n)›) for n by (simp add: f_def)
from "*" have ** : ‹∃k>f n. ∀m≥k. σ m ↓ Suc n = σ k ↓ Suc n› for n
by (metis dual_order.trans lessI linorder_not_le order_le_less)
have ‹strict_mono f›
proof (unfold strict_mono_Suc_iff, rule allI)
show ‹f n < f (Suc n)› for n
by (fact LeastI_ex[of ‹?f_Suc n›, folded f_Suc_def, OF "**", THEN conjunct1])
qed
have ‹chain⇩↓ (λn. (σ ∘ f) n ↓ n)›
proof (rule restriction_chainI)
fix n
have ‹σ (f (Suc n)) ↓ n = σ (f n) ↓ n›
proof (cases n)
show ‹n = 0 ⟹ σ (f (Suc n)) ↓ n = σ (f n) ↓ n› by simp
next
show ‹n = Suc nat ⟹ σ (f (Suc n)) ↓ n = σ (f n) ↓ n› for nat
proof (clarify, intro LeastI_ex[of ‹?f_Suc nat›,
folded f_Suc_def, THEN conjunct2, rule_format, OF "**"])
show ‹n = Suc nat ⟹ f (Suc nat) ≤ f (Suc (Suc nat))›
by (simp add: ‹strict_mono f› strict_mono_less_eq)
qed
qed
thus ‹(σ ∘ f) (Suc n) ↓ Suc n ↓ n = (σ ∘ f) n ↓ n› by simp
qed
with hyp have ‹convergent⇩↓ (λn. (σ ∘ f) n ↓ n)› by simp
hence ‹convergent⇩↓ (λn. (σ ∘ f) n)›
by (simp add: restriction_convergent_restricted_iff_restriction_convergent)
hence ‹convergent (λn. (σ ∘ f) n)›
by (simp add: convergent_iff_restriction_convergent)
with Cauchy_converges_subseq[OF ‹Cauchy σ› ‹strict_mono f›]
show ‹convergent σ› unfolding convergent_def by blast
qed
end
text ‹The following classes will be useful later.›
class complete_decseq_restriction_space = decseq_restriction_space +
assumes restriction_chain_imp_restriction_convergent' : ‹chain⇩↓ σ ⟹ convergent⇩↓ σ›
begin
subclass complete_restriction_space
by unfold_locales (fact restriction_chain_imp_restriction_convergent')
subclass complete_ultrametric_space
proof (unfold_locales)
from complete_iff_restriction_complete restriction_chain_imp_restriction_convergent
show ‹Cauchy σ ⟹ convergent σ› for σ by blast
qed
end
text ‹We hide duplicated fact @{thm restriction_chain_imp_restriction_convergent}.›
hide_fact restriction_chain_imp_restriction_convergent'
class complete_strict_decseq_restriction_space = strict_decseq_restriction_space +
assumes restriction_chain_imp_restriction_convergent' : ‹chain⇩↓ σ ⟹ convergent⇩↓ σ›
begin
subclass complete_decseq_restriction_space
by (unfold_locales) (fact restriction_chain_imp_restriction_convergent')
end
text ‹We hide duplicated fact @{thm restriction_chain_imp_restriction_convergent'}.›
hide_fact restriction_chain_imp_restriction_convergent'
class restriction_δ = restriction_σ +
fixes restriction_δ :: ‹'a itself ⇒ real› (‹δ⇩↓›)
assumes zero_less_restriction_δ [simp] : ‹0 < δ⇩↓ TYPE('a)›
and restriction_δ_less_one [simp] : ‹δ⇩↓ TYPE('a) < 1›
begin
lemma zero_le_restriction_δ [simp] : ‹0 ≤ δ⇩↓ TYPE('a)›
and restriction_δ_le_one [simp] : ‹δ⇩↓ TYPE('a) ≤ 1›
and zero_le_pow_restriction_δ [simp] : ‹0 ≤ δ⇩↓ TYPE('a) ^ n›
by (simp_all add: order_less_imp_le)
lemma pow_restriction_δ_le_one [simp] : ‹δ⇩↓ TYPE('a) ^ n ≤ 1›
by (simp add: power_le_one)
lemma pow_restriction_δ_less_one [simp] : ‹n ≠ 0 ⟹ δ⇩↓ TYPE('a) ^ n < 1›
by (metis restriction_δ_less_one zero_less_restriction_δ not_gr_zero power_0 power_strict_decreasing)
end
setup ‹Sign.add_const_constraint (\<^const_name>‹dist›, NONE)›
class at_least_geometric_restriction_space =
uniformity_dist + open_uniformity + restriction_δ +
assumes zero_less_restriction_σ' : ‹0 < σ⇩↓ TYPE('a) n›
and restriction_σ_le :
‹σ⇩↓ TYPE('a) (Suc n) ≤ δ⇩↓ TYPE('a) * σ⇩↓ TYPE('a) n›
and dist_restriction_is' :
‹dist x y = (INF n ∈ {n. x ↓ n = y ↓ n}. σ⇩↓ TYPE('a) n)›
setup ‹Sign.add_const_constraint (\<^const_name>‹dist›, SOME \<^typ>‹'a :: metric_space ⇒ 'a ⇒ real›)›
context at_least_geometric_restriction_space begin
lemma restriction_σ_le_restriction_σ_times_pow_restriction_δ :
‹σ⇩↓ TYPE('a) (n + k) ≤ σ⇩↓ TYPE('a) n * δ⇩↓ TYPE('a) ^ k›
by (induct k, simp_all)
(metis dual_order.trans restriction_σ_le zero_less_restriction_δ
mult.left_commute mult_le_cancel_left_pos)
lemma restriction_σ_le_pow_restriction_δ :
‹σ⇩↓ TYPE('a) n ≤ σ⇩↓ TYPE('a) 0 * δ⇩↓ TYPE('a) ^ n›
by (metis add_0 restriction_σ_le_restriction_σ_times_pow_restriction_δ)
subclass strict_decseq_restriction_space
proof unfold_locales
have ‹∀⇩F n in sequentially. 0 ≤ σ⇩↓ TYPE('a) n›
by (simp add: zero_less_restriction_σ' order_less_imp_le)
moreover have ‹∀⇩F n in sequentially. σ⇩↓ TYPE('a) n
≤ σ⇩↓ TYPE('a) 0 * δ⇩↓ TYPE('a) ^ n›
by (simp add: restriction_σ_le_pow_restriction_δ)
moreover have ‹(λn. 0) ⇢ 0› by simp
moreover have ‹(λn. σ⇩↓ TYPE('a) 0 * δ⇩↓ TYPE('a) ^ n) ⇢ 0›
by (simp add: LIMSEQ_abs_realpow_zero2 abs_of_pos tendsto_mult_right_zero)
ultimately show ‹σ⇩↓ TYPE('a) ⇢ 0› by (fact real_tendsto_sandwich)
next
show ‹0 < σ⇩↓ TYPE('a) n› for n
by (fact zero_less_restriction_σ')
next
show ‹dist x y = Inf (σ⇩↓ TYPE('a) ` {n. x ↓ n = y ↓ n})› for x y
by (fact dist_restriction_is')
next
show ‹strict_decseq (σ⇩↓ TYPE('a))›
by (rule strict_decseqI, rule le_less_trans[OF restriction_σ_le])
(simp add: zero_less_restriction_σ')
qed
lemma ‹0 < δ⇩↓ TYPE('a) ^ n› by simp
end
text ‹We hide duplicated facts
@{thm zero_less_restriction_σ dist_restriction_is}.›
hide_fact zero_less_restriction_σ' dist_restriction_is'
class complete_at_least_geometric_restriction_space = at_least_geometric_restriction_space +
assumes restriction_chain_imp_restriction_convergent' : ‹chain⇩↓ σ ⟹ convergent⇩↓ σ›
begin
subclass complete_strict_decseq_restriction_space
by unfold_locales (fact restriction_chain_imp_restriction_convergent')
end
text ‹We hide duplicated fact @{thm restriction_chain_imp_restriction_convergent}.›
hide_fact restriction_chain_imp_restriction_convergent'
setup ‹Sign.add_const_constraint (\<^const_name>‹dist›, NONE)›
class geometric_restriction_space = uniformity_dist + open_uniformity + restriction_δ +
assumes restriction_σ_is : ‹σ⇩↓ TYPE('a) n = δ⇩↓ TYPE('a) ^ n›
and dist_restriction_is' : ‹dist x y = (INF n ∈ {n. x ↓ n = y ↓ n}. σ⇩↓ TYPE('a) n)›
begin
text ‹This is what ``restriction space'' usually mean in the literature.
The previous classes are generalizations of this concept
(even this one is a generalization, since we usually
have \<^term>‹δ⇩↓ TYPE('a) = 1 / 2›).›
subclass at_least_geometric_restriction_space
proof unfold_locales
show ‹0 < σ⇩↓ TYPE('a) n› for n by (simp add: restriction_σ_is)
next
show ‹σ⇩↓ TYPE('a) (Suc n) ≤ δ⇩↓ TYPE('a) * σ⇩↓ TYPE('a) n› for n
by (simp add: restriction_σ_is)
next
show ‹dist x y = Inf (σ⇩↓ TYPE('a) ` {n. x ↓ n = y ↓ n})› for x y
by (fact dist_restriction_is')
qed
lemma ‹0 < δ⇩↓ TYPE('a) ^ n› by simp
end
setup ‹Sign.add_const_constraint (\<^const_name>‹dist›, SOME \<^typ>‹'a :: metric_space ⇒ 'a ⇒ real›)›
text ‹We hide duplicated fact @{thm dist_restriction_is}.›
hide_fact dist_restriction_is'
class complete_geometric_restriction_space = geometric_restriction_space +
assumes restriction_chain_imp_restriction_convergent' : ‹chain⇩↓ σ ⟹ convergent⇩↓ σ›
begin
subclass complete_at_least_geometric_restriction_space
by (unfold_locales) (fact restriction_chain_imp_restriction_convergent')
end
text ‹We hide duplicated fact @{thm restriction_chain_imp_restriction_convergent}.›
hide_fact restriction_chain_imp_restriction_convergent'
theorem geometric_restriction_space_completeI : ‹convergent σ›
if ‹⋀σ :: nat ⇒ 'a. restriction_chain σ ⟹ ∃Σ. ∀n. Σ ↓ n = σ n›
and ‹Cauchy σ› for σ :: ‹nat ⇒ 'a :: geometric_restriction_space›
by (metis complete_iff_restriction_complete convergent_def
convergent_iff_restriction_convergent ext restriction_tendsto_self that)
lemma (in non_decseq_restriction_space) restriction_cball_subset_cball :
‹σ⇩↓ TYPE('a) n ≤ r ⟹ ℬ⇩↓(Σ, n) ⊆ {x. dist Σ x ≤ r}›
by (simp add: subset_iff restriction_cball_mem_iff)
(simp add: dual_order.trans restriction_space_Inf_properties(1))
corollary restriction_cball_subset_cball_bis :
‹σ⇩↓ TYPE('a) n ≤ r ⟹ ℬ⇩↓(Σ, n) ⊆ cball Σ r›
for Σ :: ‹'a :: non_decseq_restriction_space›
unfolding cball_def by (fact restriction_cball_subset_cball)
lemma (in non_decseq_restriction_space) restriction_ball_subset_ball :
‹σ⇩↓ TYPE('a) n < r ⟹ restriction_ball Σ n ⊆ {x. dist Σ x < r}›
by (simp add: subset_iff restriction_cball_mem_iff)
(metis (mono_tags, lifting) image_eqI mem_Collect_eq order_le_less_trans
restriction_related_pred restriction_space_Inf_properties(1))
corollary restriction_ball_subset_ball_bis :
‹σ⇩↓ TYPE('a) n < r ⟹ restriction_ball Σ n ⊆ ball Σ r›
for Σ :: ‹'a :: non_decseq_restriction_space›
unfolding ball_def by (fact restriction_ball_subset_ball)
lemma (in strict_decseq_restriction_space)
restriction_cball_is_cball : ‹ℬ⇩↓(Σ, n) = {x. dist Σ x ≤ σ⇩↓ TYPE('a) n}›
proof (intro subset_antisym subsetI)
from restriction_cball_subset_cball
show ‹x ∈ ℬ⇩↓(Σ, n) ⟹ x ∈ {x. dist Σ x ≤ σ⇩↓ TYPE('a) n}› for x by blast
next
show ‹x ∈ ℬ⇩↓(Σ, n)› if ‹x ∈ {x. dist Σ x ≤ σ⇩↓ TYPE('a) n}› for x
proof (cases ‹Σ = x›)
show ‹Σ = x ⟹ x ∈ ℬ⇩↓(Σ, n)› by simp
next
assume ‹Σ ≠ x›
with not_related_imp_dist_restriction_is_some_restriction_σ obtain m
where ‹dist Σ x = σ⇩↓ TYPE('a) m› ‹∀k≤m. Σ ↓ k = x ↓ k› by blast
from ‹x ∈ {x. dist Σ x ≤ σ⇩↓ TYPE('a) n}›
have ‹dist Σ x ≤ σ⇩↓ TYPE('a) n› by simp
with ‹dist Σ x = σ⇩↓ TYPE('a) m› have ‹n ≤ m›
by (metis linorder_not_less strict_decseq_restriction_σ strict_decseq_def_bis)
with ‹∀k≤m. Σ ↓ k = x ↓ k› have ‹Σ ↓ n = x ↓ n› by simp
thus ‹x ∈ ℬ⇩↓(Σ, n)› by (simp add: restriction_cball_mem_iff)
qed
qed
lemma restriction_cball_is_cball_bis : ‹ℬ⇩↓(Σ, n) = cball Σ (σ⇩↓ TYPE('a) n)›
for Σ :: ‹'a :: strict_decseq_restriction_space›
by (simp add: cball_def restriction_cball_is_cball)
lemma (in strict_decseq_restriction_space)
restriction_ball_is_ball : ‹restriction_ball Σ n = {x. dist Σ x < σ⇩↓ TYPE('a) n}›
proof (intro subset_antisym subsetI)
show ‹x ∈ restriction_ball Σ n ⟹ x ∈ {x. dist Σ x < σ⇩↓ TYPE('a) n}› for x
by (simp add: subset_iff)
(metis lessI local.restriction_cball_is_cball strict_decseq_restriction_σ
mem_Collect_eq order_le_less_trans strict_decseq_def_bis)
next
show ‹x ∈ restriction_ball Σ n› if ‹x ∈ {x. dist Σ x < σ⇩↓ TYPE('a) n}› for x
proof (cases ‹Σ = x›)
show ‹Σ = x ⟹ x ∈ restriction_ball Σ n› by simp
next
assume ‹Σ ≠ x›
with not_related_imp_dist_restriction_is_some_restriction_σ obtain m
where ‹dist Σ x = σ⇩↓ TYPE('a) m› ‹∀k≤m. Σ ↓ k = x ↓ k› by blast
from ‹x ∈ {x. dist Σ x < σ⇩↓ TYPE('a) n}›
have ‹dist Σ x < σ⇩↓ TYPE('a) n› by simp
with ‹dist Σ x = σ⇩↓ TYPE('a) m› have ‹n < m›
using strict_decseq_restriction_σ strict_decseq_def_bis by auto
with ‹∀k≤m. Σ ↓ k = x ↓ k› have ‹Σ ↓ Suc n = x ↓ Suc n› by simp
thus ‹x ∈ restriction_ball Σ n› by (simp add: restriction_cball_mem_iff)
qed
qed
lemma restriction_ball_is_ball_bis : ‹restriction_ball Σ n = ball Σ (σ⇩↓ TYPE('a) n)›
for Σ :: ‹'a :: strict_decseq_restriction_space›
by (simp add: ball_def restriction_ball_is_ball)
lemma isCont_iff_restriction_cont_at : ‹isCont f Σ ⟷ restriction_cont_at f Σ›
for f :: ‹'a :: decseq_restriction_space ⇒ 'b :: decseq_restriction_space›
by (unfold restriction_cont_at_def continuous_at_sequentially comp_def,
fold tendsto_iff_restriction_tendsto) simp
lemma (in strict_decseq_restriction_space)
open_iff_restriction_open : ‹open U ⟷ open⇩↓ U›
proof (unfold open_dist restriction_open_iff_restriction_cball_characterization, intro iffI ballI)
fix Σ assume ‹∀x∈U. ∃e>0. ∀y. dist y x < e ⟶ y ∈ U› and ‹Σ ∈ U›
then obtain e where ‹0 < e› ‹∀y. dist y Σ < e ⟶ y ∈ U› by blast
from ‹0 < e› obtain n where ‹σ⇩↓ TYPE('a) n < e›
by (metis eventually_at_top_linorder le_refl restriction_σ_tendsto_zero order_tendstoD(2))
with ‹∀y. dist y Σ < e ⟶ y ∈ U› dist_commute restriction_cball_is_cball
have ‹ℬ⇩↓(Σ, n) ⊆ U› by auto
thus ‹∃n. ℬ⇩↓(Σ, n) ⊆ U› ..
next
fix x assume ‹∀Σ∈U. ∃n. ℬ⇩↓(Σ, n) ⊆ U› ‹x ∈ U›
then obtain n where ‹ℬ⇩↓(x, n) ⊆ U› by blast
hence ‹∀y. dist y x < σ⇩↓ TYPE('a) n ⟶ y ∈ U›
by (simp add: dist_commute restriction_cball_is_cball subset_iff)
thus ‹∃e>0. ∀y. dist y x < e ⟶ y ∈ U›
using zero_less_restriction_σ' by blast
qed
lemma (in strict_decseq_restriction_space)
closed_iff_restriction_closed : ‹closed U ⟷ closed⇩↓ U›
by (simp add: closed_open open_iff_restriction_open restriction_open_Compl_iff)
lemma continuous_on_iff_restriction_cont_on :
‹open U ⟹ continuous_on U f ⟷ restriction_cont_on f U›
for f :: ‹'a :: decseq_restriction_space ⇒ 'b :: decseq_restriction_space›
by (simp add: restriction_cont_on_def continuous_on_eq_continuous_at
flip: isCont_iff_restriction_cont_at)
subsection ‹Equivalence between Lipschitz Map and Restriction shift Map›
text ‹For a function @{term [show_types] ‹f :: 'a ⇒ 'b›}, it is equivalent to have
\<^term>‹restriction_shift_on f k A› and
\<^term>‹lipschitz_with_on f (restriction_δ TYPE('b :: geometric_restriction_space) ^ k) A›
when \<^typ>‹'a› is of sort \<^class>‹geometric_restriction_space› and
\<^term>‹restriction_σ TYPE('b :: geometric_restriction_space) =
restriction_σ TYPE('a :: geometric_restriction_space)›
(\<^typ>‹'b› is then necessarily also of sort \<^class>‹geometric_restriction_space›).›
text ‹Weaker versions of this result wan be established with weaker assumptions on the sort,
this is what we do below.›
lemma restriction_shift_nonneg_on_imp_lipschitz_with_on :
‹lipschitz_with_on f (restriction_δ TYPE('b) ^ k) A› if ‹restriction_shift_on f (int k) A›
and le_restriction_σ : ‹⋀n. restriction_σ TYPE('b) n ≤ restriction_σ TYPE('a) n›
for f :: ‹'a :: decseq_restriction_space ⇒ 'b :: at_least_geometric_restriction_space›
proof (rule lipschitz_with_onI)
show ‹0 ≤ restriction_δ TYPE('b) ^ k› by simp
next
fix x y assume ‹x ∈ A› ‹y ∈ A› ‹x ≠ y› ‹f x ≠ f y›
from ‹restriction_shift_on f k A›[THEN restriction_shift_onD, OF ‹x ∈ A› ‹y ∈ A›]
have ‹i ∈ restriction_related_set x y ⟹ i + k ∈ restriction_related_set (f x) (f y)› for i
by (simp add: nat_int_add)
hence ‹Sup (restriction_related_set x y) + k ∈ restriction_related_set (f x) (f y)›
using ‹x ≠ y› Sup_in_restriction_related_set by blast
hence ‹Sup (restriction_related_set x y) + k ≤ Sup (restriction_related_set (f x) (f y))›
by (simp add: ‹f x ≠ f y› bdd_above_restriction_related_set_iff cSup_upper)
moreover have ‹dist (f x) (f y) = restriction_σ TYPE('b) (Sup (restriction_related_set (f x) (f y)))›
by (simp add: ‹f x ≠ f y› dist_restriction_is_bis_simplified)
ultimately have ‹dist (f x) (f y) ≤ restriction_σ TYPE('b) (Sup (restriction_related_set x y) + k)›
by (simp add: decseqD decseq_restriction_space_class.decseq_restriction_σ)
hence ‹dist (f x) (f y) ≤ restriction_σ TYPE('b) (Sup (restriction_related_set x y)) * restriction_δ TYPE('b) ^ k›
by (meson order.trans restriction_σ_le_restriction_σ_times_pow_restriction_δ)
also have ‹… ≤ restriction_σ TYPE('a) (Sup (restriction_related_set x y)) * restriction_δ TYPE('b) ^ k›
by (simp add: le_restriction_σ)
finally show ‹dist (f x) (f y) ≤ restriction_δ TYPE('b) ^ k * dist x y›
by (simp add: dist_restriction_is_bis[of x y] ‹x ≠ y› mult.commute)
qed
corollary restriction_shift_nonneg_imp_lipschitz_with :
‹⟦restriction_shift f (int k); ⋀n. restriction_σ TYPE('b) n ≤ restriction_σ TYPE('a) n⟧
⟹ lipschitz_with f (restriction_δ TYPE('b) ^ k)›
for f :: ‹'a :: decseq_restriction_space ⇒ 'b :: at_least_geometric_restriction_space›
using restriction_shift_def restriction_shift_nonneg_on_imp_lipschitz_with_on by blast
lemma lipschitz_with_on_imp_restriction_shift_neg_on :
‹restriction_shift_on f (- int k) A› if ‹lipschitz_with_on f (restriction_δ TYPE('b) powi - int k) A›
and le_restriction_σ : ‹⋀n. restriction_σ TYPE('a) n ≤ restriction_σ TYPE('b) n›
for f :: ‹'a :: decseq_restriction_space ⇒ 'b :: at_least_geometric_restriction_space›
proof (rule restriction_shift_onI, goal_cases)
fix x y n assume ‹x ∈ A› ‹y ∈ A› ‹f x ≠ f y› ‹x ↓ n = y ↓ n›
from ‹f x ≠ f y› have ‹x ≠ y› by blast
from ‹lipschitz_with_on f (restriction_δ TYPE('b) powi - int k) A›
[THEN lipschitz_with_onD2, OF ‹x ∈ A› ‹y ∈ A›]
have ‹dist (f x) (f y) ≤ restriction_δ TYPE('b) powi - int k * dist x y› .
hence ‹dist (f x) (f y) * restriction_δ TYPE('b) ^ k ≤ dist x y›
by (subst (asm) mult.commute)
(drule mult_imp_div_pos_le[rotated]; simp add: power_int_minus_divide)
hence ‹restriction_σ TYPE('b) (Sup (restriction_related_set (f x) (f y))) * restriction_δ TYPE('b) ^ k
≤ restriction_σ TYPE('b) (Sup (restriction_related_set x y))›
by (simp add: dist_restriction_is_bis ‹x ≠ y› ‹f x ≠ f y› )
(drule order_trans[OF _ le_restriction_σ], simp)
from order_trans[OF restriction_σ_le_restriction_σ_times_pow_restriction_δ
[of ‹Sup (restriction_related_set (f x) (f y))› k] this]
have ‹restriction_σ TYPE('b) (Sup (restriction_related_set (f x) (f y)) + k)
≤ restriction_σ TYPE('b) (Sup (restriction_related_set x y))› .
hence ‹Sup (restriction_related_set x y) ≤ Sup (restriction_related_set (f x) (f y)) + k›
using strict_decseq_def_ter strict_decseq_restriction_σ by blast
from order_trans[OF cSup_upper this] have ‹n ≤ Sup (restriction_related_set (f x) (f y)) + k›
by (simp add: ‹x ↓ n = y ↓ n› ‹x ≠ y› bdd_above_restriction_related_set_iff)
hence ‹nat (int n + - int k) ≤ Sup (restriction_related_set (f x) (f y))› by linarith
thus ‹f x ↓ nat (int n + - int k) = f y ↓ nat (int n + - int k)›
by (metis not_eq_imp_dist_restriction_is_restriction_σ_Sup_restriction_eq_simplified(2))
qed
corollary lipschitz_with_imp_restriction_shift_neg :
‹⟦lipschitz_with f (restriction_δ TYPE('b) powi - int k);
⋀n. restriction_σ TYPE('a) n ≤ restriction_σ TYPE('b) n⟧
⟹ restriction_shift f (- int k)›
for f :: ‹'a :: decseq_restriction_space ⇒ 'b :: at_least_geometric_restriction_space›
using lipschitz_with_on_imp_restriction_shift_neg_on restriction_shift_def by blast
text ‹We obtained that \<^const>‹restriction_shift› implies \<^const>‹lipschitz_with›
when \<^term>‹0 ≤ k› and that \<^const>‹lipschitz_with› implies
\<^const>‹restriction_shift› when \<^term>‹k ≤ 0›. To cover the remaining cases,
we give move from \<^class>‹at_least_geometric_restriction_space›
to \<^class>‹geometric_restriction_space›.›
theorem lipschitz_with_on_iff_restriction_shift_on :
‹lipschitz_with_on f (restriction_δ TYPE('b) powi k) A ⟷ restriction_shift_on f k A›
if same_restriction_σ : ‹restriction_σ TYPE('b) = restriction_σ TYPE('a)›
for f :: ‹'a :: decseq_restriction_space ⇒ 'b :: geometric_restriction_space›
proof (rule iffI)
show ‹restriction_shift_on f k A› if ‹lipschitz_with_on f (restriction_δ TYPE('b) powi k) A›
proof (rule restriction_shift_onI)
fix x y n assume ‹x ∈ A› ‹y ∈ A› ‹f x ≠ f y› ‹x ↓ n = y ↓ n›
from ‹f x ≠ f y› have ‹x ≠ y› by blast
from ‹lipschitz_with_on f (restriction_δ TYPE('b) powi k) A›
[THEN lipschitz_with_onD2, OF ‹x ∈ A› ‹y ∈ A›]
have ‹dist (f x) (f y) ≤ restriction_δ TYPE('b) powi k * dist x y› .
also have ‹dist (f x) (f y) = restriction_δ TYPE('b) ^ Sup (restriction_related_set (f x) (f y))›
by (simp add: dist_restriction_is_bis ‹f x ≠ f y› restriction_σ_is)
also have ‹dist x y = restriction_δ TYPE('b) ^ Sup (restriction_related_set x y)›
by (simp add: dist_restriction_is_bis ‹x ≠ y› restriction_σ_is same_restriction_σ[symmetric])
finally have ‹restriction_δ TYPE('b) ^ Sup (restriction_related_set (f x) (f y))
≤ restriction_δ TYPE('b) powi k * restriction_δ TYPE('b) ^ Sup (restriction_related_set x y)› .
also have ‹… = restriction_δ TYPE('b) powi (k + Sup (restriction_related_set x y))›
by (subst power_int_add, metis order_less_irrefl zero_less_restriction_δ) simp
finally have ‹restriction_δ TYPE('b) ^ Sup (restriction_related_set (f x) (f y)) ≤ …› .
moreover have ‹restriction_δ TYPE('b) powi m ≤ restriction_δ TYPE('b) powi m' ⟹ m' ≤ m› for m m'
by (rule ccontr, unfold not_le,
drule power_int_strict_decreasing[OF _ zero_less_restriction_δ restriction_δ_less_one])
(fold not_le, blast)
ultimately have ‹k + Sup (restriction_related_set x y) ≤ Sup (restriction_related_set (f x) (f y))› by simp
hence ‹Sup (restriction_related_set x y) ≤ Sup (restriction_related_set (f x) (f y)) - k› by simp
with ‹x ↓ n = y ↓ n› ‹x ≠ y› linorder_not_le
not_eq_imp_dist_restriction_is_restriction_σ_Sup_restriction_eq_simplified(3)
have ‹n ≤ Sup (restriction_related_set (f x) (f y)) - k› by fastforce
hence ‹nat (int n + k) ≤ Sup (restriction_related_set (f x) (f y))› by simp
thus ‹f x ↓ nat (int n + k) = f y ↓ nat (int n + k)›
by (metis not_eq_imp_dist_restriction_is_restriction_σ_Sup_restriction_eq_simplified(2))
qed
next
show ‹lipschitz_with_on f (restriction_δ TYPE('b) powi k) A› if ‹restriction_shift_on f k A›
proof (cases k)
show ‹k = int k' ⟹ lipschitz_with_on f (restriction_δ TYPE('b) powi k) A› for k'
by (simp, rule restriction_shift_nonneg_on_imp_lipschitz_with_on)
(use ‹restriction_shift_on f k A› same_restriction_σ in simp_all)
next
fix k' assume ‹k = - int (Suc k')›
show ‹lipschitz_with_on f (restriction_δ TYPE('b) powi k) A›
proof (rule lipschitz_with_onI)
show ‹0 ≤ restriction_δ TYPE('b) powi k› by simp
next
fix x y assume ‹x ∈ A› ‹y ∈ A› ‹x ≠ y› ‹f x ≠ f y›
have ‹i ∈ restriction_related_set x y ⟹ i - Suc k' ∈ restriction_related_set (f x) (f y)› for i
using ‹restriction_shift_on f k A›[THEN restriction_shift_onD, OF ‹x ∈ A› ‹y ∈ A›, of i]
by (unfold ‹k = - int (Suc k')›, clarify) (metis diff_conv_add_uminus nat_minus_as_int)
hence ‹Sup (restriction_related_set x y) - Suc k' ∈ restriction_related_set (f x) (f y)›
using ‹x ≠ y› not_eq_imp_dist_restriction_is_restriction_σ_Sup_restriction_eq_simplified by blast
hence ‹Sup (restriction_related_set x y) - Suc k' ≤ Sup (restriction_related_set (f x) (f y))›
by (simp add: ‹f x ≠ f y› bdd_above_restriction_related_set_iff cSup_upper)
hence * : ‹Sup (restriction_related_set x y) + k ≤ Sup (restriction_related_set (f x) (f y))›
by (simp add: ‹k = - int (Suc k')›)
have ‹dist (f x) (f y) = restriction_δ TYPE('b) powi Sup (restriction_related_set (f x) (f y))›
by (simp add: ‹f x ≠ f y› dist_restriction_is_bis_simplified restriction_σ_is)
also have ‹… ≤ restriction_δ TYPE('b) powi (Sup (restriction_related_set x y) + k)›
by (rule power_int_decreasing[OF "*"]; simp)
(metis order_less_irrefl zero_less_restriction_δ)
also have ‹… = restriction_δ TYPE('b) powi k * restriction_δ TYPE('b) powi (Sup (restriction_related_set x y))›
by (subst power_int_add, metis order_less_irrefl zero_less_restriction_δ) simp
also have ‹restriction_δ TYPE('b) powi (Sup (restriction_related_set x y)) = dist x y›
by (simp add: ‹x ≠ y› dist_restriction_is_bis_simplified
restriction_σ_is same_restriction_σ[symmetric])
finally show ‹dist (f x) (f y) ≤ restriction_δ TYPE('b) powi k * dist x y› .
qed
qed
qed
corollary lipschitz_with_iff_restriction_shift :
‹restriction_σ TYPE('b) = restriction_σ TYPE('a) ⟹
lipschitz_with f (restriction_δ TYPE('b) powi k) ⟷ restriction_shift f k›
for f :: ‹'a :: decseq_restriction_space ⇒ 'b :: geometric_restriction_space›
by (simp add: lipschitz_with_on_iff_restriction_shift_on restriction_shift_def)
end