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 q1, 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::'areal). e2ennreal(esssup M (λx. ereal ¦f x¦)))"
    apply (rule quasinorm_onI) using T H Z by auto
  have **: "quasinorm_on UNIV 1 (λ(f::'areal). 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:
  "spaceN (𝔏  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  spaceN (𝔏  M)"
  then show "f  borel_measurable M"
    unfolding spaceN_def using L_infinity(1)[of M] top.not_eq_extremum by fastforce
  then have *: "esssup M (λx. ¦f x¦) < "
    using H unfolding spaceN_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  spaceN (𝔏  M)"
    using spaceN_iff le_less_trans by fastforce
qed

lemma L_infinity_zero_space:
  "zero_spaceN (𝔏  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_spaceN (𝔏  M)"
  then show "f  borel_measurable M"
    unfolding zero_spaceN_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_spaceN_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_spaceN (𝔏  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  spaceN (𝔏  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  spaceN (𝔏  M)"
        "Norm (𝔏  M) f  C"
proof -
  show "f  spaceN (𝔏  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  spaceN (𝔏  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)  (eesssup 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_inN (𝔏  M) f g"
          "n. f n  spaceN (𝔏  M)"
          "g  spaceN (𝔏  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_inN (𝔏  M) f g unfolding tendsto_inN_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 "spaceN bcontfunN  spaceN (𝔏  M)"
        "f. f  spaceN bcontfunN  Norm (𝔏  M) f  Norm bcontfunN f"
        "f. eNorm (𝔏  M) f  eNorm bcontfunN f"
        "bcontfunN N 𝔏  M"
proof -
  have *: "f  spaceN (𝔏  M)  Norm (𝔏  M) f  Norm bcontfunN f" if "f  spaceN bcontfunN" for f
  proof -
    have H: "continuous_on UNIV f" "x. abs(f x)  Norm bcontfunN f"
      using bcontfunND[OF f  spaceN bcontfunN] 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 bcontfunN f" using H(2) by auto
    show ?thesis using L_infinity_I[OF f  borel_measurable M * Norm_nonneg] by auto
  qed
  show "spaceN bcontfunN  spaceN (𝔏  M)"
       "f. f  spaceN bcontfunN  Norm (𝔏  M) f  Norm bcontfunN f"
    using * by auto
  show **: "bcontfunN N 𝔏  M"
    apply (rule quasinorm_subsetI'[of _ _ 1]) using * by auto
  have "eNorm (𝔏  M) f  ennreal 1 * eNorm bcontfunN f" for f
    apply (rule quasinorm_subset_Norm_eNorm) using * ** by auto
  then show "eNorm (𝔏  M) f  eNorm bcontfunN 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::'areal). (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::'areal). (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 "spaceN (𝔏 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  spaceN (𝔏 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  spaceN (𝔏 p M)" unfolding spaceN_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  spaceN (𝔏 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  spaceN (𝔏 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_spaceN (𝔏 p M) = {f  borel_measurable M. AE x in M. f x = 0}"
proof (auto)
  fix f assume H: "f  zero_spaceN (𝔏 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_spaceN_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_spaceN (𝔏 p M)"
    using zero_spaceN_iff by auto
qed

lemma Lp_tendsto_AE_subseq:
  assumes "p>(0::real)"
          "tendsto_inN (𝔏 p M) f g"
          "n. f n  spaceN (𝔏 p M)"
          "g  spaceN (𝔏 p M)"
  shows "r. strict_mono r  (AE x in M. (λn. f (r n) x)  g x)"
proof -
  have "f n - g  spaceN (𝔏 p M)" for n
    using spaceN_diff[OF n. f n  spaceN (𝔏 p M) g  spaceN (𝔏 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  spaceN (𝔏 p M)] by auto

  have "(λn. Norm (𝔏 p M) (f n - g))  0"
    using tendsto_inN (𝔏 p M) f g unfolding tendsto_inN_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  spaceN (𝔏 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:
  "spaceN (𝔏 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  spaceN (𝔏 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  spaceN (𝔏 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