Theory Lebesgue_Functional
section ‹Alternative Lebesgue Measure Definition›
theory Lebesgue_Functional
imports "HOL-Analysis.Lebesgue_Measure"
begin
text ‹Lebesgue\_Measure.lborel is defined on the typeclass euclidean\_space, which does not allow the
space dimension to be dependent on a variable. As the Lebesgue measure of higher dimensions is the
product measure of the one dimensional Lebesgue measure, we can easily define a more flexible version
of the Lebesgue measure as follows. This version of the Lebesgue measure measures sets of functions
from nat to real whose values are undefined for arguments higher than n. These "Extensional Function Spaces"
are defined in HOL/FuncSet. ›
definition lborel_f :: "nat ⇒ (nat ⇒ real) measure" where
"lborel_f n = (Π⇩M b∈{..<n}. lborel)"
lemma product_sigma_finite_interval: "product_sigma_finite (λb. interval_measure (λx. x))"
unfolding product_sigma_finite_def using sigma_finite_interval_measure by auto
lemma l_borel_f_1: "distr (lborel_f 1) lborel (λx. x 0) = lborel"
unfolding lborel_f_def
using product_sigma_finite.distr_singleton[OF product_sigma_finite_interval, of 0]
lborel_eq_real lessThan_Suc by auto
lemma space_lborel_f: "space (lborel_f n) = Pi⇩E {..<n} (λ_. UNIV)" unfolding lborel_f_def
unfolding space_PiM space_lborel space_borel by metis
lemma space_lborel_f_subset: "space (lborel_f n) ⊆ space (lborel_f (Suc n))"
unfolding space_lborel_f by (rule subsetI, rule PiE_I, blast,
metis PiE_E Suc_n_not_le_n le_cases lessThan_subset_iff subsetCE)
lemma space_lborel_add_dim:
assumes "f ∈ space (lborel_f n)"
shows "f(n:=x) ∈ space (lborel_f (Suc n))"
unfolding space_lborel_f
using assms lessThan_Suc space_lborel_f by auto
lemma integral_lborel_f:
assumes "f ∈ borel_measurable (lborel_f (Suc n))"
shows "integral⇧N (lborel_f (Suc n)) f = ∫⇧+ y. ∫⇧+ x. f (x(n := y)) ∂lborel_f n ∂lborel"
unfolding lborel_f_def
using product_sigma_finite.product_nn_integral_insert_rev[OF product_sigma_finite_interval, of "{..<n}", OF finite_lessThan _]
assms[unfolded lborel_f_def] lborel_eq_real by (simp add: lessThan_Suc)
lemma emeasure_lborel_f_Suc:
assumes "A ∈ sets (lborel_f (Suc n))"
assumes "⋀y. {x∈space (lborel_f n). x(n := y) ∈ A} ∈ sets (lborel_f n)"
shows "emeasure (lborel_f (Suc n)) A = ∫⇧+ y. emeasure (lborel_f n) {x∈space (lborel_f n). x(n := y) ∈ A} ∂lborel"
proof -
{
fix x y assume "x∈space (lborel_f n)"
then have "(indicator A) (x(n := y)) = (indicator {x∈space (lborel_f n). x(n := y) ∈ A}) x"
by (simp add: indicator_def)
}
then show ?thesis
unfolding nn_integral_indicator[OF assms(1), symmetric] nn_integral_indicator[OF assms(2), symmetric]
integral_lborel_f[OF borel_measurable_indicator, OF assms(1)]
using nn_integral_cong by (metis (no_types, lifting))
qed
lemma lborel_f_measurable_add_dim: "(λf. f(n := x)) ∈ measurable (lborel_f n) (lborel_f (Suc n))"
proof -
have "x ∈ space lborel" by simp
have 0:"(λ(f, y). f(n := y)) ∘ (λxa. (xa, x)) = (λf. f(n := x))" unfolding comp_def using case_prod_conv by fast
show ?thesis unfolding lborel_f_def
using measurable_comp[OF measurable_Pair2'[of x lborel "Pi⇩M {..<n} (λb. lborel)", OF ‹x ∈ space lborel›]
measurable_add_dim[of n "{..<n}" "λb. lborel"], unfolded 0] lessThan_Suc by auto
qed
lemma sets_lborel_f_sub_dim:
assumes "A ∈ sets (lborel_f (Suc n))"
shows "{x. x(n := y) ∈ A} ∩ space (lborel_f n) ∈ sets (lborel_f n)"
proof -
have "(λf. f(n := y)) -` A ∩ space (lborel_f n) ∈ sets (lborel_f n)"
using measurable_sets[OF lborel_f_measurable_add_dim assms] by auto
moreover have "(λf. f(n := y)) -` A = {x. x(n := y) ∈ A}" by auto
finally show ?thesis by metis
qed
lemma lborel_f_measurable_restrict:
assumes "m ≤ n"
shows "(λf. restrict f {..<m}) ∈ measurable (lborel_f n) (lborel_f m)"
using measurable_restrict_subset lborel_f_def assms by auto
lemma lborel_measurable_sub_dim: "(λf. restrict f {..<n}) ∈ measurable (lborel_f (Suc n)) (lborel_f n)"
using lborel_f_measurable_restrict[of "n" "Suc n"] by linarith
lemma measurable_lborel_component [measurable]:
assumes "k<n"
shows "(λx. x k) ∈ borel_measurable (lborel_f n)"
unfolding lborel_f_def using assms measurable_PiM_component_rev by simp_all
end