Theory Kolmogorov_Chentsov
section "The Kolomgorov-Chentsov theorem"
theory Kolmogorov_Chentsov
imports Stochastic_Processes Holder_Continuous Dyadic_Interval Measure_Convergence
begin
subsection "Supporting lemmas"
text ‹ The main contribution of this file is the Kolmogorov-Chentsov theorem: given a stochastic
process that satisfies some continuity properties, we can construct a H{\"o}lder continuous modification.
We first prove some auxiliary lemmas before moving on to the main construction. ›
text ‹ Klenke 5.11: Markov inequality. Compare with @{thm nn_integral_Markov_inequality} ›
lemma nn_integral_Markov_inequality_extended:
fixes f :: "real ⇒ ennreal" and ε :: real and X :: "'a ⇒ real"
assumes mono: "mono_on (range X ∪ {0<..}) f"
and finite: "⋀x. f x < ∞"
and e: "ε > 0" "f ε > 0"
and [measurable]: "X ∈ borel_measurable M"
shows "emeasure M {p ∈ space M. (X p) ≥ ε} ≤ (∫⇧+ x. f (X x) ∂M) / f ε"
proof -
have f_eq: "f = (λx. ennreal (enn2real (f x)))"
using finite by simp
have "mono_on (range X) (λx. enn2real (f x))"
apply (intro mono_onI)
using mono[THEN mono_onD] finite by (simp add: enn2real_mono)
then have "f ∈ borel_measurable (restrict_space borel (range X))"
apply (subst f_eq)
apply (intro measurable_compose[where f="λx. enn2real (f x)" and g=ennreal])
using borel_measurable_mono_on_fnc apply blast
apply simp
done
then have "(λx. f (X x)) ∈ borel_measurable M"
apply (intro measurable_compose[where g=f and f=X and N="restrict_space borel (range X)"])
apply (simp_all add: measurable_restrict_space2)
done
then have "{x ∈ space M. f (X x) ≥ f ε} ∈ sets M"
by measurable
then have "f ε * emeasure M {x ∈ space M. X x ≥ ε} ≤ (∫⇧+x∈{x ∈ space M. f ε ≤ f (X x)}. f ε ∂M)"
apply (simp add: nn_integral_cmult_indicator)
using e mono_onD[OF mono] zero_le apply (blast intro: mult_left_mono emeasure_mono)
done
also have "... ≤ (∫⇧+x∈{x ∈ space M. f ε ≤ f (X x)}. f (X x) ∂M)"
apply (rule nn_integral_mono)
subgoal for x
apply (cases "f ε ≤ f (X x)")
using ennreal_leI by auto
done
also have "... ≤ ∫⇧+ x. f (X x) ∂M"
by (simp add: nn_integral_mono indicator_def)
finally have "emeasure M {p ∈ space M. ε ≤ X p} * f ε / f ε ≤ (∫⇧+ x. f (X x) ∂M) / f ε"
by (simp add: divide_right_mono_ennreal field_simps)
then show ?thesis
using mult_divide_eq_ennreal finite[of "ε"] e(2) by simp
qed
lemma nn_integral_Markov_inequality_extended_rnv:
fixes f :: "real ⇒ real" and ε :: real and X :: "'a ⇒ 'b :: real_normed_vector"
assumes [measurable]: "X ∈ borel_measurable M"
and mono: "mono_on {0..} f"
and e: "ε > 0" "f ε > 0"
shows "emeasure M {p ∈ space M. norm (X p) ≥ ε} ≤ (∫⇧+ x. f (norm (X x)) ∂M) / f ε"
apply (rule nn_integral_Markov_inequality_extended)
using mono ennreal_leI unfolding mono_on_def apply force
apply (simp_all add: e)
done
subsection "Kolmogorov-Chentsov"
text ‹ Klenke theorem 21.6 - Kolmorogov-Chentsov ›
locale Kolmogorov_Chentsov =
fixes X :: "(real, 'a, 'b :: polish_space) stochastic_process"
and a b C γ :: real
assumes index[simp]: "proc_index X = {0..}"
and target_borel[simp]: "proc_target X = borel"
and gt_0: "a > 0" "b > 0" "C > 0"
and b_leq_a: "b ≤ a"
and gamma: "γ ∈ {0<..<b/a}"
and expectation: "⋀s t. ⟦s ≥ 0; t ≥ 0⟧ ⟹
(∫⇧+ x. dist (X t x) (X s x) powr a ∂proc_source X) ≤ C * dist t s powr (1+b)"
begin
lemma gamma_0_1[simp]:"γ ∈ {0<..1}"
using gt_0 b_leq_a gamma
by (metis divide_less_eq_1_pos divide_self greaterThanAtMost_iff
greaterThanLessThan_iff nless_le order_less_trans)
lemma gamma_gt_0[simp]: "γ > 0"
using gamma greaterThanLessThan_iff by blast
lemma gamma_le_1[simp]: "γ ≤ 1"
using gamma_0_1 by auto
abbreviation "source ≡ proc_source X"
lemma X_borel_measurable[measurable]: "X t ∈ borel_measurable source" for t
by (metis random_process target_borel)
lemma markov: "𝒫(x in source. ε ≤ dist (X t x) (X s x)) ≤ (C * dist t s powr (1 + b)) / ε powr a"
if "s ≥ 0" "t ≥ 0" "ε > 0" for s t ε
proof -
let ?inc = "λx. dist (X t x) (X s x) powr a"
have "emeasure source {x ∈ space source. ε ≤ dist (X t x) (X s x)}
≤ integral⇧N source ?inc / ε powr a"
apply (rule nn_integral_Markov_inequality_extended)
using that(1,2) apply measurable
subgoal using gt_0(1) imageE powr_mono2 by (auto intro: mono_onI)
using that apply simp_all
done
also have "... ≤ (C * dist t s powr (1 + b)) / ennreal (ε powr a)"
apply (rule divide_right_mono_ennreal)
using expectation[OF that(1,2)] ennreal_leI by simp
finally have "emeasure source {x ∈ space source. ε ≤ dist (X t x) (X s x)}
≤ (C * dist t s powr (1 + b)) / ε powr a"
using that(3) divide_ennreal gt_0(3) by simp
moreover have "C * dist t s powr (1 + b) / ε powr a ≥ 0"
using gt_0(3) by auto
ultimately show ?thesis
by (simp add: proc_source.emeasure_eq_measure)
qed
lemma conv_in_prob:
assumes "t ≥ 0"
shows "tendsto_measure (proc_source X) X (X t) (at t within {0..})"
proof -
{
fix p ε :: real assume "0 < p" "0 < ε"
let ?q = "(p * ε powr a / C) powr (1/(1+b))"
have "0 < ?q"
using ‹0 < p› gt_0(3) ‹0 < ε› by simp
have p_eq: "p = (C * ?q powr (1 + b)) / ε powr a"
using gt_0 ‹0 < ?q› ‹0 < p› by (simp add: field_simps powr_powr)
have "0 < dist r t ∧ dist r t < ?q ⟶ dist 𝒫(x in source. ε ≤ dist (X t x) (X r x)) 0 ≤ p"
if "r ∈ {0..}" for r
proof safe
assume "0 < dist r t" "dist r t < ?q"
have "0 ≤ r"
using that by auto
from ‹dist r t < ?q› have "C * dist r t powr (1 + b) / ε powr a ≤ p"
apply (subst p_eq)
using gt_0(2) gt_0(3) apply (simp add: divide_le_cancel powr_mono2)
done
then show "dist 𝒫(x in source. ε ≤ dist (process X t x) (process X r x)) 0 ≤ p"
using markov[OF ‹0 ≤ r› assms ‹0 < ε›] by (simp add: dist_commute)
qed
then have "∃d>0. ∀r∈{0..}. 0 < dist r t ∧ dist r t < d ⟶
dist 𝒫(x in source. ε ≤ dist (X r x) (X t x)) 0 ≤ p"
apply (intro exI[where x="?q"])
apply (subst(3) dist_commute)
using ‹0 < p› gt_0(3) ‹0 < ε› dist_commute by fastforce
} then show ?thesis
by (simp add: finite_measure.tendsto_measure_leq, safe, intro Lim_withinI)
qed
lemma conv_in_prob_finite:
assumes "t ≥ 0"
shows "tendsto_measure (proc_source X) X (X t) (at t within {0..T})"
proof -
have "at t within {0..T} ≤ at t within {0..}"
by (simp add: at_le)
then show ?thesis
apply (rule tendsto_measure_mono)
using assms by (rule conv_in_prob)
qed
lemma incr: "𝒫(x in source. 2 powr (- γ * n) ≤ dist (X ((k - 1) * 2 powr - n) x) (X (k * 2 powr - n) x))
≤ C * 2 powr (-n * (1+b-a*γ))"
if "k ≥ 1" "n ≥ 0" for k n
proof -
have "𝒫(x in source. 2 powr (- γ * n) ≤ dist (X ((k - 1) * 2 powr - n) x) (X (k * 2 powr - n) x))
≤ C * dist ((k - 1) * 2 powr - n) (k * 2 powr - n) powr (1 + b) / (2 powr (- γ * n)) powr a"
using that by (auto intro: markov)
also have "... = C * 2 powr (- n - b * n) / 2 powr (- γ * n * a)"
by (auto simp: dist_real_def powr_powr field_simps)
also have "... = C * 2 powr (-n * (1+b-a*γ))"
by (simp add: field_simps powr_add[symmetric])
finally show ?thesis .
qed
end
text ‹ In order to construct the modification of $X$, it suffices to construct a modification of $X$
on $\{0..T\}$ for all finite $T$, from which we construct the modification on $\{0..\}$ via a countable
union. ›
locale Kolmogorov_Chentsov_finite = Kolmogorov_Chentsov +
fixes T :: real
assumes zero_le_T: "0 < T"
begin
text ‹ $A_n$ will characterise the set of states with increments that exceed the bounds required for
H{\"o}lder continuity. As $n \longrightarrow \infty$, this approaches the set of states for which $X$ is not
H{\"o}lder continuous. We define $N$ as this limit, and show that $N$ is a null set. On $\omega \in \Omega - N$,
we show that $X(\omega)$ is H{\"o}lder continuous (and therefore uniformly continuious) on the dyadic
rationals, and construct a modification by taking the continuous extension on the reals. ›
definition "A ≡ λn. if 2 ^ n * T < 1 then space source else
{x ∈ space source.
Max {dist (X (real_of_int (k - 1) * 2 powr - real n) x) (X (real_of_int k * 2 powr - real n) x)
| k. k ∈ {1..⌊2^n * T⌋}} ≥ 2 powr (-γ * real n)}"
abbreviation "B ≡ λn. (⋃m. A (m + n))"
abbreviation "N ≡ ⋂(range B)"
lemma A_geq: "2 ^ n * T ≥ 1 ⟹ A n = {x ∈ space source.
Max {dist (X (real_of_int (k - 1) * 2 powr - real n) x) (X (real_of_int k * 2 powr - real n) x)
| k. k ∈ {1..⌊2^n * T⌋}} ≥ 2 powr (-γ * real n)}" for n
by (simp add: A_def)
lemma A_measurable[measurable]: "A n ∈ sets source"
unfolding A_def apply (cases "2 ^ n * T < 1")
apply simp
apply (simp only: if_False)
apply measurable
done
lemma emeasure_A_leq:
fixes n :: nat
assumes [simp]: "2^n * T ≥ 1"
shows "emeasure source (A n) ≤ C * T * 2 powr (- n * (b - a * γ))"
proof -
have nonempty: "{1..⌊2^n * T⌋} ≠ {}"
using assms by fastforce
have finite: "finite {1..⌊2^n * T⌋}"
by simp
have "emeasure source (A n) ≤ emeasure source (⋃k ∈ {1..⌊2^n * T⌋}.
{x∈space source. dist (X (real_of_int (k - 1) * 2 powr - real n) x) (X (real_of_int k * 2 powr - real n) x) ≥ 2 powr (- γ * real n)})"
(is "emeasure source (A n) ≤ emeasure source ?R")
proof (rule emeasure_mono, intro subsetI)
fix x assume *: "x ∈ A n"
from * have in_space: "x ∈ space source"
using A_measurable sets.sets_into_space by blast
from * have "2 powr (- γ * real n) ≤ Max {dist (X (real_of_int (k - 1) * 2 powr - real n) x) (X (real_of_int k * 2 powr - real n) x) |k. k ∈ {1..⌊2 ^ n * T⌋}}"
using A_geq assms by blast
then have "∃k ∈ {1..⌊2 ^ n * T⌋}. 2 powr (- γ * real n) ≤ dist (X (real_of_int (k - 1) * 2 powr - real n) x) (X (real_of_int k * 2 powr - real n) x)"
apply (simp only: setcompr_eq_image)
apply (rule Max_finite_image_ex[where P="λx. 2 powr (- γ * real n) ≤ x", OF finite nonempty])
apply (metis Collect_mem_eq)
done
then show "x ∈ ?R"
using in_space by simp
next
show "?R ∈ sets source"
by measurable
qed
also have "... ≤ (∑k∈{1..⌊2^n * T⌋}. emeasure source
{x∈space source. dist (X (real_of_int (k - 1) * 2 powr - real n) x) (X (real_of_int k * 2 powr - real n) x) ≥ 2 powr (- γ * real n)})"
apply (rule emeasure_subadditive_finite)
apply blast
apply (subst image_subset_iff)
apply (intro ballI)
apply measurable
done
also have "... ≤ C * 2 powr (- n * (1 + b - a * γ)) * (card {1..⌊2 ^ n * T⌋})"
proof -
{
fix k assume "k ∈ {1..⌊2 ^ n * T⌋}"
then have "real_of_int k ≥ 1"
by presburger
then have "𝒫(x in source. 2 powr (- γ * real n) ≤ dist (X (real_of_int (k - 1) * 2 powr - real n) x) (X (real_of_int k * 2 powr - real n) x))
≤ C * 2 powr (-(real n) * (1+b-a*γ))"
using incr gamma by force
} note X = this
then have "sum (λk. 𝒫(x in source. 2 powr (- γ * real n) ≤ dist (X (real_of_int (k - 1) * 2 powr - real n) x) (X (real_of_int k * 2 powr - real n) x)))
{1..⌊2 ^ n * T⌋} ≤ of_nat (card {1..⌊2 ^ n * T⌋}) * (C * 2 powr (-(real n) * (1+b-a*γ)))"
by (fact sum_bounded_above)
then show ?thesis
using ennreal_leI by (auto simp: proc_source.emeasure_eq_measure mult.commute)
qed
also have "... ≤ C * 2 powr (- n * (1 + b - a * γ)) * ⌊2 ^ n * T⌋"
using nonempty zle_iff_zadd by force
also have "... ≤ C * 2 powr (- n * (1+b - a * γ)) * 2^n * T"
by (simp add:ennreal_leI gt_0(3))
also have "... = C * 1/(2^n) * 2 powr (- n * (b - a * γ)) * 2^n * T"
apply (intro ennreal_cong)
apply (simp add: scale_left_imp_eq field_simps)
by (smt (verit) powr_add powr_realpow)
also have "... = C * T * 2 powr (- n * (b - a * γ))"
by (simp add: field_simps)
finally show ?thesis .
qed
lemma measure_A_leq:
assumes "2^n * T ≥ 1"
shows "measure source (A n) ≤ C * T * 2 powr (- n * (b - a * γ))"
apply (intro measure_leq_emeasure_ennreal)
subgoal using gt_0(3) zero_le_T by auto
using emeasure_A_leq apply (simp add: A_geq assms)
done
lemma summable_A: "summable (λm. measure source (A m))"
proof -
have "b - a * γ > 0"
by (metis diff_gt_0_iff_gt gamma greaterThanLessThan_iff gt_0(1) mult.commute pos_less_divide_eq)
have 1: "2 powr (- real x * (b - a * γ)) = (1 / 2 powr (b - a * γ)) ^ x" for x
apply (cases "x = 0")
by (simp_all add: field_simps powr_add[symmetric] powr_realpow[symmetric] powr_powr)
have 2: "summable (λn. 2 powr (- n * (b - a * γ)))" (is "summable ?C")
proof -
have "summable (λn. (1 / 2 powr (b - a * γ)) ^ n)"
using ‹b - a * γ > 0› by auto
then show "summable (λx. 2 powr (- real x * (b - a * γ)))"
using 1 by simp
qed
from zero_le_T obtain N where "2^N * T ≥ 1"
by (metis dual_order.order_iff_strict mult.commute one_less_numeral_iff pos_divide_le_eq
power_one_over reals_power_lt_ex semiring_norm(76) zero_less_numeral zero_less_power)
then have "⋀n. n ≥ N ⟹ 2^n * T ≥ 1"
by (smt (verit, best) ‹0 < T› mult_right_mono power_increasing_iff)
then have "⋀n. n ≥ N ⟹ norm (measure source (A n)) ≤ C * T * 2 powr (- n * (b - a * γ))"
using measure_A_leq by simp
moreover have "summable (λn. C * T * 2 powr (- n * (b - a * γ)))"
using 2 summable_mult by simp
ultimately show ?thesis
using summable_comparison_test' by fast
qed
lemma lim_B: "(λn. measure source (B n)) ⇢ 0"
proof -
have measure_B_le: "measure source (B n) ≤ (∑m. measure source (A (m + n)))" for n
apply (rule proc_source.finite_measure_subadditive_countably)
subgoal by auto
apply (subst summable_iff_shift)
using summable_A by blast
have lim_A: "(λn. (∑m. measure source (A (m + n)))) ⇢ 0"
by (fact suminf_exist_split2[OF summable_A])
have "convergent (λn. measure source (B n))"
proof (intro Bseq_monoseq_convergent)
show "Bseq (λn. Sigma_Algebra.measure source (⋃m. A (m + n)))"
apply (rule BseqI'[where K="measure source (⋃ (range A))"])
apply (auto intro!: proc_source.finite_measure_mono)
done
show "monoseq (λn. Sigma_Algebra.measure source (⋃m. A (m + n)))"
apply (intro decseq_imp_monoseq[unfolded decseq_def] allI impI proc_source.finite_measure_mono)
apply (simp_all add: Union_add_subset)
done
qed
then obtain L where lim_B: "(λn. measure source (B n)) ⇢ L"
unfolding convergent_def by auto
then have "L ≥ 0"
by (simp add: LIMSEQ_le_const)
moreover have "L ≤ 0"
using measure_B_le by (simp add: LIMSEQ_le[OF lim_B lim_A])
ultimately show ?thesis
using lim_B by simp
qed
lemma N_null: "N ∈ null_sets source"
proof -
have "(λn. measure source (B n)) ⇢ measure source N"
apply (rule proc_source.finite_Lim_measure_decseq)
using A_measurable apply fast
apply (intro monotoneI, simp add: Union_add_subset)
done
then have "measure source N = 0"
using lim_B LIMSEQ_unique by blast
then show ?thesis
by (auto simp add: emeasure_eq_ennreal_measure)
qed
lemma notin_N_index:
assumes "ω ∈ space source - N"
obtains n⇩0 where "ω ∉ (⋃n. A (n + n⇩0))"
using assms by blast
context
fixes ω
assumes ω: "ω ∈ space source - N"
begin
definition "n⇩0 ≡ SOME m. ω ∉ (⋃n. A (n + m)) ∧ m > 0"
lemma
shows n_zero: "ω ∉ (⋃n. A (n + n⇩0))"
and n_zero_nonzero: "n⇩0 > 0"
proof -
have "∃m. ω ∉ (⋃n. A (n + m))"
using ω by blast
then have "∃m. ω ∉ (⋃n. A (n + m)) ∧ m > 0"
by (metis (no_types, lifting) UNIV_I UN_iff add.comm_neutral not_gr_zero zero_less_Suc)
then have "ω ∉ (⋃n. A (n + n⇩0)) ∧ n⇩0 > 0"
unfolding n⇩0_def by (rule someI_ex)
then show "ω ∉ (⋃n. A (n + n⇩0))" "n⇩0 > 0"
by blast+
qed
lemma nzero_ge: "⋀n. n ≥ n⇩0 ⟹ 2^n * T ≥ 1"
proof (rule ccontr)
fix n assume "n⇩0 ≤ n" "¬ 1 ≤ 2 ^ n * T"
then have "A n = space source"
unfolding A_def by simp
then have "space source ⊆ (⋃m. A (m + n))"
by (smt (verit, del_insts) UNIV_I UN_upper add_0)
also have "(⋃m. A (m + n)) ⊆ (⋃m. A (m + n⇩0))"
by (simp add: Union_add_subset ‹n⇩0 ≤ n›)
finally show False
using ω n_zero by blast
qed
lemma omega_notin: "⋀n. n ≥ n⇩0 ⟹ ω ∉ A n"
by (metis n_zero UNIV_I UN_iff add.commute le_Suc_ex)
text ‹Klenke 21.7›
lemma X_dyadic_incr:
assumes "k ∈ {1..⌊2^n * T⌋}" "n ≥ n⇩0"
shows "dist (X ((real_of_int k-1)/2^n) ω) (X (real_of_int k/2^n) ω) < 2 powr (- γ * n)"
proof -
have "finite {1..⌊2^n * T⌋}" "{1..⌊2^n * T⌋} ≠ {}"
using assms nzero_ge by blast+
then have fin_nonempty: "finite {dist (X (real_of_int (k - 1) * 2 powr - real n) ω) (X (real_of_int k * 2 powr - real n) ω) |k.
k ∈ {1..⌊2 ^ n * T⌋}}" "{dist (X (real_of_int (k - 1) * 2 powr - real n) ω) (X (real_of_int k * 2 powr - real n) ω) |k.
k ∈ {1..⌊2 ^ n * T⌋}} ≠ {}"
by fastforce+
have "2 powr (- γ * real n)
> Max {dist (X (real_of_int (k - 1) * 2 powr - real n) ω) (X (real_of_int k * 2 powr - real n) ω) |k.
k ∈ {1..⌊2 ^ n * T⌋}}"
using nzero_ge[OF assms(2)] omega_notin[OF assms(2)] ω A_def by auto
then have "2 powr (- γ * real n) > dist (X (real_of_int (k - 1) * 2 powr - real n) ω) (X (real_of_int k * 2 powr - real n) ω)"
using Max_less_iff[OF fin_nonempty] assms(1) by blast
then show ?thesis
by (simp, smt (verit, ccfv_threshold) divide_powr_uminus powr_realpow)
qed
text ‹ Klenke (21.8) ›
lemma dist_dyadic_mn:
assumes mn: "n⇩0 ≤ n" "n ≤ m"
and t_dyadic: "t ∈ dyadic_interval_step m 0 T"
and u_dyadic_n: "u ∈ dyadic_interval_step n 0 T"
and ut: "u ≤ t" "t - u < 2/2^n"
shows "dist (X u ω) (X t ω) ≤ 2 powr (- γ * n) / (1 - 2 powr - γ)"
proof -
have u_dyadic: "u ∈ dyadic_interval_step m 0 T"
using mn(2) dyadic_interval_step_subset u_dyadic_n by fast
have "0 < n"
using mn(1) n_zero_nonzero by linarith
then have "t - u < 1"
by (smt (verit) ut(2) One_nat_def Suc_le_eq divide_le_eq_1_pos power_increasing power_one_right)
obtain b_tu k_tu where tu_exp: "dyadic_expansion (t-u) m b_tu k_tu"
using dyadic_expansion_ex dyadic_interval_minus[OF u_dyadic t_dyadic ‹u ≤ t›] by blast
then have "k_tu = 0"
using dyadic_expansion_floor[OF tu_exp] ‹t - u < 1› ‹u ≤ t› by linarith
have b_tu_0_1: "b_tu ! i ∈ {0,1}" if "i ∈ {0..m-1}" for i
using dyadic_expansionD(1,2)[OF tu_exp] that
by (metis Suc_pred' ‹0 < n› atLeastAtMost_iff le_imp_less_Suc le_trans less_eq_Suc_le mn(2) nth_mem subsetD)
text ‹ And hence $b_i (t - u) = b_i (s-u) = 0$ for $i < n$. ›
have b_t_zero: "b_tu ! i = 0" if "i+1 < n" for i
proof (rule ccontr)
assume "b_tu ! i ≠ 0"
then have "b_tu ! i = 1"
by (smt (verit) add_lessD1 dyadic_expansionD(1,2) insertE mn(2) nth_mem order_less_le_trans
singletonD subset_iff that tu_exp)
then have "t - u ≥ (real_of_int 0) + 1/2^(i+1)"
apply (intro dyadic_expansion_nth_geq)
using tu_exp ‹k_tu = 0› apply blast
apply (metis One_nat_def Suc_eq_plus1 Suc_le_mono atLeastAtMost_iff le_trans less_Suc_eq linorder_not_le mn(2) nat_less_le that zero_order(1))
apply simp
done
moreover have "1/2^(n-1) ≤ 1/(2^(i+1) :: real)"
apply (intro divide_left_mono)
apply (metis that Suc_eq_plus1 Suc_leI less_diff_conv power_increasing power_one_right two_realpow_ge_one)
by simp_all
ultimately have "t - u ≥ 1 / 2 ^ (n - 1)"
by linarith
then show False
using ‹t - u < 2/2^n› ‹n > 0› by (auto simp: power_diff)
qed
define t' where "t' ≡ λl. (u + (∑i = n..l. b_tu!(i-1) / 2 ^ i))"
have "t' (n-1) = u"
unfolding t'_def using ‹n > 0› by simp
have "t' m = t"
proof -
have b_tu_eq_0: "(∑ i = 1..n-1. b_tu!(i-1) / 2 ^ i) = 0"
by (subst sum_nonneg_eq_0_iff, auto simp add: sum_nonneg_eq_0_iff b_t_zero)
have "t - u = (∑i = 1..m. b_tu!(i-1) / 2 ^ i)"
using tu_exp[THEN dyadic_expansionD(3)] ‹k_tu = 0› by linarith
also have "... = (∑i = 1..n-1. b_tu!(i-1) / 2 ^ i) + (∑i = n..m. b_tu!(i-1) / 2 ^ i)"
proof -
have 1: "{1..m} = {1..n-1} ∪ {n..m}"
using ‹n > 0› mn(2) by fastforce
show ?thesis
by (subst 1, auto simp: sum.union_disjoint)
qed
finally have "t-u = (∑i = n..m. b_tu!(i-1) / 2 ^ i)"
using b_tu_eq_0 by algebra
then show ?thesis
unfolding t'_def by argo
qed
have t_pos: "t' l ≥ 0" if ‹l ∈ {n..m}› for l
unfolding t'_def apply (rule add_nonneg_nonneg)
using dyadic_step_geq u_dyadic apply blast
by (simp add: sum_nonneg)
have t'_Suc: "t' (Suc l) = t' l + b_tu ! l / 2^(Suc l)" if "l ∈{n-1..m-1}" for l
unfolding t'_def by (simp add: b_t_zero)
have le_add_diff: "b ≤ c - a ⟹ a + b ≤ c" for a b c :: real
by argo
have t'_leq: "t' l ≤ t" if ‹l ∈ {n..m}› for l
unfolding t'_def apply (intro le_add_diff)
apply (simp only: tu_exp[THEN dyadic_expansionD(3)] ‹k_tu = 0› of_int_0 add_0)
apply (rule sum_mono2)
using ‹0 < n› that by auto
have t'_dyadic: "t' l ∈ dyadic_interval_step l 0 T" if "l ∈ {n..m}" for l
using that
proof (induct l rule: atLeastAtMost_induct)
case base
consider "b_tu ! (n - 1) = 0" | "b_tu ! (n-1) = 1"
using dyadic_expansion_frac_range[OF tu_exp(1), of n] ‹0 < n› mn(2) by auto
then show ?case
apply cases
using ‹0 < n› t'_def apply simp
using u_dyadic_n apply blast
apply (rule dyadic_interval_step_memI)
apply (simp add: t'_def)
using u_dyadic_n
apply (metis add_divide_distrib dyadic_interval_step_iff of_int_1 of_int_add)
apply (simp add: mn(2) t_pos)
by (meson t'_leq[OF that] atLeastAtMost_iff dual_order.refl dual_order.trans dyadic_step_leq mn(2) t'_leq t_dyadic)
next
case (Suc l)
then have t'_dyadic_Suc: "t' l ∈ dyadic_interval_step (Suc l) 0 T"
using dyadic_interval_step_mono le_SucI by blast
from Suc have "l ∈ {0..m-1}"
by force
then consider "b_tu!l = 0" | "b_tu!l = 1"
using b_tu_0_1 by fastforce
then obtain k :: int where k: "t' l + (b_tu ! l) / 2 ^ Suc l = k / 2 ^ Suc l"
apply cases
subgoal using dyadic_interval_step_iff t'_dyadic_Suc by auto
by (metis add.commute add_divide_distrib dyadic_as_natural of_int_of_nat_eq of_nat_1 of_nat_Suc t'_dyadic_Suc)
have "t' (Suc l) ≤ t"
by (meson Suc atLeastAtMost_iff le_SucI less_eq_Suc_le t'_leq)
with Suc(1,2) show ?case
apply (subst t'_Suc)
apply (metis Suc_leD Suc_pred' ‹0 < n› atLeastAtMost_iff less_Suc_eq_le mn(2) order_less_le_trans)
apply (intro dyadic_interval_step_memI)
apply (rule exI[where x=k])
using k apply blast
using dyadic_step_geq t'_dyadic_Suc apply force
apply (subst t'_Suc[symmetric])
apply force
using dyadic_step_leq order_trans t_dyadic by blast
qed
have "dist (X (t' (n-1)) ω) (X (t' m) ω) ≤ (∑ l=Suc (n-1)..m. dist (X (t' l) ω) (X (t' (l-1)) ω))"
apply (rule triangle_ineq_sum)
using diff_le_self dual_order.trans mn(2) by blast
also have "... = (∑ l=n..m. dist (X (t' l) ω) (X (t' (l-1)) ω))"
using Suc_diff_1 ‹0 < n› by presburger
also have "... ≤ (∑ l=n..m. 2 powr (-γ * l))"
proof (rule sum_mono)
fix l assume *: "l ∈ {n..m}"
then have "l ∈ {n-1..m}"
by (metis atLeastAtMost_iff less_imp_diff_less linorder_not_less order_le_less)
from * have [simp]: "0 < l"
using ‹0 < n› by fastforce
from ‹l ∈ {n..m}› have "b_tu ! (l-1) ∈ {0, 1}"
apply (intro dyadic_expansion_frac_range)
apply (rule tu_exp)
using ‹n > 0› by simp
then consider (zero) "b_tu ! (l-1) = 0" | (one) "b_tu ! (l-1) = 1"
by fast
then show "dist (X (t' l) ω) (X (t' (l - 1)) ω) ≤ 2 powr (- γ * l)"
proof cases
case zero
have "{n..l} = insert l {n..l-1}"
using ‹0 < n› ‹l ∈ {n..m}› by auto
then have "sum f {n..l} = sum f {n..l-1} + f l" for f :: "nat ⇒ real"
by (metis (no_types, opaque_lifting) Groups.add_ac(3) Suc_le_eq Suc_pred' ‹0 < n› atLeastAtMost_iff finite_atLeastAtMost group_cancel.rule0 linorder_not_le nle_le sum.insert zero_diff zero_less_diff)
then have "t' l = t' (l-1)"
unfolding t'_def using zero by simp
then show ?thesis
by simp
next
case one
then have [simp]: "b_tu ! (l - Suc 0) = 1"
by simp
obtain k where k: "k ≥ 0" "k ≤ ⌊2^l * T⌋" "t' l = k/2^l"
using t'_dyadic ‹l ∈ {n..m}› dyadic_interval_step_iff by force
have "t' (l-1) ∈ dyadic_interval_step l 0 T"
proof (cases "l = n")
case True
then have "t' (l-1) = u"
using ‹t' (n - 1) = u› by presburger
then show "t' (l-1) ∈ dyadic_interval_step l 0 T"
using True u_dyadic_n by blast
next
case False
then have "l-1 ∈ {n..m}"
by (metis "*" Suc_eq_plus1 add_leD2 atLeastAtMost_iff diff_le_self dual_order.trans
le_antisym not_less_eq_eq ordered_cancel_comm_monoid_diff_class.le_diff_conv2)
then show "t' (l-1) ∈ dyadic_interval_step l 0 T"
using t'_dyadic dyadic_interval_step_subset diff_le_self by blast
qed
then obtain k' where k': "k' ≥ 0" "k' ≤ ⌊2^l * T⌋" "t' (l-1) = k'/2^l"
using dyadic_interval_step_iff by auto
then have t'_k: "t' (l-1) = (k-1) / 2^l"
proof -
have "t' l = t' (l-1) + real (b_tu ! (l-1)) / 2 ^ l"
using t'_Suc[of "l-1"] apply simp
using "*" diff_le_mono by presburger
then have "k / 2^l = t' (l-1) + 1/2^l"
by (simp add: k(3))
then show ?thesis
by (simp add: diff_divide_distrib)
qed
then have "k ≥ 1"
using k'(1) k'(3) by auto
then show ?thesis
apply (simp only: k(3) t'_k)
apply (subst dist_commute)
apply (intro less_imp_le)
apply (simp only: of_int_diff of_int_1)
apply (rule X_dyadic_incr[of k l])
using k(2) apply presburger
using ‹l ∈ {n..m}› mn(1) by auto
qed
qed
also have "... = (∑ l=n..m. (2 powr -γ) ^ l)"
apply (intro sum.cong; simp add: field_simps)
by (smt (verit, ccfv_SIG) powr_powr[symmetric] mult_minus_left powr_gt_zero powr_realpow)
also have "... ≤ 2 powr (-γ * n) / (1 - 2 powr -γ)"
apply (subst sum_gp)
using ‹m ≥ n› apply (simp add: field_simps)
apply safe
using gamma_gt_0 apply force
apply (rule divide_right_mono)
apply (simp only: minus_mult_left)
apply (subst powr_powr[symmetric])
apply (subst powr_realpow[symmetric]; simp)+
by (metis diff_ge_0_iff_ge gamma_gt_0 less_eq_real_def
neg_le_0_iff_le one_le_numeral powr_mono powr_nonneg_iff powr_zero_eq_one)
finally show "dist (X u ω) (X t ω) ≤ 2 powr (- γ * real n) / (1 - 2 powr - γ)"
using ‹t' (n - 1) = u› ‹t' m = t› by blast
qed
lemma dist_dyadic_fixed:
assumes mn: "n⇩0 ≤ n" "n ≤ m"
and s_dyadic: "s ∈ dyadic_interval_step m 0 T"
and t_dyadic: "t ∈ dyadic_interval_step m 0 T"
and st: "s ≤ t" "t - s ≤ 1/2^n"
shows "dist (X t ω) (X s ω) ≤ 2 * 2 powr (- γ * n) / (1 - 2 powr - γ)"
proof -
have "n > 0"
using mn(1) n_zero_nonzero by linarith
define u where "u ≡ ⌊2^n * s⌋ / 2^n"
have "u = Max (dyadic_interval_step n 0 s)"
unfolding u_def using dyadic_interval_step_Max[symmetric] dyadic_step_geq[OF s_dyadic]
by blast
then have u_dyadic_n: "u ∈ dyadic_interval_step n 0 T"
using dyadic_interval_step_mem dyadic_step_geq dyadic_step_leq s_dyadic u_def by force
text ‹ Then, $u \leq s < u + 2^{-n}$ and $u \leq t < u + 2^{1-n}$›
have "u ≤ s"
unfolding u_def using floor_pow2_leq by blast
have "s < u + 1/2^n"
unfolding u_def apply (simp add: field_simps)
using floor_le_iff apply linarith
done
then have "s - u < 2/2^n"
using ‹u ≤ s› by auto
then have dist_us: "dist (X u ω) (X s ω) ≤ 2 powr (- γ * real n) / (1 - 2 powr - γ)"
by (rule dist_dyadic_mn[OF mn s_dyadic u_dyadic_n ‹u ≤ s›])
have "u ≤ t"
using ‹u ≤ s› st(1) by linarith
have "t < u + 2/2^n"
using ‹s <u + 1/2^n› st(2) by force
then have "t - u < 2/2^n"
by force
then have "dist (X u ω) (X t ω) ≤ 2 powr (- γ * real n) / (1 - 2 powr - γ)"
by (rule dist_dyadic_mn[OF mn t_dyadic u_dyadic_n ‹u ≤ t›])
then show "dist (X t ω) (X s ω) ≤ 2 * (2 powr (-γ * n)) / (1 - 2 powr - γ)"
using dist_us by metric
qed
definition "C⇩0 ≡ 2 * 2 powr γ / (1 - 2 powr - γ)"
lemma C_zero_ge[simp]: "C⇩0 > 0"
by (smt (verit, ccfv_SIG) C⇩0_def divide_pos_pos gamma_gt_0 powr_eq_one_iff powr_less_mono)
text ‹ Klenke (21.9) ›
text ‹ Let $s, t \in D$ with $|s-t| \leq \frac{1}{2^n_0}$. By choosing the minimal $n \geq n_0$ such
that $|t-s| \geq 2^{-n}$, we obtain by @{thm dist_dyadic_fixed}:
\[|X_t(\omega) - X_s(\omega)| \leq C_0 |t-s|^\gamma\]›
lemma dist_dyadic:
assumes t: "t ∈ dyadic_interval 0 T"
and s: "s ∈ dyadic_interval 0 T"
and st_dist: "dist t s ≤ 1 / 2 ^ n⇩0"
shows "dist (X t ω) (X s ω) ≤ C⇩0 * (dist t s) powr γ"
proof (cases "s = t")
case True
then show ?thesis by simp
next
case False
define n where "n ≡ LEAST n. dist t s ≥ 1/2^n"
have "dist t s > 0"
using False by simp
then have "∃n. dist t s ≥ 1 / 2^n"
by (metis less_eq_real_def one_less_numeral_iff power_one_over reals_power_lt_ex semiring_norm(76))
then have "dist t s ≥ 1/2^n"
unfolding n_def by (meson LeastI_ex)
then have "n ≥ n⇩0"
using order_trans[OF ‹dist t s ≥ 1/2^n› st_dist]
by (simp add: field_simps)
have "dist t s ≤ 1/2^(n-1)"
proof -
have "n-1 < (LEAST n. dist t s ≥ 1/2^n)"
using ‹n⇩0 ≤ n› n_zero_nonzero n_def by fastforce
then have "¬ (dist t s ≥ 1/2^(n-1))"
by (rule not_less_Least)
then show ?thesis
by auto
qed
obtain m where m: "m ≥ n" "s ∈ dyadic_interval_step m 0 T" "t ∈ dyadic_interval_step m 0 T"
by (metis dyadic_interval_step_mono linorder_not_le mem_dyadic_interval order.asym s t)
from ‹n ≥ n⇩0› consider (eq) "n = n⇩0" | (gt) "n > n⇩0"
using less_eq_real_def by linarith
then show ?thesis
proof cases
case eq
consider "t ≤ s" | "s ≤ t"
by fastforce
then have "dist (X t ω) (X s ω) ≤ 2 * 2 powr (- γ * n) / (1 - 2 powr - γ)"
apply cases
apply (subst dist_commute)
apply (rule dist_dyadic_fixed[OF ‹n ≥ n⇩0› m(1,3,2)])
apply simp
using dist_real_def eq st_dist apply force
apply (rule dist_dyadic_fixed[OF ‹n ≥ n⇩0› m])
apply simp
using dist_real_def eq st_dist apply force
done
also have "... ≤ C⇩0 * 2 powr (- γ * n)"
unfolding C⇩0_def apply (simp add: field_simps)
apply (intro divide_right_mono mult_left_mono)
apply (simp add: less_eq_real_def)
apply simp
by (smt (verit) gamma_gt_0 powr_le_cancel_iff powr_zero_eq_one)
also have "... = C⇩0 * (1/2^n) powr γ"
by (smt (verit, del_insts) powr_minus_divide powr_powr powr_powr_swap powr_realpow)
also have "... ≤ C⇩0 * (dist t s) powr γ"
using ‹1 / 2 ^ n ≤ dist t s› eq st_dist by auto
finally show ?thesis .
next
case gt
consider "t ≤ s" | "s ≤ t"
by fastforce
then have "dist (X t ω) (X s ω) ≤ 2 * 2 powr (- γ * (n-1)) / (1 - 2 powr - γ)"
apply cases
apply (subst dist_commute)
apply (rule dist_dyadic_fixed[where m=m])
prefer 7 apply (rule dist_dyadic_fixed[where m=m])
using gt m apply simp_all
using ‹dist t s ≤ 1 / 2 ^ (n - 1)› dist_real_def apply force+
done
also have "... ≤ C⇩0 * 2 powr (- γ * n)"
unfolding C⇩0_def apply simp
apply (intro divide_right_mono)
apply (simp add: powr_add[symmetric])
apply (metis One_nat_def Suc_leI dual_order.refl gt less_imp_Suc_add minus_diff_eq mult.right_neutral of_nat_1 of_nat_diff right_diff_distrib zero_less_Suc)
by (metis gamma_gt_0 ge_iff_diff_ge_0 less_eq_real_def neg_le_0_iff_le one_le_numeral powr_mono powr_zero_eq_one zero_neq_numeral)
also have "... = C⇩0 * (1/2^n) powr γ"
by (smt (verit, best) powr_minus_divide powr_powr powr_powr_swap powr_realpow)
also have "C⇩0 * (1/2^n) powr γ ≤ C⇩0 * dist t s powr γ"
apply (rule mult_left_mono)
using ‹1 / 2 ^ n ≤ dist t s› less_eq_real_def powr_mono2 apply force
using C_zero_ge by linarith
finally show ?thesis .
qed
qed
definition "K ≡ C⇩0 * (2^nat ⌈2^n⇩0 * T⌉) powr (1 - γ)"
lemma C⇩0_le_K: "C⇩0 ≤ K"
unfolding K_def using nzero_ge[of n⇩0] ge_one_powr_ge_zero by force
lemma K_pos: "0 < K"
using C⇩0_le_K C_zero_ge by linarith
text ‹ Klenke (21.10) ›
lemma X_dyadic_le_K':
assumes dyadic: "s ∈ dyadic_interval 0 T" "t ∈ dyadic_interval 0 T"
and st: "s ≤ t"
shows "dist (X s ω) (X t ω) ≤ K * dist s t powr γ"
proof (cases "dist s t ≤ 1 / 2^n⇩0")
case True
then have "C⇩0 * dist t s powr γ ≤ K * dist t s powr γ"
by (simp add: C⇩0_le_K powr_def)
then show ?thesis
using dist_dyadic[OF assms(1,2) True] by (simp add: dist_commute)
next
case False
define n :: nat where "n ≡ nat ⌈2^n⇩0 * T⌉"
have "dist s t / n ≤ 1/2^n⇩0"
apply (simp add: n_def field_simps)
by (smt (verit, best) dyadic dist_real_def divide_le_eq_1 dyadics_geq dyadics_leq
mem_dyadic_interval mult_mono of_nat_eq_0_iff of_nat_le_0_iff real_nat_ceiling_ge zero_le_power)
have dist_st: "dist s t / 2^n ≤ 1/2^n⇩0"
apply (rule order_trans[where y="dist s t / n"])
apply (rule divide_left_mono; simp?)
apply (simp add: n_def zero_le_T)
apply (fact ‹dist s t / n ≤ 1/2^n⇩0›)
done
define f where "f ≡ λi::nat. (s + (t-s) * i/2^n)"
have f_inc: "f k = f (k - 1) + (t - s) / 2^n" if "k > 0" for k
proof -
have "f (Suc k) = f k + (t - s) / 2^n" for k
by (simp add: f_def field_simps)
then show ?thesis
by (metis Suc_pred' that)
qed
have f_inc_le: "dist (f i) (f (i - 1)) ≤ 1 / 2 ^ n⇩0" for i
proof (cases "i=0")
case True
then show ?thesis by simp
next
case False
then show ?thesis
using f_inc dist_real_def dist_st st by auto
qed
have f_ge_s: "⋀i. i ≤ 2^n ⟹ f i ≥ s"
unfolding f_def using st by auto
have f_le_t: "⋀i. i ≤ 2^n ⟹ f i ≤ t"
by (smt (verit, del_insts) f_def st divide_le_eq_1 mult_less_cancel_left1 of_nat_1 of_nat_add
of_nat_le_iff of_nat_power one_add_one times_divide_eq_right zero_less_power)
have f_dyadic: "f i ∈ dyadic_interval 0 T" if "i ≤ 2^n" for i
proof (rule mem_dyadic_intervalI)
have "f i ≤ T"
proof -
have "f i ≤ s + t - s"
using f_le_t[OF that] by simp
also have "... ≤ T"
using dyadic(2) dyadics_leq by simp
finally show ?thesis .
qed
obtain m where "s ∈ dyadic_interval_step m 0 T" "t ∈ dyadic_interval_step m 0 T"
by (metis dyadic dyadic_interval_step_mono mem_dyadic_interval nle_le)
then obtain ks kt where ks: "s = real ks / 2^m" and kt: "t = real kt / 2^m"
using dyadic_as_natural by metis
then have "ks ≤ kt"
using st by (simp add: divide_le_cancel)
from ks kt have "ks = 2^m * s" "kt = 2^m * t"
by simp_all
from ks kt have "f i = (ks / 2^m) + (kt / 2^m - ks / 2^m) * i / 2^n"
unfolding f_def by auto
also have "... = (ks * (2^n - i) + kt * i) / 2^(m+n)"
using ‹ks ≤ kt› apply (simp add: right_diff_distrib field_simps power_add)
by (metis distrib_left le_add_diff_inverse mult.commute of_nat_add of_nat_numeral of_nat_power that)
finally have "f i ∈ dyadic_interval_step (m+n) 0 T"
apply (intro dyadic_interval_step_memI)
apply (rule exI[where x="int (ks * (2^n - i) + kt * i)"])
prefer 3 apply (rule ‹f i ≤ T›)
by simp_all
then show "∃n. f i ∈ dyadic_interval_step n 0 T"
by blast
qed
have "dist (X s ω) (X t ω) ≤ (∑ i=1..2^n. dist (X (f i) ω) (X (f (i-1)) ω))"
proof -
have "f 0 = s"
unfolding f_def by (simp add: field_simps)
moreover have "f (2^n) = t"
unfolding f_def by (simp add: field_simps)
moreover have "dist (X (f 0) ω) (X (f (2^n)) ω) ≤ (∑ i=Suc 0..2^n. dist (X (f i) ω) (X (f (i-1)) ω))"
by (rule triangle_ineq_sum, simp)
ultimately show ?thesis
by simp
qed
also have "... ≤ (∑ i=1..2^n::nat. C⇩0 * (dist (f i) (f (i-1))) powr γ)"
apply (rule sum_mono)
apply (intro dist_dyadic f_dyadic)
apply fastforce
apply fastforce
using f_inc_le .
also have "... ≤ (∑ i=1..2^n::nat. C⇩0 * (dist t s / 2^n) powr γ)"
apply (rule sum_mono)
using f_inc by (simp add: dist_real_def)
also have "... ≤ 2^n * C⇩0 * (dist t s / 2^n) powr γ"
by (subst sum_constant, force)
also have "... ≤ K * dist t s powr γ"
unfolding K_def n_def apply (simp add: powr_divide field_simps)
apply (rule mult_left_mono)
apply (smt (verit, ccfv_threshold) powr_add powr_one zero_le_power)
by simp
finally show ?thesis
by (metis dist_commute)
qed
lemma X_dyadic_le_K:
assumes "s ∈ dyadic_interval 0 T"
and "t ∈ dyadic_interval 0 T"
shows "dist (X s ω) (X t ω) ≤ K * dist s t powr γ"
by (metis nle_le assms X_dyadic_le_K' dist_commute)
corollary holder_dyadic: "γ-holder_on (dyadic_interval 0 T) (λt. X t ω)"
apply (intro holder_onI[OF gamma_0_1] exI[where x=K])
using K_pos X_dyadic_le_K by force
lemma uniformly_continuous_dyadic: "uniformly_continuous_on (dyadic_interval 0 T) (λt. X t ω)"
using holder_dyadic by (fact holder_uniform_continuous)
lemma Lim_exists: "∃L. ((λs. X s ω) ⤏ L) (at t within (dyadic_interval 0 T))"
if "t ∈ {0..T}"
apply (rule uniformly_continuous_on_extension_at_closure[where x = t])
using that dyadic_interval_dense uniformly_continuous_dyadic apply fast
using that apply (simp add: dyadic_interval_dense)
by blast
lemma Lim_unique: "∃!L. ((λs. X s ω) ⤏ L) (at t within (dyadic_interval 0 T))"
if "t ∈ {0..T}"
by (metis that Lim_exists dyadic_interval_islimpt tendsto_Lim trivial_limit_within zero_le_T)
definition "L ≡ (λt. (Lim (at t within dyadic_interval 0 T) (λs. X s ω)))"
lemma X_tendsto_L:
assumes "t ∈ {0..T}"
shows "((λs. X s ω) ⤏ L t) (at t within (dyadic_interval 0 T))"
proof -
have "at t within dyadic_interval 0 T ≠ ⊥"
by (simp add: trivial_limit_within dyadic_interval_islimpt[OF zero_le_T assms])
moreover obtain L' where L': "((λs. X s ω) ⤏ L') (at t within (dyadic_interval 0 T))"
using Lim_exists[OF assms] by blast
ultimately have "L t = L'"
unfolding L_def by (rule tendsto_Lim)
then show ?thesis
using L' by blast
qed
lemma L_dist_K:
assumes s: "s ∈ {0..T}"
and t: "t ∈ {0..T}"
shows "dist (L s) (L t) ≤ K * dist s t powr γ"
proof (cases "s = t")
case True
then show ?thesis by simp
next
case False
let ?F = "λx. at x within dyadic_interval 0 T"
have "(?F s ×⇩F ?F t) ≠ ⊥"
by (meson dyadic_interval_islimpt prod_filter_eq_bot s t trivial_limit_within zero_le_T)
moreover have "((λx. K * dist (fst x) (snd x) powr γ) ⤏ K * dist s t powr γ) (?F s ×⇩F ?F t)"
apply (rule tendsto_mult_left)
apply (rule tendsto_powr)
using tendsto_dist_prod apply blast
apply simp
using False by simp
moreover have "((λx. dist (X (fst x) ω) (X (snd x) ω)) ⤏ dist (L s) (L t)) (?F s ×⇩F ?F t)"
using X_tendsto_L t s tendsto_dist_prod by blast
moreover have "∀⇩F x in ?F s ×⇩F ?F t. dist (process X (fst x) ω) (process X (snd x) ω)
≤ K * dist (fst x) (snd x) powr γ"
apply (rule eventually_prodI'[where P = "λx. x ∈ dyadic_interval 0 T"
and Q = "λx. x ∈ dyadic_interval 0 T"])
using eventually_at_topological apply blast
using eventually_at_topological apply blast
using X_dyadic_le_K by simp
ultimately show ?thesis
by (rule tendsto_le)
qed
corollary L_holder: "γ-holder_on {0..T} L"
using K_pos L_dist_K by (auto intro!: holder_onI[OF gamma_0_1] exI[where x=K])
corollary L_local_holder: "local_holder_on γ {0..T} L"
using holder_implies_local_holder[OF L_holder] by blast
lemma X_dyadic_eq_L:
assumes "t ∈ dyadic_interval 0 T"
shows "X t ω = L t"
proof -
have "((λx. X x ω) ⤏ X t ω) (at t within dyadic_interval 0 T)"
using continuous_within[symmetric] uniformly_continuous_dyadic uniformly_continuous_imp_continuous
continuous_on_eq_continuous_within assms by fast
then show ?thesis
by (metis L_def assms dyadic_interval_islimpt dyadic_interval_subset_interval subsetD
tendsto_Lim trivial_limit_within zero_le_T)
qed
end
definition default :: 'b where "default = (SOME x. True)"
definition X_tilde :: "real ⇒ 'a ⇒ 'b" where
"X_tilde ≡ (λt ω. if ω ∈ N then default else (Lim (at t within dyadic_interval 0 T) (λs. X s ω)))"
lemma X_tilde_not_N_Lim:
assumes "ω ∈ space source - N"
shows "X_tilde t ω = Lim (at t within dyadic_interval 0 T) (λs. X s ω)"
using assms X_tilde_def by auto
lemma X_tilde_not_N_L:
assumes "ω ∈ space source - N"
shows "X_tilde t ω = L ω t"
using assms X_tilde_def L_def[OF assms] by auto
lemma local_holder_X_tilde: "local_holder_on γ {0..T} (λt. X_tilde t ω)"
if "ω ∈ space source" for ω
proof (cases "ω ∈ N")
case True
then show ?thesis
unfolding X_tilde_def using local_holder_const by fastforce
next
case False
then have 1: "ω ∈ space source - N"
using that by blast
show ?thesis
using L_local_holder[OF 1] X_tilde_not_N_L[OF 1]
by (simp only: False if_False)
qed
corollary X_tilde_eq_L_AE: "AE ω in source. X_tilde t ω = L ω t"
apply (rule AE_I[where N=N])
apply (smt (verit, del_insts) X_tilde_def Diff_iff L_def mem_Collect_eq subsetI)
using N_null apply blast+
done
corollary X_tilde_eq_Lim_AE:
"AE ω in source. X_tilde t ω = Lim (at t within dyadic_interval 0 T) (λs. X s ω)"
apply (rule AE_I[where N=N])
apply (smt (verit, del_insts) X_tilde_def Diff_iff L_def mem_Collect_eq subsetI)
using N_null apply blast+
done
lemma X_tilde_tendsto_AE: "t ∈ {0..T} ⟹ tendsto_AE source X (X_tilde t) (at t within dyadic_interval 0 T)"
apply (unfold tendsto_AE_def)
apply (rule AE_I3[where N=N])
apply (subst X_tilde_not_N_Lim, argo)
unfolding t2_space_class.Lim_def apply (rule the1I2)
using Lim_unique apply presburger
apply blast
using N_null by blast
end
context Kolmogorov_Chentsov_finite
begin
text ‹ By (21.5) @{thm conv_in_prob_finite} and (21.11) @{thm L_def}, $P[X \neq \tilde{X}] = 0$›
lemma X_tilde_measurable[measurable]:
assumes "t ∈ {0..T}"
shows "X_tilde t ∈ borel_measurable source"
proof -
let ?Lim = "(λω. Lim (at t within dyadic_interval 0 T) (λs. process X s ω))"
have "?Lim ∈ borel_measurable (restrict_space source (space source - N))"
unfolding X_tilde_def apply measurable
using measurable_id measurable_restrict_space1 apply blast
using assms Lim_exists space_restrict_space apply simp
using assms dyadic_interval_islimpt trivial_limit_within zero_le_T by blast
then have "(λω. if ω ∈ space source - N then ?Lim ω else default) ∈ borel_measurable source"
by (subst measurable_restrict_space_iff[symmetric]; simp)
then show ?thesis
apply (subst measurable_cong[where g="(λω. if ω ∈ space source - N then ?Lim ω else default)"])
unfolding X_tilde_def by auto
qed
lemma X_eq_X_tilde_AE: "AE ω in source. X t ω = X_tilde t ω" if "t ∈ {0..T}" for t
apply (rule sigma_finite_measure.tendsto_measure_at_within_eq_AE[where f="process X" and S="dyadic_interval 0 T"])
using proc_source.sigma_finite_measure_axioms apply blast
using X_borel_measurable apply blast
apply measurable
using X_tilde_def apply simp
using that apply simp
using tendsto_measure_mono[OF at_le[OF dyadic_interval_subset_interval] conv_in_prob_finite] that
apply force
using X_borel_measurable X_tilde_measurable X_tilde_tendsto_AE measure_conv_imp_AE_at_within that apply blast
using dyadic_interval_islimpt that trivial_limit_within zero_le_T by blast
lemma X_tilde_modification: "modification (restrict_index X {0..T})
(prob_space.process_of source (proc_target X) {0..T} X_tilde default)"
apply (intro modificationI compatibleI)
apply simp_all
apply (subst restrict_index_source)
apply (auto simp: X_eq_X_tilde_AE)
done
end
text ‹ We have now shown that we can construct a modification of $X$ for any interval $\{0..T\}$. We want
to extend this result to construct a modification on the interval $\{0..\}$ - this can be constructed
by gluing together all modifications with natural-valued T which results in a countable union of
modifications, which itself is a modification. ›
context Kolmogorov_Chentsov
begin
lemma Kolmogorov_Chentsov_finite: "T > 0 ⟹ Kolmogorov_Chentsov_finite X a b C γ T"
by (simp add: Kolmogorov_Chentsov_axioms Kolmogorov_Chentsov_finite.intro Kolmogorov_Chentsov_finite_axioms_def)
definition "Mod ≡ λT. SOME Y. modification (restrict_index X {0..T}) Y ∧
(∀x∈space source. local_holder_on γ {0..T} (λt. Y t x))"
lemma Mod: "modification (restrict_index X {0..T}) (Mod T)"
"(∀x∈space source. local_holder_on γ {0..T} (λt. (Mod T) t x)) " if "0 < T" for T
proof -
interpret Kolmogorov_Chentsov_finite X a b C γ T
using that by (simp add: Kolmogorov_Chentsov_finite)
have "modification (restrict_index X {0..T}) (Mod T) ∧
(∀x∈space source. local_holder_on γ {0..T} (λt. (Mod T) t x))"
unfolding Mod_def apply (rule someI_ex)
apply (rule exI[where x="prob_space.process_of source (proc_target X) {0..T} X_tilde default"])
apply safe
apply (fact X_tilde_modification)
apply (subst local_holder_on_cong[OF refl refl])
using local_holder_X_tilde X_tilde_measurable apply (auto cong: local_holder_on_cong)
done
then show "modification (restrict_index X {0..T}) (Mod T)"
"(∀x∈space source. local_holder_on γ {0..T} (λt. (Mod T) t x)) "
by blast+
qed
lemma compatible_Mod: "compatible (restrict_index X {0..T}) (Mod T)" if "0 < T" for T
using Mod that modificationD(1) by blast
lemma Mod_source[simp]: "proc_source (Mod T) = source" if "0 < T" for T
by (metis compatible_Mod compatible_source restrict_index_source that)
lemma Mod_target: "sets (proc_target (Mod T)) = sets (proc_target X)" if "0 < T" for T
by (metis compatible_Mod[OF that] compatible_target restrict_index_target)
lemma Mod_index[simp]: "0 < T ⟹ proc_index (Mod T) = {0..T}"
using compatible_Mod[THEN compatible_index] by simp
lemma indistinguishable_mod:
"indistinguishable (restrict_index (Mod S) {0..min S T}) (restrict_index (Mod T) {0..min S T})"
if "S > 0" "T > 0" for S T
proof -
have *: "modification (restrict_index (Mod S) {0..min S T}) (restrict_index (Mod T) {0..min S T})"
proof -
have "modification (restrict_index X {0..min S T}) (restrict_index (Mod S) {0..min S T})"
apply (cases "S ≤ T")
using Mod(1)[OF that(1)] apply clarsimp
apply (metis modification_restrict_index order_refl restrict_index_index restrict_index_override)
using Mod(1)[OF that(2)] apply clarsimp
by (metis (mono_tags, opaque_lifting) ‹modification (restrict_index X {0..S}) (Mod S)› atLeastatMost_subset_iff modification_restrict_index nle_le restrict_index_index restrict_index_override)
moreover have "modification (restrict_index X {0..min S T}) (restrict_index (Mod T) {0..min S T})"
apply (cases "S ≤ T")
using Mod(1)[OF that(1)] apply clarsimp
apply (metis Mod(1) atLeastatMost_subset_iff modification_restrict_index order.refl restrict_index_index restrict_index_override that(2))
using Mod(1)[OF that(2)] apply clarsimp
by (metis (mono_tags, opaque_lifting) atLeastatMost_subset_iff modification_restrict_index nle_le restrict_index_index restrict_index_override)
ultimately show ?thesis
using modification_sym modification_trans by metis
qed
then show ?thesis
proof (rule modification_continuous_indistinguishable,
goal_cases _ continuous_S continuous_T)
show "∃Ta>0. proc_index (restrict_index (Mod S) {0..min S T}) = {0..Ta}"
by (metis that min_def restrict_index_index)
next
case (continuous_S)
have "∀x ∈ space source. continuous_on {0..S} (λt. (Mod S) t x)"
using Mod[OF that(1)] local_holder_imp_continuous by blast
then have "∀x ∈ space source. continuous_on {0..min S T} (λt. (Mod S) t x)"
using continuous_on_subset by fastforce
then show ?case
by (auto simp: that(1))
next
case (continuous_T)
have "∀x ∈ space source. continuous_on {0..T} (λt. (Mod T) t x)"
using Mod[OF that(2)] local_holder_imp_continuous by fast
then have 2: "∀x ∈ space source. continuous_on {0..min S T} (λt. (Mod T) t x)"
using continuous_on_subset by fastforce
then show ?case
by (auto simp: that(2))
qed
qed
definition "N S T ≡ SOME N. N ∈ null_sets source ∧ {ω ∈ space source. ∃t ∈ {0..min S T}. (Mod S) t ω ≠ (Mod T) t ω} ⊆ N"
lemma N:
assumes "S > 0" "T > 0"
shows "N S T ∈ null_sets source ∧ {ω ∈ space source. ∃t ∈ {0..min S T}. (Mod S) t ω ≠ (Mod T) t ω} ⊆ N S T"
proof -
have ex: "∀S > 0. ∀T > 0. ∃N. N ∈ null_sets source ∧ {ω ∈ space source. ∃t ∈ {0..min S T}.
(Mod S) t ω ≠ (Mod T) t ω} ⊆ N"
apply (fold Bex_def)
using indistinguishable_mod[THEN indistinguishable_null_ex] by simp
show ?thesis
unfolding N_def apply (rule someI_ex)
using ex assms by blast
qed
definition N_inf where "N_inf ≡ (⋃S ∈ ℕ - {0}. (⋃ T ∈ ℕ - {0}. N S T))"
lemma N_inf_null: "N_inf ∈ null_sets source"
unfolding N_inf_def
apply (intro null_sets_UN')
apply (rule countable_Diff)
apply (simp add: Nats_def)+
using N by force
lemma Mod_eq_N_inf: "(Mod S) t ω = (Mod T) t ω"
if "ω ∈ space source - N_inf" "t ∈ {0..min S T}" "S ∈ ℕ - {0}" "T ∈ ℕ - {0}" for ω t S T
proof -
have "ω ∈ space source - N S T"
using that(1,3,4) unfolding N_inf_def by blast
moreover have "S > 0" "T > 0"
using that(2,3,4) by auto
ultimately have "ω ∈ {ω ∈ space source. ∀t ∈{0..min S T}. (Mod S) t ω = (Mod T) t ω}"
using N by auto
then show ?thesis
using that(2) by blast
qed
definition default :: 'b where "default = (SOME x. True)"
definition "X_mod ≡ λt ω. if ω ∈ space source - N_inf then (Mod ⌊t+1⌋) t ω else default"
definition "X_mod_process ≡ prob_space.process_of source (proc_target X) {0..} X_mod default"
lemma Mod_measurable[measurable]: "∀t∈{0..}. X_mod t ∈ source →⇩M proc_target X"
proof (intro ballI)
fix t :: real assume "t ∈ {0..}"
then have "0 < ⌊t + 1⌋"
by force
then show "X_mod t ∈ source →⇩M proc_target X"
unfolding X_mod_def apply measurable
apply (subst measurable_cong_sets[where M'= "proc_source (Mod ⌊t + 1⌋)" and N' = "proc_target (Mod ⌊t + 1⌋)"])
using Mod_source ‹0 < ⌊t + 1⌋› apply presburger
using Mod_target ‹0 < ⌊t + 1⌋› apply presburger
apply (meson random_process)
apply simp
apply (metis N_inf_null Int_def null_setsD2 sets.Int_space_eq1 sets.compl_sets)
done
qed
lemma modification_X_mod_process: "modification X X_mod_process"
proof (intro modificationI ballI)
show "compatible X X_mod_process"
apply (intro compatibleI)
unfolding X_mod_process_def
apply (subst proc_source.source_process_of)
using Mod_measurable proc_source.prob_space_axioms apply auto
done
fix t assume "t ∈ proc_index X"
then have "t ∈ {0..}"
by simp
then have "real_of_int ⌊t⌋ + 1 > 0"
by (simp add: add.commute add_pos_nonneg)
then have "∃N ∈ null_sets source. ∀ω ∈ space source - N.
X t ω = (prob_space.process_of source (proc_target X) {0..} X_mod default) t ω"
proof -
have 1: "(prob_space.process_of source (proc_target X) {0..} X_mod default) t ω = (Mod (real_of_int ⌊t⌋ + 1)) t ω"
if "ω ∈ space source - N_inf" for ω
apply (subst proc_source.process_process_of)
apply measurable
unfolding X_mod_def using that ‹t ∈ {0..}› apply simp
done
have "∃N ∈ null_sets source. ∀ω ∈ space source - N. X t ω = (Mod (real_of_int ⌊t⌋ + 1)) t ω"
proof -
obtain N where "{x ∈ space source. (restrict_index X {0..real_of_int ⌊t⌋ + 1}) t x ≠ (Mod (real_of_int ⌊t⌋ + 1)) t x} ⊆ N ∧
N ∈ null_sets (proc_source (restrict_index X {0..(real_of_int ⌊t⌋ + 1)}))"
using Mod(1)[OF ‹real_of_int ⌊t⌋ + 1 > 0›, THEN modification_null_set, of t]
using ‹t ∈ {0..}› by fastforce
then show ?thesis
by (smt (verit, ccfv_threshold) DiffE mem_Collect_eq restrict_index_process restrict_index_source subset_eq)
qed
then obtain N where "N ∈ null_sets source" "∀ω ∈ space source - N. X t ω = (Mod (real_of_int ⌊t⌋ + 1)) t ω"
by blast
then show ?thesis
apply (intro bexI[where x="N ∪ N_inf"])
apply (metis 1 DiffE DiffI UnCI)
using N_inf_null by blast
qed
then show "AE x in source. X t x = X_mod_process t x"
by (smt (verit, del_insts) X_mod_process_def DiffI eventually_ae_filter mem_Collect_eq subsetI)
qed
lemma local_holder_X_mod: "local_holder_on γ {0..} (λt. X_mod t ω)" for ω
proof (cases "ω ∈ space source - N_inf")
case False
then show ?thesis
apply (simp only: X_mod_def)
apply (metis local_holder_const gamma_0_1)
done
next
case True
then have ω: "ω ∈ space source" "ω ∉ N_inf"
by simp_all
then show ?thesis
proof (intro local_holder_ballI[OF gamma_0_1] ballI)
fix t::real assume "t ∈ {0..}"
then have "real_of_int ⌊t⌋ + 1 > 0"
using floor_le_iff by force
have "t < real_of_int ⌊t⌋ + 1"
by simp
then have "local_holder_on γ {0..real_of_int ⌊t⌋ + 1} (λs. Mod (real_of_int ⌊t⌋ + 1) s ω)"
using Mod(2) ω(1) ‹real_of_int ⌊t⌋ + 1 > 0› by blast
then obtain ε C where eC: "ε > 0" "C ≥ 0" "⋀r s. r ∈ ball t ε ∩ {0..real_of_int ⌊t⌋ + 1} ⟹
s ∈ ball t ε ∩ {0..real_of_int ⌊t⌋ + 1} ⟹
dist (Mod (real_of_int ⌊t⌋ + 1) r ω) (Mod (real_of_int ⌊t⌋ + 1) s ω) ≤ C * dist r s powr γ"
apply -
apply (erule local_holder_onE)
apply (rule gamma_0_1)
using ‹t ∈ {0..}› ‹t < real_of_int ⌊t⌋ + 1› apply fastforce
apply blast
done
define ε' where "ε' = min ε (if frac t = 0 then 1/2 else 1 - frac t)"
have e': "ε' ≤ ε ∧ ε' > 0 ∧ ball t ε' ∩ {0..} ⊆ {0..real_of_int ⌊t⌋ + 1}"
unfolding ε'_def apply (simp add: eC(1))
apply safe
apply (simp_all add: eC(1) dist_real_def frac_lt_1 frac_floor)
apply argo+
done
{
fix r s
assume r: "r ∈ ball t ε' ∩ {0..}"
assume s: "s ∈ ball t ε' ∩ {0..}"
then have rs_ball: "r ∈ ball t ε ∩ {0..real_of_int ⌊t⌋ + 1}"
"s ∈ ball t ε ∩ {0..real_of_int ⌊t⌋ + 1}"
using e' r s by auto
then have "r ∈ {0..min (real_of_int ⌊t⌋ + 1) (real_of_int ⌊r + 1⌋)}"
by auto
then have "(Mod (real_of_int ⌊t⌋ + 1)) r ω = X_mod r ω"
unfolding X_mod_def apply (simp only: True if_True)
apply (intro Mod_eq_N_inf[OF True])
apply simp
using ‹t ∈ {0..}› by auto
(metis (no_types, opaque_lifting) floor_in_Nats Nats_1 Nats_add Nats_cases
of_int_of_nat_eq of_nat_in_Nats, linarith)+
moreover have "(Mod (real_of_int ⌊t⌋ + 1)) s ω = X_mod s ω"
unfolding X_mod_def apply (simp only: True if_True)
apply (intro Mod_eq_N_inf[OF True])
using ‹s ∈ ball t ε ∩ {0..real_of_int ⌊t⌋ + 1}› apply simp
using ‹t ∈ {0..}› apply safe
apply (metis (no_types, opaque_lifting) floor_in_Nats Nats_1 Nats_add Nats_cases of_int_of_nat_eq of_nat_in_Nats)
apply linarith
apply (smt (verit) Int_iff Nats_1 Nats_add Nats_altdef1 atLeast_iff mem_Collect_eq s zero_le_floor)
apply (metis Int_iff atLeast_iff floor_correct linorder_not_less one_add_floor s)
done
ultimately have "dist (X_mod r ω) (X_mod s ω) ≤ C * dist r s powr γ"
using eC(3)[OF rs_ball] by simp
}
then show "∃ε>0. ∃C≥0. ∀r∈ball t ε ∩ {0..}. ∀s∈ball t ε ∩ {0..}. dist (X_mod r ω) (X_mod s ω) ≤ C * dist r s powr γ"
using e' eC(2) by blast
qed
qed
lemma local_holder_X_mod_process: "local_holder_on γ {0..} (λt. X_mod_process t ω)" for ω
unfolding X_mod_process_def
by (smt (verit, best) Mod_measurable UNIV_I local_holder_X_mod local_holder_on_cong
proc_source.process_process_of space_borel target_borel)
theorem continuous_modification:
"∃X'. modification X X' ∧ (∀ω. local_holder_on γ {0..} (λt. X' t ω))"
using local_holder_X_mod_process modification_X_mod_process by blast
end
theorem Kolmogorov_Chentsov:
fixes X :: "(real, 'a, 'b :: polish_space) stochastic_process"
and a b C γ :: real
assumes index[simp]: "proc_index X = {0..}"
and target_borel[simp]: "proc_target X = borel"
and gt_0: "a > 0" "b > 0" "C > 0"
and b_leq_a: "b ≤ a"
and gamma: "γ ∈ {0<..<b/a}"
and expectation: "⋀s t. ⟦s ≥ 0; t ≥ 0⟧ ⟹
(∫⇧+ x. dist (X t x) (X s x) powr a ∂proc_source X) ≤ C * dist t s powr (1+b)"
shows "∃X'. modification X X' ∧ (∀ω. local_holder_on γ {0..} (λt. X' t ω))"
using Kolmogorov_Chentsov.continuous_modification Kolmogorov_Chentsov.intro[OF assms]
by blast
end