Theory Lp.Lp

(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
    License: BSD
*)

theory Lp
imports Functional_Spaces
begin

text ‹The material in this file is essentially of analytic nature. However, one of the central
proofs (the proof of Holder inequality below) uses a probability space, and Jensen's inequality
there. Hence, we need to import \verb+Probability+. Moreover, we use several lemmas from
\verb+SG_Library_Complement+.›


section ‹Conjugate exponents›

text ‹Two numbers $p$ and $q$ are \emph{conjugate} if $1/p + 1/q = 1$. This relation keeps
appearing in the theory of $L^p$ spaces, as the dual of $L^p$ is $L^q$ where $q$ is the conjugate
of $p$. This relation makes sense for real numbers, but also for ennreals
(where the case $p=1$ and $q=\infty$ is most important). Unfortunately, manipulating the
previous relation with ennreals is tedious as there is no good simproc involving addition and
division there. To mitigate this difficulty, we prove once and for all most useful properties
of such conjugates exponents in this paragraph.›

lemma Lp_cases_1_PInf:
  assumes "p ≥ (1::ennreal)"
  obtains (gr) p2 where "p = ennreal p2" "p2 > 1" "p > 1"
    | (one) "p = 1"
    | (PInf) "p = ∞"
using assms by (metis (full_types) antisym_conv ennreal_cases ennreal_le_1 infinity_ennreal_def not_le)

lemma Lp_cases:
  obtains (real_pos) p2 where "p = ennreal p2" "p2 > 0" "p > 0"
    | (zero) "p = 0"
    | (PInf) "p = ∞"
by (metis enn2real_positive_iff ennreal_enn2real_if infinity_ennreal_def not_gr_zero top.not_eq_extremum)

definition
  "conjugate_exponent p = 1 + 1/(p-1)"

lemma conjugate_exponent_real:
  assumes "p > (1::real)"
  shows "1/p + 1/(conjugate_exponent p) = 1"
        "conjugate_exponent p > 1"
        "conjugate_exponent(conjugate_exponent p) = p"
        "(p-1) * conjugate_exponent p = p"
        "p - p / conjugate_exponent p = 1"
unfolding conjugate_exponent_def using assms by (auto simp add: algebra_simps divide_simps)

lemma conjugate_exponent_real_iff:
  assumes "p > (1::real)"
  shows "q = conjugate_exponent p ⟷ (1/p + 1/q = 1)"
unfolding conjugate_exponent_def using assms by (auto simp add: algebra_simps divide_simps)

lemma conjugate_exponent_real_2 [simp]:
  "conjugate_exponent (2::real) = 2"
  unfolding conjugate_exponent_def by (auto simp add: algebra_simps divide_simps)

lemma conjugate_exponent_realI:
  assumes "p > (0::real)" "q > 0" "1/p + 1/q = 1"
  shows "p > 1" "q = conjugate_exponent p" "q > 1" "p = conjugate_exponent q"
unfolding conjugate_exponent_def using assms apply (auto simp add: algebra_simps divide_simps)
apply (metis assms(3) divide_less_eq_1_pos less_add_same_cancel1 zero_less_divide_1_iff)
using mult_less_cancel_left_pos by fastforce


lemma conjugate_exponent_real_ennreal:
  assumes "p> (1::real)"
  shows "conjugate_exponent(ennreal p) = ennreal(conjugate_exponent p)"
unfolding conjugate_exponent_def using assms
by (auto, metis diff_gt_0_iff_gt divide_ennreal ennreal_1 ennreal_minus zero_le_one)

lemma conjugate_exponent_ennreal_1_2_PInf [simp]:
  "conjugate_exponent (1::ennreal) = ∞"
  "conjugate_exponent (∞::ennreal) = 1"
  "conjugate_exponent (⊤::ennreal) = 1"
  "conjugate_exponent (2::ennreal) = 2"
using conjugate_exponent_real_ennreal[of 2] by (auto simp add: conjugate_exponent_def)

lemma conjugate_exponent_ennreal:
  assumes "p ≥ (1::ennreal)"
  shows "1/p + 1/(conjugate_exponent p) = 1"
        "conjugate_exponent p ≥ 1"
        "conjugate_exponent(conjugate_exponent p) = p"
proof -
  have "(1/p + 1/(conjugate_exponent p) = 1) ∧ (conjugate_exponent p ≥ 1) ∧ conjugate_exponent(conjugate_exponent p) = p"
  using ‹p ≥ 1› proof (cases rule: Lp_cases_1_PInf)
    case (gr p2)
    then have *: "conjugate_exponent p = ennreal (conjugate_exponent p2)" using conjugate_exponent_real_ennreal[OF ‹p2 > 1›] by auto
    have a: "conjugate_exponent p ≥ 1" using * conjugate_exponent_real[OF ‹p2 > 1›] by auto
    have b: "conjugate_exponent(conjugate_exponent p) = p"
      using conjugate_exponent_real(3)[OF ‹p2 > 1›] conjugate_exponent_real_ennreal[OF ‹p2 > 1›]
      conjugate_exponent_real_ennreal[OF conjugate_exponent_real(2)[OF ‹p2 > 1›]] unfolding * ‹p = ennreal p2› by auto
    have "1 / p + 1 / conjugate_exponent p = ennreal(1/p2 + 1/(conjugate_exponent p2))" unfolding * unfolding ‹p = ennreal p2›
      using conjugate_exponent_real(2)[OF ‹p2 > 1›] ‹p2 > 1›
      apply (subst ennreal_plus, auto) apply (subst divide_ennreal[symmetric], auto)
      using divide_ennreal_def inverse_ennreal inverse_eq_divide by auto
    then have c: "1 / p + 1 / conjugate_exponent p = 1" using conjugate_exponent_real[OF ‹p2 > 1›] by auto
    show ?thesis using a b c by simp
  qed (auto)
  then show "1/p + 1/(conjugate_exponent p) = 1"
            "conjugate_exponent p ≥ 1"
            "conjugate_exponent(conjugate_exponent p) = p"
    by auto
qed

lemma conjugate_exponent_ennreal_iff:
  assumes "p ≥ (1::ennreal)"
  shows "q = conjugate_exponent p ⟷ (1/p + 1/q = 1)"
using conjugate_exponent_ennreal[OF assms]
by (auto, metis ennreal_add_diff_cancel_left ennreal_add_eq_top ennreal_top_neq_one one_divide_one_divide_ennreal)

lemma conjugate_exponent_ennrealI:
  assumes "1/p + 1/q = (1::ennreal)"
  shows "p ≥ 1" "q ≥ 1" "p = conjugate_exponent q" "q = conjugate_exponent p"
proof -
  have "1/p ≤ 1" using assms using le_iff_add by fastforce
  then show "p ≥ 1"
    by (metis assms divide_ennreal_def ennreal_add_eq_top ennreal_divide_self ennreal_divide_zero ennreal_le_epsilon ennreal_one_neq_top mult.left_neutral mult_left_le zero_le)
  then show "q = conjugate_exponent p" using conjugate_exponent_ennreal_iff assms by auto
  then show "q ≥ 1" using conjugate_exponent_ennreal[OF ‹p ≥ 1›] by auto
  show "p = conjugate_exponent q"
    using conjugate_exponent_ennreal_iff[OF ‹q≥1›, of p] assms by (simp add: add.commute)
qed


section ‹Convexity inequalities and integration›

text ‹In this paragraph, we describe the basic inequalities relating the integral of a function
and of its $p$-th power, for $p > 0$. These inequalities imply in particular that the $L^p$ norm
satisfies the triangular inequality, a feature we will need when defining the $L^p$ spaces below.
In particular, we prove the Hölder and Minkowski inequalities. The Hölder inequality,
especially, is the basis of all further inequalities for $L^p$ spaces.
›

lemma (in prob_space) bound_L1_Lp:
  assumes "p ≥ (1::real)"
          "f ∈ borel_measurable M"
          "integrable M (λx. ¦f x¦ powr p)"
  shows "integrable M f"
        "abs(∫x. f x ∂M) powr p ≤ (∫x. ¦f x¦ powr p ∂M)"
        "abs(∫x. f x ∂M) ≤ (∫x. ¦f x¦ powr p ∂M) powr (1/p)"
proof -
  have *: "norm x ≤ 1 + (norm x) powr p" for x::real
    apply (cases "norm x ≤ 1")
    apply (meson le_add_same_cancel1 order.trans powr_ge_pzero)
    apply (metis add_le_same_cancel2 assms(1) less_le_trans linear not_less not_one_le_zero powr_le_cancel_iff powr_one_gt_zero_iff)
    done
  show *: "integrable M f"
    apply (rule Bochner_Integration.integrable_bound[of _ "λx. 1 + ¦f x¦ powr p"], auto simp add: assms) using * by auto
  show "abs(∫x. f x ∂M) powr p ≤ (∫x. ¦f x¦ powr p ∂M)"
    by (rule jensens_inequality[OF * _ _ assms(3) convex_abs_powr[OF ‹p ≥ 1›]], auto)
  then have "(abs(∫x. f x ∂M) powr p) powr (1/p) ≤ (∫x. ¦f x¦ powr p ∂M) powr (1/p)"
    using assms(1) powr_mono2 by auto
  then show "abs(∫x. f x ∂M) ≤ (∫x. ¦f x¦ powr p ∂M) powr (1/p)"
    using ‹p ≥ 1› by (auto simp add: powr_powr)
qed


theorem Holder_inequality:
  assumes "p > (0::real)" "q > 0" "1/p + 1/q = 1"
      and [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
          "integrable M (λx. ¦f x¦ powr p)"
          "integrable M (λx. ¦g x¦ powr q)"
  shows "integrable M (λx. f x * g x)"
        "(∫x. ¦f x * g x¦ ∂M) ≤ (∫x. ¦f x¦ powr p ∂M) powr (1/p) * (∫x. ¦g x¦ powr q ∂M) powr (1/q)"
        "abs(∫x. f x * g x ∂M) ≤ (∫x. ¦f x¦ powr p ∂M) powr (1/p) * (∫x. ¦g x¦ powr q ∂M) powr (1/q)"
proof -
  have "p > 1" using conjugate_exponent_realI(1)[OF ‹p>0› ‹q>0› ‹1/p+1/q=1›].

  have *: "x * y ≤ x powr p + y powr q" if "x ≥ 0" "y ≥ 0" for x y
  proof -
    have "x * y = (x powr p) powr (1/p) * (y powr q) powr (1/q)"
      using ‹p > 0› ‹q > 0› powr_powr that(1) that(2) by auto
    also have "... ≤ (max (x powr p) (y powr q)) powr (1/p) * (max (x powr p) (y powr q)) powr (1/q)"
      apply (rule mult_mono, auto) using assms(1) assms(2) powr_mono2 by auto
    also have "... = max (x powr p) (y powr q)"
      by (metis max_def mult.right_neutral powr_add powr_powr assms(3))
    also have "... ≤ x powr p + y powr q"
      by auto
    finally show ?thesis by simp
  qed
  show [simp]: "integrable M (λx. f x * g x)"
    apply (rule Bochner_Integration.integrable_bound[of _ "λx. ¦f x¦ powr p + ¦g x¦ powr q"], auto)
    by (rule Bochner_Integration.integrable_add, auto simp add: assms * abs_mult)

  text ‹The proof of the main inequality is done by applying the inequality
        $(\int |h| d\mu \leq \int |h|^p d\mu)^{1/p}$ to the right function $h$ in the right
        probability space. One should take $h = f \cdot |g|^{1-q}$, and $d\mu = |g|^q dM / I$,
        where $I = \int |g|^q$. This readily gives the result.›

  show *: "(∫x. ¦f x * g x¦ ∂M) ≤ (∫x. ¦f x¦ powr p ∂M) powr (1/p) * (∫x. ¦g x¦ powr q ∂M) powr (1/q)"
  proof (cases "(∫x. ¦g x¦ powr q ∂M) = 0")
    case True
    then have "AE x in M. ¦g x¦ powr q = 0"
      by (subst integral_nonneg_eq_0_iff_AE[symmetric], auto simp add: assms)
    then have *: "AE x in M. f x * g x = 0"
      using ‹q > 0› by auto
    have "(∫x. ¦f x * g x¦ ∂M) = (∫x. 0 ∂M)"
      apply (rule integral_cong_AE) using * by auto
    then show ?thesis by auto
  next
    case False
    moreover have "(∫x. ¦g x¦ powr q ∂M) ≥ (∫x. 0 ∂M)" by (rule integral_mono, auto simp add: assms)
    ultimately have *: "(∫x. ¦g x¦ powr q ∂M) > 0" by (simp add: le_less)
    define I where "I = (∫x. ¦g x¦ powr q ∂M)"
    have [simp]: "I > 0" unfolding I_def using * by auto
    define M2 where "M2 = density M (λx. ¦g x¦ powr q / I)"
    interpret prob_space M2
      apply (standard, unfold M2_def, auto, subst emeasure_density, auto)
      apply (subst divide_ennreal[symmetric], auto, subst nn_integral_divide, auto)
      apply (subst nn_integral_eq_integral, auto simp add: assms, unfold I_def)
      using * by auto

    have [simp]: "p ≥ 1" "p ≥ 0" using ‹p > 1› by auto
    have A: "q + (1 - q) * p = 0" using assms by (auto simp add: divide_simps algebra_simps)
    have B: "1 - 1/p = 1/q" using ‹1/p + 1/q = 1› by auto
    define f2 where "f2 = (λx. f x * indicator {y∈ space M. g y ≠ 0} x)"
    have [measurable]: "f2 ∈ borel_measurable M" unfolding f2_def by auto
    define h where "h = (λx. ¦f2 x¦ * ¦g x¦ powr (1-q))"
    have [measurable]: "h ∈ borel_measurable M" unfolding h_def by auto
    have [measurable]: "h ∈ borel_measurable M2" unfolding M2_def by auto

    have Eq: "(¦g x¦ powr q / I) *⇩R ¦h x¦ powr p = ¦f2 x¦ powr p / I" for x
      apply (insert ‹I>0›, auto simp add: divide_simps, unfold h_def)
      apply (auto simp add: divide_nonneg_pos divide_simps powr_mult powr_powr powr_add[symmetric] A)
      unfolding f2_def by auto
    have "integrable M2 (λx. ¦h x¦ powr p)"
      unfolding M2_def apply (subst integrable_density, simp, simp, simp add: divide_simps)
      apply (subst Eq, rule integrable_divide, rule Bochner_Integration.integrable_bound[of _ "λx. ¦f x¦ powr p"], unfold f2_def)
      by (unfold indicator_def, auto simp add: ‹integrable M (λx. ¦f x¦ powr p)›)
    then have "integrable M2 (λx. ¦h x¦)"
      by (metis bound_L1_Lp(1) ‹random_variable borel h› ‹p > 1› integrable_abs le_less)

    have "(∫x. ¦h x¦ powr p ∂M2) = (∫x. (¦g x¦ powr q / I) *⇩R (¦h x¦ powr p) ∂M)"
      unfolding M2_def by (rule integral_density[of "λx. ¦h x¦ powr p" M "λx. ¦g x¦ powr q / I"], auto simp add: divide_simps)
    also have "... = (∫x. ¦f2 x¦ powr p / I ∂M)"
      apply (rule Bochner_Integration.integral_cong) using Eq by auto
    also have "... ≤ (∫x. ¦f x¦ powr p / I ∂M)"
      apply (rule integral_mono', rule integrable_divide[OF ‹integrable M (λx. ¦f x¦ powr p)›])
      unfolding f2_def indicator_def using ‹I > 0› by (auto simp add: divide_simps)
    finally have C: "(∫x. ¦h x¦ powr p ∂M2) ≤ (∫x. ¦f x¦ powr p / I ∂M)" by simp

    have "(∫x. ¦f x * g x¦ ∂M) / I = (∫x. ¦f x * g x¦ / I ∂M)"
      by auto
    also have "... = (∫x. ¦f2 x * g x¦ / I ∂M)"
      by (auto simp add: divide_simps, rule Bochner_Integration.integral_cong, unfold f2_def indicator_def, auto)
    also have "... = (∫x. ¦h x¦ ∂M2)"
      apply (unfold M2_def, subst integral_density, simp, simp, simp add: divide_simps)
      by (rule Bochner_Integration.integral_cong, unfold h_def, auto simp add: divide_simps algebra_simps powr_add[symmetric] abs_mult)
    also have "... ≤ abs (∫x. ¦h x¦ ∂M2)"
      by auto
    also have "... ≤ (∫x. abs(¦h x¦) powr p ∂M2) powr (1/p)"
      apply (rule bound_L1_Lp(3)[of p "λx. ¦h x¦"])
      by (auto simp add: ‹integrable M2 (λx. ¦h x¦ powr p)›)
    also have "... ≤ (∫x. ¦f x¦ powr p / I ∂M) powr (1/p)"
      by (rule powr_mono2, insert C, auto)
    also have "... ≤ ((∫x. ¦f x¦ powr p ∂M) / I) powr (1/p)"
      apply (rule powr_mono2, auto simp add: divide_simps) using ‹p ≥ 0› by auto
    also have "... = (∫x. ¦f x¦ powr p ∂M) powr (1/p) * I powr(-1/p)"
      by (auto simp add: less_imp_le powr_divide powr_minus_divide)
    finally have "(∫x. ¦f x * g x¦ ∂M) ≤ (∫x. ¦f x¦ powr p ∂M) powr (1/p) * I * I powr(-1/p)"
      by (auto simp add: divide_simps algebra_simps)
    also have "... = (∫x. ¦f x¦ powr p ∂M) powr (1/p) * I powr (1-1/p)"
      by (auto simp add: powr_mult_base less_imp_le)
    also have "... = (∫x. ¦f x¦ powr p ∂M) powr (1/p) * (∫x. ¦g x¦ powr q ∂M) powr (1/q)"
      unfolding I_def using B by auto
    finally show ?thesis
      by simp
  qed
  have "abs(∫x. f x * g x ∂M) ≤ (∫x. ¦f x * g x¦ ∂M)" by auto
  then show "abs(∫x. f x * g x ∂M) ≤ (∫x. ¦f x¦ powr p ∂M) powr (1/p) * (∫x. ¦g x¦ powr q ∂M) powr (1/q)"
    using * by linarith
qed

theorem Minkowski_inequality:
  assumes "p ≥ (1::real)"
      and [measurable, simp]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
          "integrable M (λx. ¦f x¦ powr p)"
          "integrable M (λx. ¦g x¦ powr p)"
  shows "integrable M (λx. ¦f x + g x¦ powr p)"
        "(∫x. ¦f x + g x¦ powr p ∂M) powr (1/p)
          ≤ (∫x. ¦f x¦ powr p ∂M) powr (1/p) + (∫x. ¦g x¦ powr p ∂M) powr (1/p)"
proof -
  have *: "¦x + y¦ powr p ≤ 2 powr p * (¦x¦ powr p + ¦y¦ powr p)" for x y::real
  proof -
    have "¦x + y¦ ≤ ¦x¦ + ¦y¦" by auto
    also have "... ≤ (max ¦x¦ ¦y¦) + max ¦x¦ ¦y¦" by auto
    also have "... = 2 * max ¦x¦ ¦y¦" by auto
    finally have "¦x + y¦ powr p ≤ (2 * max ¦x¦ ¦y¦) powr p"
      using powr_mono2 ‹p ≥ 1› by auto
    also have "... = 2 powr p * (max ¦x¦ ¦y¦) powr p"
      using powr_mult by auto
    also have "... ≤ 2 powr p * (¦x¦ powr p + ¦y¦ powr p)"
      unfolding max_def by auto
    finally show ?thesis by simp
  qed
  show [simp]: "integrable M (λx. ¦f x + g x¦ powr p)"
    by (rule Bochner_Integration.integrable_bound[of _ "λx. 2 powr p * (¦f x¦ powr p + ¦g x¦ powr p)"], auto simp add: *)

  show "(∫x. ¦f x + g x¦ powr p ∂M) powr (1/p) ≤ (∫x. ¦f x¦ powr p ∂M) powr (1/p) + (∫x. ¦g x¦ powr p ∂M) powr (1/p)"
  proof (cases "p=1")
    case True
    then show ?thesis
      apply (auto, subst Bochner_Integration.integral_add[symmetric], insert assms(4) assms(5), simp, simp)
      by (rule integral_mono', auto)
  next
    case False
    then have [simp]: "p > 1" "p ≥ 1" "p > 0" "p ≠ 0" using assms(1) by auto
    define q where "q = conjugate_exponent p"
    have [simp]: "q > 1" "q > 0" "1/p + 1/q = 1" "(p-1) * q = p"
      unfolding q_def using conjugate_exponent_real[OF ‹p>1›] by auto
    then have [simp]: "(z powr (p-1)) powr q = z powr p" for z
      by (simp add: powr_powr)
    have "(∫x. ¦f x + g x¦ powr p ∂M) = (∫x. ¦f x + g x¦ * ¦f x + g x¦ powr (p-1) ∂M)"
      by (subst powr_mult_base, auto)
    also have "... ≤ (∫x. ¦f x¦ * ¦f x + g x¦ powr (p-1) + ¦g x¦ * ¦f x + g x¦ powr (p-1) ∂M)"
      apply (rule integral_mono', rule Bochner_Integration.integrable_add)
      apply (rule Holder_inequality(1)[of p q], auto)
      apply (rule Holder_inequality(1)[of p q], auto)
      by (metis abs_ge_zero abs_triangle_ineq comm_semiring_class.distrib le_less mult_mono' powr_ge_pzero)
    also have "... = (∫x. ¦f x¦ * ¦f x + g x¦ powr (p-1) ∂M) + (∫x. ¦g x¦ * ¦f x + g x¦ powr (p-1) ∂M)"
      apply (rule Bochner_Integration.integral_add) by (rule Holder_inequality(1)[of p q], auto)+
    also have "... ≤ abs (∫x. ¦f x¦ * ¦f x + g x¦ powr (p-1) ∂M) + abs (∫x. ¦g x¦ * ¦f x + g x¦ powr (p-1) ∂M)"
      by auto
    also have "... ≤ (∫x. abs(¦f x¦) powr p ∂M) powr (1/p) * (∫x. abs(¦f x + g x¦ powr (p-1)) powr q ∂M) powr (1/q)
                      + (∫x. abs(¦g x¦) powr p ∂M) powr (1/p) * (∫x. abs(¦f x + g x¦ powr (p-1)) powr q ∂M) powr (1/q)"
      apply (rule add_mono)
      apply (rule Holder_inequality(3)[of p q], simp, simp, simp, simp, simp, simp, simp)
      apply (rule Holder_inequality(3)[of p q], simp, simp, simp, simp, simp, simp, simp)
      done
    also have "... = (∫x. ¦f x + g x¦ powr p ∂M) powr (1/q) *
            ((∫x. abs(¦f x¦) powr p ∂M) powr (1/p) + (∫x. abs(¦g x¦) powr p ∂M) powr (1/p))"
      by (auto simp add: algebra_simps)
    finally have *: "(∫x. ¦f x + g x¦ powr p ∂M) ≤ (∫x. ¦f x + g x¦ powr p ∂M) powr (1/q) *
        ((∫x. abs(¦f x¦) powr p ∂M) powr (1/p) + (∫x. abs(¦g x¦) powr p ∂M) powr (1/p))"
      by simp
    show ?thesis
    proof (cases "(∫x. ¦f x + g x¦ powr p ∂M) = 0")
      case True
      then show ?thesis by auto
    next
      case False
      then have **: "(∫x. ¦f x + g x¦ powr p ∂M) powr (1/q) > 0"
        by auto
      have "(∫x. ¦f x + g x¦ powr p ∂M) powr (1/q) * (∫x. ¦f x + g x¦ powr p ∂M) powr (1/p)
              = (∫x. ¦f x + g x¦ powr p ∂M)"
        by (auto simp add: powr_add[symmetric] add.commute)
      then have "(∫x. ¦f x + g x¦ powr p ∂M) powr (1/q) * (∫x. ¦f x + g x¦ powr p ∂M) powr (1/p) ≤
              (∫x. ¦f x + g x¦ powr p ∂M) powr (1/q) *
              ((∫x. abs(¦f x¦) powr p ∂M) powr (1/p) + (∫x. abs(¦g x¦) powr p ∂M) powr (1/p))"
        using * by auto
      then show ?thesis using ** by auto
    qed
  qed
qed

text ‹When $p<1$, the function $x \mapsto |x|^p$ is not convex any more. Hence, the $L^p$ ``norm''
is not a norm any more, but a quasinorm. This is proved using a different convexity argument, as
follows.›

theorem Minkowski_inequality_le_1:
  assumes "p > (0::real)" "p ≤ 1"
      and [measurable, simp]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
          "integrable M (λx. ¦f x¦ powr p)"
          "integrable M (λx. ¦g x¦ powr p)"
  shows "integrable M (λx. ¦f x + g x¦ powr p)"
        "(∫x. ¦f x + g x¦ powr p ∂M) powr (1/p)
          ≤ 2 powr (1/p-1) * (∫x. ¦f x¦ powr p ∂M) powr (1/p) + 2 powr (1/p-1) * (∫x. ¦g x¦ powr p ∂M) powr (1/p)"
proof -
  have *: "¦a + b¦ powr p ≤ ¦a¦ powr p + ¦b¦ powr p" for a b
    using x_plus_y_p_le_xp_plus_yp[OF ‹p > 0› ‹p ≤ 1›, of "¦a¦" "¦b¦"]
    by (auto, meson abs_ge_zero abs_triangle_ineq assms(1) le_less order.trans powr_mono2)
  show "integrable M (λx. ¦f x + g x¦ powr p)"
    by (rule Bochner_Integration.integrable_bound[of _ "λx. ¦f x¦ powr p + ¦g x¦ powr p"], auto simp add: *)

  have "(∫x. ¦f x + g x¦ powr p ∂M) powr (1/p) ≤ (∫x. ¦f x¦ powr p + ¦g x¦ powr p ∂M) powr (1/p)"
    by (rule powr_mono2, simp add: ‹p > 0› less_imp_le, simp, rule integral_mono', auto simp add: *)
  also have "... = 2 powr (1/p) * (((∫x. ¦f x¦ powr p ∂M) + (∫x. ¦g x¦ powr p ∂M)) / 2) powr (1/p)"
    by (auto simp add: powr_mult[symmetric] add_divide_distrib)
  also have "... ≤ 2 powr (1/p) * (((∫x. ¦f x¦ powr p ∂M) powr (1/p) + (∫x. ¦g x¦ powr p ∂M) powr (1/p)) / 2)"
    apply (rule mult_mono, simp, rule convex_on_mean_ineq[OF convex_powr[of "1/p"]])
    using ‹p ≤ 1› ‹p > 0› by auto
  also have "... = 2 powr (1/p - 1) * ((∫x. ¦f x¦ powr p ∂M) powr (1/p) + (∫x. ¦g x¦ powr p ∂M) powr (1/p))"
    by (simp add: powr_diff)
  finally show "(∫x. ¦f x + g x¦ powr p ∂M) powr (1/p)
      ≤ 2 powr (1/p-1) * (∫x. ¦f x¦ powr p ∂M) powr (1/p) + 2 powr (1/p-1) * (∫x. ¦g x¦ powr p ∂M) powr (1/p)"
    by (auto simp add: algebra_simps)
qed


section ‹$L^p$ spaces›

text ‹We define $L^p$ spaces by giving their defining quasinorm. It is a norm for $p\in [1, \infty]$,
and a quasinorm for $p \in (0,1)$. The construction of a quasinorm from a formula only makes sense
if this formula is indeed a quasinorm, i.e., it is homogeneous and satisfies the triangular
inequality with the given multiplicative defect. Thus, we have to show that this is indeed
the case to be able to use the definition.›

definition Lp_space::"ennreal ⇒ 'a measure ⇒ ('a ⇒ real) quasinorm"
  where "Lp_space p M = (
    if p = 0 then quasinorm_of (1, (λf. if (f ∈ borel_measurable M) then 0 else ∞))
    else if p < ∞ then quasinorm_of (
        if p < 1 then 2 powr (1/enn2real p - 1) else 1,
        (λf. if (f ∈ borel_measurable M ∧ integrable M (λx. ¦f x¦ powr (enn2real p)))
              then (∫x. ¦f x¦ powr (enn2real p) ∂M) powr (1/(enn2real p))
              else (∞::ennreal)))
    else quasinorm_of (1, (λf. if f ∈ borel_measurable M then esssup M (λx. ereal ¦f x¦) else (∞::ennreal))))"

abbreviation "𝔏 == Lp_space"


subsection ‹$L^\infty$›

text ‹Let us check that, for $L^\infty$, the above definition makes sense.›

lemma L_infinity:
  "eNorm (𝔏 ∞ M) f = (if f ∈ borel_measurable M then esssup M (λx. ereal ¦f x¦) else (∞::ennreal))"
  "defect (𝔏 ∞ M) = 1"
proof -
  have T: "esssup M (λx. ereal ¦(f + g) x¦) ≤ e2ennreal (esssup M (λx. ereal ¦f x¦)) + esssup M (λx. ereal ¦g x¦)"
    if [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M" for f g
  proof (cases "emeasure M (space M) = 0")
    case True
    then have "e2ennreal (esssup M (λx. ereal ¦(f + g) x¦)) = 0"
      using esssup_zero_space[OF True] by (simp add: e2ennreal_neg)
    then show ?thesis by simp
  next
    case False
    have *: "esssup M (λx. ¦h x¦) ≥ 0" for h::"'a ⇒ real"
    proof -
      have "esssup M (λx. 0) ≤ esssup M (λx. ¦h x¦)" by (rule esssup_mono, auto)
      then show ?thesis using esssup_const[OF False, of "0::ereal"] by simp
    qed
    have "esssup M (λx. ereal ¦(f + g) x¦) ≤ esssup M (λx. ereal ¦f x¦ + ereal ¦g x¦)"
      by (rule esssup_mono, auto simp add: plus_fun_def)
    also have "... ≤ esssup M (λx. ereal ¦f x¦) + esssup M (λx. ereal ¦g x¦)"
      by (rule esssup_add)
    finally show ?thesis
      using * by (simp add: e2ennreal_mono eq_onp_def plus_ennreal.abs_eq)
  qed

  have H: "esssup M (λx. ereal ¦(c *⇩R f) x¦) ≤ ennreal ¦c¦ * esssup M (λx. ereal ¦f x¦)" if "c ≠ 0" for f c
  proof -
    have "abs c > 0" "ereal ¦c¦ ≥ 0" using that by auto
    have *: "esssup M (λx. abs(c *⇩R f x)) = abs c * esssup M (λx. ¦f x¦)"
      apply (subst esssup_cmult[OF ‹abs c > 0›, of M "λx. ereal ¦f x¦", symmetric])
      using times_ereal.simps(1) by (auto simp add: abs_mult)
    show ?thesis
      unfolding e2ennreal_mult[OF ‹ereal ¦c¦ ≥ 0›] * scaleR_fun_def
      by simp
  qed

  have "esssup M (λx. ereal 0) ≤ 0" using esssup_I by auto
  then have Z: "e2ennreal (esssup M (λx. ereal 0)) = 0" using e2ennreal_neg by auto

  have *: "quasinorm_on (borel_measurable M) 1 (λ(f::'a⇒real). e2ennreal(esssup M (λx. ereal ¦f x¦)))"
    apply (rule quasinorm_onI) using T H Z by auto
  have **: "quasinorm_on UNIV 1 (λ(f::'a⇒real). if f ∈ borel_measurable M then e2ennreal(esssup M (λx. ereal ¦f x¦)) else ∞)"
    by (rule extend_quasinorm[OF *])
  show "eNorm (𝔏 ∞ M) f = (if f ∈ borel_measurable M then e2ennreal(esssup M (λx. ¦f x¦)) else ∞)"
       "defect (𝔏 ∞ M) = 1"
    unfolding Lp_space_def using quasinorm_of[OF **] by auto
qed

lemma L_infinity_space:
  "space⇩N (𝔏 ∞ M) = {f ∈ borel_measurable M. ∃C. AE x in M. ¦f x¦ ≤ C}"
proof (auto simp del: infinity_ennreal_def)
  fix f assume H: "f ∈ space⇩N (𝔏 ∞ M)"
  then show "f ∈ borel_measurable M"
    unfolding space⇩N_def using L_infinity(1)[of M] top.not_eq_extremum by fastforce
  then have *: "esssup M (λx. ¦f x¦) < ∞"
    using H unfolding space⇩N_def L_infinity(1)[of M] by (auto simp add: e2ennreal_infty)
  define C where "C = real_of_ereal(esssup M (λx. ¦f x¦))"
  have "AE x in M. ereal ¦f x¦ ≤ ereal C"
  proof (cases "emeasure M (space M) = 0")
    case True
    then show ?thesis using emeasure_0_AE by simp
  next
    case False
    then have "esssup M (λx. ¦f x¦) ≥ 0"
      using esssup_mono[of "λx. 0" M "(λx. ¦f x¦)"] esssup_const[OF False, of "0::ereal"] by auto
    then have "esssup M (λx. ¦f x¦) = ereal C" unfolding C_def using * ereal_real by auto
    then show ?thesis using esssup_AE[of "(λx. ereal ¦f x¦)" M] by simp
  qed
  then have "AE x in M. ¦f x¦ ≤ C" by auto
  then show "∃C. AE x in M. ¦f x¦ ≤ C" by blast
next
  fix f::"'a ⇒ real" and C::real
  assume H: "f ∈ borel_measurable M" "AE x in M. ¦f x¦ ≤ C"
  then have "esssup M (λx. ¦f x¦) ≤ C" using esssup_I by auto
  then have "eNorm (𝔏 ∞ M) f ≤ C" unfolding L_infinity(1) using H(1)
    by auto (metis e2ennreal_ereal e2ennreal_mono)
  then show "f ∈ space⇩N (𝔏 ∞ M)"
    using spaceN_iff le_less_trans by fastforce
qed

lemma L_infinity_zero_space:
  "zero_space⇩N (𝔏 ∞ M) = {f ∈ borel_measurable M. AE x in M. f x = 0}"
proof (auto simp del: infinity_ennreal_def)
  fix f assume H: "f ∈ zero_space⇩N (𝔏 ∞ M)"
  then show "f ∈ borel_measurable M"
    unfolding zero_space⇩N_def using L_infinity(1)[of M] top.not_eq_extremum by fastforce
  then have *: "e2ennreal(esssup M (λx. ¦f x¦)) = 0"
    using H unfolding zero_space⇩N_def using L_infinity(1)[of M] e2ennreal_infty by auto
  then have "esssup M (λx. ¦f x¦) ≤ 0"
    by (metis e2ennreal_infty e2ennreal_mult ennreal_top_neq_zero ereal_mult_infty leI linear mult_zero_left)
  then have "f x = 0" if "ereal ¦f x¦ ≤ esssup M (λx. ¦f x¦)" for x
    using that order.trans by fastforce
  then show "AE x in M. f x = 0" using esssup_AE[of "λx. ereal ¦f x¦" M] by auto
next
  fix f::"'a ⇒ real"
  assume H: "f ∈ borel_measurable M" "AE x in M. f x = 0"
  then have "esssup M (λx. ¦f x¦) ≤ 0" using esssup_I by auto
  then have "eNorm (𝔏 ∞ M) f = 0" unfolding L_infinity(1) using H(1)
    by (simp add: e2ennreal_neg)
  then show "f ∈ zero_space⇩N (𝔏 ∞ M)"
    using zero_spaceN_iff by auto
qed

lemma L_infinity_AE_ebound:
  "AE x in M. ennreal ¦f x¦ ≤ eNorm (𝔏 ∞ M) f"
proof (cases "f ∈ borel_measurable M")
  case False
  then have "eNorm (𝔏 ∞ M) f = ∞"
    unfolding L_infinity(1) by auto
  then show ?thesis by simp
next
  case True
  then have "ennreal ¦f x¦ ≤ eNorm (𝔏 ∞ M) f" if "¦f x¦ ≤ esssup M (λx. ¦f x¦)" for x
    unfolding L_infinity(1) using that e2ennreal_mono
    by fastforce
  then show ?thesis using esssup_AE[of "λx. ereal ¦f x¦"] by force
qed

lemma L_infinity_AE_bound:
  assumes "f ∈ space⇩N (𝔏 ∞ M)"
  shows "AE x in M. ¦f x¦ ≤ Norm (𝔏 ∞ M) f"
using L_infinity_AE_ebound[of f M] unfolding eNorm_Norm[OF assms] by (simp)

text ‹In the next lemma, the assumption $C \geq 0$ that might seem useless is in fact
necessary for the second statement when the space has zero measure. Indeed, any function is
then almost surely bounded by any constant!›

lemma L_infinity_I:
  assumes "f ∈ borel_measurable M"
          "AE x in M. ¦f x¦ ≤ C"
          "C ≥ 0"
  shows "f ∈ space⇩N (𝔏 ∞ M)"
        "Norm (𝔏 ∞ M) f ≤ C"
proof -
  show "f ∈ space⇩N (𝔏 ∞ M)"
    using L_infinity_space assms(1) assms(2) by force
  have "esssup M (λx. ¦f x¦) ≤ C" using assms(1) assms(2) esssup_I by auto
  then have "eNorm (𝔏 ∞ M) f ≤ ereal C"
    unfolding L_infinity(1) using assms(1) e2ennreal_mono by force
  then have "ennreal (Norm (𝔏 ∞ M) f) ≤ ennreal C"
    using eNorm_Norm[OF ‹f ∈ space⇩N (𝔏 ∞ M)›] assms(3) by auto
  then show "Norm (𝔏 ∞ M) f ≤ C" using assms(3) by auto
qed

lemma L_infinity_I':
  assumes [measurable]: "f ∈ borel_measurable M"
      and "AE x in M. ennreal ¦f x¦ ≤ C"
  shows "eNorm (𝔏 ∞ M) f ≤ C"
proof -
  have "esssup M (λx. ¦f x¦) ≤ enn2ereal C"
    apply (rule esssup_I, auto) using assms(2) less_eq_ennreal.rep_eq by auto
  then show ?thesis unfolding L_infinity using assms apply auto
    using e2ennreal_mono by fastforce
qed

lemma L_infinity_pos_measure:
  assumes [measurable]: "f ∈ borel_measurable M"
      and "eNorm (𝔏 ∞ M) f > (C::real)"
  shows "emeasure M {x ∈ space M. ¦f x¦ > C} > 0"
proof -
  have *: "esssup M (λx. ereal(¦f x¦)) > ereal C" using ‹eNorm (𝔏 ∞ M) f > C› unfolding L_infinity
  proof (auto)
    assume a1: "ennreal C < e2ennreal (esssup M (λx. ereal ¦f x¦))"
    have "¬ e2ennreal (esssup M (λa. ereal ¦f a¦)) ≤ e2ennreal (ereal C)" if "¬ C < 0"
      using a1 that by (metis (no_types) e2ennreal_enn2ereal enn2ereal_ennreal leD leI)
    then have "e2ennreal (esssup M (λa. ereal ¦f a¦)) ≤ e2ennreal (ereal C) ⟶ (∃e≤esssup M (λa. ereal ¦f a¦). ereal C < e)"
      using a1 e2ennreal_neg by fastforce
    then show ?thesis
      by (meson e2ennreal_mono leI less_le_trans)
  qed
  have "emeasure M {x ∈ space M. ereal(¦f x¦) > C} > 0"
    by (rule esssup_pos_measure[OF _ *], auto)
  then show ?thesis by auto
qed

lemma L_infinity_tendsto_AE:
  assumes "tendsto_in⇩N (𝔏 ∞ M) f g"
          "⋀n. f n ∈ space⇩N (𝔏 ∞ M)"
          "g ∈ space⇩N (𝔏 ∞ M)"
  shows "AE x in M. (λn. f n x) ⇢ g x"
proof -
  have *: "AE x in M. ¦(f n - g) x¦ ≤ Norm (𝔏 ∞ M) (f n - g)" for n
    apply (rule L_infinity_AE_bound) using assms spaceN_diff by blast
  have "AE x in M. ∀n. ¦(f n - g) x¦ ≤ Norm (𝔏 ∞ M) (f n - g)"
    apply (subst AE_all_countable) using * by auto
  moreover have "(λn. f n x) ⇢ g x" if "∀n. ¦(f n - g) x¦ ≤ Norm (𝔏 ∞ M) (f n - g)" for x
  proof -
    have "(λn. ¦(f n - g) x¦) ⇢ 0"
      apply (rule tendsto_sandwich[of "λn. 0" _ _ "λn. Norm (𝔏 ∞ M) (f n - g)"])
      using that ‹tendsto_in⇩N (𝔏 ∞ M) f g› unfolding tendsto_in⇩N_def by auto
    then have "(λn. ¦f n x - g x¦) ⇢ 0" by auto
    then show ?thesis
      by (simp add: ‹(λn. ¦f n x - g x¦) ⇢ 0› LIM_zero_cancel tendsto_rabs_zero_cancel)
  qed
  ultimately show ?thesis by auto
qed

text ‹As an illustration of the mechanism of spaces inclusion, let us show that bounded
continuous functions belong to $L^\infty$.›

lemma bcontfun_subset_L_infinity:
  assumes "sets M = sets borel"
  shows "space⇩N bcontfun⇩N ⊆ space⇩N (𝔏 ∞ M)"
        "⋀f. f ∈ space⇩N bcontfun⇩N ⟹ Norm (𝔏 ∞ M) f ≤ Norm bcontfun⇩N f"
        "⋀f. eNorm (𝔏 ∞ M) f ≤ eNorm bcontfun⇩N f"
        "bcontfun⇩N ⊆⇩N 𝔏 ∞ M"
proof -
  have *: "f ∈ space⇩N (𝔏 ∞ M) ∧ Norm (𝔏 ∞ M) f ≤ Norm bcontfun⇩N f" if "f ∈ space⇩N bcontfun⇩N" for f
  proof -
    have H: "continuous_on UNIV f" "⋀x. abs(f x) ≤ Norm bcontfun⇩N f"
      using bcontfun⇩ND[OF ‹f ∈ space⇩N bcontfun⇩N›] by auto
    then have "f ∈ borel_measurable borel" using borel_measurable_continuous_onI by simp
    then have "f ∈ borel_measurable M" using assms by auto
    have *: "AE x in M. ¦f x¦ ≤ Norm bcontfun⇩N f" using H(2) by auto
    show ?thesis using L_infinity_I[OF ‹f ∈ borel_measurable M› * Norm_nonneg] by auto
  qed
  show "space⇩N bcontfun⇩N ⊆ space⇩N (𝔏 ∞ M)"
       "⋀f. f ∈ space⇩N bcontfun⇩N ⟹ Norm (𝔏 ∞ M) f ≤ Norm bcontfun⇩N f"
    using * by auto
  show **: "bcontfun⇩N ⊆⇩N 𝔏 ∞ M"
    apply (rule quasinorm_subsetI'[of _ _ 1]) using * by auto
  have "eNorm (𝔏 ∞ M) f ≤ ennreal 1 * eNorm bcontfun⇩N f" for f
    apply (rule quasinorm_subset_Norm_eNorm) using * ** by auto
  then show "eNorm (𝔏 ∞ M) f ≤ eNorm bcontfun⇩N f" for f by simp
qed


subsection ‹$L^p$ for $0 < p < \infty$›

lemma Lp:
  assumes "p ≥ (1::real)"
  shows "eNorm (𝔏 p M) f = (if (f ∈ borel_measurable M ∧ integrable M (λx. ¦f x¦ powr p))
                            then (∫x. ¦f x¦ powr p ∂M) powr (1/p)
                            else (∞::ennreal))"
        "defect (𝔏 p M) = 1"
proof -
  define F where "F = {f ∈ borel_measurable M. integrable M (λx. ¦f x¦ powr p)}"
  have *: "quasinorm_on F 1 (λ(f::'a⇒real). (∫x. ¦f x¦ powr p ∂M) powr (1/p))"
  proof (rule quasinorm_onI)
    fix f g assume "f ∈ F" "g ∈ F"
    then show "f + g ∈ F"
      unfolding F_def plus_fun_def apply (auto) by (rule Minkowski_inequality(1), auto simp add: ‹p ≥ 1›)
    show "ennreal ((∫x. ¦(f + g) x¦ powr p ∂M) powr (1/p))
          ≤ ennreal 1 * (∫x. ¦f x¦ powr p ∂M) powr (1/p) + ennreal 1 * (∫x. ¦g x¦ powr p ∂M) powr (1/p)"
      apply (auto, subst ennreal_plus[symmetric], simp, simp, rule ennreal_leI)
      unfolding plus_fun_def apply (rule Minkowski_inequality(2)[of p f M g], auto simp add: ‹p ≥ 1›)
      using ‹f ∈ F› ‹g ∈ F› unfolding F_def by auto
  next
    fix f and c::real assume "f ∈ F"
    show "c *⇩R f ∈ F" using ‹f ∈ F› unfolding scaleR_fun_def F_def by (auto simp add: abs_mult powr_mult)
    show "(∫x. ¦(c *⇩R f) x¦ powr p ∂M) powr (1/p) ≤ ennreal(abs(c)) * (∫x. ¦f x¦ powr p ∂M) powr (1/p)"
      apply (rule eq_refl, subst ennreal_mult[symmetric], simp, simp, rule ennreal_cong)
      apply (unfold scaleR_fun_def, simp add: abs_mult powr_mult powr_powr) using ‹p ≥ 1› by auto
  next
    show "0 ∈ F" unfolding zero_fun_def F_def by auto
  qed (auto)

  have "p ≥ 0" using ‹p ≥ 1› by auto
  have **: "𝔏 p M = quasinorm_of (1,
              (λf. if (f ∈ borel_measurable M ∧ integrable M (λx. ¦f x¦ powr p))
              then (∫x. ¦f x¦ powr p ∂M) powr (1/p)
              else (∞::ennreal)))"
    unfolding Lp_space_def using enn2real_ennreal[OF ‹p ≥ 0›] ‹p ≥ 1› apply auto
    using enn2real_ennreal[OF ‹p ≥ 0›] by presburger
  show "eNorm (𝔏 p M) f = (if (f ∈ borel_measurable M ∧ integrable M (λx. ¦f x¦ powr p))
                            then (∫x. ¦f x¦ powr p ∂M) powr (1/p)
                            else (∞::ennreal))"
      "defect (𝔏 p M) = 1"
    unfolding ** using quasinorm_of[OF extend_quasinorm[OF *]] unfolding F_def by auto
qed

lemma Lp_le_1:
  assumes "p > 0" "p ≤ (1::real)"
  shows "eNorm (𝔏 p M) f = (if (f ∈ borel_measurable M ∧ integrable M (λx. ¦f x¦ powr p))
                            then (∫x. ¦f x¦ powr p ∂M) powr (1/p)
                            else (∞::ennreal))"
        "defect (𝔏 p M) = 2 powr (1/p - 1)"
proof -
  define F where "F = {f ∈ borel_measurable M. integrable M (λx. ¦f x¦ powr p)}"
  have *: "quasinorm_on F (2 powr (1/p-1)) (λ(f::'a⇒real). (∫x. ¦f x¦ powr p ∂M) powr (1/p))"
  proof (rule quasinorm_onI)
    fix f g assume "f ∈ F" "g ∈ F"
    then show "f + g ∈ F"
      unfolding F_def plus_fun_def apply (auto) by (rule Minkowski_inequality_le_1(1), auto simp add: ‹p > 0› ‹p ≤ 1›)
    show "ennreal ((∫x. ¦(f + g) x¦ powr p ∂M) powr (1/p))
          ≤ ennreal (2 powr (1/p-1)) * (∫x. ¦f x¦ powr p ∂M) powr (1/p) + ennreal (2 powr (1/p-1)) * (∫x. ¦g x¦ powr p ∂M) powr (1/p)"
      apply (subst ennreal_mult[symmetric], auto)+
      apply (subst ennreal_plus[symmetric], simp, simp)
      apply (rule ennreal_leI)
      unfolding plus_fun_def apply (rule Minkowski_inequality_le_1(2)[of p f M g], auto simp add: ‹p > 0› ‹p ≤ 1›)
      using ‹f ∈ F› ‹g ∈ F› unfolding F_def by auto
  next
    fix f and c::real assume "f ∈ F"
    show "c *⇩R f ∈ F" using ‹f ∈ F› unfolding scaleR_fun_def F_def by (auto simp add: abs_mult powr_mult)
    show "(∫x. ¦(c *⇩R f) x¦ powr p ∂M) powr (1/p) ≤ ennreal(abs(c)) * (∫x. ¦f x¦ powr p ∂M) powr (1/p)"
      apply (rule eq_refl, subst ennreal_mult[symmetric], simp, simp, rule ennreal_cong)
      apply (unfold scaleR_fun_def, simp add: abs_mult powr_mult powr_powr) using ‹p > 0› by auto
  next
    show "0 ∈ F" unfolding zero_fun_def F_def by auto
    show "1 ≤ 2 powr (1 / p - 1)" using ‹p > 0› ‹p ≤ 1› by (auto simp add: ge_one_powr_ge_zero)
  qed (auto)

  have "p ≥ 0" using ‹p > 0› by auto
  have **: "𝔏 p M = quasinorm_of (2 powr (1/p-1),
              (λf. if (f ∈ borel_measurable M ∧ integrable M (λx. ¦f x¦ powr p))
              then (∫x. ¦f x¦ powr p ∂M) powr (1/p)
              else (∞::ennreal)))"
    unfolding Lp_space_def using ‹p > 0› ‹p ≤ 1› using enn2real_ennreal[OF ‹p ≥ 0›] apply auto
    by (insert enn2real_ennreal[OF ‹p ≥ 0›], presburger)+
  show "eNorm (𝔏 p M) f = (if (f ∈ borel_measurable M ∧ integrable M (λx. ¦f x¦ powr p))
                            then (∫x. ¦f x¦ powr p ∂M) powr (1/p)
                            else (∞::ennreal))"
      "defect (𝔏 p M) = 2 powr (1/p-1)"
    unfolding ** using quasinorm_of[OF extend_quasinorm[OF *]] unfolding F_def by auto
qed

lemma Lp_space:
  assumes "p > (0::real)"
  shows "space⇩N (𝔏 p M) = {f ∈ borel_measurable M. integrable M (λx. ¦f x¦ powr p)}"
apply (auto simp add: spaceN_iff)
using Lp(1) Lp_le_1(1) ‹p > 0› apply (metis infinity_ennreal_def less_le not_less)
using Lp(1) Lp_le_1(1) ‹p > 0› apply (metis infinity_ennreal_def less_le not_less)
using Lp(1) Lp_le_1(1) ‹p > 0› by (metis ennreal_neq_top linear top.not_eq_extremum)

lemma Lp_I:
  assumes "p > (0::real)"
          "f ∈ borel_measurable M" "integrable M (λx. ¦f x¦ powr p)"
  shows "f ∈ space⇩N (𝔏 p M)"
        "Norm (𝔏 p M) f = (∫x. ¦f x¦ powr p ∂M) powr (1/p)"
        "eNorm (𝔏 p M) f = (∫x. ¦f x¦ powr p ∂M) powr (1/p)"
proof -
  have *: "eNorm (𝔏 p M) f = (∫x. ¦f x¦ powr p ∂M) powr (1/p)"
    by (cases "p ≤ 1", insert assms, auto simp add: Lp_le_1(1) Lp(1))
  then show **: "f ∈ space⇩N (𝔏 p M)" unfolding space⇩N_def by auto
  show "Norm (𝔏 p M) f = (∫x. ¦f x¦ powr p ∂M) powr (1/p)" using * unfolding Norm_def by auto
  then show "eNorm (𝔏 p M) f = (∫x. ¦f x¦ powr p ∂M) powr (1/p)" using eNorm_Norm[OF **] by auto
qed

lemma Lp_D:
  assumes "p>0" "f ∈ space⇩N (𝔏 p M)"
  shows "f ∈ borel_measurable M"
        "integrable M (λx. ¦f x¦ powr p)"
        "Norm (𝔏 p M) f = (∫x. ¦f x¦ powr p ∂M) powr (1/p)"
        "eNorm (𝔏 p M) f = (∫x. ¦f x¦ powr p ∂M) powr (1/p)"
proof -
  show *: "f ∈ borel_measurable M"
          "integrable M (λx. ¦f x¦ powr p)"
    using Lp_space[OF ‹p > 0›] assms(2) by auto
  then show "Norm (𝔏 p M) f = (∫x. ¦f x¦ powr p ∂M) powr (1/p)"
            "eNorm (𝔏 p M) f = (∫x. ¦f x¦ powr p ∂M) powr (1/p)"
    using Lp_I[OF ‹p > 0›] by auto
qed

lemma Lp_Norm:
  assumes "p > (0::real)"
          "f ∈ borel_measurable M"
  shows "Norm (𝔏 p M) f = (∫x. ¦f x¦ powr p ∂M) powr (1/p)"
        "(Norm (𝔏 p M) f) powr p = (∫x. ¦f x¦ powr p ∂M)"
proof -
  show *: "Norm (𝔏 p M) f = (∫x. ¦f x¦ powr p ∂M) powr (1/p)"
  proof (cases "integrable M (λx. ¦f x¦ powr p)")
    case True
    then show ?thesis using Lp_I[OF assms True] by auto
  next
    case False
    then have "f ∉ space⇩N (𝔏 p M)" using Lp_space[OF ‹p > 0›, of M] by auto
    then have *: "Norm (𝔏 p M) f = 0" using eNorm_Norm' by auto
    have "(∫x. ¦f x¦ powr p ∂M) = 0" using False by (simp add: not_integrable_integral_eq)
    then have "(∫x. ¦f x¦ powr p ∂M) powr (1/p) = 0" by auto
    then show ?thesis using * by auto
  qed
  then show "(Norm (𝔏 p M) f) powr p = (∫x. ¦f x¦ powr p ∂M)"
    unfolding * using powr_powr ‹p > 0› by auto
qed

lemma Lp_zero_space:
  assumes "p > (0::real)"
  shows "zero_space⇩N (𝔏 p M) = {f ∈ borel_measurable M. AE x in M. f x = 0}"
proof (auto)
  fix f assume H: "f ∈ zero_space⇩N (𝔏 p M)"
  then have *: "f ∈ {f ∈ borel_measurable M. integrable M (λx. ¦f x¦ powr p)}"
    using Lp_space[OF assms] zero_spaceN_subset_spaceN by auto
  then show "f ∈ borel_measurable M" by auto
  have "eNorm (𝔏 p M) f = (∫x. ¦f x¦ powr p ∂M) powr (1/p)"
    by (cases "p ≤ 1", insert * ‹p > 0›, auto simp add: Lp_le_1(1) Lp(1))
  then have "(∫x. ¦f x¦ powr p ∂M) = 0" using H unfolding zero_space⇩N_def by auto
  then have "AE x in M. ¦f x¦ powr p = 0"
    by (subst integral_nonneg_eq_0_iff_AE[symmetric], insert *, auto)
  then show "AE x in M. f x = 0" by auto
next
  fix f::"'a ⇒ real"
  assume H [measurable]: "f ∈ borel_measurable M" "AE x in M. f x = 0"
  then have *: "AE x in M. ¦f x¦ powr p = 0" by auto
  have "integrable M (λx. ¦f x¦ powr p)"
    using integrable_cong_AE[OF _ _ *] by auto
  have **: "(∫x. ¦f x¦ powr p ∂M) = 0"
    using integral_cong_AE[OF _ _ *] by auto
  have "eNorm (𝔏 p M) f = (∫x. ¦f x¦ powr p ∂M) powr (1/p)"
    by (cases "p ≤ 1", insert H(1) ‹integrable M (λx. ¦f x¦ powr p)› ‹p > 0›, auto simp add: Lp_le_1(1) Lp(1))
  then have "eNorm (𝔏 p M) f = 0" using ** by simp
  then show "f ∈ zero_space⇩N (𝔏 p M)"
    using zero_spaceN_iff by auto
qed

lemma Lp_tendsto_AE_subseq:
  assumes "p>(0::real)"
          "tendsto_in⇩N (𝔏 p M) f g"
          "⋀n. f n ∈ space⇩N (𝔏 p M)"
          "g ∈ space⇩N (𝔏 p M)"
  shows "∃r. strict_mono r ∧ (AE x in M. (λn. f (r n) x) ⇢ g x)"
proof -
  have "f n - g ∈ space⇩N (𝔏 p M)" for n
    using spaceN_diff[OF ‹⋀n. f n ∈ space⇩N (𝔏 p M)› ‹g ∈ space⇩N (𝔏 p M)›] by simp
  have int: "integrable M (λx. ¦f n x - g x¦ powr p)" for n
    using Lp_D(2)[OF ‹p > 0› ‹f n - g ∈ space⇩N (𝔏 p M)›] by auto

  have "(λn. Norm (𝔏 p M) (f n - g)) ⇢ 0"
    using ‹tendsto_in⇩N (𝔏 p M) f g› unfolding tendsto_in⇩N_def by auto
  then have *: "(λn. (∫x. ¦f n x - g x¦ powr p ∂M) powr (1/p)) ⇢ 0"
    using Lp_D(3)[OF ‹p > 0› ‹⋀n. f n - g ∈ space⇩N (𝔏 p M)›] by auto
  have "(λn. ((∫x. ¦f n x - g x¦ powr p ∂M) powr (1/p)) powr p) ⇢ 0"
    apply (rule tendsto_zero_powrI[of _ _ _ p]) using ‹p > 0› * by auto
  then have **: "(λn. (∫x. ¦f n x - g x¦ powr p ∂M)) ⇢ 0"
    using powr_powr ‹p > 0› by auto
  have "∃r. strict_mono r ∧ (AE x in M. (λn. ¦f (r n) x - g x¦ powr p) ⇢ 0)"
    apply (rule tendsto_L1_AE_subseq) using int ** by auto
  then obtain r where "strict_mono r" "AE x in M. (λn. ¦f (r n) x - g x¦ powr p) ⇢ 0"
    by blast
  moreover have "(λn. f (r n) x) ⇢ g x" if "(λn. ¦f (r n) x - g x¦ powr p) ⇢ 0" for x
  proof -
    have "(λn. (¦f (r n) x - g x¦ powr p) powr (1/p)) ⇢ 0"
      apply (rule tendsto_zero_powrI[of _ _ _ "1/p"]) using ‹p > 0› that by auto
    then have "(λn. ¦f (r n) x - g x¦) ⇢ 0"
      using powr_powr ‹p > 0› by auto
    show ?thesis
      by (simp add: ‹(λn. ¦f (r n) x - g x¦) ⇢ 0› Limits.LIM_zero_cancel tendsto_rabs_zero_cancel)
  qed
  ultimately have "AE x in M. (λn. f (r n) x) ⇢ g x" by auto
  then show ?thesis using ‹strict_mono r› by auto
qed

subsection ‹Specialization to $L^1$›

lemma L1_space:
  "space⇩N (𝔏 1 M) = {f. integrable M f}"
unfolding one_ereal_def using Lp_space[of 1 M] integrable_abs_iff by auto

lemma L1_I:
  assumes "integrable M f"
  shows "f ∈ space⇩N (𝔏 1 M)"
        "Norm (𝔏 1 M) f = (∫x. ¦f x¦ ∂M)"
        "eNorm (𝔏 1 M) f = (∫x. ¦f x¦ ∂M)"
unfolding one_ereal_def using Lp_I[of 1, OF _ borel_measurable_integrable[OF assms]] assms powr_to_1 by auto

lemma L1_D:
  assumes "f ∈ space⇩N (𝔏 1 M)"
  shows "f ∈ borel_measurable M"
        "integrable M f"
        "Norm (𝔏 1 M) f = (∫x. ¦f x¦ ∂M)"
        "eNorm (𝔏 1 M) f = (∫x. ¦f x¦ ∂M)"
  using assms by (auto simp add: L1_space L1_I)

lemma L1_int_ineq:
  "abs(∫x. f x ∂M) ≤ Norm (𝔏 1 M) f"
proof (cases "integrable M f")
  case True
  then show ?thesis using L1_I(2)[OF True] by auto
next
  case False
  then have "(∫x. f x ∂M) = 0" by (simp add: not_integrable_integral_eq)
  then show ?thesis using Norm_nonneg by auto
qed

text ‹In $L^1$, one can give a direct formula for the eNorm of a measurable function, using a
nonnegative integral. The same formula holds in $L^p$ for $p > 0$, with additional powers $p$ and
$1/p$, but one can not write it down since \verb+powr+ is not defined on \verb+ennreal+.›

lemma L1_Norm:
  assumes [measurable]: "f ∈ borel_measurable M"
  shows "Norm (𝔏 1 M) f = (∫x. ¦f x¦ ∂M)"
        "eNorm (𝔏 1 M) f = (∫⇧+x. ¦f x¦ ∂M)"
proof -
  show *: "Norm (𝔏 1 M) f = (∫x. ¦f x¦ ∂M)"
    using Lp_Norm[of 1, OF _ assms] unfolding one_ereal_def by auto
  show "eNorm (𝔏 1 M) f = (∫⇧+x. ¦f x¦ ∂M)"
  proof (cases "integrable M f")
    case True
    then have "f ∈ space⇩N (𝔏 1 M)" using L1_space by auto
    then have "eNorm (𝔏 1 M) f = ennreal (Norm (𝔏 1 M) f)"
      using eNorm_Norm by auto
    then show ?thesis
      by (metis (mono_tags) * AE_I2 True abs_ge_zero integrable_abs nn_integral_eq_integral)
  next
    case False
    then have "eNorm (𝔏 1 M) f = ∞" using L1_space space⇩N_def
      by (metis ennreal_add_eq_top infinity_ennreal_def le_iff_add le_less_linear mem_Collect_eq)
    moreover have "(∫⇧+x. ¦f x¦ ∂M) = ∞"
      apply (rule nn_integral_nonneg_infinite) using False by (auto simp add: integrable_abs_iff)
    ultimately show ?thesis by simp
  qed
qed

lemma L1_indicator:
  assumes [measurable]: "A ∈ sets M"
  shows "eNorm (𝔏 1 M) (indicator A) = emeasure M A"
by (subst L1_Norm, auto, metis assms ennreal_indicator nn_integral_cong nn_integral_indicator)

lemma L1_indicator':
  assumes [measurable]: "A ∈ sets M"
      and "emeasure M A ≠ ∞"
  shows "indicator A ∈ space⇩N (𝔏 1 M)"
        "Norm (𝔏 1 M) (indicator A) = measure M A"
unfolding space⇩N_def Norm_def using L1_indicator[OF ‹A ∈ sets M›] ‹emeasure M A ≠ ∞›
by (auto simp add: top.not_eq_extremum Sigma_Algebra.measure_def)


subsection ‹$L^0$›

text ‹We have defined $L^p$ for all exponents $p$, although it does not really make sense for $p = 0$.
We have chosen a definition in this case (the space of all measurable functions) so that many
statements are true for all exponents. In this paragraph, we show the consistency of this definition.›

lemma L_zero:
  "eNorm (𝔏 0 M) f = (if f ∈ borel_measurable M then 0 else ∞)"
  "defect (𝔏 0 M) = 1"
proof -
  have *: "quasinorm_on UNIV 1 (λ(f::'a⇒real). (if f ∈ borel_measurable M then 0 else ∞))"
    by (rule extend_quasinorm, rule quasinorm_onI, auto)
  show "eNorm (𝔏 0 M) f = (if f ∈ borel_measurable M then 0 else ∞)"
       "defect (𝔏 0 M) = 1"
    using quasinorm_of[OF *] unfolding Lp_space_def by auto
qed

lemma L_zero_space [simp]:
  "space⇩N (𝔏 0 M) = borel_measurable M"
  "zero_space⇩N (𝔏 0 M) = borel_measurable M"
apply (auto simp add: spaceN_iff zero_spaceN_iff L_zero(1))
using top.not_eq_extremum by force+

subsection ‹Basic results on $L^p$ for general $p$›

lemma Lp_measurable_subset:
  "space⇩N (𝔏 p M) ⊆ borel_measurable M"
proof (cases rule: Lp_cases[of p])
  case zero
  then show ?thesis using L_zero_space by auto
next
  case (real_pos p2)
  then show ?thesis using Lp_space[OF ‹p2 > 0›] by auto
next
  case PInf
  then show ?thesis using L_infinity_space by auto
qed

lemma Lp_measurable:
  assumes "f ∈ space⇩N (𝔏 p M)"
  shows "f ∈ borel_measurable M"
using assms Lp_measurable_subset by auto

lemma Lp_infinity_zero_space:
  assumes "p > (0::ennreal)"
  shows "zero_space⇩N (𝔏 p M) = {f ∈ borel_measurable M. AE x in M. f x = 0}"
proof (cases rule: Lp_cases[of p])
  case PInf
  then show ?thesis using L_infinity_zero_space by auto
next
  case (real_pos p2)
  then show ?thesis using Lp_zero_space[OF ‹p2 > 0›] unfolding ‹p = ennreal p2› by auto
next
  case zero
  then have False using assms by auto
  then show ?thesis by simp
qed

lemma (in prob_space) Lp_subset_Lq:
  assumes "p ≤ q"
  shows "⋀f. eNorm (𝔏 p M) f ≤ eNorm (𝔏 q M) f"
        "𝔏 q M ⊆⇩N 𝔏 p M"
        "space⇩N (𝔏 q M) ⊆ space⇩N (𝔏 p M)"
        "⋀f. f ∈ space⇩N (𝔏 q M) ⟹ Norm (𝔏 p M) f ≤ Norm (𝔏 q M) f"
proof -
  show "eNorm (𝔏 p M) f ≤ eNorm (𝔏 q M) f" for f
  proof (cases "eNorm (𝔏 q M) f < ∞")
    case True
    then have "f ∈ space⇩N (𝔏 q M)" using spaceN_iff by auto
    then have f_meas [measurable]: "f ∈ borel_measurable M" using Lp_measurable by auto
    consider "p = 0" | "p = q" | "p > 0 ∧ p < ∞ ∧ q = ∞" | "p > 0 ∧ p < q ∧ q < ∞"
      using ‹p ≤ q› apply (simp add: top.not_eq_extremum)
      using not_less_iff_gr_or_eq order.order_iff_strict by fastforce
    then show ?thesis
    proof (cases)
      case 1
      then show ?thesis by (simp add: L_zero(1))
    next
      case 2
      then show ?thesis by auto
    next
      case 3
      then have "q = ∞" by simp
      obtain p2 where "p = ennreal p2" "p2 > 0"
        using 3 enn2real_positive_iff[of p] by (cases p) auto
      have *: "AE x in M. ¦f x¦ ≤ Norm (𝔏 ∞ M) f"
        using L_infinity_AE_bound ‹f ∈ space⇩N (𝔏 q M)› ‹q = ∞› by auto
      have **: "integrable M (λx. ¦f x¦ powr p2)"
        apply (rule Bochner_Integration.integrable_bound[of _ "λx. (Norm (𝔏 ∞ M) f) powr p2"], auto)
        using * powr_mono2 ‹p2 > 0› by force
      then have "eNorm (𝔏 p2 M) f = (∫x. ¦f x¦ powr p2 ∂M) powr (1/p2)"
        using Lp_I(3)[OF ‹p2 > 0› f_meas] by simp
      also have "... ≤ (∫x. (Norm (𝔏 ∞ M) f) powr p2 ∂M) powr (1/p2)"
        apply (rule ennreal_leI, rule powr_mono2, simp add: ‹p2 > 0› less_imp_le, simp)
        apply (rule integral_mono_AE, auto simp add: **)
        using * powr_mono2 ‹p2 > 0› by force
      also have "... = Norm (𝔏 ∞ M) f"
        using ‹p2 > 0› by (auto simp add: prob_space powr_powr)
      finally show ?thesis
        using ‹p = ennreal p2› ‹q = ∞› eNorm_Norm[OF ‹f ∈ space⇩N (𝔏 q M)›] by auto
    next
      case 4
      then have "0 < p" "p < ∞" by auto
      then obtain p2 where "p = ennreal p2" "p2 > 0"
        using enn2real_positive_iff[of p] by (cases p) auto
      have "0 < q" "q < ∞" using 4 by auto
      then obtain q2 where "q = ennreal q2" "q2 > 0"
        using enn2real_positive_iff[of q] by (cases q) auto
      have "p2 < q2" using 4 ‹p = ennreal p2› ‹q = ennreal q2›
        using ennreal_less_iff by auto
      define r2 where "r2 = q2 / p2"
      have "r2 ≥ 1" unfolding r2_def using ‹p2 < q2› ‹p2 > 0› by auto
      have *: "abs (¦z¦ powr p2) powr r2 = ¦z¦ powr q2" for z::real
        unfolding r2_def using ‹p2 > 0› by (simp add: powr_powr)
      have I: "integrable M (λx. abs(¦f x¦ powr p2) powr r2)"
        unfolding * using ‹f ∈ space⇩N (𝔏 q M)› ‹q = ennreal q2› Lp_D(2)[OF ‹q2 > 0›] by auto
      have J: "integrable M (λx. ¦f x¦ powr p2)"
        by (rule bound_L1_Lp(1)[OF ‹r2 ≥ 1› _ I], auto)
      have "f ∈ space⇩N (𝔏 p2 M)"
        by (rule Lp_I(1)[OF ‹p2 > 0› _ J], simp)
      have "(∫x. ¦f x¦ powr p2 ∂M) powr (1/p2) = abs(∫x. ¦f x¦ powr p2 ∂M) powr (1/p2)"
        by auto
      also have "... ≤ ((∫x. abs (¦f x¦ powr p2) powr r2 ∂M) powr (1/r2)) powr (1/p2)"
        apply (subst powr_mono2, simp add: ‹p2 > 0› less_imp_le, simp)
        apply (rule bound_L1_Lp, simp add: ‹r2 ≥ 1›, simp)
        unfolding * using ‹f ∈ space⇩N (𝔏 q M)› ‹q = ennreal q2› Lp_D(2)[OF ‹q2 > 0›] by auto
      also have "... = (∫x. ¦f x¦ powr q2 ∂M) powr (1/q2)"
        unfolding * using ‹p2 > 0› by (simp add: powr_powr r2_def)
      finally show ?thesis
        using ‹f ∈ space⇩N (𝔏 q M)› Lp_D(4)[OF ‹q2 > 0›] ennreal_leI
        unfolding ‹p = ennreal p2› ‹q = ennreal q2› Lp_D(4)[OF ‹p2 > 0› ‹f ∈ space⇩N (𝔏 p2 M)›] by force
    qed
  next
    case False
    then have "eNorm (𝔏 q M) f = ∞"
      using top.not_eq_extremum by fastforce
    then show ?thesis by auto
  qed
  then show "𝔏 q M ⊆⇩N 𝔏 p M" using quasinorm_subsetI[of _ _ 1] by auto
  then show "space⇩N (𝔏 q M) ⊆ space⇩N (𝔏 p M)" using quasinorm_subset_space by auto
  then show "Norm (𝔏 p M) f ≤ Norm (𝔏 q M) f" if "f ∈ space⇩N (𝔏 q M)" for f
    using eNorm_Norm that ‹eNorm (𝔏 p M) f ≤ eNorm (𝔏 q M) f› ennreal_le_iff Norm_nonneg
    by (metis rev_subsetD)
qed

proposition Lp_domination:
  assumes [measurable]: "g ∈ borel_measurable M"
      and "f ∈ space⇩N (𝔏 p M)"
          "AE x in M. ¦g x¦ ≤ ¦f x¦"
  shows "g ∈ space⇩N (𝔏 p M)"
        "Norm (𝔏 p M) g ≤ Norm (𝔏 p M) f"
proof -
  have [measurable]: "f ∈ borel_measurable M" using Lp_measurable[OF assms(2)] by simp
  have "g ∈ space⇩N (𝔏 p M) ∧ Norm (𝔏 p M) g ≤ Norm (𝔏 p M) f"
  proof (cases rule: Lp_cases[of p])
    case zero
    then have "Norm (𝔏 p M) g = 0"
      unfolding Norm_def using L_zero(1)[of M] by auto
    then have "Norm (𝔏 p M) g ≤ Norm (𝔏 p M) f" using Norm_nonneg by auto
    then show ?thesis unfolding ‹p = 0› L_zero_space by auto
  next
    case (real_pos p2)
    have *: "integrable M (λx. ¦f x¦ powr p2)"
      using ‹f ∈ space⇩N (𝔏 p M)› unfolding ‹p = ennreal p2› using Lp_D(2) ‹p2 > 0› by auto
    have **: "integrable M (λx. ¦g x¦ powr p2)"
      apply (rule Bochner_Integration.integrable_bound[of _ "λx. ¦f x¦ powr p2"]) using * apply auto
      using assms(3) powr_mono2 ‹p2 > 0› by (auto simp add: less_imp_le)
    then have "g ∈ space⇩N (𝔏 p M)"
      unfolding ‹p = ennreal p2› using Lp_space[OF ‹p2 > 0›, of M] by auto
    have "Norm (𝔏 p M) g = (∫x. ¦g x¦ powr p2 ∂M) powr (1/p2)"
      unfolding ‹p = ennreal p2› by (rule Lp_I(2)[OF ‹p2 > 0› _ **], simp)
    also have "... ≤ (∫x. ¦f x¦ powr p2 ∂M) powr (1/p2)"
      apply (rule powr_mono2, simp add: ‹p2 > 0› less_imp_le, simp)
      apply (rule integral_mono_AE, auto simp add: * **)
      using ‹p2 > 0› less_imp_le powr_mono2 assms(3) by auto
    also have "... = Norm (𝔏 p M) f"
      unfolding ‹p = ennreal p2› by (rule Lp_I(2)[OF ‹p2 > 0› _ *, symmetric], simp)
    finally show ?thesis using ‹g ∈ space⇩N (𝔏 p M)› by auto
  next
    case PInf
    have "AE x in M. ¦f x¦ ≤ Norm (𝔏 p M) f"
      using ‹f ∈ space⇩N (𝔏 p M)› L_infinity_AE_bound unfolding ‹p = ∞› by auto
    then have *: "AE x in M. ¦g x¦ ≤ Norm (𝔏 p M) f"
      using assms(3) by auto
    show ?thesis
      using L_infinity_I[OF assms(1) *] Norm_nonneg ‹p = ∞› by auto
  qed
  then show "g ∈ space⇩N (𝔏 p M)" "Norm (𝔏 p M) g ≤ Norm (𝔏 p M) f"
    by auto
qed

lemma Lp_Banach_lattice:
  assumes "f ∈ space⇩N (𝔏 p M)"
  shows "(λx. ¦f x¦) ∈ space⇩N (𝔏 p M)"
        "Norm (𝔏 p M) (λx. ¦f x¦) = Norm (𝔏 p M) f"
proof -
  have [measurable]: "f ∈ borel_measurable M" using Lp_measurable[OF assms] by simp
  show "(λx. ¦f x¦) ∈ space⇩N (𝔏 p M)"
    by (rule Lp_domination(1)[OF _ assms], auto)
  have "Norm (𝔏 p M) (λx. ¦f x¦) ≤ Norm (𝔏 p M) f"
    by (rule Lp_domination[OF _ assms], auto)
  moreover have "Norm (𝔏 p M) f ≤ Norm (𝔏 p M) (λx. ¦f x¦)"
    by (rule Lp_domination[OF _ ‹(λx. ¦f x¦) ∈ space⇩N (𝔏 p M)›], auto)
  ultimately show "Norm (𝔏 p M) (λx. ¦f x¦) = Norm (𝔏 p M) f"
    by auto
qed

lemma Lp_bounded_bounded_support:
  assumes [measurable]: "f ∈ borel_measurable M"
      and "AE x in M. ¦f x¦ ≤ C"
          "emeasure M {x ∈ space M. f x ≠ 0} ≠ ∞"
  shows "f ∈ space⇩N(𝔏 p M)"
proof (cases rule: Lp_cases[of p])
  case zero
  then show ?thesis using L_zero_space assms by blast
next
  case PInf
  then show ?thesis using L_infinity_space assms by blast
next
  case (real_pos p2)
  have *: "integrable M (λx. ¦f x¦ powr p2)"
    apply (rule integrableI_bounded_set[of "{x ∈ space M. f x ≠ 0}" _ _ "C powr p2"])
    using assms powr_mono2[OF less_imp_le[OF ‹p2 > 0›]] by (auto simp add: top.not_eq_extremum)
  show ?thesis
    unfolding ‹p = ennreal p2› apply (rule Lp_I[OF ‹p2 > 0›]) using * by auto
qed


subsection ‹$L^p$ versions of the main theorems in integration theory›

text ‹The space $L^p$ is stable under almost sure convergence, for sequence with bounded norm.
This is a version of Fatou's lemma (and it indeed follows from this lemma in the only
nontrivial situation where $p \in (0, +\infty)$.›

proposition Lp_AE_limit:
  assumes [measurable]: "g ∈ borel_measurable M"
      and "AE x in M. (λn. f n x) ⇢ g x"
  shows "eNorm (𝔏 p M) g ≤ liminf (λn. eNorm (𝔏 p M) (f n))"
proof (cases "liminf (λn. eNorm (𝔏 p M) (f n)) = ∞")
  case True
  then show ?thesis by auto
next
  case False
  define le where "le = liminf (λn. eNorm (𝔏 p M) (f n))"
  then have "le < ∞" using False by (simp add: top.not_eq_extremum)
  obtain r0 where r0: "strict_mono r0" "(λn. eNorm (𝔏 p M) (f (r0 n))) ⇢ le"
    using liminf_subseq_lim[of "λn. eNorm (𝔏 p M) (f n)"]
    unfolding comp_def le_def
    by blast
  then have "eventually (λn. eNorm (𝔏 p M) (f (r0 n)) < ∞) sequentially"
    using False unfolding order_tendsto_iff le_def by (simp add: top.not_eq_extremum)
  then obtain N where N: "⋀n. n ≥ N ⟹ eNorm (𝔏 p M) (f (r0 n)) < ∞"
    unfolding eventually_sequentially by blast
  define r where "r = (λn. r0 (n + N))"
  have "strict_mono r" unfolding r_def using ‹strict_mono r0› 
    by (simp add: strict_mono_Suc_iff)
  have *: "(λn. eNorm (𝔏 p M) (f (r n))) ⇢ le"
    unfolding r_def using LIMSEQ_ignore_initial_segment[OF r0(2), of N].
  have "f (r n) ∈ space⇩N (𝔏 p M)" for n
    using N spaceN_iff unfolding r_def by force
  then have [measurable]: "f (r n) ∈ borel_measurable M" for n
    using Lp_measurable by auto
  define l where "l = enn2real le"
  have "l ≥ 0" unfolding l_def by auto
  have "le = ennreal l" using ‹le < ∞› unfolding l_def by auto
  have [tendsto_intros]: "(λn. Norm (𝔏 p M) (f (r n))) ⇢ l"
    apply (rule tendsto_ennrealD)
    using * ‹le < ∞› unfolding eNorm_Norm[OF ‹⋀n. f (r n) ∈ space⇩N (𝔏 p M)›] l_def by auto

  show ?thesis
  proof (cases rule: Lp_cases[of p])
    case zero
    then have "eNorm (𝔏 p M) g = 0"
      using assms(1) by (simp add: L_zero(1))
    then show ?thesis by auto
  next
    case (real_pos p2)
    then have "f (r n) ∈ space⇩N (𝔏 p2 M)" for n
      using ‹⋀n. f (r n) ∈ space⇩N(𝔏 p M)› by auto
    have "liminf (λn. ennreal(¦f (r n) x¦ powr p2)) = ¦g x¦ powr p2" if "(λn. f n x) ⇢ g x" for x
      apply (rule lim_imp_Liminf, auto intro!: tendsto_intros simp add: ‹p2 > 0›)
      using LIMSEQ_subseq_LIMSEQ[OF that ‹strict_mono r›] unfolding comp_def by auto
    then have *: "AE x in M. liminf (λn. ennreal(¦f (r n) x¦ powr p2)) = ¦g x¦ powr p2"
      using ‹AE x in M. (λn. f n x) ⇢ g x› by auto

    have "(∫⇧+x. ennreal(¦f (r n) x¦ powr p2) ∂M) = ennreal((Norm (𝔏 p M) (f (r n))) powr p2)" for n
    proof -
      have "(∫⇧+x. ennreal(¦f (r n) x¦ powr p2) ∂M) = ennreal (∫x. ¦f (r n) x¦ powr p2 ∂M)"
        by (rule nn_integral_eq_integral, auto simp add: Lp_D(2)[OF ‹p2 > 0› ‹f (r n) ∈ space⇩N (𝔏 p2 M)›])
      also have "... = ennreal((Norm (𝔏 p2 M) (f (r n))) powr p2)"
        unfolding Lp_D(3)[OF ‹p2 > 0› ‹f (r n) ∈ space⇩N (𝔏 p2 M)›] using powr_powr ‹p2 > 0› by auto
      finally show ?thesis using ‹p = ennreal p2› by simp
    qed
    moreover have "(λn. ennreal((Norm (𝔏 p M) (f (r n))) powr p2)) ⇢ ennreal(l powr p2)"
      by (auto intro!:tendsto_intros simp add: ‹p2 > 0›)
    ultimately have **: "liminf (λn. (∫⇧+x. ennreal(¦f (r n) x¦ powr p2) ∂M)) = ennreal(l powr p2)"
      using lim_imp_Liminf by force

    have "(∫⇧+x. ¦g x¦ powr p2 ∂M) = (∫⇧+x. liminf (λn. ennreal(¦f (r n) x¦ powr p2)) ∂M)"
      apply (rule nn_integral_cong_AE) using * by auto
    also have "... ≤ liminf (λn. ∫⇧+x. ennreal(¦f (r n) x¦ powr p2) ∂M)"
      by (rule nn_integral_liminf, auto)
    finally have "(∫⇧+x. ¦g x¦ powr p2 ∂M) ≤ ennreal(l powr p2)" using ** by auto
    then have "(∫⇧+x. ¦g x¦ powr p2 ∂M) < ∞" using le_less_trans by fastforce
    then have intg: "integrable M (λx. ¦g x¦ powr p2)"
      apply (intro integrableI_nonneg) by auto
    then have "g ∈ space⇩N (𝔏 p2 M)" using Lp_I(1)[OF ‹p2 > 0›, of _ M] by fastforce
    have "ennreal((Norm (𝔏 p2 M) g) powr p2) = ennreal(∫x. ¦g x¦ powr p2 ∂M)"
      unfolding Lp_D(3)[OF ‹p2 > 0› ‹g ∈ space⇩N (𝔏 p2 M)›] using powr_powr ‹p2 > 0› by auto
    also have "... = (∫⇧+x. ¦g x¦ powr p2 ∂M)"
      by (rule nn_integral_eq_integral[symmetric], auto simp add: intg)
    finally have "ennreal((Norm (𝔏 p2 M) g) powr p2) ≤ ennreal(l powr p2)"
      using ‹(∫⇧+x. ¦g x¦ powr p2 ∂M) ≤ ennreal(l powr p2)› by auto
    then have "((Norm (𝔏 p2 M) g) powr p2) powr (1/p2) ≤ (l powr p2) powr (1/p2)"
      using ennreal_le_iff ‹l ≥ 0› ‹p2 > 0› powr_mono2 by auto
    then have "Norm (𝔏 p2 M) g ≤ l"
      using ‹p2 > 0› ‹l ≥ 0› by (auto simp add: powr_powr)
    then have "eNorm (𝔏 p2 M) g ≤ le"
      unfolding eNorm_Norm[OF ‹g ∈ space⇩N (𝔏 p2 M)›] ‹le = ennreal l› using ennreal_leI by auto
    then show ?thesis unfolding le_def ‹p = ennreal p2› by simp
  next
    case PInf
    then have "AE x in M. ∀n. ¦f (r n) x¦ ≤ Norm (𝔏 ∞ M) (f (r n))"
      apply (subst AE_all_countable) using L_infinity_AE_bound ‹⋀n. f (r n) ∈ space⇩N (𝔏 p M)› by blast
    moreover have "¦g x¦ ≤ l" if "∀n. ¦f (r n) x¦ ≤ Norm (𝔏 ∞ M) (f (r n))" "(λn. f n x) ⇢ g x" for x
    proof -
      have "(λn. f (r n) x) ⇢ g x"
        using that LIMSEQ_subseq_LIMSEQ[OF _ ‹strict_mono r›] unfolding comp_def by auto
      then have *: "(λn. ¦f (r n) x¦) ⇢ ¦g x¦"
        by (auto intro!:tendsto_intros)
      show ?thesis
        apply (rule LIMSEQ_le[OF *]) using that(1) ‹(λn. Norm (𝔏 p M) (f (r n))) ⇢ l› unfolding PInf by auto
    qed
    ultimately have "AE x in M. ¦g x¦ ≤ l" using ‹AE x in M. (λn. f n x) ⇢ g x› by auto
    then have "g ∈ space⇩N (𝔏 ∞ M)" "Norm (𝔏 ∞ M) g ≤ l"
      using L_infinity_I[OF ‹g ∈ borel_measurable M› _ ‹l ≥ 0›] by auto
    then have "eNorm (𝔏 ∞ M) g ≤ le"
      unfolding eNorm_Norm[OF ‹g ∈ space⇩N (𝔏 ∞ M)›] ‹le = ennreal l› using ennreal_leI by auto
    then show ?thesis unfolding le_def ‹p = ∞› by simp
  qed
qed

lemma Lp_AE_limit':
  assumes "g ∈ borel_measurable M"
          "⋀n. f n ∈ space⇩N (𝔏 p M)"
          "AE x in M. (λn. f n x) ⇢ g x"
          "(λn. Norm (𝔏 p M) (f n)) ⇢ l"
  shows "g ∈ space⇩N (𝔏 p M)"
        "Norm (𝔏 p M) g ≤ l"
proof -
  have "l ≥ 0" by (rule LIMSEQ_le_const[OF ‹(λn. Norm (𝔏 p M) (f n)) ⇢ l›], auto)
  have "(λn. eNorm (𝔏 p M) (f n)) ⇢ ennreal l"
    unfolding eNorm_Norm[OF ‹⋀n. f n ∈ space⇩N (𝔏 p M)›] using ‹(λn. Norm (𝔏 p M) (f n)) ⇢ l› by auto
  then have *: "ennreal l = liminf (λn. eNorm (𝔏 p M) (f n))"
    using lim_imp_Liminf[symmetric] trivial_limit_sequentially by blast
  have "eNorm (𝔏 p M) g ≤ ennreal l"
    unfolding * apply (rule Lp_AE_limit) using assms by auto
  then have "eNorm (𝔏 p M) g < ∞" using le_less_trans by fastforce
  then show "g ∈ space⇩N (𝔏 p M)" using spaceN_iff by auto
  show "Norm (𝔏 p M) g ≤ l"
    using ‹eNorm (𝔏 p M) g ≤ ennreal l› ennreal_le_iff[OF ‹l ≥ 0›]
    unfolding eNorm_Norm[OF ‹g ∈ space⇩N (𝔏 p M)›] by auto
qed

lemma Lp_AE_limit'':
  assumes "g ∈ borel_measurable M"
          "⋀n. f n ∈ space⇩N (𝔏 p M)"
          "AE x in M. (λn. f n x) ⇢ g x"
          "⋀n. Norm (𝔏 p M) (f n) ≤ C"
  shows "g ∈ space⇩N (𝔏 p M)"
        "Norm (𝔏 p M) g ≤ C"
proof -
  have "C ≥ 0" by (rule order_trans[OF Norm_nonneg[of "𝔏 p M" "f 0"] ‹Norm (𝔏 p M) (f 0) ≤ C›])
  have *: "liminf (λn. ennreal C) = ennreal C"
    using Liminf_const trivial_limit_at_top_linorder by blast
  have "eNorm (𝔏 p M) (f n) ≤ ennreal C" for n
    unfolding eNorm_Norm[OF ‹f n ∈ space⇩N (𝔏 p M)›]
    using ‹Norm (𝔏 p M) (f n) ≤ C› by (auto simp add: ennreal_leI)
  then have "liminf (λn. eNorm (𝔏 p M) (f n)) ≤ ennreal C"
    using Liminf_mono[of "(λn. eNorm (𝔏 p M) (f n))" "λ_. C" sequentially] * by auto
  then have "eNorm (𝔏 p M) g ≤ ennreal C" using
    Lp_AE_limit[OF ‹g ∈ borel_measurable M› ‹AE x in M. (λn. f n x) ⇢ g x›, of p] by auto
  then have "eNorm (𝔏 p M) g < ∞" using le_less_trans by fastforce
  then show "g ∈ space⇩N (𝔏 p M)" using spaceN_iff by auto
  show "Norm (𝔏 p M) g ≤ C"
    using ‹eNorm (𝔏 p M) g ≤ ennreal C› ennreal_le_iff[OF ‹C ≥ 0›]
    unfolding eNorm_Norm[OF ‹g ∈ space⇩N (𝔏 p M)›] by auto
qed

text ‹We give the version of Lebesgue dominated convergence theorem in the setting of
$L^p$ spaces.›

proposition Lp_domination_limit:
  fixes p::real
  assumes [measurable]: "g ∈ borel_measurable M"
          "⋀n. f n ∈ borel_measurable M"
      and "m ∈ space⇩N (𝔏 p M)"
          "AE x in M. (λn. f n x) ⇢ g x"
          "⋀n. AE x in M. ¦f n x¦ ≤ m x"
  shows "g ∈ space⇩N (𝔏 p M)"
        "tendsto_in⇩N (𝔏 p M) f g"
proof -
  have [measurable]: "m ∈ borel_measurable M" using Lp_measurable[OF ‹m ∈ space⇩N (𝔏 p M)›] by auto
  have "f n ∈ space⇩N(𝔏 p M)" for n
    apply (rule Lp_domination[OF _ ‹m ∈ space⇩N (𝔏 p M)›]) using ‹AE x in M. ¦f n x¦ ≤ m x› by auto

  have "AE x in M. ∀n. ¦f n x¦ ≤ m x"
    apply (subst AE_all_countable) using ‹⋀n. AE x in M. ¦f n x¦ ≤ m x› by auto
  moreover have "¦g x¦ ≤ m x" if "∀n. ¦f n x¦ ≤ m x" "(λn. f n x) ⇢ g x" for x
    apply (rule LIMSEQ_le_const2[of "λn. ¦f n x¦"]) using that by (auto intro!:tendsto_intros)
  ultimately have *: "AE x in M. ¦g x¦ ≤ m x" using ‹AE x in M. (λn. f n x) ⇢ g x› by auto
  show "g ∈ space⇩N(𝔏 p M)"
    apply (rule Lp_domination[OF _ ‹m ∈ space⇩N (𝔏 p M)›]) using * by auto

  have "(λn. Norm (𝔏 p M) (f n - g)) ⇢ 0"
  proof (cases "p ≤ 0")
    case True
    then have "ennreal p = 0" by (simp add: ennreal_eq_0_iff)
    then show ?thesis unfolding Norm_def by (auto simp add: L_zero(1))
  next
    case False
    then have "p > 0" by auto
    have "(λn. (∫x. ¦f n x - g x¦ powr p ∂M)) ⇢ (∫x. ¦0¦ powr p ∂M)"
    proof (rule integral_dominated_convergence[of _ _ _ "(λx. ¦2 * m x¦ powr p)"], auto)
      show "integrable M (λx. ¦2 * m x¦ powr p)"
        unfolding abs_mult apply (subst powr_mult)
        using Lp_D(2)[OF ‹p > 0› ‹m ∈ space⇩N (𝔏 p M)›] by auto
      have "(λn. ¦f n x - g x¦ powr p) ⇢ ¦0¦ powr p" if "(λn. f n x) ⇢ g x" for x
        apply (rule tendsto_powr') using ‹p > 0› that apply (auto)
        using Lim_null tendsto_rabs_zero_iff by fastforce
      then show "AE x in M. (λn. ¦f n x - g x¦ powr p) ⇢ 0"
        using ‹AE x in M. (λn. f n x) ⇢ g x› by auto
      have "¦f n x - g x¦ powr p ≤ ¦2 * m x¦ powr p" if "¦f n x¦ ≤ m x" "¦g x¦ ≤ m x" for n x
        using powr_mono2 ‹p > 0› that by auto
      then show "AE x in M. ¦f n x - g x¦ powr p ≤ ¦2 * m x¦ powr p" for n
        using ‹AE x in M. ¦f n x¦ ≤ m x› ‹AE x in M. ¦g x¦ ≤ m x› by auto
    qed
    then have "(λn. (Norm (𝔏 p M) (f n - g)) powr p) ⇢ (Norm (𝔏 p M) 0) powr p"
      unfolding Lp_D[OF ‹p > 0› spaceN_diff[OF ‹⋀n. f n ∈ space⇩N(𝔏 p M)› ‹g ∈ space⇩N(𝔏 p M)›]]
      using ‹p > 0› by (auto simp add: powr_powr)
    then have "(λn. ((Norm (𝔏 p M) (f n - g)) powr p) powr (1/p)) ⇢ ((Norm (𝔏 p M) 0) powr p) powr (1/p)"
      by (rule tendsto_powr', auto simp add: ‹p > 0›)
    then show ?thesis using powr_powr ‹p > 0› by auto
  qed
  then show "tendsto_in⇩N (𝔏 p M) f g"
    unfolding tendsto_in⇩N_def by auto
qed

text ‹We give the version of the monotone convergence theorem in the setting of
$L^p$ spaces.›

proposition Lp_monotone_limit:
  fixes f::"nat ⇒ 'a ⇒ real"
  assumes "p > (0::ennreal)"
          "AE x in M. incseq (λn. f n x)"
          "⋀n. Norm (𝔏 p M) (f n) ≤ C"
          "⋀n. f n ∈ space⇩N (𝔏 p M)"
  shows "AE x in M. convergent (λn. f n x)"
        "(λx. lim (λn. f n x)) ∈ space⇩N (𝔏 p M)"
        "Norm (𝔏 p M) (λx. lim (λn. f n x)) ≤ C"
proof -
  have [measurable]: "f n ∈ borel_measurable M" for n using Lp_measurable[OF assms(4)].
  show "AE x in M. convergent (λn. f n x)"
  proof (cases rule: Lp_cases[of p])
    case PInf
    have "AE x in M. ¦f n x¦ ≤ C" for n
      using L_infinity_AE_bound[of "f n" M] ‹Norm (𝔏 p M) (f n) ≤ C› ‹f n ∈ space⇩N (𝔏 p M)›
      unfolding ‹p=∞› by auto
    then have *: "AE x in M. ∀n. ¦f n x¦ ≤ C"
      by (subst AE_all_countable, auto)
    have "(λn. f n x) ⇢ (SUP n. f n x)" if "incseq (λn. f n x)" "⋀n. ¦f n x¦ ≤ C" for x
      apply (rule LIMSEQ_incseq_SUP[OF _ ‹incseq (λn. f n x)›]) using that(2) abs_le_D1 by fastforce
    then have "convergent (λn. f n x)" if "incseq (λn. f n x)" "⋀n. ¦f n x¦ ≤ C" for x
      unfolding convergent_def using that by auto
    then show ?thesis using ‹AE x in M. incseq (λn. f n x)› * by auto
  next
    case (real_pos p2)
    define g where "g = (λn. f n - f 0)"
    have "AE x in M. incseq (λn. g n x)"
      unfolding g_def using ‹AE x in M. incseq (λn. f n x)› by (simp add: incseq_def)
    have "g n ∈ space⇩N (𝔏 p2 M)" for n
      unfolding g_def using ‹⋀n. f n ∈ space⇩N (𝔏 p M)› unfolding ‹p = ennreal p2› by auto
    then have [measurable]: "g n ∈ borel_measurable M" for n using Lp_measurable by auto
    define D where "D = defect (𝔏 p2 M) * C + defect (𝔏 p2 M) * C"
    have "Norm (𝔏 p2 M) (g n) ≤ D" for n
    proof -
      have "f n ∈ space⇩N (𝔏 p2 M)" using ‹f n ∈ space⇩N (𝔏 p M)› unfolding ‹p = ennreal p2› by auto
      have "Norm (𝔏 p2 M) (g n) ≤ defect (𝔏 p2 M) * Norm (𝔏 p2 M) (f n) + defect (𝔏 p2 M) * Norm (𝔏 p2 M) (f 0)"
        unfolding g_def using Norm_triangular_ineq_diff[OF ‹f n ∈ space⇩N (𝔏 p2 M)›] by auto
      also have "... ≤ D"
        unfolding D_def apply(rule add_mono)
        using mult_left_mono defect_ge_1[of "𝔏 p2 M"] ‹⋀n. Norm (𝔏 p M) (f n) ≤ C› unfolding ‹p = ennreal p2› by auto
      finally show ?thesis by simp
    qed
    have g_bound: "(∫⇧+x. ¦g n x¦ powr p2 ∂M) ≤ ennreal(D powr p2)" for n
    proof -
      have "(∫⇧+x. ¦g n x¦ powr p2 ∂M) = ennreal(∫x. ¦g n x¦ powr p2 ∂M)"
        apply (rule nn_integral_eq_integral) using Lp_D(2)[OF ‹p2 > 0› ‹g n ∈ space⇩N (𝔏 p2 M)›] by auto
      also have "... = ennreal((Norm (𝔏 p2 M) (g n)) powr p2)"
        apply (subst Lp_Norm(2)[OF ‹p2 > 0›, of "g n", symmetric]) by auto
      also have "... ≤ ennreal(D powr p2)"
        by (auto intro!: powr_mono2 simp add: less_imp_le[OF ‹p2 > 0›] ‹Norm (𝔏 p2 M) (g n) ≤ D›)
      finally show ?thesis by simp
    qed
    have "∀n. g n x ≥ 0" if "incseq (λn. f n x)" for x
      unfolding g_def using that by (auto simp add: incseq_def)
    then have "AE x in M. ∀n. g n x ≥ 0" using ‹AE x in M. incseq (λn. f n x)› by auto

    define h where "h = (λn x. ennreal(¦g n x¦ powr p2))"
    have [measurable]: "h n ∈ borel_measurable M" for n unfolding h_def by auto
    define H where "H = (λx. (SUP n. h n x))"
    have [measurable]: "H ∈ borel_measurable M" unfolding H_def by auto
    have "⋀n. h n x ≤ h (Suc n) x" if "∀n. g n x ≥ 0" "incseq (λn. g n x)" for x
      unfolding h_def apply (auto intro!:powr_mono2)
      apply (auto simp add: less_imp_le[OF ‹p2 > 0›]) using that incseq_SucD by auto
    then have *: "AE x in M. h n x ≤ h (Suc n) x" for n
      using ‹AE x in M. ∀n. g n x ≥ 0› ‹AE x in M. incseq (λn. g n x)› by auto
    have "(∫⇧+x. H x ∂M) = (SUP n. ∫⇧+x. h n x ∂M)"
      unfolding H_def by (rule nn_integral_monotone_convergence_SUP_AE, auto simp add: *)
    also have "... ≤ ennreal(D powr p2)"
      unfolding H_def h_def using g_bound by (simp add: SUP_least)
    finally have "(∫⇧+x. H x ∂M) < ∞" by (simp add: le_less_trans)
    then have "AE x in M. H x ≠ ∞"
      by (metis (mono_tags, lifting) ‹H ∈ borel_measurable M› infinity_ennreal_def nn_integral_noteq_infinite top.not_eq_extremum)

    have "convergent (λn. f n x)" if "H x ≠ ∞" "incseq (λn. f n x)" for x
    proof -
      define A where "A = enn2real(H x)"
      then have "H x = ennreal A" using ‹H x ≠ ∞› by (simp add: ennreal_enn2real_if)
      have "f n x ≤ f 0 x + A powr (1/p2)" for n
      proof -
        have "ennreal(¦g n x¦ powr p2) ≤ ennreal A"
          unfolding ‹H x = ennreal A›[symmetric] H_def h_def by (meson SUP_upper2 UNIV_I order_refl)
        then have "¦g n x¦ powr p2 ≤ A"
          by (subst ennreal_le_iff[symmetric], auto simp add: A_def)
        have "¦g n x¦ = (¦g n x¦ powr p2) powr (1/p2)"
          using ‹p2 > 0› by (simp add: powr_powr)
        also have "... ≤ A powr (1/p2)"
          apply (rule powr_mono2) using ‹p2 > 0› ‹¦g n x¦ powr p2 ≤ A› by auto
        finally have "¦g n x¦ ≤ A powr (1/p2)" by simp
        then show ?thesis unfolding g_def by auto
      qed
      then show "convergent (λn. f n x)"
        using LIMSEQ_incseq_SUP[OF _ ‹incseq (λn. f n x)›] convergent_def by (metis bdd_aboveI2)
    qed
    then show "AE x in M. convergent (λn. f n x)"
      using ‹AE x in M. H x ≠ ∞› ‹AE x in M. incseq (λn. f n x)› by auto
  qed (insert ‹p>0›, simp)
  then have lim: "AE x in M. (λn. f n x) ⇢ lim (λn. f n x)"
    using convergent_LIMSEQ_iff by auto
  show "(λx. lim (λn. f n x)) ∈ space⇩N (𝔏 p M)"
    apply (rule Lp_AE_limit''[of _ _ f, OF _ ‹⋀n. f n ∈ space⇩N (𝔏 p M)› lim ‹⋀n. Norm (𝔏 p M) (f n) ≤ C›])
    by auto
  show "Norm (𝔏 p M) (λx. lim (λn. f n x)) ≤ C"
    apply (rule Lp_AE_limit''[of _ _ f, OF _ ‹⋀n. f n ∈ space⇩N (𝔏 p M)› lim ‹⋀n. Norm (𝔏 p M) (f n) ≤ C›])
    by auto
qed


subsection ‹Completeness of $L^p$›

text ‹We prove the completeness of $L^p$.›

theorem Lp_complete:
  "complete⇩N (𝔏 p M)"
proof (cases rule: Lp_cases[of p])
  case zero
  show ?thesis
  proof (rule complete⇩N_I)
    fix u assume "∀(n::nat). u n ∈ space⇩N (𝔏 p M)"
    then have "tendsto_in⇩N (𝔏 p M) u 0"
      unfolding tendsto_in⇩N_def Norm_def ‹p = 0› L_zero(1) L_zero_space by auto
    then show "∃x∈space⇩N (𝔏 p M). tendsto_in⇩N (𝔏 p M) u x"
      by auto
  qed
next
  case (real_pos p2)
  show ?thesis
  proof (rule complete⇩N_I'[of "λn. (1/2)^n * (1/(defect (𝔏 p M))^(Suc n))"], unfold ‹p = ennreal p2›)
    show "0 < (1/2) ^ n * (1 / defect (𝔏 (ennreal p2) M) ^ Suc n)" for n
      using defect_ge_1[of "𝔏 (ennreal p2) M"] by (auto simp add: divide_simps)

    fix u assume "∀(n::nat). u n ∈ space⇩N (𝔏 p2 M)" "∀n. Norm (𝔏 p2 M) (u n) ≤ (1/2)^n * (1/(defect (𝔏 p2 M))^(Suc n))"
    then have H: "⋀n. u n ∈ space⇩N (𝔏 p2 M)"
                 "⋀n. Norm (𝔏 p2 M) (u n) ≤ (1/2) ^ n * (1/(defect (𝔏 p2 M))^(Suc n))"
      unfolding ‹p = ennreal p2› by auto
    have [measurable]: "u n ∈ borel_measurable M" for n using Lp_measurable[OF H(1)].

    define w where "w = (λN x. (∑n∈{..<N}. ¦u n x¦))"
    have w2: "w = (λN. sum (λn x. ¦u n x¦) {..<N})" unfolding w_def apply (rule ext)+
      by (metis (mono_tags, lifting) sum.cong fun_sum_apply)
    have "incseq (λN. w N x)" for x unfolding w2 by (rule incseq_SucI, auto)
    then have wN_inc: "AE x in M. incseq (λN. w N x)" by simp

    have abs_u_space: "(λx. ¦u n x¦) ∈ space⇩N (𝔏 p2 M)" for n
      by (rule Lp_Banach_lattice[OF ‹u n ∈ space⇩N (𝔏 p2 M)›])
    then have wN_space: "w N ∈ space⇩N (𝔏 p2 M)" for N unfolding w2 using H(1) by auto
    have abs_u_Norm: "Norm (𝔏 p2 M) (λx. ¦u n x¦) ≤ (1/2) ^ n * (1/(defect (𝔏 p2 M))^(Suc n))" for n
      using Lp_Banach_lattice(2)[OF ‹u n ∈ space⇩N (𝔏 p2 M)›] H(2) by auto

    have wN_Norm: "Norm (𝔏 p2 M) (w N) ≤ 2" for N
    proof -
      have *: "(defect (𝔏 p2 M))^(Suc n) ≥ 0" "(defect (𝔏 p2 M))^(Suc n) > 0" for n
        using defect_ge_1[of "𝔏 p2 M"] by auto
      have "Norm (𝔏 p2 M) (w N) ≤ (∑n<N. (defect (𝔏 p2 M))^(Suc n) * Norm (𝔏 p2 M) (λx. ¦u n x¦))"
        unfolding w2 lessThan_Suc_atMost[symmetric] by (rule Norm_sum, simp add: abs_u_space)
      also have "... ≤ (∑n<N. (defect (𝔏 p2 M))^(Suc n) * ((1/2) ^ n * (1/(defect (𝔏 p2 M))^(Suc n))))"
        apply (rule sum_mono, rule mult_left_mono) using abs_u_Norm * by auto
      also have "... = (∑n<N. (1/2) ^ n)"
        using *(2) defect_ge_1[of "𝔏 p2 M"] by (auto simp add: algebra_simps)
      also have "... ≤ (∑n. (1/2) ^ n)"
        unfolding lessThan_Suc_atMost[symmetric] by (rule sum_le_suminf, rule summable_geometric[of "1/2"], auto)
      also have "... = 2" using suminf_geometric[of "1/2"] by auto
      finally show ?thesis by simp
    qed

    have "AE x in M. convergent (λN. w N x)"
      apply (rule Lp_monotone_limit[OF ‹p > 0›, of _ _ 2], unfold ‹p = ennreal p2›)
      using wN_inc wN_Norm wN_space by auto
    define m where "m = (λx. lim (λN. w N x))"
    have m_space: "m ∈ space⇩N (𝔏 p2 M)"
      unfolding m_def ‹p = ennreal p2›[symmetric] apply (rule Lp_monotone_limit[OF ‹p > 0›, of _ _ 2], unfold ‹p = ennreal p2›)
      using wN_inc wN_Norm wN_space by auto

    define v where "v = (λx. (∑n. u n x))"
    have v_meas: "v ∈ borel_measurable M" unfolding v_def by auto
    have u_meas: "⋀n. (sum u {0..<n}) ∈ borel_measurable M" by auto
    {
      fix x assume "convergent (λN. w N x)"
      then have S: "summable (λn. ¦u n x¦)" unfolding w_def using summable_iff_convergent by auto
      then have "m x = (∑n. ¦u n x¦)" unfolding m_def w_def by (metis suminf_eq_lim)

      have "summable (λn. u n x)" using S by (rule summable_rabs_cancel)
      then have *: "(λn. (sum u {..<n}) x) ⇢ v x"
        unfolding v_def fun_sum_apply by (metis convergent_LIMSEQ_iff suminf_eq_lim summable_iff_convergent)
      have "¦(sum u {..<n}) x¦ ≤ m x" for n
      proof -
        have "¦(sum u {..<n}) x¦ ≤ (∑i∈{..<n}. ¦u i x¦)"
          unfolding fun_sum_apply by auto
        also have "... ≤ (∑i. ¦u i x¦)"
          apply (rule sum_le_suminf) using S by auto
        finally show ?thesis using ‹m x = (∑n. ¦u n x¦)› by simp
      qed
      then have "(∀n. ¦(sum u {0..<n}) x¦ ≤ m x) ∧ (λn. (sum u {0..<n}) x) ⇢ v x"
        unfolding atLeast0LessThan using * by auto
    }
    then have m_bound: "⋀n. AE x in M. ¦(sum u {0..<n}) x¦ ≤ m x"
          and u_conv: "AE x in M. (λn. (sum u {0..<n}) x) ⇢ v x"
      using ‹AE x in M. convergent (λN. w N x)› by auto

    have "tendsto_in⇩N (𝔏 p2 M) (λn. sum u {0..<n}) v"
      by (rule Lp_domination_limit[OF v_meas u_meas m_space u_conv m_bound])
    moreover have "v ∈ space⇩N (𝔏 p2 M)"
      by (rule Lp_domination_limit[OF v_meas u_meas m_space u_conv m_bound])
    ultimately show "∃v ∈ space⇩N (𝔏 p2 M). tendsto_in⇩N (𝔏 p2 M) (λn. sum u {0..<n}) v"
      by auto
  qed
next
  case PInf
  show ?thesis
  proof (rule complete⇩N_I'[of "λn. (1/2)^n"])
    fix u assume "∀(n::nat). u n ∈ space⇩N (𝔏 p M)" "∀n. Norm (𝔏 p M) (u n) ≤ (1/2) ^ n"
    then have H: "⋀n. u n ∈ space⇩N (𝔏 ∞ M)" "⋀n. Norm (𝔏 ∞ M) (u n) ≤ (1/2) ^ n" using PInf by auto
    have [measurable]: "u n ∈ borel_measurable M" for n using Lp_measurable[OF H(1)] by auto
    define v where "v = (λx. ∑n. u n x)"
    have [measurable]: "v ∈ borel_measurable M" unfolding v_def by auto
    define w where "w = (λN x. (∑n∈{0..<N}. u n x))"
    have [measurable]: "w N ∈ borel_measurable M" for N unfolding w_def by auto

    have "AE x in M. ¦u n x¦ ≤ (1/2)^n" for n
      using L_infinity_AE_bound[OF H(1), of n] H(2)[of n] by auto
    then have "AE x in M. ∀n. ¦u n x¦ ≤ (1/2)^n"
      by (subst AE_all_countable, auto)
    moreover have "¦w N x - v x¦ ≤ (1/2)^N * 2" if "∀n. ¦u n x¦ ≤ (1/2)^n" for N x
    proof -
      have *: "⋀n. ¦u n x¦ ≤ (1/2)^n" using that by auto
      have **: "summable (λn. ¦u n x¦)"
        apply (rule summable_norm_cancel, rule summable_comparison_test'[OF summable_geometric[of "1/2"]])
        using * by auto
      have "¦w N x - v x¦ = ¦(∑n. u (n + N) x)¦"
        unfolding v_def w_def
        apply (subst suminf_split_initial_segment[OF summable_rabs_cancel[OF ‹summable (λn. ¦u n x¦)›], of "N"])
        by (simp add: lessThan_atLeast0)
      also have "... ≤ (∑n. ¦u (n + N) x¦)"
        apply (rule summable_rabs, subst summable_iff_shift) using ** by auto
      also have "... ≤ (∑n. (1/2)^(n + N))"
      proof (rule suminf_le)
        show "⋀n. ¦u (n + N) x¦ ≤ (1/2) ^ (n + N)"
          using *[of "_ + N"] by simp
        show "summable (λn. ¦u (n + N) x¦)"
          using ** by (subst summable_iff_shift) simp
        show "summable (λn. (1/2::real) ^ (n + N))"
          using summable_geometric [of "1/2"] by (subst summable_iff_shift) simp
      qed
      also have "... = (1/2)^N * (∑n. (1/2)^n)"
        by (subst power_add, subst suminf_mult2[symmetric], auto simp add: summable_geometric[of "1/2"])
      also have "... = (1/2)^N * 2"
        by (subst suminf_geometric, auto)
      finally show ?thesis by simp
    qed
    ultimately have *: "AE x in M. ¦w N x - v x¦ ≤ (1/2)^N * 2" for N by auto

    have **: "w N - v ∈ space⇩N (𝔏 ∞ M)" "Norm (𝔏 ∞ M) (w N - v) ≤ (1/2)^N * 2" for N
      unfolding fun_diff_def using L_infinity_I[OF _ *] by auto
    have l: "(λN. ((1/2)^N) * (2::real)) ⇢ 0 * 2"
      by (rule tendsto_mult, auto simp add: LIMSEQ_realpow_zero[of "1/2"])
    have "tendsto_in⇩N (𝔏 ∞ M) w v" unfolding tendsto_in⇩N_def
      apply (rule tendsto_sandwich[of "λ_. 0" _ _ "λn. (1/2)^n * 2"]) using l **(2) by auto
    have "v = - (w 0 - v)" unfolding w_def by auto
    then have "v ∈ space⇩N (𝔏 ∞ M)" using **(1)[of 0] spaceN_add spaceN_diff by fastforce
    then show "∃v ∈ space⇩N (𝔏 p M). tendsto_in⇩N (𝔏 p M) (λn. sum u {0..<n}) v"
      using ‹tendsto_in⇩N (𝔏 ∞ M) w v› unfolding ‹p = ∞› w_def fun_sum_apply[symmetric] by auto
  qed (simp)
qed


subsection ‹Multiplication of functions, duality›

text ‹The next theorem asserts that the multiplication of two functions in $L^p$ and $L^q$ belongs to
$L^r$, where $r$ is determined by the equality $1/r = 1/p + 1/q$. This is essentially a case by case
analysis, depending on the kind of $L^p$ space we are considering. The only nontrivial case is
when $p$, $q$ (and $r$) are finite and nonzero. In this case, it reduces to H\"older inequality.›

theorem Lp_Lq_mult:
  fixes p q r::ennreal
  assumes "1/p + 1/q = 1/r"
      and "f ∈ space⇩N (𝔏 p M)" "g ∈ space⇩N (𝔏 q M)"
  shows "(λx. f x * g x) ∈ space⇩N (𝔏 r M)"
        "Norm (𝔏 r M) (λx. f x * g x) ≤ Norm (𝔏 p M) f * Norm (𝔏 q M) g"
proof -
  have [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M" using Lp_measurable assms by auto
  have "(λx. f x * g x) ∈ space⇩N (𝔏 r M) ∧ Norm (𝔏 r M) (λx. f x * g x) ≤ Norm (𝔏 p M) f * Norm (𝔏 q M) g"
  proof (cases rule: Lp_cases[of r])
    case zero
    have *: "(λx. f x * g x) ∈ borel_measurable M" by auto
    then have "Norm (𝔏 r M) (λx. f x * g x) = 0" using L_zero[of M] unfolding Norm_def zero by auto
    then have "Norm (𝔏 r M) (λx. f x * g x) ≤ Norm (𝔏 p M) f * Norm (𝔏 q M) g"
      using Norm_nonneg by auto
    then show ?thesis unfolding zero using * L_zero_space[of M] by auto
  next
    case (real_pos r2)
    have "p > 0" "q > 0" using ‹1/p + 1/q = 1/r› ‹r > 0›
      by (metis ennreal_add_eq_top ennreal_divide_eq_top_iff ennreal_top_neq_one gr_zeroI zero_neq_one)+
    consider "p = ∞" | "q = ∞" | "p < ∞ ∧ q < ∞" using top.not_eq_extremum by force
    then show ?thesis
    proof (cases)
      case 1
      then have "q = r" using ‹1/p + 1/q = 1/r›
        by (metis ennreal_divide_top infinity_ennreal_def one_divide_one_divide_ennreal semiring_normalization_rules(5))
      have "AE x in M. ¦f x¦ ≤ Norm (𝔏 p M) f"
        using ‹f ∈ space⇩N (𝔏 p M)› L_infinity_AE_bound unfolding ‹p = ∞› by auto
      then have *: "AE x in M. ¦f x * g x¦ ≤ ¦Norm (𝔏 p M) f * g x¦"
        unfolding abs_mult using Norm_nonneg[of "𝔏 p M" f] mult_right_mono by fastforce
      have **: "(λx. Norm (𝔏 p M) f * g x) ∈ space⇩N (𝔏 r M)"
        using spaceN_cmult[OF ‹g ∈ space⇩N (𝔏 q M)›] unfolding ‹q = r› scaleR_fun_def by simp
      have ***: "Norm (𝔏 r M) (λx. Norm (𝔏 p M) f * g x) = Norm (𝔏 p M) f * Norm (𝔏 q M) g"
        using Norm_cmult[of "𝔏 r M"] unfolding ‹q = r› scaleR_fun_def by auto
      then show ?thesis
        using Lp_domination[of "λx. f x * g x" M "λx. Norm (𝔏 p M) f * g x" r] unfolding ‹q = r›
        using * ** *** by auto
    next
      case 2
      then have "p = r" using ‹1/p + 1/q = 1/r›
        by (metis add.right_neutral ennreal_divide_top infinity_ennreal_def one_divide_one_divide_ennreal)
      have "AE x in M. ¦g x¦ ≤ Norm (𝔏 q M) g"
        using ‹g ∈ space⇩N (𝔏 q M)› L_infinity_AE_bound unfolding ‹q = ∞› by auto
      then have *: "AE x in M. ¦f x * g x¦ ≤ ¦Norm (𝔏 q M) g * f x¦"
        apply (simp only: mult.commute[of "Norm (𝔏 q M) g" _])
        unfolding abs_mult using mult_left_mono Norm_nonneg[of "𝔏 q M" g] by fastforce
      have **: "(λx. Norm (𝔏 q M) g * f x) ∈ space⇩N (𝔏 r M)"
        using spaceN_cmult[OF ‹f ∈ space⇩N (𝔏 p M)›] unfolding ‹p = r› scaleR_fun_def by simp
      have ***: "Norm (𝔏 r M) (λx. Norm (𝔏 q M) g * f x) = Norm (𝔏 p M) f * Norm (𝔏 q M) g"
        using Norm_cmult[of "𝔏 r M"] unfolding ‹p = r› scaleR_fun_def by auto
      then show ?thesis
        using Lp_domination[of "λx. f x * g x" M "λx. Norm (𝔏 q M) g * f x" r] unfolding ‹p = r›
        using * ** *** by auto
    next
      case 3
      obtain p2 where "p = ennreal p2" "p2 > 0"
        using enn2real_positive_iff[of p] 3 ‹p > 0› by (cases p) auto
      obtain q2 where "q = ennreal q2" "q2 > 0"
        using enn2real_positive_iff[of q] 3 ‹q > 0› by (cases q) auto

      have "ennreal(1/r2) = 1/r"
        using ‹r = ennreal r2› ‹r2 > 0› divide_ennreal zero_le_one by fastforce
      also have "... = 1/p + 1/q" using assms by auto
      also have "... = ennreal(1/p2 + 1/q2)" using ‹p = ennreal p2› ‹p2 > 0› ‹q = ennreal q2› ‹q2 > 0›
        apply (simp only: divide_ennreal ennreal_1[symmetric]) using ennreal_plus[of "1/p2" "1/q2", symmetric] by auto
      finally have *: "1/r2 = 1/p2 + 1/q2"
        using ennreal_inj ‹p2 > 0› ‹q2 > 0› ‹r2 > 0› by (metis divide_pos_pos ennreal_less_zero_iff le_less zero_less_one)

      define P where "P = p2 / r2"
      define Q where "Q = q2 / r2"
      have [simp]: "P > 0" "Q > 0" and "1/P + 1/Q = 1"
        using ‹p2 > 0› ‹q2 > 0› ‹r2 > 0› * unfolding P_def Q_def by (auto simp add: divide_simps algebra_simps)
      have Pa: "(¦z¦ powr r2) powr P = ¦z¦ powr p2" for z
        unfolding P_def powr_powr using ‹r2 > 0› by auto
      have Qa: "(¦z¦ powr r2) powr Q = ¦z¦ powr q2" for z
        unfolding Q_def powr_powr using ‹r2 > 0› by auto

      have *: "integrable M (λx. ¦f x¦ powr r2 * ¦g x¦ powr r2)"
        apply (rule Holder_inequality[OF ‹P>0› ‹Q>0› ‹1/P + 1/Q = 1›], auto simp add: Pa Qa)
        using ‹f ∈ space⇩N (𝔏 p M)› unfolding ‹p = ennreal p2› using Lp_space[OF ‹p2 > 0›] apply auto
        using ‹g ∈ space⇩N (𝔏 q M)› unfolding ‹q = ennreal q2› using Lp_space[OF ‹q2 > 0›] by auto
      have "(λx. f x * g x) ∈ space⇩N (𝔏 r M)"
        unfolding ‹r = ennreal r2› using Lp_space[OF ‹r2 > 0›, of M] by (auto simp add: * abs_mult powr_mult)
      have "Norm (𝔏 r M) (λx. f x * g x) = (∫x. ¦f x * g x¦ powr r2 ∂M) powr (1/r2)"
        unfolding ‹r = ennreal r2› using Lp_Norm[OF ‹r2 > 0›, of _ M] by auto
      also have "... = abs (∫x. ¦f x¦ powr r2 * ¦g x¦ powr r2 ∂M) powr (1/r2)"
        by (auto simp add: powr_mult abs_mult)
      also have "... ≤ ((∫x. ¦ ¦f x¦ powr r2 ¦ powr P ∂M) powr (1/P) * (∫x. ¦ ¦g x¦ powr r2 ¦ powr Q ∂M) powr (1/Q)) powr (1/r2)"
        apply (rule powr_mono2, simp add: ‹r2 > 0› less_imp_le, simp)
        apply (rule Holder_inequality[OF ‹P>0› ‹Q>0› ‹1/P + 1/Q = 1›], auto simp add: Pa Qa)
        using ‹f ∈ space⇩N (𝔏 p M)› unfolding ‹p = ennreal p2› using Lp_space[OF ‹p2 > 0›] apply auto
        using ‹g ∈ space⇩N (𝔏 q M)› unfolding ‹q = ennreal q2› using Lp_space[OF ‹q2 > 0›] by auto
      also have "... = (∫x. ¦f x¦ powr p2 ∂M) powr (1/p2) * (∫x. ¦g x¦ powr q2 ∂M) powr (1/q2)"
        apply (auto simp add: powr_mult powr_powr) unfolding P_def Q_def using ‹r2 > 0› by auto
      also have "... = Norm (𝔏 p M) f * Norm (𝔏 q M) g"
        unfolding ‹p = ennreal p2› ‹q = ennreal q2›
        using Lp_Norm[OF ‹p2 > 0›, of _ M] Lp_Norm[OF ‹q2 > 0›, of _ M] by auto
      finally show ?thesis using ‹(λx. f x * g x) ∈ space⇩N (𝔏 r M)› by auto
    qed
  next
    case PInf
    then have "p = ∞" "q = r" using ‹1/p + 1/q = 1/r›
      by (metis add_eq_0_iff_both_eq_0 ennreal_divide_eq_0_iff infinity_ennreal_def not_one_le_zero order.order_iff_strict)+
    have "AE x in M. ¦f x¦ ≤ Norm (𝔏 p M) f"
      using ‹f ∈ space⇩N (𝔏 p M)› L_infinity_AE_bound unfolding ‹p = ∞› by auto
    then have *: "AE x in M. ¦f x * g x¦ ≤ ¦Norm (𝔏 p M) f * g x¦"
      unfolding abs_mult using Norm_nonneg[of "𝔏 p M" f] mult_right_mono by fastforce
    have **: "(λx. Norm (𝔏 p M) f * g x) ∈ space⇩N (𝔏 r M)"
      using spaceN_cmult[OF ‹g ∈ space⇩N (𝔏 q M)›] unfolding ‹q = r› scaleR_fun_def by simp
    have ***: "Norm (𝔏 r M) (λx. Norm (𝔏 p M) f * g x) = Norm (𝔏 p M) f * Norm (𝔏 q M) g"
      using Norm_cmult[of "𝔏 r M"] unfolding ‹q = r› scaleR_fun_def by auto
    then show ?thesis
      using Lp_domination[of "λx. f x * g x" M "λx. Norm (𝔏 p M) f * g x" r] unfolding ‹q = r›
      using * ** *** by auto
  qed
  then show "(λx. f x * g x) ∈ space⇩N (𝔏 r M)"
            "Norm (𝔏 r M) (λx. f x * g x) ≤ Norm (𝔏 p M) f * Norm (𝔏 q M) g"
    by auto
qed

text ‹The previous theorem admits an eNorm version in which one does not assume a priori
that the functions under consideration belong to $L^p$ or $L^q$.›

theorem Lp_Lq_emult:
  fixes p q r::ennreal
  assumes "1/p + 1/q = 1/r"
          "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  shows "eNorm (𝔏 r M) (λx. f x * g x) ≤ eNorm (𝔏 p M) f * eNorm (𝔏 q M) g"
proof (cases "r = 0")
  case True
  then have "eNorm (𝔏 r M) (λx. f x * g x) = 0"
    using assms by (simp add: L_zero(1))
  then show ?thesis by auto
next
  case False
  then have "r > 0" using not_gr_zero by blast
  then have "p > 0" "q > 0" using ‹1/p + 1/q = 1/r›
    by (metis ennreal_add_eq_top ennreal_divide_eq_top_iff ennreal_top_neq_one gr_zeroI zero_neq_one)+
  then have Z: "zero_space⇩N (𝔏 p M) = {f ∈ borel_measurable M. AE x in M. f x = 0}"
               "zero_space⇩N (𝔏 q M) = {f ∈ borel_measurable M. AE x in M. f x = 0}"
               "zero_space⇩N (𝔏 r M) = {f ∈ borel_measurable M. AE x in M. f x = 0}"
    using ‹r > 0› Lp_infinity_zero_space by auto
  have [measurable]: "(λx. f x * g x) ∈ borel_measurable M" using assms by auto
  consider "eNorm (𝔏 p M) f = 0 ∨ eNorm (𝔏 q M) g = 0"
         | "(eNorm (𝔏 p M) f > 0 ∧ eNorm (𝔏 q M) g = ∞) ∨ (eNorm (𝔏 p M) f = ∞ ∧ eNorm (𝔏 q M) g > 0)"
         | "eNorm (𝔏 p M) f < ∞ ∧ eNorm (𝔏 q M) g < ∞"
    using less_top by fastforce
  then show ?thesis
  proof (cases)
    case 1
    then have "(AE x in M. f x = 0) ∨ (AE x in M. g x = 0)" using Z unfolding zero_space⇩N_def by auto
    then have "AE x in M. f x * g x = 0" by auto
    then have "eNorm (𝔏 r M) (λx. f x * g x) = 0" using Z unfolding zero_space⇩N_def by auto
    then show ?thesis by simp
  next
    case 2
    then have "eNorm (𝔏 p M) f * eNorm (𝔏 q M) g = ∞" using ennreal_mult_eq_top_iff by force
    then show ?thesis by auto
  next
    case 3
    then have *: "f ∈ space⇩N (𝔏 p M)" "g ∈ space⇩N (𝔏 q M)" unfolding space⇩N_def by auto
    then have "(λx. f x * g x) ∈ space⇩N (𝔏 r M)" using Lp_Lq_mult(1)[OF assms(1)] by auto
    then show ?thesis
      using Lp_Lq_mult(2)[OF assms(1) *] by (simp add: eNorm_Norm * ennreal_mult'[symmetric])
  qed
qed

lemma Lp_Lq_duality_bound:
  fixes p q::ennreal
  assumes "1/p + 1/q = 1"
          "f ∈ space⇩N (𝔏 p M)"
          "g ∈ space⇩N (𝔏 q M)"
  shows "integrable M (λx. f x * g x)"
        "abs(∫x. f x * g x ∂M) ≤ Norm (𝔏 p M) f * Norm (𝔏 q M) g"
proof -
  have "(λx. f x * g x) ∈ space⇩N (𝔏 1 M)"
    apply (rule Lp_Lq_mult[OF _ ‹f ∈ space⇩N (𝔏 p M)› ‹g ∈ space⇩N (𝔏 q M)›])
    using ‹1/p + 1/q = 1› by auto
  then show "integrable M (λx. f x * g x)" using L1_space by auto

  have "abs(∫x. f x * g x ∂M) ≤ Norm (𝔏 1 M) (λx. f x * g x)" using L1_int_ineq by auto
  also have "... ≤ Norm (𝔏 p M) f * Norm (𝔏 q M) g"
    apply (rule Lp_Lq_mult[OF _ ‹f ∈ space⇩N (𝔏 p M)› ‹g ∈ space⇩N (𝔏 q M)›])
    using ‹1/p + 1/q = 1› by auto
  finally show "abs(∫x. f x * g x ∂M) ≤ Norm (𝔏 p M) f * Norm (𝔏 q M) g" by simp
qed

text ‹The next theorem asserts that the norm of an $L^p$ function $f$ can be obtained by estimating
the integrals of $fg$ over all $L^q$ functions $g$, where $1/p + 1/q = 1$. When $p = \infty$, it is
necessary to assume that the space is sigma-finite: for instance, if the space is one single atom
of infinite mass, then there is no nonzero $L^1$ function, so taking for $f$ the constant function
equal to $1$, it has $L^\infty$ norm equal to $1$, but $\int fg = 0$ for all $L^1$ function $g$.›

theorem Lp_Lq_duality:
  fixes p q::ennreal
  assumes "f ∈ space⇩N (𝔏 p M)"
          "1/p + 1/q = 1"
          "p = ∞ ⟹ sigma_finite_measure M"
  shows "bdd_above ((λg. (∫x. f x * g x ∂M))`{g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1})"
        "Norm (𝔏 p M) f = (SUP g∈{g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}. (∫x. f x * g x ∂M))"
proof -
  have [measurable]: "f ∈ borel_measurable M" using Lp_measurable[OF assms(1)] by auto
  have B: "(∫x. f x * g x ∂M) ≤ Norm (𝔏 p M) f" if "g ∈ {g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}" for g
  proof -
    have g: "g ∈ space⇩N (𝔏 q M)" "Norm (𝔏 q M) g ≤ 1" using that by auto
    have "(∫x. f x * g x ∂M) ≤ abs(∫x. f x * g x ∂M)" by auto
    also have "... ≤ Norm (𝔏 p M) f * Norm (𝔏 q M) g"
      using Lp_Lq_duality_bound(2)[OF ‹1/p + 1/q = 1› ‹f ∈ space⇩N (𝔏 p M)› g(1)] by auto
    also have "... ≤ Norm (𝔏 p M) f"
      using g(2) Norm_nonneg[of "𝔏 p M" f] mult_left_le by blast
    finally show "(∫x. f x * g x ∂M) ≤ Norm (𝔏 p M) f" by simp
  qed
  then show "bdd_above ((λg. (∫x. f x * g x ∂M))`{g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1})"
    by (meson bdd_aboveI2)

  show "Norm (𝔏 p M) f = (SUP g∈{g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}. (∫x. f x * g x ∂M))"
  proof (rule antisym)
    show "(SUP g∈{g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}. ∫x. f x * g x ∂M) ≤ Norm (𝔏 p M) f"
      by (rule cSUP_least, auto, rule exI[of _ 0], auto simp add: B)

    have "p ≥ 1" using conjugate_exponent_ennrealI(1)[OF ‹1/p + 1/q = 1›] by simp
    show "Norm (𝔏 p M) f ≤ (SUP g∈{g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}. (∫x. f x * g x ∂M))"
    using ‹p ≥ 1› proof (cases rule: Lp_cases_1_PInf)
      case PInf
      then have "f ∈ space⇩N (𝔏 ∞ M)"
        using ‹f ∈ space⇩N(𝔏 p M)› by simp
      have "q = 1" using ‹1/p + 1/q = 1› ‹p = ∞› by (simp add: divide_eq_1_ennreal)
      have "c ≤ (SUP g∈{g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}. (∫x. f x * g x ∂M))" if "c < Norm (𝔏 p M) f" for c
      proof (cases "c < 0")
        case True
        then have "c ≤ (∫x. f x * 0 x ∂M)" by auto
        also have "... ≤ (SUP g∈{g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}. (∫x. f x * g x ∂M))"
          apply (rule cSUP_upper, auto simp add: zero_fun_def[symmetric]) using B by (meson bdd_aboveI2)
        finally show ?thesis by simp
      next
        case False
        then have "ennreal c < eNorm (𝔏 ∞ M) f"
          using eNorm_Norm[OF ‹f ∈ space⇩N (𝔏 p M)›] that ennreal_less_iff unfolding ‹p = ∞› by auto
        then have *: "emeasure M {x ∈ space M. ¦f x¦ > c} > 0" using L_infinity_pos_measure[of f M c] by auto
        obtain A where [measurable]: "⋀(n::nat). A n ∈ sets M" and "(⋃i. A i) = space M" "⋀i. emeasure M (A i) ≠ ∞"
          using sigma_finite_measure.sigma_finite[OF ‹p = ∞ ⟹ sigma_finite_measure M›[OF ‹p = ∞›]] by (metis UNIV_I sets_range)
        define Y where "Y = (λn::nat. {x ∈ A n. ¦f x¦ > c})"
        have [measurable]: "Y n ∈ sets M" for n unfolding Y_def by auto
        have "{x ∈ space M. ¦f x¦ > c} = (⋃n. Y n)" unfolding Y_def using ‹(⋃i. A i) = space M› by auto
        then have "emeasure M (⋃n. Y n) > 0" using * by auto
        then obtain n where "emeasure M (Y n) > 0"
          using emeasure_pos_unionE[of Y, OF ‹⋀n. Y n ∈ sets M›] by auto
        have "emeasure M (Y n) ≤ emeasure M (A n)" apply (rule emeasure_mono) unfolding Y_def by auto
        then have "emeasure M (Y n) ≠ ∞" using ‹emeasure M (A n) ≠ ∞›
          by (metis infinity_ennreal_def neq_top_trans)
        then have "measure M (Y n) > 0" using ‹emeasure M (Y n) > 0› unfolding measure_def
          by (simp add: enn2real_positive_iff top.not_eq_extremum)
        have "¦f x¦ ≥ c" if "x ∈ Y n" for x using that less_imp_le unfolding Y_def by auto

        define g where "g = (λx. indicator (Y n) x * sgn(f x)) /⇩R measure M (Y n)"
        have "g ∈ space⇩N (𝔏 1 M)"
          apply (rule Lp_domination[of _ _ "indicator (Y n) /⇩R measure M (Y n)"]) unfolding g_def
          using L1_indicator'[OF ‹Y n ∈ sets M› ‹emeasure M (Y n) ≠ ∞›] by (auto simp add: abs_mult indicator_def abs_sgn_eq)
        have "Norm (𝔏 1 M) g = Norm (𝔏 1 M) (λx. indicator (Y n) x * sgn(f x)) / abs(measure M (Y n))"
          unfolding g_def Norm_cmult by (simp add: divide_inverse)
        also have "... ≤ Norm (𝔏 1 M) (indicator (Y n)) / abs(measure M (Y n))"
          using ‹measure M (Y n) > 0› apply (auto simp add: divide_simps) apply (rule Lp_domination)
          using L1_indicator'[OF ‹Y n ∈ sets M› ‹emeasure M (Y n) ≠ ∞›] by (auto simp add: abs_mult indicator_def abs_sgn_eq)
        also have "... = measure M (Y n) / abs(measure M (Y n))"
          using L1_indicator'[OF ‹Y n ∈ sets M› ‹emeasure M (Y n) ≠ ∞›] by (auto simp add: abs_mult indicator_def abs_sgn_eq)
        also have "... = 1" using ‹measure M (Y n) > 0› by auto
        finally have "Norm (𝔏 1 M) g ≤ 1" by simp

        have "c * measure M (Y n) = (∫x. c * indicator (Y n) x ∂M)"
          using ‹measure M (Y n) > 0› ‹emeasure M (Y n) ≠ ∞› by auto
        also have "... ≤ (∫x. ¦f x¦ * indicator (Y n) x ∂M)"
          apply (rule integral_mono)
          using ‹emeasure M (Y n) ≠ ∞› ‹0 < Sigma_Algebra.measure M (Y n)› not_integrable_integral_eq apply fastforce
          apply (rule Bochner_Integration.integrable_bound[of _ "λx. Norm (𝔏 ∞ M) f * indicator (Y n) x"])
          using ‹emeasure M (Y n) ≠ ∞› ‹0 < Sigma_Algebra.measure M (Y n)› not_integrable_integral_eq apply fastforce
          using L_infinity_AE_bound[OF ‹f ∈ space⇩N (𝔏 ∞ M)›] by (auto simp add: indicator_def Y_def)
        finally have "c ≤ (∫x. ¦f x¦ * indicator (Y n) x ∂M) / measure M (Y n)"
          using ‹measure M (Y n) > 0› by (auto simp add: divide_simps)
        also have "... = (∫x. f x * indicator (Y n) x * sgn(f x) / measure M (Y n) ∂M)"
          using ‹measure M (Y n) > 0› by (simp add: abs_sgn mult.commute mult.left_commute)
        also have "... = (∫x. f x * g x ∂M)"
          unfolding divide_inverse g_def divideR_apply by (auto simp add: algebra_simps)
        also have "... ≤ (SUP g∈{g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}. (∫x. f x * g x ∂M))"
          unfolding ‹q = 1› apply (rule cSUP_upper, auto)
          using ‹g ∈ space⇩N (𝔏 1 M)› ‹Norm (𝔏 1 M) g ≤ 1› apply auto using B ‹p = ∞› ‹q = 1› by (meson bdd_aboveI2)
        finally show ?thesis by simp
      qed
      then show ?thesis using dense_le by auto
    next
      case one
      then have "q = ∞" using ‹1/p + 1/q = 1› by simp
      define g where "g = (λx. sgn (f x))"
      have [measurable]: "g ∈ space⇩N (𝔏 ∞ M)"
        apply (rule L_infinity_I[of g M 1]) unfolding g_def by (auto simp add: abs_sgn_eq)
      have "Norm (𝔏 ∞ M) g ≤ 1"
        apply (rule L_infinity_I[of g M 1]) unfolding g_def by (auto simp add: abs_sgn_eq)
      have "Norm (𝔏 p M) f = (∫x. ¦f x¦ ∂M)"
        unfolding ‹p = 1› apply (rule L1_D(3)) using ‹f ∈ space⇩N (𝔏 p M)› unfolding ‹p = 1› by auto
      also have "... = (∫x. f x * g x ∂M)"
        unfolding g_def by (simp add: abs_sgn)
      also have "... ≤ (SUP g∈{g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}. (∫x. f x * g x ∂M))"
        unfolding ‹q = ∞› apply (rule cSUP_upper, auto)
        using ‹g ∈ space⇩N (𝔏 ∞ M)› ‹Norm (𝔏 ∞ M) g ≤ 1› apply auto
        using B ‹q = ∞› by fastforce
      finally show ?thesis by simp
    next
      case (gr p2)
      then have "p2 > 0" by simp
      have "f ∈ space⇩N (𝔏 p2 M)" using ‹f ∈ space⇩N (𝔏 p M)› ‹p = ennreal p2› by auto
      define q2 where "q2 = conjugate_exponent p2"
      have "q2 > 1" "q2 > 0" using conjugate_exponent_real(2)[OF ‹p2 > 1›] unfolding q2_def by auto
      have "q = ennreal q2"
        unfolding q2_def conjugate_exponent_real_ennreal[OF ‹p2 > 1›, symmetric] ‹p = ennreal p2›[symmetric]
        using conjugate_exponent_ennreal_iff[OF ‹p ≥ 1›] ‹1/p + 1/q = 1› by auto

      show ?thesis
      proof (cases "Norm (𝔏 p M) f = 0")
        case True
        then have "Norm (𝔏 p M) f ≤ (∫x. f x * 0 x ∂M)" by auto
        also have "... ≤ (SUP g∈{g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}. (∫x. f x * g x ∂M))"
          apply (rule cSUP_upper, auto simp add: zero_fun_def[symmetric]) using B by (meson bdd_aboveI2)
        finally show ?thesis by simp
      next
        case False
        then have "Norm (𝔏 p2 M) f > 0"
          unfolding ‹p = ennreal p2› using Norm_nonneg[of "𝔏 p2 M" f] by linarith

        define h where "h = (λx. sgn(f x) * ¦f x¦ powr (p2 - 1))"
        have [measurable]: "h ∈ borel_measurable M" unfolding h_def by auto
        have "(∫⇧+x. ¦h x¦ powr q2 ∂M) = (∫⇧+x. (¦f x¦ powr (p2 - 1)) powr q2 ∂M)"
          unfolding h_def by (rule nn_integral_cong, auto simp add: abs_mult abs_sgn_eq)
        also have "... = (∫⇧+x. ¦f x¦ powr p2 ∂M)"
          unfolding powr_powr q2_def using conjugate_exponent_real(4)[OF ‹p2 > 1›] by auto
        also have "... = (Norm (𝔏 p2 M) f) powr p2"
          apply (subst Lp_Norm(2), auto simp add: ‹p2 > 0›)
          by (rule nn_integral_eq_integral, auto simp add: Lp_D(2)[OF ‹p2 > 0› ‹f ∈ space⇩N (𝔏 p2 M)›])
        finally have *: "(∫⇧+x. ¦h x¦ powr q2 ∂M) = (Norm (𝔏 p2 M) f) powr p2" by simp
        have "integrable M (λx. ¦h x¦ powr q2)"
          apply (rule integrableI_bounded, auto) using * by auto
        then have "(∫x. ¦h x¦ powr q2 ∂M) = (∫⇧+x. ¦h x¦ powr q2 ∂M)"
          by (rule nn_integral_eq_integral[symmetric], auto)
        then have **: "(∫x. ¦h x¦ powr q2 ∂M) = (Norm (𝔏 p2 M) f) powr p2" using * by auto

        define g where "g = (λx. h x / (Norm (𝔏 p2 M) f) powr (p2 / q2))"
        have [measurable]: "g ∈ borel_measurable M" unfolding g_def by auto
        have intg: "integrable M (λx. ¦g x¦ powr q2)"
          unfolding g_def using ‹Norm (𝔏 p2 M) f > 0› ‹q2 > 1› apply (simp add: abs_mult powr_divide powr_powr)
          using ‹integrable M (λx. ¦h x¦ powr q2)› integrable_divide_zero by blast
        have "g ∈ space⇩N (𝔏 q2 M)" by (rule Lp_I(1)[OF ‹q2 > 0› _ intg], auto)
        have "(∫x. ¦g x¦ powr q2 ∂M) = 1"
          unfolding g_def using ‹Norm (𝔏 p2 M) f > 0› ‹q2 > 1› by (simp add: abs_mult powr_divide powr_powr **)
        then have "Norm (𝔏 q2 M) g = 1"
          apply (subst Lp_D[OF ‹q2 > 0›]) using ‹g ∈ space⇩N (𝔏 q2 M)› by auto

        have "(∫x. f x * g x ∂M) = (∫x. f x * sgn(f x) * ¦f x¦ powr (p2 - 1) / (Norm (𝔏 p2 M) f) powr (p2 / q2) ∂M)"
          unfolding g_def h_def by (simp add: mult.assoc)
        also have "... = (∫x. ¦f x¦ * ¦f x¦ powr (p2-1) ∂M) / (Norm (𝔏 p2 M) f) powr (p2 / q2)"
          by (auto simp add: abs_sgn)
        also have "... = (∫x. ¦f x¦ powr p2 ∂M) / (Norm (𝔏 p2 M) f) powr (p2 / q2)"
          by (subst powr_mult_base, auto)
        also have "... = (Norm (𝔏 p2 M) f) powr p2 / (Norm (𝔏 p2 M) f) powr (p2 / q2)"
          by (subst Lp_Norm(2)[OF ‹p2 > 0›], auto)
        also have "... = (Norm (𝔏 p2 M) f) powr (p2 - p2/q2)"
          by (simp add: powr_diff [symmetric] )
        also have "... = Norm (𝔏 p2 M) f"
          unfolding q2_def using conjugate_exponent_real(5)[OF ‹p2 > 1›] by auto
        finally have "Norm (𝔏 p M) f = (∫x. f x * g x ∂M)"
          unfolding ‹p = ennreal p2› by simp
        also have "... ≤ (SUP g∈{g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}. (∫x. f x * g x ∂M))"
          unfolding ‹q = ennreal q2› apply (rule cSUP_upper, auto)
          using ‹g ∈ space⇩N (𝔏 q2 M)› ‹Norm (𝔏 q2 M) g = 1› apply auto
          using B ‹q = ennreal q2› by fastforce
        finally show ?thesis by simp
      qed
    qed
  qed
qed

text ‹The previous theorem admits a version in which one does not assume a priori that the
function under consideration belongs to $L^p$. This gives an efficient criterion to check
if a function is indeed in $L^p$. In this case, it is always necessary to assume that the
measure is sigma-finite.

Note that, in the statement, the Bochner integral $\int fg$ vanishes by definition if
$fg$ is not integrable. Hence, the statement really says that the eNorm can be estimated
using functions $g$ for which $fg$ is integrable. It is precisely the construction of such
functions $g$ that requires the space to be sigma-finite.›

theorem Lp_Lq_duality':
  fixes p q::ennreal
  assumes "1/p + 1/q = 1"
          "sigma_finite_measure M"
      and [measurable]: "f ∈ borel_measurable M"
  shows "eNorm (𝔏 p M) f = (SUP g∈{g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}. ennreal(∫x. f x * g x ∂M))"
proof (cases "eNorm (𝔏 p M) f ≠ ∞")
  case True
  then have "f ∈ space⇩N (𝔏 p M)" unfolding space⇩N_def by (simp add: top.not_eq_extremum)
  show ?thesis
    unfolding eNorm_Norm[OF ‹f ∈ space⇩N (𝔏 p M)›] Lp_Lq_duality[OF ‹f ∈ space⇩N (𝔏 p M)› ‹1/p + 1/q = 1› ‹sigma_finite_measure M›]
    apply (rule SUP_real_ennreal[symmetric], auto, rule exI[of _ 0], auto)
    by (rule Lp_Lq_duality[OF ‹f ∈ space⇩N (𝔏 p M)› ‹1/p + 1/q = 1› ‹sigma_finite_measure M›])
next
  case False
  have B: "∃g ∈ {g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}. (∫x. f x * g x ∂M) ≥ C" if "C < ∞" for C::ennreal
  proof -
    obtain Cr where "C = ennreal Cr" "Cr ≥ 0" using ‹C < ∞› ennreal_cases less_irrefl by auto
    obtain A where A: "⋀n::nat. A n ∈ sets M" "incseq A" "(⋃n. A n) = space M"
            "⋀n. emeasure M (A n) ≠ ∞"
      using sigma_finite_measure.sigma_finite_incseq[OF ‹sigma_finite_measure M›] by (metis range_subsetD)
    define Y where "Y = (λn. {x ∈ A n. ¦f x¦ ≤ n})"
    have [measurable]: "⋀n. Y n ∈ sets M" unfolding Y_def using ‹⋀n::nat. A n ∈ sets M› by auto
    have "incseq Y"
      apply (rule incseq_SucI) unfolding Y_def using incseq_SucD[OF ‹incseq A›] by auto
    have *: "∃N. ∀n ≥ N. f x * indicator (Y n) x = f x" if "x ∈ space M" for x
    proof -
      obtain n0 where n0: "x ∈ A n0" using ‹x ∈ space M› ‹(⋃n. A n) = space M› by auto
      obtain n1::nat where n1: "¦f x¦ ≤ n1" using real_arch_simple by blast
      have "x ∈ Y (max n0 n1)"
        unfolding Y_def using n1 apply auto
        using n0 ‹incseq A› incseq_def max.cobounded1 by blast
      then have *: "x ∈ Y n" if "n ≥ max n0 n1" for n
        using ‹incseq Y› that incseq_def by blast
      show ?thesis by (rule exI[of _ "max n0 n1"], auto simp add: *)
    qed
    have *: "(λn. f x * indicator (Y n) x) ⇢ f x" if "x ∈ space M" for x
      using *[OF that] unfolding eventually_sequentially[symmetric] by (simp add: tendsto_eventually)
    have "liminf (λn. eNorm (𝔏 p M) (λx. f x * indicator (Y n) x)) ≥ eNorm (𝔏 p M) f"
      apply (rule Lp_AE_limit) using * by auto
    then have "liminf (λn. eNorm (𝔏 p M) (λx. f x * indicator (Y n) x)) > Cr" using False neq_top_trans by force
    then have "limsup (λn. eNorm (𝔏 p M) (λx. f x * indicator (Y n) x)) > Cr"
      using Liminf_le_Limsup less_le_trans trivial_limit_sequentially by blast
    then obtain n where n: "eNorm (𝔏 p M) (λx. f x * indicator (Y n) x) > Cr"
      using Limsup_obtain by blast

    have "(λx. f x * indicator (Y n) x) ∈ space⇩N (𝔏 p M)"
      apply (rule Lp_bounded_bounded_support[of _ _ n], auto)
      unfolding Y_def indicator_def apply auto
      by (metis (mono_tags, lifting) A(1) A(4) emeasure_mono infinity_ennreal_def mem_Collect_eq neq_top_trans subsetI)
    have "Norm (𝔏 p M) (λx. f x * indicator (Y n) x) > Cr"
      using n unfolding eNorm_Norm[OF ‹(λx. f x * indicator (Y n) x) ∈ space⇩N (𝔏 p M)›]
      by (meson ennreal_leI not_le)
    then have "(SUP g∈{g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}. (∫x. f x * indicator (Y n) x * g x ∂M)) > Cr"
      using Lp_Lq_duality(2)[OF ‹(λx. f x * indicator (Y n) x) ∈ space⇩N (𝔏 p M)› ‹1/p + 1/q = 1› ‹sigma_finite_measure M›]
      by auto
    then have "∃g ∈ {g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}. (∫x. f x * indicator (Y n) x * g x ∂M) > Cr"
      apply (subst less_cSUP_iff[symmetric])
      using Lp_Lq_duality(1)[OF ‹(λx. f x * indicator (Y n) x) ∈ space⇩N (𝔏 p M)› ‹1/p + 1/q = 1› ‹sigma_finite_measure M›] apply auto
      by (rule exI[of _ 0], auto)
    then obtain g where g: "g ∈ space⇩N (𝔏 q M)" "Norm (𝔏 q M) g ≤ 1" "(∫x. f x * indicator (Y n) x * g x ∂M) > Cr"
      by auto
    then have [measurable]: "g ∈ borel_measurable M" using Lp_measurable by auto
    define h where "h = (λx. indicator (Y n) x * g x)"
    have "Norm (𝔏 q M) h ≤ Norm (𝔏 q M) g"
      apply (rule Lp_domination[of _ _ g]) unfolding h_def indicator_def using ‹g ∈ space⇩N (𝔏 q M)› by auto
    then have a: "Norm (𝔏 q M) h ≤ 1" using ‹Norm (𝔏 q M) g ≤ 1› by auto
    have b: "h ∈ space⇩N (𝔏 q M)"
      apply (rule Lp_domination[of _ _ g]) unfolding h_def indicator_def using ‹g ∈ space⇩N (𝔏 q M)› by auto
    have "(∫x. f x * h x ∂M) > Cr" unfolding h_def using g(3) by (auto simp add: mult.assoc)
    then have "(∫x. f x * h x ∂M) > C"
      unfolding ‹C = ennreal Cr› using ‹Cr ≥ 0› by (simp add: ennreal_less_iff)
    then show ?thesis using a b by auto
  qed
  have "(SUP g∈{g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}. ennreal(∫x. f x * g x ∂M)) ≥ ∞"
    apply (rule dense_le) using B by (meson SUP_upper2)
  then show ?thesis using False neq_top_trans by force
qed


subsection ‹Conditional expectations and $L^p$›

text ‹The $L^p$ space with respect to a subalgebra is included in the whole $L^p$ space.›

lemma Lp_subalgebra:
  assumes "subalgebra M F"
  shows "⋀f. eNorm (𝔏 p M) f ≤ eNorm (𝔏 p (restr_to_subalg M F)) f"
        "(𝔏 p (restr_to_subalg M F)) ⊆⇩N 𝔏 p M"
        "space⇩N ((𝔏 p (restr_to_subalg M F))) ⊆ space⇩N (𝔏 p M)"
        "⋀f. f ∈ space⇩N ((𝔏 p (restr_to_subalg M F))) ⟹ Norm (𝔏 p M) f = Norm (𝔏 p (restr_to_subalg M F)) f"
proof -
  have *: "f ∈ space⇩N (𝔏 p M) ∧ Norm (𝔏 p M) f = Norm (𝔏 p (restr_to_subalg M F)) f"
       if "f ∈ space⇩N (𝔏 p (restr_to_subalg M F))" for f
  proof -
    have [measurable]: "f ∈ borel_measurable (restr_to_subalg M F)" using that Lp_measurable by auto
    then have [measurable]: "f ∈ borel_measurable M"
      using assms measurable_from_subalg measurable_in_subalg' by blast
    show ?thesis
    proof (cases rule: Lp_cases[of p])
      case zero
      then show ?thesis using that unfolding ‹p = 0› L_zero_space Norm_def L_zero by auto
    next
      case PInf
      have [measurable]: "f ∈ borel_measurable (restr_to_subalg M F)" using that Lp_measurable by auto
      then have [measurable]: "f ∈ borel_measurable F" using assms measurable_in_subalg' by blast
      then have [measurable]: "f ∈ borel_measurable M" using assms measurable_from_subalg by blast
      have "AE x in (restr_to_subalg M F). ¦f x¦ ≤ Norm (𝔏 ∞ (restr_to_subalg M F)) f"
        using L_infinity_AE_bound that unfolding ‹p = ∞› by auto
      then have a: "AE x in M. ¦f x¦ ≤ Norm (𝔏 ∞ (restr_to_subalg M F)) f"
        using assms AE_restr_to_subalg by blast
      have *: "f ∈ space⇩N (𝔏 ∞ M)" "Norm (𝔏 ∞ M) f ≤ Norm (𝔏 ∞ (restr_to_subalg M F)) f"
        using L_infinity_I[OF ‹f ∈ borel_measurable M› a] by auto
      then have b: "AE x in M. ¦f x¦ ≤ Norm (𝔏 ∞ M) f"
        using L_infinity_AE_bound by auto
      have c: "AE x in (restr_to_subalg M F). ¦f x¦ ≤ Norm (𝔏 ∞ M) f"
        apply (rule AE_restr_to_subalg2[OF assms]) using b by auto
      have "Norm (𝔏 ∞ (restr_to_subalg M F)) f ≤ Norm (𝔏 ∞ M) f"
        using L_infinity_I[OF ‹f ∈ borel_measurable (restr_to_subalg M F)› c] by auto
      then show ?thesis using * unfolding ‹p = ∞› by auto
    next
      case (real_pos p2)
      then have a [measurable]: "f ∈ space⇩N (𝔏 p2 (restr_to_subalg M F))"
        using that unfolding ‹p = ennreal p2› by auto
      then have b [measurable]: "f ∈ space⇩N (𝔏 p2 M)"
        unfolding Lp_space[OF ‹p2 > 0›] using integrable_from_subalg[OF assms] by auto
      show ?thesis
        unfolding ‹p = ennreal p2› Lp_D[OF ‹p2 > 0› a] Lp_D[OF ‹p2 > 0› b]
        using integral_subalgebra2[OF assms, symmetric, of f] apply (auto simp add: b)
        by (metis (mono_tags, lifting) ‹integrable (restr_to_subalg M F) (λx. ¦f x¦ powr p2)› assms integrableD(1) integral_subalgebra2 measurable_in_subalg')
    qed
  qed
  show "space⇩N ((𝔏 p (restr_to_subalg M F))) ⊆ space⇩N (𝔏 p M)" using * by auto
  show "Norm (𝔏 p M) f = Norm (𝔏 p (restr_to_subalg M F)) f" if "f ∈ space⇩N ((𝔏 p (restr_to_subalg M F)))" for f
    using * that by auto
  show "eNorm (𝔏 p M) f ≤ eNorm (𝔏 p (restr_to_subalg M F)) f" for f
    by (metis "*" eNorm_Norm eq_iff infinity_ennreal_def less_imp_le spaceN_iff top.not_eq_extremum)
  then show "(𝔏 p (restr_to_subalg M F)) ⊆⇩N 𝔏 p M"
    by (metis ennreal_1 mult.left_neutral quasinorm_subsetI)
qed

text ‹For $p \geq 1$, the conditional expectation of an $L^p$ function still belongs to $L^p$,
with an $L^p$ norm which is bounded by the norm of the original function. This is wrong for
$p < 1$. One can prove this separating the cases and using the conditional version of Jensen's
inequality, but it is much more efficient to do it with duality arguments, as follows.›

proposition Lp_real_cond_exp:
  assumes [simp]: "subalgebra M F"
      and "p ≥ (1::ennreal)"
          "sigma_finite_measure (restr_to_subalg M F)"
          "f ∈ space⇩N (𝔏 p M)"
  shows "real_cond_exp M F f ∈ space⇩N (𝔏 p (restr_to_subalg M F))"
        "Norm (𝔏 p (restr_to_subalg M F)) (real_cond_exp M F f) ≤ Norm (𝔏 p M) f"
proof -
  have [measurable]: "f ∈ borel_measurable M" using Lp_measurable assms by auto
  define q where "q = conjugate_exponent p"
  have "1/p + 1/q = 1" unfolding q_def using conjugate_exponent_ennreal[OF ‹p ≥ 1›] by simp
  have "eNorm (𝔏 p (restr_to_subalg M F)) (real_cond_exp M F f)
    = (SUP g∈{g ∈ space⇩N (𝔏 q (restr_to_subalg M F)). Norm (𝔏 q (restr_to_subalg M F)) g ≤ 1}. ennreal(∫x. (real_cond_exp M F f) x * g x ∂(restr_to_subalg M F)))"
    by (rule Lp_Lq_duality'[OF ‹1/p + 1/q = 1› ‹sigma_finite_measure (restr_to_subalg M F)›], simp)
  also have "... ≤ (SUP g∈{g ∈ space⇩N (𝔏 q M). Norm (𝔏 q M) g ≤ 1}. ennreal(∫x. f x * g x ∂M))"
  proof (rule SUP_mono, auto)
    fix g assume H: "g ∈ space⇩N (𝔏 q (restr_to_subalg M F))"
                    "Norm (𝔏 q (restr_to_subalg M F)) g ≤ 1"
    then have H2: "g ∈ space⇩N (𝔏 q M)" "Norm (𝔏 q M) g ≤ 1"
      using Lp_subalgebra[OF ‹subalgebra M F›] by (auto simp add: subset_iff)
    have [measurable]: "g ∈ borel_measurable M" "g ∈ borel_measurable F"
      using Lp_measurable[OF H(1)] Lp_measurable[OF H2(1)] by auto
    have int: "integrable M (λx. f x * g x)"
      using Lp_Lq_duality_bound(1)[OF ‹1/p + 1/q = 1› ‹f ∈ space⇩N (𝔏 p M)› H2(1)].
    have "(∫x. (real_cond_exp M F f) x * g x ∂(restr_to_subalg M F)) = (∫x. g x * (real_cond_exp M F f) x ∂M)"
      by (subst mult.commute, rule integral_subalgebra2[OF ‹subalgebra M F›], auto)
    also have "... = (∫x. g x * f x ∂M)"
      apply (rule sigma_finite_subalgebra.real_cond_exp_intg, auto simp add: int mult.commute)
      unfolding sigma_finite_subalgebra_def using assms by auto
    finally have "ennreal (∫x. (real_cond_exp M F f) x * g x ∂(restr_to_subalg M F)) ≤ ennreal (∫x. f x * g x ∂M)"
      by (auto intro!: ennreal_leI simp add: mult.commute)
    then show "∃m. m ∈ space⇩N (𝔏 q M) ∧ Norm (𝔏 q M) m ≤ 1
        ∧ ennreal (LINT x|restr_to_subalg M F. real_cond_exp M F f x * g x) ≤ ennreal (LINT x|M. f x * m x)"
      using H2 by blast
  qed
  also have "... = eNorm (𝔏 p M) f"
    apply (rule Lp_Lq_duality'[OF ‹1/p + 1/q = 1›, symmetric], auto intro!: sigma_finite_subalgebra_is_sigma_finite[of _ F])
    unfolding sigma_finite_subalgebra_def using assms by auto
  finally have *: "eNorm (𝔏 p (restr_to_subalg M F)) (real_cond_exp M F f) ≤ eNorm (𝔏 p M) f"
    by simp
  then show a: "real_cond_exp M F f ∈ space⇩N (𝔏 p (restr_to_subalg M F))"
    by (meson ‹f ∈ space⇩N (𝔏 p M)› order_le_less_trans spaceN_iff)
  show "Norm (𝔏 p (restr_to_subalg M F)) (real_cond_exp M F f) ≤ Norm (𝔏 p M) f"
    using * unfolding eNorm_Norm[OF ‹f ∈ space⇩N (𝔏 p M)›] eNorm_Norm[OF a] by simp
qed

lemma Lp_real_cond_exp_eNorm:
  assumes [simp]: "subalgebra M F"
      and "p ≥ (1::ennreal)"
          "sigma_finite_measure (restr_to_subalg M F)"
  shows "eNorm (𝔏 p (restr_to_subalg M F)) (real_cond_exp M F f) ≤ eNorm (𝔏 p M) f"
proof (cases "eNorm (𝔏 p M) f = ∞")
  case False
  then have *: "f ∈ space⇩N (𝔏 p M)"
    unfolding spaceN_iff by (simp add: top.not_eq_extremum)
  show ?thesis
    using Lp_real_cond_exp[OF assms ‹f ∈ space⇩N (𝔏 p M)›] by (subst eNorm_Norm, auto simp: ‹f ∈ space⇩N (𝔏 p M)›)+
qed (simp)

end