# Theory Lp.Lp

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

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]

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"
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 (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)

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)
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
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 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 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))"
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)"
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)"
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))"
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)"
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¦)"
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)
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)}"
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