Theory Lspace

section‹Lspace as it is in HOL Light›

text‹Mainly a repackaging of existing material from Lp›

theory Lspace
  imports Lp.Lp 
begin

abbreviation lspace :: "'a measure ⇒ ennreal ⇒ ('a ⇒ real) set"
  where "lspace M p ≡ space⇩N (𝔏 p M)"

lemma lspace_1:
  assumes "S ∈ sets lebesgue"
  shows "f ∈ lspace (lebesgue_on S) 1 ⟷ f absolutely_integrable_on S"
  using assms by (simp add: L1_space integrable_restrict_space set_integrable_def)

lemma lspace_ennreal_iff:
  assumes "p > 0"
  shows "lspace (lebesgue_on S) (ennreal p) = {f ∈ borel_measurable (lebesgue_on S). integrable (lebesgue_on S) (λx. (norm(f x) powr p))}"
  using assms  by (fastforce simp: Lp_measurable Lp_D intro: Lp_I)

lemma lspace_iff:
  assumes "∞ > p" "p > 0"
  shows "lspace (lebesgue_on S) p = {f ∈ borel_measurable (lebesgue_on S). integrable (lebesgue_on S) (λx. (norm(f x) powr (enn2real p)))}"
proof -
  obtain q::real where "p = enn2real q"
    using Lp_cases assms by auto
  then show ?thesis
    using assms lspace_ennreal_iff by auto
qed

lemma lspace_iff':
  assumes p: "∞ > p" "p > 0" and S: "S ∈ sets lebesgue"
  shows "lspace (lebesgue_on S) p = {f ∈ borel_measurable (lebesgue_on S). (λx. (norm(f x) powr (enn2real p))) integrable_on S}"
    (is "?lhs = ?rhs")
proof
  show "?lhs ⊆ ?rhs"
    using assms integrable_on_lebesgue_on by (auto simp: lspace_iff)
next
  show "?rhs ⊆ ?lhs"
  proof (clarsimp simp: lspace_iff [OF p])
    show "integrable (lebesgue_on S) (λxa. ¦f xa¦ powr enn2real p)"
      if "f ∈ borel_measurable (lebesgue_on S)" and "(λx. ¦f x¦ powr enn2real p) integrable_on S" for f
    proof -
      have "(λx. ¦f x¦ powr enn2real p) absolutely_integrable_on S"
        by (simp add: absolutely_integrable_on_iff_nonneg that(2))
      then show ?thesis
        using L1_space S lspace_1 by blast
    qed
  qed
qed

lemma lspace_mono:
  assumes "f ∈ lspace (lebesgue_on S) q" and S: "S ∈ lmeasurable" and "p > 0" "p ≤ q" "q < ∞"
  shows "f ∈ lspace (lebesgue_on S) p"
proof -
  have "p < ∞"
    using assms by (simp add: top.not_eq_extremum)
  with assms show ?thesis
  proof (clarsimp simp add: lspace_iff')
    show "(λx. ¦f x¦ powr enn2real p) integrable_on S"
      if "f ∈ borel_measurable (lebesgue_on S)"
        and "(λx. ¦f x¦ powr enn2real q) integrable_on S"
    proof (rule measurable_bounded_by_integrable_imp_integrable)
      show "(λx. ¦f x¦ powr enn2real p) ∈ borel_measurable (lebesgue_on S)"
        using measurable_abs_powr that(1) by blast
      let ?g = "λx. max 1 (norm(f x) powr enn2real q)"
      have "?g absolutely_integrable_on S"
      proof (rule absolutely_integrable_max_1)
        show "(λx. norm (f x) powr enn2real q) absolutely_integrable_on S"
          by (simp add: nonnegative_absolutely_integrable_1 that(2))
      qed (simp add: S)
      then show "?g integrable_on S"
        using absolutely_integrable_abs_iff by blast
      show "norm (¦f x¦ powr enn2real p) ≤ ?g x" if "x ∈ S" for x
      proof -
        have "¦f x¦ powr enn2real p ≤ ¦f x¦ powr enn2real q" if "1 ≤ ¦f x¦"
          using assms enn2real_mono powr_mono that by auto
        then show ?thesis
          using powr_le1 by (fastforce simp add: le_max_iff_disj)
      qed
      show "S ∈ sets lebesgue"
        by (simp add: S fmeasurableD)
    qed
  qed
qed

lemma lspace_inclusion:
  assumes "S ∈ lmeasurable" and "p > 0" "p ≤ q" "q < ∞"
  shows "lspace (lebesgue_on S) q ⊆ lspace (lebesgue_on S) p"
  using assms lspace_mono by auto

lemma lspace_const:
  fixes p::real
  assumes "p > 0""S ∈ lmeasurable"
  shows "(λx. c) ∈ lspace (lebesgue_on S) p"
  by (simp add: Lp_space assms finite_measure.integrable_const finite_measure_lebesgue_on)

lemma lspace_max:
  fixes p::real
  assumes "f ∈ lspace (lebesgue_on S) p" "g ∈ lspace (lebesgue_on S) p" "p > 0"
  shows "(λx. max (f x) (g x)) ∈ lspace (lebesgue_on S) p"
proof -
  have "integrable (lebesgue_on S) (λx. ¦max (f x) (g x)¦ powr p)"
    if f: "f ∈ borel_measurable (lebesgue_on S)" "integrable (lebesgue_on S) (λx. ¦f x¦ powr p)"
      and g: "g ∈ borel_measurable (lebesgue_on S)" "integrable (lebesgue_on S) (λx. ¦g x¦ powr p)"
  proof -
    have "integrable (lebesgue_on S) (λx. ¦¦f x¦ powr p¦)" "integrable (lebesgue_on S) (λx. ¦¦g x¦ powr p¦)"
      using integrable_abs that by blast+
    then have "integrable (lebesgue_on S) (λx. max (¦¦f x¦ powr p¦) (¦¦g x¦ powr p¦))"
      using integrable_max by blast
    then show ?thesis
    proof (rule Bochner_Integration.integrable_bound)
      show "(λx. ¦max (f x) (g x)¦ powr p) ∈ borel_measurable (lebesgue_on S)"
        using borel_measurable_max measurable_abs_powr that by blast
    qed auto
  qed
  then show ?thesis
    using assms by (auto simp: Lp_space borel_measurable_max)
qed

lemma lspace_min:
  fixes p::real
  assumes "f ∈ lspace (lebesgue_on S) p" "g ∈ lspace (lebesgue_on S) p" "p > 0"
  shows "(λx. min (f x) (g x)) ∈ lspace (lebesgue_on S) p"
proof -
  have "integrable (lebesgue_on S) (λx. ¦min (f x) (g x)¦ powr p)"
    if f: "f ∈ borel_measurable (lebesgue_on S)" "integrable (lebesgue_on S) (λx. ¦f x¦ powr p)"
      and g: "g ∈ borel_measurable (lebesgue_on S)" "integrable (lebesgue_on S) (λx. ¦g x¦ powr p)"
  proof -
    have "integrable (lebesgue_on S) (λx. ¦¦f x¦ powr p¦)" "integrable (lebesgue_on S) (λx. ¦¦g x¦ powr p¦)"
      using integrable_abs that by blast+
    then have "integrable (lebesgue_on S) (λx. max (¦¦f x¦ powr p¦) (¦¦g x¦ powr p¦))"
      using integrable_max by blast
    then show ?thesis
    proof (rule Bochner_Integration.integrable_bound)
      show "(λx. ¦min (f x) (g x)¦ powr p) ∈ borel_measurable (lebesgue_on S)"
        using borel_measurable_min measurable_abs_powr that by blast
    qed auto
  qed
  then show ?thesis
    using assms by (auto simp: Lp_space borel_measurable_min)
qed

lemma Lp_space_numeral:
  assumes "numeral n > (0::int)"
  shows "space⇩N (𝔏 (numeral n) M) = {f ∈ borel_measurable M. integrable M (λx. ¦f x¦ ^ numeral n)}"
  using Lp_space [of "numeral n" M] assms by simp

end