Theory Lebesgue_Functional

theory Lebesgue_Functional
imports Lebesgue_Measure
(* Author: Alexander Bentkamp, Universit├Ąt des Saarlandes
section ‹Alternative Lebesgue Measure Definition›

theory Lebesgue_Functional
imports "HOL-Analysis.Lebesgue_Measure"

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) = PiE {..<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 "integralN (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))

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 "PiM {..<n} (λb. lborel)", OF ‹x ∈ space lborel›]
    measurable_add_dim[of n "{..<n}" "λb. lborel"], unfolded 0] lessThan_Suc by auto

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

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