Theory Holder_Continuous
section "Hölder continuity"
theory Holder_Continuous
imports "HOL-Analysis.Analysis"
begin
text ‹ H{\"o}lder continuity is a weaker version of Lipschitz continuity. ›
definition holder_at_within :: "real ⇒ 'a set ⇒ 'a ⇒ ('a :: metric_space ⇒ 'b :: metric_space) ⇒ bool" where
"holder_at_within γ D r φ ≡ γ ∈ {0<..1} ∧
(∃ε > 0. ∃C ≥ 0. ∀s ∈ D. dist r s < ε ⟶ dist (φ r) (φ s) ≤ C * dist r s powr γ)"
definition local_holder_on :: "real ⇒ 'a :: metric_space set ⇒ ('a ⇒ 'b :: metric_space) ⇒ bool" where
"local_holder_on γ D φ ≡ γ ∈ {0<..1} ∧
(∀t∈D. ∃ε > 0. ∃C ≥ 0. (∀r∈D. ∀s∈D. dist s t < ε ∧ dist r t < ε ⟶ dist (φ r) (φ s) ≤ C * dist r s powr γ))"
definition holder_on :: "real ⇒ 'a :: metric_space set ⇒ ('a ⇒ 'b :: metric_space) ⇒ bool" ("_-holder'_on" 1000) where
"γ-holder_on D φ ⟷ γ ∈ {0<..1} ∧ (∃C ≥ 0. (∀r∈D. ∀s∈D. dist (φ r) (φ s) ≤ C * dist r s powr γ))"
lemma holder_onI:
assumes "γ ∈ {0<..1}" "∃C ≥ 0. (∀r∈D. ∀s∈D. dist (φ r) (φ s) ≤ C * dist r s powr γ)"
shows "γ-holder_on D φ"
unfolding holder_on_def using assms by blast
text ‹ We prove various equivalent formulations of local holder continuity, using open and closed
balls and inequalities. ›
lemma local_holder_on_cball:
"local_holder_on γ D φ ⟷ γ ∈ {0<..1} ∧
(∀t∈D. ∃ε > 0. ∃C ≥ 0. (∀r∈cball t ε ∩ D. ∀s∈cball t ε ∩ D. dist (φ r) (φ s) ≤ C * dist r s powr γ))"
(is "?L ⟷ ?R")
proof
assume *: ?L
{
fix t assume "t ∈ D"
then obtain ε C where "ε > 0" "C ≥ 0"
"∀r∈ball t ε ∩ D. ∀s∈ball t ε ∩ D. dist (φ r) (φ s) ≤ C * dist r s powr γ"
using * unfolding local_holder_on_def apply simp
by (metis Int_iff dist_commute mem_ball)
then have **: "∀r∈cball t (ε/2) ∩ D. ∀s∈cball t (ε/2) ∩ D. dist (φ r) (φ s) ≤ C * dist r s powr γ"
by auto
have "∃ε > 0. ∃C ≥ 0. ∀r∈cball t ε ∩ D. ∀s∈cball t ε ∩ D. dist (φ r) (φ s) ≤ C * dist r s powr γ"
apply (rule exI[where x = "ε/2"])
apply (simp add: ‹ε > 0›)
apply (rule exI[where x = "C"])
using ** ‹C ≥ 0› by blast
}
then show ?R
using * local_holder_on_def by blast
next
assume *: ?R
{
fix t assume "t ∈ D"
then obtain ε C where eC: "ε > 0" "C ≥ 0"
"∀r∈cball t ε ∩ D. ∀s∈cball t ε ∩ D. dist (φ r) (φ s) ≤ C * dist r s powr γ"
using * by blast
then have "∀r ∈ D. ∀s ∈ D. dist r t < ε ∧ dist s t < ε ⟶ dist (φ r) (φ s) ≤ C * dist r s powr γ"
unfolding cball_def by (simp add: dist_commute)
then have "∃ε>0. ∃C≥0. ∀r ∈ D. ∀s ∈ D. dist r t < ε ∧ dist s t < ε ⟶ dist (φ r) (φ s) ≤ C * dist r s powr γ"
using eC by blast
}
then show "local_holder_on γ D φ"
using * unfolding local_holder_on_def by metis
qed
corollary local_holder_on_leq_def: "local_holder_on γ D φ ⟷ γ ∈ {0<..1} ∧
(∀t∈D. ∃ε > 0. ∃C ≥ 0. (∀r∈D. ∀s∈D. dist s t ≤ ε ∧ dist r t ≤ ε ⟶ dist (φ r) (φ s) ≤ C * dist r s powr γ))"
unfolding local_holder_on_cball by (metis dist_commute Int_iff mem_cball)
corollary local_holder_on_ball: "local_holder_on γ D φ ⟷ γ ∈ {0<..1} ∧
(∀t∈D. ∃ε > 0. ∃C ≥ 0. (∀r∈ball t ε ∩ D. ∀s∈ball t ε ∩ D. dist (φ r) (φ s) ≤ C * dist r s powr γ))"
unfolding local_holder_on_def by (metis dist_commute Int_iff mem_ball)
lemma local_holder_on_altdef:
assumes "D ≠ {}"
shows "local_holder_on γ D φ = (∀t ∈ D. (∃ε > 0. (γ-holder_on ((cball t ε) ∩ D) φ)))"
unfolding local_holder_on_cball holder_on_def using assms by blast
lemma local_holder_on_cong[cong]:
assumes "γ = ε" "C = D" "⋀x. x ∈ C ⟹ φ x = ψ x"
shows "local_holder_on γ C φ ⟷ local_holder_on ε D ψ"
unfolding local_holder_on_def using assms by presburger
lemma local_holder_onI:
assumes "γ ∈ {0<..1}" "(∀t∈D. ∃ε > 0. ∃C ≥ 0. (∀r∈D. ∀s∈D. dist s t < ε ∧ dist r t < ε ⟶ dist (φ r) (φ s) ≤ C * dist r s powr γ))"
shows "local_holder_on γ D φ"
using assms unfolding local_holder_on_def by blast
lemma local_holder_ballI:
assumes "γ ∈ {0<..1}"
and "⋀t. t ∈ D ⟹ ∃ε > 0. ∃C ≥ 0. ∀r∈ball t ε ∩ D. ∀s∈ball t ε ∩ D.
dist (φ r) (φ s) ≤ C * dist r s powr γ"
shows "local_holder_on γ D φ"
using assms unfolding local_holder_on_ball by blast
lemma local_holder_onE:
assumes local_holder: "local_holder_on γ D φ"
and gamma: "γ ∈ {0<..1}"
and "t ∈ D"
obtains ε C where "ε > 0" "C ≥ 0"
"⋀r s. r ∈ ball t ε ∩ D ⟹ s ∈ ball t ε ∩ D ⟹ dist (φ r) (φ s) ≤ C * dist r s powr γ"
using assms unfolding local_holder_on_ball by auto
text ‹ Holder continuity matches up with the existing definitions in @{theory "HOL-Analysis.Lipschitz"}›
lemma holder_1_eq_lipschitz: "1-holder_on D φ = (∃C. lipschitz_on C D φ)"
unfolding holder_on_def lipschitz_on_def by (auto simp: fun_eq_iff dist_commute)
lemma local_holder_1_eq_local_lipschitz:
assumes "T ≠ {}"
shows "local_holder_on 1 D φ = local_lipschitz T D (λ_. φ)"
proof
assume *: "local_holder_on 1 D φ"
{
fix t assume "t ∈ D"
then obtain ε C where eC: "ε > 0" "C ≥ 0"
"(∀r∈D. ∀s∈D. dist s t ≤ ε ∧ dist r t ≤ ε ⟶ dist (φ r) (φ s) ≤ C * dist r s)"
using * powr_to_1 unfolding local_holder_on_cball apply simp
by (metis Int_iff dist_commute mem_cball)
{
fix r s assume rs: "r ∈ D" "s ∈ D" "dist s t ≤ ε ∧ dist r t ≤ ε"
then have "r ∈ cball t ε ∩ D" "s∈cball t ε ∩ D" "dist (φ r) (φ s) ≤ C * dist r s"
unfolding cball_def using rs eC by (auto simp: dist_commute)
}
then have "∀r∈cball t ε ∩ D. ∀s∈cball t ε ∩ D. dist (φ r) (φ s) ≤ C * dist r s"
by (simp add: dist_commute)
then have "C-lipschitz_on ((cball t ε) ∩ D) φ"
using eC lipschitz_on_def by blast
then have "∃ε>0. ∃C. C-lipschitz_on ((cball t ε) ∩ D) φ"
using eC(1) by blast
}
then show "local_lipschitz T D (λ_. φ)"
unfolding local_lipschitz_def by blast
next
assume *: "local_lipschitz T D (λ_. φ)"
{
fix x assume x: "x ∈ D"
fix t assume t: "t ∈ T"
then obtain u L where uL: "u > 0" "∀t∈cball t u ∩ T. L-lipschitz_on (cball x u ∩ D) φ"
using * x t unfolding local_lipschitz_def by blast
then have "L-lipschitz_on (cball x u ∩ D) φ"
using t by force
then have "1-holder_on (cball x u ∩ D) φ"
using holder_1_eq_lipschitz by blast
then have "∃ε > 0. (1-holder_on ((cball x ε) ∩ D) φ)"
using uL by blast
}
then have "x ∈ D ⟹ ∃ε>0. (1-holder_on (cball x ε ∩ D) φ)" for x
using assms by blast
then show "local_holder_on 1 D φ"
unfolding local_holder_on_cball holder_on_def by (auto simp: dist_commute)
qed
lemma local_holder_refine:
assumes g: "local_holder_on g D φ" "g ≤ 1"
and h: "h ≤ g" "h > 0"
shows "local_holder_on h D φ"
proof -
{
fix t assume t: "t ∈ D"
then have "∃ε>0. ∃C≥0. (∀r∈D. ∀s∈D. dist s t ≤ ε ∧ dist r t ≤ ε ⟶ dist (φ r) (φ s) ≤ C * dist r s powr g)"
using g(1) unfolding local_holder_on_leq_def by blast
then obtain ε C where eC: "ε > 0" "C ≥ 0"
"(∀s∈D. ∀r∈D. dist s t ≤ ε ∧ dist r t ≤ ε ⟶ dist (φ r) (φ s) ≤ C * dist r s powr g)"
by blast
let ?e = "min ε (1/2)"
{
fix s r assume *: "s ∈ D" "r ∈ D" "dist s t ≤ ?e" "dist r t ≤ ?e"
then have "dist (φ r) (φ s) ≤ C * dist r s powr g"
using eC by simp
moreover have "dist r s ≤ 1"
by (smt (verit) * dist_triangle2 half_bounded_equal)
ultimately have "dist (φ r) (φ s) ≤ C * dist r s powr h"
by (metis dual_order.trans zero_le_dist powr_mono' assms(3) eC(2) mult_left_mono )
}
then have "(∀s∈D. ∀r∈D. dist s t ≤ ?e ∧ dist r t ≤ ?e ⟶ dist (φ r) (φ s) ≤ C * dist r s powr h)"
by blast
moreover have "?e > 0" "C ≥ 0"
using eC by linarith+
ultimately have "∃ε>0. ∃C≥0. (∀r∈D. ∀s∈D. dist s t ≤ ε ∧ dist r t ≤ ε ⟶ dist (φ r) (φ s) ≤ C * dist r s powr h)"
by blast
}
then show ?thesis
unfolding local_holder_on_leq_def using assms by force
qed
lemma holder_uniform_continuous:
assumes "γ-holder_on X φ"
shows "uniformly_continuous_on X φ"
unfolding uniformly_continuous_on_def
proof safe
fix e::real
assume "0 < e"
from assms obtain C where C: "C ≥ 1" "(∀r∈X. ∀s∈X. dist (φ r) (φ s) ≤ C * dist r s powr γ)"
unfolding holder_on_def
by (smt (verit) dist_eq_0_iff mult_le_cancel_right1 powr_0 powr_gt_zero)
{
fix r s assume "r ∈ X" "s ∈ X"
have dist_0: "dist (φ r) (φ s) = 0 ⟹ dist (φ r) (φ s) < e"
using ‹0 < e› by linarith
then have holder_neq_0: "dist (φ r) (φ s) < (C + 1) * dist r s powr γ" if "dist (φ r) (φ s) > 0"
using C(2) that
by (smt (verit, ccfv_SIG) ‹r ∈ X› ‹s ∈ X› dist_eq_0_iff mult_le_cancel_right powr_gt_zero)
have gamma: "γ ∈ {0<..1}"
using assms holder_on_def by blast+
assume "dist r s < (e/C) powr (1 / γ)"
then have "C * dist r s powr γ < C * ((e/C) powr (1 / γ)) powr γ" if "dist (φ r) (φ s) > 0"
using holder_neq_0 C(1) powr_less_mono2 gamma by fastforce
also have "... = e"
using C(1) gamma ‹0 < e› powr_powr by auto
finally have "dist (φ r) (φ s) < e"
using dist_0 holder_neq_0 C(2) ‹r ∈ X› ‹s ∈ X› by fastforce
}
then show "∃d>0. ∀x∈X. ∀x'∈X. dist x' x < d ⟶ dist (φ x') (φ x) < e"
by (metis C(1) ‹0 < e› divide_eq_0_iff linorder_not_le order_less_irrefl powr_gt_zero zero_less_one)
qed
corollary holder_on_continuous_on: "γ-holder_on X φ ⟹ continuous_on X φ"
using holder_uniform_continuous uniformly_continuous_imp_continuous by blast
lemma holder_implies_local_holder: "γ-holder_on D φ ⟹ local_holder_on γ D φ"
apply (cases "D = {}")
apply (simp add: holder_on_def local_holder_on_def)
apply (simp add: local_holder_on_altdef holder_on_def)
apply (metis IntD1 inf.commute)
done
lemma local_holder_imp_continuous:
assumes local_holder: "local_holder_on γ X φ"
shows "continuous_on X φ"
unfolding continuous_on_def
proof safe
fix x assume "x ∈ X"
{
assume "X ≠ {}"
from local_holder obtain ε where "0 < ε" and holder: "γ-holder_on ((cball x ε) ∩ X) φ"
unfolding local_holder_on_altdef[OF ‹X ≠ {}›] using ‹x ∈ X› by blast
have "x ∈ ball x ε" using ‹0 < ε› by simp
then have "(φ ⤏ φ x) (at x within cball x ε ∩ X)"
using holder_on_continuous_on[OF holder] ‹x ∈ X› unfolding continuous_on_def by simp
moreover have "∀⇩F xa in at x. (xa ∈ cball x ε ∩ X) = (xa ∈ X)"
using eventually_at_ball[OF ‹0 < ε›, of x UNIV]
by eventually_elim auto
ultimately have "(φ ⤏ φ x) (at x within X)"
by (rule Lim_transform_within_set)
}
then show "(φ ⤏ φ x) (at x within X)"
by fastforce
qed
lemma local_holder_compact_imp_holder:
assumes "compact I" "local_holder_on γ I φ"
shows "γ-holder_on I φ"
proof -
have *: "γ ∈ {0<..1}" "(∀t∈I. ∃ε. ∃C. ε > 0 ∧ C ≥ 0 ∧
(∀r ∈ ball t ε ∩ I. ∀s ∈ ball t ε ∩ I. dist (φ r) (φ s) ≤ C * dist r s powr γ))"
using assms(2) unfolding local_holder_on_ball by simp_all
obtain ε C where eC: "t ∈ I ⟹ ε t > 0 ∧ C t ≥ 0 ∧ (∀r ∈ ball t (ε t) ∩ I. ∀s ∈ ball t (ε t) ∩ I. dist (φ r) (φ s) ≤ C t * dist r s powr γ)" for t
by (metis *(2))
have "I ⊆ (⋃t ∈ I. ball t (ε t))"
apply (simp add: subset_iff)
using eC by force
then obtain D where D: "D ⊆ (λt. ball t (ε t)) ` I" "finite D" "I ⊆ ⋃ D"
using compact_eq_Heine_Borel[of I] apply (simp add: assms(1))
by (smt (verit, ccfv_SIG) open_ball imageE mem_Collect_eq subset_iff)
then obtain T where T: "D = (λt. ball t (ε t)) ` T" "T ⊆ I" "finite T"
by (meson finite_subset_image subset_image_iff)
text ‹ $\varrho$ is the Lebesgue number of the cover ›
from D obtain ρ :: real where ρ: "∀t ∈ I. ∃U ∈ D. ball t ρ ⊆ U" "ρ > 0"
by (smt (verit, del_insts) Elementary_Metric_Spaces.open_ball Heine_Borel_lemma assms(1) imageE subset_image_iff)
have "bounded (φ ` I)"
by (metis compact_continuous_image compact_imp_bounded assms local_holder_imp_continuous)
then obtain l where l: "∀x ∈ I. ∀y ∈ I. dist (φ x) (φ y) ≤ l"
by (metis bounded_two_points image_eqI)
text ‹ Simply need to construct C\_bar such that it is greater than any of these ›
define C_bar where "C_bar ≡ max ((∑t ∈ T. C t)) (l * ρ powr (- γ))"
have C_bar_le: "C_bar ≥ C t" if "t ∈ T" for t
proof -
have ge_0: "t ∈ T ⟹ C t ≥ 0" for t
using T(2) eC by blast
then have "∑ (C ` (T - {t})) ≥ 0"
by (metis (mono_tags, lifting) Diff_subset imageE subset_eq sum_nonneg)
then have "(∑t ∈ T. C t) ≥ C t"
by (metis T(3) ge_0 sum_nonneg_leq_bound that)
then have "max ((∑t ∈ T. C t)) S ≥ C t" for S
by argo
then show "C_bar ≥ C t"
unfolding C_bar_def by blast
qed
{
fix s r assume sr: "s ∈ I" "r ∈ I"
{
assume "dist s r < ρ"
then obtain t where t: "t ∈ T" "s ∈ ball t (ε t)" "r ∈ ball t (ε t)"
by (smt (verit) sr D T ρ ball_eq_empty centre_in_ball imageE mem_ball subset_iff)
then have "dist (φ s) (φ r) ≤ C t * dist s r powr γ"
using eC[of t] T(2) sr by blast
then have "dist (φ s) (φ r) ≤ C_bar * dist s r powr γ"
by (smt (verit, best) t C_bar_le mult_right_mono powr_non_neg)
} note le_rho = this
{
assume "dist s r ≥ ρ"
then have "dist (φ s) (φ r) ≤ l * (dist s r / ρ) powr γ"
proof -
have "(dist s r / ρ) ≥ 1"
using ‹dist s r ≥ ρ› ‹ρ > 0› by auto
then have "(dist s r / ρ) powr γ ≥ 1"
using "*"(1) ge_one_powr_ge_zero by auto
then show "dist (φ s) (φ r) ≤ l * (dist s r / ρ) powr γ"
using l
by (metis dist_self dual_order.strict_trans1 leI less_le_not_le mult_less_cancel_left2 sr)
qed
also have "... ≤ C_bar * dist s r powr γ"
proof -
have "l * (dist s r / ρ) powr γ = l * ρ powr (- γ) * dist s r powr γ "
using ρ(2) divide_powr_uminus powr_divide by force
also have "... ≤ C_bar * dist s r powr γ"
unfolding C_bar_def by (simp add: mult_right_mono)
finally show "l * (dist s r / ρ) powr γ ≤ C_bar * dist s r powr γ"
.
qed
finally have "dist (φ s) (φ r) ≤ C_bar * dist s r powr γ"
.
}
then have "dist (φ s) (φ r) ≤ C_bar * dist s r powr γ"
using le_rho by argo
}
then have "∀r∈I. ∀s∈I. dist (φ r) (φ s) ≤ C_bar * dist r s powr γ"
by simp
then show ?thesis
unfolding holder_on_def
by (metis "*"(1) C_bar_def dist_self div_by_0 divide_nonneg_pos divide_powr_uminus
dual_order.trans l max.cobounded2 powr_0 powr_gt_zero)
qed
lemma holder_const: "γ-holder_on C (λ_. c) ⟷ γ ∈ {0<..1}"
unfolding holder_on_def by auto
lemma local_holder_const: "local_holder_on γ C (λ_. c) ⟷ γ ∈ {0<..1}"
using holder_const holder_implies_local_holder local_holder_on_def by blast
end