(* Author: Alexander Bentkamp, Universität des Saarlandes *) 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" using indicator_def by (metis (no_types, lifting) mem_Collect_eq) } 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