[STATEMENT]
lemma Lp_zero_space:
  assumes "p > (0::real)"
  shows "zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_space\<^sub>N (\<LL> (ennreal p) M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M) \<Longrightarrow> x \<in> borel_measurable M
 2. \<And>x. x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M) \<Longrightarrow> AE xa in M. x xa = 0
 3. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M) \<Longrightarrow> x \<in> borel_measurable M
 2. \<And>x. x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M) \<Longrightarrow> AE xa in M. x xa = 0
 3. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
assume H: "f \<in> zero_space\<^sub>N (\<LL> p M)"
[PROOF STATE]
proof (state)
this:
f \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)

goal (3 subgoals):
 1. \<And>x. x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M) \<Longrightarrow> x \<in> borel_measurable M
 2. \<And>x. x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M) \<Longrightarrow> AE xa in M. x xa = 0
 3. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
have *: "f \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}"
[PROOF STATE]
proof (prove)
using this:
f \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)

goal (1 subgoal):
 1. f \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}
[PROOF STEP]
using Lp_space[OF assms] zero_spaceN_subset_spaceN
[PROOF STATE]
proof (prove)
using this:
f \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
space\<^sub>N (\<LL> (ennreal p) ?M) = {f \<in> borel_measurable ?M. integrable ?M (\<lambda>x. \<bar>f x\<bar> powr p)}
zero_space\<^sub>N ?N \<subseteq> space\<^sub>N ?N

goal (1 subgoal):
 1. f \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}

goal (3 subgoals):
 1. \<And>x. x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M) \<Longrightarrow> x \<in> borel_measurable M
 2. \<And>x. x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M) \<Longrightarrow> AE xa in M. x xa = 0
 3. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}
[PROOF STEP]
show "f \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}

goal (1 subgoal):
 1. f \<in> borel_measurable M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> borel_measurable M

goal (2 subgoals):
 1. \<And>x. x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M) \<Longrightarrow> AE xa in M. x xa = 0
 2. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
have "eNorm (\<LL> p M) f = (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))
[PROOF STEP]
by (cases "p \<le> 1", insert * \<open>p > 0\<close>, auto simp add: Lp_le_1(1) Lp(1))
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))

goal (2 subgoals):
 1. \<And>x. x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M) \<Longrightarrow> AE xa in M. x xa = 0
 2. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))
[PROOF STEP]
have "(\<integral>x. \<bar>f x\<bar> powr p \<partial>M) = 0"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))

goal (1 subgoal):
 1. LINT x|M. \<bar>f x\<bar> powr p = 0
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))
f \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)

goal (1 subgoal):
 1. LINT x|M. \<bar>f x\<bar> powr p = 0
[PROOF STEP]
unfolding zero_space\<^sub>N_def
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))
f \<in> {f. eNorm (\<LL> (ennreal p) M) f = 0}

goal (1 subgoal):
 1. LINT x|M. \<bar>f x\<bar> powr p = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>f x\<bar> powr p = 0

goal (2 subgoals):
 1. \<And>x. x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M) \<Longrightarrow> AE xa in M. x xa = 0
 2. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
LINT x|M. \<bar>f x\<bar> powr p = 0
[PROOF STEP]
have "AE x in M. \<bar>f x\<bar> powr p = 0"
[PROOF STATE]
proof (prove)
using this:
LINT x|M. \<bar>f x\<bar> powr p = 0

goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> powr p = 0
[PROOF STEP]
by (subst integral_nonneg_eq_0_iff_AE[symmetric], insert *, auto)
[PROOF STATE]
proof (state)
this:
AE x in M. \<bar>f x\<bar> powr p = 0

goal (2 subgoals):
 1. \<And>x. x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M) \<Longrightarrow> AE xa in M. x xa = 0
 2. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. \<bar>f x\<bar> powr p = 0
[PROOF STEP]
show "AE x in M. f x = 0"
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<bar>f x\<bar> powr p = 0

goal (1 subgoal):
 1. AE x in M. f x = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. f x = 0

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
fix f::"'a \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
assume H [measurable]: "f \<in> borel_measurable M" "AE x in M. f x = 0"
[PROOF STATE]
proof (state)
this:
f \<in> borel_measurable M
AE x in M. f x = 0

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> borel_measurable M
AE x in M. f x = 0
[PROOF STEP]
have *: "AE x in M. \<bar>f x\<bar> powr p = 0"
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M
AE x in M. f x = 0

goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> powr p = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. \<bar>f x\<bar> powr p = 0

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
have "integrable M (\<lambda>x. \<bar>f x\<bar> powr p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
[PROOF STEP]
using integrable_cong_AE[OF _ _ *]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(\<lambda>x. \<bar>f x\<bar> powr p) \<in> borel_measurable M; (\<lambda>x. 0) \<in> borel_measurable M\<rbrakk> \<Longrightarrow> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) = integrable M (\<lambda>x. 0)

goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. \<bar>f x\<bar> powr p)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
have **: "(\<integral>x. \<bar>f x\<bar> powr p \<partial>M) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. \<bar>f x\<bar> powr p = 0
[PROOF STEP]
using integral_cong_AE[OF _ _ *]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(\<lambda>x. \<bar>f x\<bar> powr p) \<in> borel_measurable M; (\<lambda>x. 0) \<in> borel_measurable M\<rbrakk> \<Longrightarrow> LINT x|M. \<bar>f x\<bar> powr p = LINT x|M. 0

goal (1 subgoal):
 1. LINT x|M. \<bar>f x\<bar> powr p = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>f x\<bar> powr p = 0

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
have "eNorm (\<LL> p M) f = (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))
[PROOF STEP]
by (cases "p \<le> 1", insert H(1) \<open>integrable M (\<lambda>x. \<bar>f x\<bar> powr p)\<close> \<open>p > 0\<close>, auto simp add: Lp_le_1(1) Lp(1))
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))
[PROOF STEP]
have "eNorm (\<LL> p M) f = 0"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))

goal (1 subgoal):
 1. eNorm (\<LL> (ennreal p) M) f = 0
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))
LINT x|M. \<bar>f x\<bar> powr p = 0

goal (1 subgoal):
 1. eNorm (\<LL> (ennreal p) M) f = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> (ennreal p) M) f = 0

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> (ennreal p) M) f = 0
[PROOF STEP]
show "f \<in> zero_space\<^sub>N (\<LL> p M)"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> (ennreal p) M) f = 0

goal (1 subgoal):
 1. f \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
using zero_spaceN_iff
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> (ennreal p) M) f = 0
(?x \<in> zero_space\<^sub>N ?N) = (eNorm ?N ?x = 0)

goal (1 subgoal):
 1. f \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> zero_space\<^sub>N (\<LL> (ennreal p) M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Lp_tendsto_AE_subseq:
  assumes "p>(0::real)"
          "tendsto_in\<^sub>N (\<LL> p M) f g"
          "\<And>n. f n \<in> space\<^sub>N (\<LL> p M)"
          "g \<in> space\<^sub>N (\<LL> p M)"
  shows "\<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)
[PROOF STEP]
have "f n - g \<in> space\<^sub>N (\<LL> p M)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n - g \<in> space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
using spaceN_diff[OF \<open>\<And>n. f n \<in> space\<^sub>N (\<LL> p M)\<close> \<open>g \<in> space\<^sub>N (\<LL> p M)\<close>]
[PROOF STATE]
proof (prove)
using this:
f ?n1 - g \<in> space\<^sub>N (\<LL> (ennreal p) M)

goal (1 subgoal):
 1. f n - g \<in> space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f ?n - g \<in> space\<^sub>N (\<LL> (ennreal p) M)

goal (1 subgoal):
 1. \<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)
[PROOF STEP]
have int: "integrable M (\<lambda>x. \<bar>f n x - g x\<bar> powr p)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>f n x - g x\<bar> powr p)
[PROOF STEP]
using Lp_D(2)[OF \<open>p > 0\<close> \<open>f n - g \<in> space\<^sub>N (\<LL> p M)\<close>]
[PROOF STATE]
proof (prove)
using this:
integrable M (\<lambda>x. \<bar>(f n - g) x\<bar> powr p)

goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>f n x - g x\<bar> powr p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. \<bar>f ?n x - g x\<bar> powr p)

goal (1 subgoal):
 1. \<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)
[PROOF STEP]
have "(\<lambda>n. Norm (\<LL> p M) (f n - g)) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. Norm (\<LL> (ennreal p) M) (f n - g)) \<longlonglongrightarrow> 0
[PROOF STEP]
using \<open>tendsto_in\<^sub>N (\<LL> p M) f g\<close>
[PROOF STATE]
proof (prove)
using this:
tendsto_in\<^sub>N (\<LL> (ennreal p) M) f g

goal (1 subgoal):
 1. (\<lambda>n. Norm (\<LL> (ennreal p) M) (f n - g)) \<longlonglongrightarrow> 0
[PROOF STEP]
unfolding tendsto_in\<^sub>N_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. Norm (\<LL> (ennreal p) M) (f n - g)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. Norm (\<LL> (ennreal p) M) (f n - g)) \<longlonglongrightarrow> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. Norm (\<LL> (ennreal p) M) (f n - g)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. \<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. Norm (\<LL> (ennreal p) M) (f n - g)) \<longlonglongrightarrow> 0
[PROOF STEP]
have *: "(\<lambda>n. (\<integral>x. \<bar>f n x - g x\<bar> powr p \<partial>M) powr (1/p)) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. Norm (\<LL> (ennreal p) M) (f n - g)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. (LINT x|M. \<bar>f n x - g x\<bar> powr p) powr (1 / p)) \<longlonglongrightarrow> 0
[PROOF STEP]
using Lp_D(3)[OF \<open>p > 0\<close> \<open>\<And>n. f n - g \<in> space\<^sub>N (\<LL> p M)\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. Norm (\<LL> (ennreal p) M) (f n - g)) \<longlonglongrightarrow> 0
Norm (\<LL> (ennreal p) M) (f ?n1 - g) = (LINT x|M. \<bar>(f ?n1 - g) x\<bar> powr p) powr (1 / p)

goal (1 subgoal):
 1. (\<lambda>n. (LINT x|M. \<bar>f n x - g x\<bar> powr p) powr (1 / p)) \<longlonglongrightarrow> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (LINT x|M. \<bar>f n x - g x\<bar> powr p) powr (1 / p)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. \<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)
[PROOF STEP]
have "(\<lambda>n. ((\<integral>x. \<bar>f n x - g x\<bar> powr p \<partial>M) powr (1/p)) powr p) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. ((LINT x|M. \<bar>f n x - g x\<bar> powr p) powr (1 / p)) powr p) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (rule tendsto_zero_powrI[of _ _ _ p])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (\<lambda>x. (LINT xa|M. \<bar>f x xa - g xa\<bar> powr p) powr (1 / p)) \<longlonglongrightarrow> 0
 2. (\<lambda>x. p) \<longlonglongrightarrow> p
 3. \<forall>\<^sub>F n in sequentially. 0 \<le> (LINT x|M. \<bar>f n x - g x\<bar> powr p) powr (1 / p)
 4. 0 < p
[PROOF STEP]
using \<open>p > 0\<close> *
[PROOF STATE]
proof (prove)
using this:
0 < p
(\<lambda>n. (LINT x|M. \<bar>f n x - g x\<bar> powr p) powr (1 / p)) \<longlonglongrightarrow> 0

goal (4 subgoals):
 1. (\<lambda>x. (LINT xa|M. \<bar>f x xa - g xa\<bar> powr p) powr (1 / p)) \<longlonglongrightarrow> 0
 2. (\<lambda>x. p) \<longlonglongrightarrow> p
 3. \<forall>\<^sub>F n in sequentially. 0 \<le> (LINT x|M. \<bar>f n x - g x\<bar> powr p) powr (1 / p)
 4. 0 < p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. ((LINT x|M. \<bar>f n x - g x\<bar> powr p) powr (1 / p)) powr p) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. \<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. ((LINT x|M. \<bar>f n x - g x\<bar> powr p) powr (1 / p)) powr p) \<longlonglongrightarrow> 0
[PROOF STEP]
have **: "(\<lambda>n. (\<integral>x. \<bar>f n x - g x\<bar> powr p \<partial>M)) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. ((LINT x|M. \<bar>f n x - g x\<bar> powr p) powr (1 / p)) powr p) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. LINT x|M. \<bar>f n x - g x\<bar> powr p) \<longlonglongrightarrow> 0
[PROOF STEP]
using powr_powr \<open>p > 0\<close>
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. ((LINT x|M. \<bar>f n x - g x\<bar> powr p) powr (1 / p)) powr p) \<longlonglongrightarrow> 0
(?x powr ?a) powr ?b = ?x powr (?a * ?b)
0 < p

goal (1 subgoal):
 1. (\<lambda>n. LINT x|M. \<bar>f n x - g x\<bar> powr p) \<longlonglongrightarrow> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. LINT x|M. \<bar>f n x - g x\<bar> powr p) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. \<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)
[PROOF STEP]
have "\<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. \<bar>f (r n) x - g x\<bar> powr p) \<longlonglongrightarrow> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. \<bar>f (r n) x - g x\<bar> powr p) \<longlonglongrightarrow> 0)
[PROOF STEP]
apply (rule tendsto_L1_AE_subseq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. integrable M (\<lambda>a. \<bar>f n a - g a\<bar> powr p)
 2. (\<lambda>n. LINT x|M. norm (\<bar>f n x - g x\<bar> powr p)) \<longlonglongrightarrow> 0
[PROOF STEP]
using int **
[PROOF STATE]
proof (prove)
using this:
integrable M (\<lambda>x. \<bar>f ?n x - g x\<bar> powr p)
(\<lambda>n. LINT x|M. \<bar>f n x - g x\<bar> powr p) \<longlonglongrightarrow> 0

goal (2 subgoals):
 1. \<And>n. integrable M (\<lambda>a. \<bar>f n a - g a\<bar> powr p)
 2. (\<lambda>n. LINT x|M. norm (\<bar>f n x - g x\<bar> powr p)) \<longlonglongrightarrow> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. \<bar>f (r n) x - g x\<bar> powr p) \<longlonglongrightarrow> 0)

goal (1 subgoal):
 1. \<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. \<bar>f (r n) x - g x\<bar> powr p) \<longlonglongrightarrow> 0)
[PROOF STEP]
obtain r where "strict_mono r" "AE x in M. (\<lambda>n. \<bar>f (r n) x - g x\<bar> powr p) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. \<bar>f (r n) x - g x\<bar> powr p) \<longlonglongrightarrow> 0)

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>strict_mono r; AE x in M. (\<lambda>n. \<bar>f (r n) x - g x\<bar> powr p) \<longlonglongrightarrow> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
strict_mono r
AE x in M. (\<lambda>n. \<bar>f (r n) x - g x\<bar> powr p) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. \<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
strict_mono r
AE x in M. (\<lambda>n. \<bar>f (r n) x - g x\<bar> powr p) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. \<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)
[PROOF STEP]
have "(\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x" if "(\<lambda>n. \<bar>f (r n) x - g x\<bar> powr p) \<longlonglongrightarrow> 0" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x
[PROOF STEP]
have "(\<lambda>n. (\<bar>f (r n) x - g x\<bar> powr p) powr (1/p)) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. (\<bar>f (r n) x - g x\<bar> powr p) powr (1 / p)) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (rule tendsto_zero_powrI[of _ _ _ "1/p"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (\<lambda>xa. \<bar>f (r xa) x - g x\<bar> powr p) \<longlonglongrightarrow> 0
 2. (\<lambda>x. 1 / p) \<longlonglongrightarrow> 1 / p
 3. \<forall>\<^sub>F n in sequentially. 0 \<le> \<bar>f (r n) x - g x\<bar> powr p
 4. 0 < 1 / p
[PROOF STEP]
using \<open>p > 0\<close> that
[PROOF STATE]
proof (prove)
using this:
0 < p
(\<lambda>n. \<bar>f (r n) x - g x\<bar> powr p) \<longlonglongrightarrow> 0

goal (4 subgoals):
 1. (\<lambda>xa. \<bar>f (r xa) x - g x\<bar> powr p) \<longlonglongrightarrow> 0
 2. (\<lambda>x. 1 / p) \<longlonglongrightarrow> 1 / p
 3. \<forall>\<^sub>F n in sequentially. 0 \<le> \<bar>f (r n) x - g x\<bar> powr p
 4. 0 < 1 / p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (\<bar>f (r n) x - g x\<bar> powr p) powr (1 / p)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. (\<bar>f (r n) x - g x\<bar> powr p) powr (1 / p)) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>n. \<bar>f (r n) x - g x\<bar>) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (\<bar>f (r n) x - g x\<bar> powr p) powr (1 / p)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. \<bar>f (r n) x - g x\<bar>) \<longlonglongrightarrow> 0
[PROOF STEP]
using powr_powr \<open>p > 0\<close>
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (\<bar>f (r n) x - g x\<bar> powr p) powr (1 / p)) \<longlonglongrightarrow> 0
(?x powr ?a) powr ?b = ?x powr (?a * ?b)
0 < p

goal (1 subgoal):
 1. (\<lambda>n. \<bar>f (r n) x - g x\<bar>) \<longlonglongrightarrow> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<bar>f (r n) x - g x\<bar>) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x
[PROOF STEP]
by (simp add: \<open>(\<lambda>n. \<bar>f (r n) x - g x\<bar>) \<longlonglongrightarrow> 0\<close> Limits.LIM_zero_cancel tendsto_rabs_zero_cancel)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<bar>f (r n) ?x - g ?x\<bar> powr p) \<longlonglongrightarrow> 0 \<Longrightarrow> (\<lambda>n. f (r n) ?x) \<longlonglongrightarrow> g ?x

goal (1 subgoal):
 1. \<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
strict_mono r
AE x in M. (\<lambda>n. \<bar>f (r n) x - g x\<bar> powr p) \<longlonglongrightarrow> 0
(\<lambda>n. \<bar>f (r n) ?x - g ?x\<bar> powr p) \<longlonglongrightarrow> 0 \<Longrightarrow> (\<lambda>n. f (r n) ?x) \<longlonglongrightarrow> g ?x
[PROOF STEP]
have "AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x"
[PROOF STATE]
proof (prove)
using this:
strict_mono r
AE x in M. (\<lambda>n. \<bar>f (r n) x - g x\<bar> powr p) \<longlonglongrightarrow> 0
(\<lambda>n. \<bar>f (r n) ?x - g ?x\<bar> powr p) \<longlonglongrightarrow> 0 \<Longrightarrow> (\<lambda>n. f (r n) ?x) \<longlonglongrightarrow> g ?x

goal (1 subgoal):
 1. AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x

goal (1 subgoal):
 1. \<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x

goal (1 subgoal):
 1. \<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)
[PROOF STEP]
using \<open>strict_mono r\<close>
[PROOF STATE]
proof (prove)
using this:
AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x
strict_mono r

goal (1 subgoal):
 1. \<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r. strict_mono r \<and> (AE x in M. (\<lambda>n. f (r n) x) \<longlonglongrightarrow> g x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma L1_space:
  "space\<^sub>N (\<LL> 1 M) = {f. integrable M f}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space\<^sub>N (\<LL> 1 M) = {f. integrable M f}
[PROOF STEP]
unfolding one_ereal_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space\<^sub>N (\<LL> 1 M) = {f. integrable M f}
[PROOF STEP]
using Lp_space[of 1 M] integrable_abs_iff
[PROOF STATE]
proof (prove)
using this:
0 < 1 \<Longrightarrow> space\<^sub>N (\<LL> (ennreal 1) M) = {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr 1)}
?f \<in> borel_measurable ?M \<Longrightarrow> integrable ?M (\<lambda>x. \<bar>?f x\<bar>) = integrable ?M ?f

goal (1 subgoal):
 1. space\<^sub>N (\<LL> 1 M) = {f. integrable M f}
[PROOF STEP]
by auto


[STATEMENT]
lemma L1_I:
  assumes "integrable M f"
  shows "f \<in> space\<^sub>N (\<LL> 1 M)"
        "Norm (\<LL> 1 M) f = (\<integral>x. \<bar>f x\<bar> \<partial>M)"
        "eNorm (\<LL> 1 M) f = (\<integral>x. \<bar>f x\<bar> \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> 1 M) &&& Norm (\<LL> 1 M) f = LINT x|M. \<bar>f x\<bar> &&& eNorm (\<LL> 1 M) f = ennreal (LINT x|M. \<bar>f x\<bar>)
[PROOF STEP]
unfolding one_ereal_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> 1 M) &&& Norm (\<LL> 1 M) f = LINT x|M. \<bar>f x\<bar> &&& eNorm (\<LL> 1 M) f = ennreal (LINT x|M. \<bar>f x\<bar>)
[PROOF STEP]
using Lp_I[of 1, OF _ borel_measurable_integrable[OF assms]] assms powr_to_1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < 1; integrable M (\<lambda>x. \<bar>f x\<bar> powr 1)\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> (ennreal 1) M)
\<lbrakk>0 < 1; integrable M (\<lambda>x. \<bar>f x\<bar> powr 1)\<rbrakk> \<Longrightarrow> Norm (\<LL> (ennreal 1) M) f = (LINT x|M. \<bar>f x\<bar> powr 1) powr (1 / 1)
\<lbrakk>0 < 1; integrable M (\<lambda>x. \<bar>f x\<bar> powr 1)\<rbrakk> \<Longrightarrow> eNorm (\<LL> (ennreal 1) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr 1) powr (1 / 1))
integrable M f
?z powr 1 = ?z

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> 1 M) &&& Norm (\<LL> 1 M) f = LINT x|M. \<bar>f x\<bar> &&& eNorm (\<LL> 1 M) f = ennreal (LINT x|M. \<bar>f x\<bar>)
[PROOF STEP]
by auto


[STATEMENT]
lemma L1_D:
  assumes "f \<in> space\<^sub>N (\<LL> 1 M)"
  shows "f \<in> borel_measurable M"
        "integrable M f"
        "Norm (\<LL> 1 M) f = (\<integral>x. \<bar>f x\<bar> \<partial>M)"
        "eNorm (\<LL> 1 M) f = (\<integral>x. \<bar>f x\<bar> \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<in> borel_measurable M &&& integrable M f) &&& Norm (\<LL> 1 M) f = LINT x|M. \<bar>f x\<bar> &&& eNorm (\<LL> 1 M) f = ennreal (LINT x|M. \<bar>f x\<bar>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> 1 M)

goal (1 subgoal):
 1. (f \<in> borel_measurable M &&& integrable M f) &&& Norm (\<LL> 1 M) f = LINT x|M. \<bar>f x\<bar> &&& eNorm (\<LL> 1 M) f = ennreal (LINT x|M. \<bar>f x\<bar>)
[PROOF STEP]
by (auto simp add: L1_space L1_I)


[STATEMENT]
lemma L1_int_ineq:
  "abs(\<integral>x. f x \<partial>M) \<le> Norm (\<LL> 1 M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>integral\<^sup>L M f\<bar> \<le> Norm (\<LL> 1 M) f
[PROOF STEP]
proof (cases "integrable M f")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. integrable M f \<Longrightarrow> \<bar>integral\<^sup>L M f\<bar> \<le> Norm (\<LL> 1 M) f
 2. \<not> integrable M f \<Longrightarrow> \<bar>integral\<^sup>L M f\<bar> \<le> Norm (\<LL> 1 M) f
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
integrable M f

goal (2 subgoals):
 1. integrable M f \<Longrightarrow> \<bar>integral\<^sup>L M f\<bar> \<le> Norm (\<LL> 1 M) f
 2. \<not> integrable M f \<Longrightarrow> \<bar>integral\<^sup>L M f\<bar> \<le> Norm (\<LL> 1 M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
integrable M f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
integrable M f

goal (1 subgoal):
 1. \<bar>integral\<^sup>L M f\<bar> \<le> Norm (\<LL> 1 M) f
[PROOF STEP]
using L1_I(2)[OF True]
[PROOF STATE]
proof (prove)
using this:
integrable M f
Norm (\<LL> 1 M) f = LINT x|M. \<bar>f x\<bar>

goal (1 subgoal):
 1. \<bar>integral\<^sup>L M f\<bar> \<le> Norm (\<LL> 1 M) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>integral\<^sup>L M f\<bar> \<le> Norm (\<LL> 1 M) f

goal (1 subgoal):
 1. \<not> integrable M f \<Longrightarrow> \<bar>integral\<^sup>L M f\<bar> \<le> Norm (\<LL> 1 M) f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> integrable M f \<Longrightarrow> \<bar>integral\<^sup>L M f\<bar> \<le> Norm (\<LL> 1 M) f
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> integrable M f

goal (1 subgoal):
 1. \<not> integrable M f \<Longrightarrow> \<bar>integral\<^sup>L M f\<bar> \<le> Norm (\<LL> 1 M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> integrable M f
[PROOF STEP]
have "(\<integral>x. f x \<partial>M) = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> integrable M f

goal (1 subgoal):
 1. integral\<^sup>L M f = 0
[PROOF STEP]
by (simp add: not_integrable_integral_eq)
[PROOF STATE]
proof (state)
this:
integral\<^sup>L M f = 0

goal (1 subgoal):
 1. \<not> integrable M f \<Longrightarrow> \<bar>integral\<^sup>L M f\<bar> \<le> Norm (\<LL> 1 M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
integral\<^sup>L M f = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
integral\<^sup>L M f = 0

goal (1 subgoal):
 1. \<bar>integral\<^sup>L M f\<bar> \<le> Norm (\<LL> 1 M) f
[PROOF STEP]
using Norm_nonneg
[PROOF STATE]
proof (prove)
using this:
integral\<^sup>L M f = 0
0 \<le> Norm ?N ?x

goal (1 subgoal):
 1. \<bar>integral\<^sup>L M f\<bar> \<le> Norm (\<LL> 1 M) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>integral\<^sup>L M f\<bar> \<le> Norm (\<LL> 1 M) f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma L1_Norm:
  assumes [measurable]: "f \<in> borel_measurable M"
  shows "Norm (\<LL> 1 M) f = (\<integral>x. \<bar>f x\<bar> \<partial>M)"
        "eNorm (\<LL> 1 M) f = (\<integral>\<^sup>+x. \<bar>f x\<bar> \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> 1 M) f = LINT x|M. \<bar>f x\<bar> &&& eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Norm (\<LL> 1 M) f = LINT x|M. \<bar>f x\<bar>
 2. eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
[PROOF STEP]
show *: "Norm (\<LL> 1 M) f = (\<integral>x. \<bar>f x\<bar> \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> 1 M) f = LINT x|M. \<bar>f x\<bar>
[PROOF STEP]
using Lp_Norm[of 1, OF _ assms]
[PROOF STATE]
proof (prove)
using this:
0 < 1 \<Longrightarrow> Norm (\<LL> (ennreal 1) M) f = (LINT x|M. \<bar>f x\<bar> powr 1) powr (1 / 1)
0 < 1 \<Longrightarrow> Norm (\<LL> (ennreal 1) M) f powr 1 = LINT x|M. \<bar>f x\<bar> powr 1

goal (1 subgoal):
 1. Norm (\<LL> 1 M) f = LINT x|M. \<bar>f x\<bar>
[PROOF STEP]
unfolding one_ereal_def
[PROOF STATE]
proof (prove)
using this:
0 < 1 \<Longrightarrow> Norm (\<LL> (ennreal 1) M) f = (LINT x|M. \<bar>f x\<bar> powr 1) powr (1 / 1)
0 < 1 \<Longrightarrow> Norm (\<LL> (ennreal 1) M) f powr 1 = LINT x|M. \<bar>f x\<bar> powr 1

goal (1 subgoal):
 1. Norm (\<LL> 1 M) f = LINT x|M. \<bar>f x\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Norm (\<LL> 1 M) f = LINT x|M. \<bar>f x\<bar>

goal (1 subgoal):
 1. eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
[PROOF STEP]
show "eNorm (\<LL> 1 M) f = (\<integral>\<^sup>+x. \<bar>f x\<bar> \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
[PROOF STEP]
proof (cases "integrable M f")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. integrable M f \<Longrightarrow> eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
 2. \<not> integrable M f \<Longrightarrow> eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
integrable M f

goal (2 subgoals):
 1. integrable M f \<Longrightarrow> eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
 2. \<not> integrable M f \<Longrightarrow> eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
integrable M f
[PROOF STEP]
have "f \<in> space\<^sub>N (\<LL> 1 M)"
[PROOF STATE]
proof (prove)
using this:
integrable M f

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> 1 M)
[PROOF STEP]
using L1_space
[PROOF STATE]
proof (prove)
using this:
integrable M f
space\<^sub>N (\<LL> 1 ?M) = {f. integrable ?M f}

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> 1 M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> space\<^sub>N (\<LL> 1 M)

goal (2 subgoals):
 1. integrable M f \<Longrightarrow> eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
 2. \<not> integrable M f \<Longrightarrow> eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> space\<^sub>N (\<LL> 1 M)
[PROOF STEP]
have "eNorm (\<LL> 1 M) f = ennreal (Norm (\<LL> 1 M) f)"
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> 1 M)

goal (1 subgoal):
 1. eNorm (\<LL> 1 M) f = ennreal (Norm (\<LL> 1 M) f)
[PROOF STEP]
using eNorm_Norm
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> 1 M)
?x \<in> space\<^sub>N ?N \<Longrightarrow> eNorm ?N ?x = ennreal (Norm ?N ?x)

goal (1 subgoal):
 1. eNorm (\<LL> 1 M) f = ennreal (Norm (\<LL> 1 M) f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> 1 M) f = ennreal (Norm (\<LL> 1 M) f)

goal (2 subgoals):
 1. integrable M f \<Longrightarrow> eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
 2. \<not> integrable M f \<Longrightarrow> eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> 1 M) f = ennreal (Norm (\<LL> 1 M) f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> 1 M) f = ennreal (Norm (\<LL> 1 M) f)

goal (1 subgoal):
 1. eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
[PROOF STEP]
by (metis (mono_tags) * AE_I2 True abs_ge_zero integrable_abs nn_integral_eq_integral)
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M

goal (1 subgoal):
 1. \<not> integrable M f \<Longrightarrow> eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> integrable M f \<Longrightarrow> eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> integrable M f

goal (1 subgoal):
 1. \<not> integrable M f \<Longrightarrow> eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> integrable M f
[PROOF STEP]
have "eNorm (\<LL> 1 M) f = \<infinity>"
[PROOF STATE]
proof (prove)
using this:
\<not> integrable M f

goal (1 subgoal):
 1. eNorm (\<LL> 1 M) f = \<infinity>
[PROOF STEP]
using L1_space space\<^sub>N_def
[PROOF STATE]
proof (prove)
using this:
\<not> integrable M f
space\<^sub>N (\<LL> 1 ?M) = {f. integrable ?M f}
space\<^sub>N ?N = {f. eNorm ?N f < \<infinity>}

goal (1 subgoal):
 1. eNorm (\<LL> 1 M) f = \<infinity>
[PROOF STEP]
by (metis ennreal_add_eq_top infinity_ennreal_def le_iff_add le_less_linear mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> 1 M) f = \<infinity>

goal (1 subgoal):
 1. \<not> integrable M f \<Longrightarrow> eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> 1 M) f = \<infinity>

goal (1 subgoal):
 1. \<not> integrable M f \<Longrightarrow> eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
[PROOF STEP]
have "(\<integral>\<^sup>+x. \<bar>f x\<bar> \<partial>M) = \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M = \<infinity>
[PROOF STEP]
apply (rule nn_integral_nonneg_infinite)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M
 2. \<not> integrable M (\<lambda>x. \<bar>f x\<bar>)
 3. AE x in M. 0 \<le> \<bar>f x\<bar>
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> integrable M f

goal (3 subgoals):
 1. (\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M
 2. \<not> integrable M (\<lambda>x. \<bar>f x\<bar>)
 3. AE x in M. 0 \<le> \<bar>f x\<bar>
[PROOF STEP]
by (auto simp add: integrable_abs_iff)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M = \<infinity>

goal (1 subgoal):
 1. \<not> integrable M f \<Longrightarrow> eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> 1 M) f = \<infinity>
\<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M = \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> 1 M) f = \<infinity>
\<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M = \<infinity>

goal (1 subgoal):
 1. eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> 1 M) f = \<integral>\<^sup>+ x. ennreal \<bar>f x\<bar> \<partial>M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma L1_indicator:
  assumes [measurable]: "A \<in> sets M"
  shows "eNorm (\<LL> 1 M) (indicator A) = emeasure M A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> 1 M) (indicat_real A) = emeasure M A
[PROOF STEP]
by (subst L1_Norm, auto, metis assms ennreal_indicator nn_integral_cong nn_integral_indicator)


[STATEMENT]
lemma L1_indicator':
  assumes [measurable]: "A \<in> sets M"
      and "emeasure M A \<noteq> \<infinity>"
  shows "indicator A \<in> space\<^sub>N (\<LL> 1 M)"
        "Norm (\<LL> 1 M) (indicator A) = measure M A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indicat_real A \<in> space\<^sub>N (\<LL> 1 M) &&& Norm (\<LL> 1 M) (indicat_real A) = Sigma_Algebra.measure M A
[PROOF STEP]
unfolding space\<^sub>N_def Norm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indicat_real A \<in> {f. eNorm (\<LL> 1 M) f < \<infinity>} &&& enn2real (eNorm (\<LL> 1 M) (indicat_real A)) = Sigma_Algebra.measure M A
[PROOF STEP]
using L1_indicator[OF \<open>A \<in> sets M\<close>] \<open>emeasure M A \<noteq> \<infinity>\<close>
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> 1 M) (indicat_real A) = emeasure M A
emeasure M A \<noteq> \<infinity>

goal (1 subgoal):
 1. indicat_real A \<in> {f. eNorm (\<LL> 1 M) f < \<infinity>} &&& enn2real (eNorm (\<LL> 1 M) (indicat_real A)) = Sigma_Algebra.measure M A
[PROOF STEP]
by (auto simp add: top.not_eq_extremum Sigma_Algebra.measure_def)


[STATEMENT]
lemma L_zero:
  "eNorm (\<LL> 0 M) f = (if f \<in> borel_measurable M then 0 else \<infinity>)"
  "defect (\<LL> 0 M) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> 0 M) f = (if f \<in> borel_measurable M then 0 else \<infinity>) &&& defect (\<LL> 0 M) = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eNorm (\<LL> 0 M) f = (if f \<in> borel_measurable M then 0 else \<infinity>)
 2. defect (\<LL> 0 M) = 1
[PROOF STEP]
have *: "quasinorm_on UNIV 1 (\<lambda>(f::'a\<Rightarrow>real). (if f \<in> borel_measurable M then 0 else \<infinity>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quasinorm_on UNIV 1 (\<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>)
[PROOF STEP]
by (rule extend_quasinorm, rule quasinorm_onI, auto)
[PROOF STATE]
proof (state)
this:
quasinorm_on UNIV 1 (\<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>)

goal (2 subgoals):
 1. eNorm (\<LL> 0 M) f = (if f \<in> borel_measurable M then 0 else \<infinity>)
 2. defect (\<LL> 0 M) = 1
[PROOF STEP]
show "eNorm (\<LL> 0 M) f = (if f \<in> borel_measurable M then 0 else \<infinity>)"
       "defect (\<LL> 0 M) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> 0 M) f = (if f \<in> borel_measurable M then 0 else \<infinity>) &&& defect (\<LL> 0 M) = 1
[PROOF STEP]
using quasinorm_of[OF *]
[PROOF STATE]
proof (prove)
using this:
eNorm (quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>)) ?x = (if ?x \<in> borel_measurable M then 0 else \<infinity>)
defect (quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>)) = 1

goal (1 subgoal):
 1. eNorm (\<LL> 0 M) f = (if f \<in> borel_measurable M then 0 else \<infinity>) &&& defect (\<LL> 0 M) = 1
[PROOF STEP]
unfolding Lp_space_def
[PROOF STATE]
proof (prove)
using this:
eNorm (quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>)) ?x = (if ?x \<in> borel_measurable M then 0 else \<infinity>)
defect (quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>)) = 1

goal (1 subgoal):
 1. eNorm (if 0 = 0 then quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>) else if 0 < \<infinity> then quasinorm_of (if 0 < 1 then 2 powr (1 / enn2real 0 - 1) else 1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr enn2real 0) then ennreal ((LINT x|M. \<bar>f x\<bar> powr enn2real 0) powr (1 / enn2real 0)) else \<infinity>) else quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)) f = (if f \<in> borel_measurable M then 0 else \<infinity>) &&& defect (if 0 = 0 then quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>) else if 0 < \<infinity> then quasinorm_of (if 0 < 1 then 2 powr (1 / enn2real 0 - 1) else 1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr enn2real 0) then ennreal ((LINT x|M. \<bar>f x\<bar> powr enn2real 0) powr (1 / enn2real 0)) else \<infinity>) else quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> 0 M) f = (if f \<in> borel_measurable M then 0 else \<infinity>)
defect (\<LL> 0 M) = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma L_zero_space [simp]:
  "space\<^sub>N (\<LL> 0 M) = borel_measurable M"
  "zero_space\<^sub>N (\<LL> 0 M) = borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space\<^sub>N (\<LL> 0 M) = borel_measurable M &&& zero_space\<^sub>N (\<LL> 0 M) = borel_measurable M
[PROOF STEP]
apply (auto simp add: spaceN_iff zero_spaceN_iff L_zero(1))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. (if x \<in> borel_measurable M then 0 else \<infinity>) < \<top> \<Longrightarrow> x \<in> borel_measurable M
 2. \<And>x. (if x \<in> borel_measurable M then 0 else \<infinity>) = 0 \<Longrightarrow> x \<in> borel_measurable M
[PROOF STEP]
using top.not_eq_extremum
[PROOF STATE]
proof (prove)
using this:
(?a \<noteq> \<top>) = (?a < \<top>)

goal (2 subgoals):
 1. \<And>x. (if x \<in> borel_measurable M then 0 else \<infinity>) < \<top> \<Longrightarrow> x \<in> borel_measurable M
 2. \<And>x. (if x \<in> borel_measurable M then 0 else \<infinity>) = 0 \<Longrightarrow> x \<in> borel_measurable M
[PROOF STEP]
by force+


[STATEMENT]
lemma Lp_measurable_subset:
  "space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
[PROOF STEP]
proof (cases rule: Lp_cases[of p])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
 2. p = 0 \<Longrightarrow> space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
 3. p = \<infinity> \<Longrightarrow> space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
[PROOF STEP]
case zero
[PROOF STATE]
proof (state)
this:
p = 0

goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
 2. p = 0 \<Longrightarrow> space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
 3. p = \<infinity> \<Longrightarrow> space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = 0

goal (1 subgoal):
 1. space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
[PROOF STEP]
using L_zero_space
[PROOF STATE]
proof (prove)
using this:
p = 0
space\<^sub>N (\<LL> 0 ?M) = borel_measurable ?M
zero_space\<^sub>N (\<LL> 0 ?M) = borel_measurable ?M

goal (1 subgoal):
 1. space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
 2. p = \<infinity> \<Longrightarrow> space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
 2. p = \<infinity> \<Longrightarrow> space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
[PROOF STEP]
case (real_pos p2)
[PROOF STATE]
proof (state)
this:
p = ennreal p2
0 < p2
0 < p

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
 2. p = \<infinity> \<Longrightarrow> space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = ennreal p2
0 < p2
0 < p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = ennreal p2
0 < p2
0 < p

goal (1 subgoal):
 1. space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
[PROOF STEP]
using Lp_space[OF \<open>p2 > 0\<close>]
[PROOF STATE]
proof (prove)
using this:
p = ennreal p2
0 < p2
0 < p
space\<^sub>N (\<LL> (ennreal p2) ?M) = {f \<in> borel_measurable ?M. integrable ?M (\<lambda>x. \<bar>f x\<bar> powr p2)}

goal (1 subgoal):
 1. space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M

goal (1 subgoal):
 1. p = \<infinity> \<Longrightarrow> space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = \<infinity> \<Longrightarrow> space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
[PROOF STEP]
case PInf
[PROOF STATE]
proof (state)
this:
p = \<infinity>

goal (1 subgoal):
 1. p = \<infinity> \<Longrightarrow> space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = \<infinity>

goal (1 subgoal):
 1. space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
[PROOF STEP]
using L_infinity_space
[PROOF STATE]
proof (prove)
using this:
p = \<infinity>
space\<^sub>N (\<LL> \<infinity> ?M) = {f \<in> borel_measurable ?M. \<exists>C. AE x in ?M. \<bar>f x\<bar> \<le> C}

goal (1 subgoal):
 1. space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
space\<^sub>N (\<LL> p M) \<subseteq> borel_measurable M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Lp_measurable:
  assumes "f \<in> space\<^sub>N (\<LL> p M)"
  shows "f \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> borel_measurable M
[PROOF STEP]
using assms Lp_measurable_subset
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> p M)
space\<^sub>N (\<LL> ?p ?M) \<subseteq> borel_measurable ?M

goal (1 subgoal):
 1. f \<in> borel_measurable M
[PROOF STEP]
by auto


[STATEMENT]
lemma Lp_infinity_zero_space:
  assumes "p > (0::ennreal)"
  shows "zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
proof (cases rule: Lp_cases[of p])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
 2. p = 0 \<Longrightarrow> zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
 3. p = \<infinity> \<Longrightarrow> zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
case PInf
[PROOF STATE]
proof (state)
this:
p = \<infinity>

goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
 2. p = 0 \<Longrightarrow> zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
 3. p = \<infinity> \<Longrightarrow> zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = \<infinity>

goal (1 subgoal):
 1. zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
using L_infinity_zero_space
[PROOF STATE]
proof (prove)
using this:
p = \<infinity>
zero_space\<^sub>N (\<LL> \<infinity> ?M) = {f \<in> borel_measurable ?M. AE x in ?M. f x = 0}

goal (1 subgoal):
 1. zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
 2. p = 0 \<Longrightarrow> zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
 2. p = 0 \<Longrightarrow> zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
case (real_pos p2)
[PROOF STATE]
proof (state)
this:
p = ennreal p2
0 < p2
0 < p

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
 2. p = 0 \<Longrightarrow> zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = ennreal p2
0 < p2
0 < p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = ennreal p2
0 < p2
0 < p

goal (1 subgoal):
 1. zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
using Lp_zero_space[OF \<open>p2 > 0\<close>]
[PROOF STATE]
proof (prove)
using this:
p = ennreal p2
0 < p2
0 < p
zero_space\<^sub>N (\<LL> (ennreal p2) ?M) = {f \<in> borel_measurable ?M. AE x in ?M. f x = 0}

goal (1 subgoal):
 1. zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
unfolding \<open>p = ennreal p2\<close>
[PROOF STATE]
proof (prove)
using this:
ennreal p2 = ennreal p2
0 < p2
0 < ennreal p2
zero_space\<^sub>N (\<LL> (ennreal p2) ?M) = {f \<in> borel_measurable ?M. AE x in ?M. f x = 0}

goal (1 subgoal):
 1. zero_space\<^sub>N (\<LL> (ennreal p2) M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}

goal (1 subgoal):
 1. p = 0 \<Longrightarrow> zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = 0 \<Longrightarrow> zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
case zero
[PROOF STATE]
proof (state)
this:
p = 0

goal (1 subgoal):
 1. p = 0 \<Longrightarrow> zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = 0
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
p = 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p = 0
0 < p

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. p = 0 \<Longrightarrow> zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in prob_space) Lp_subset_Lq:
  assumes "p \<le> q"
  shows "\<And>f. eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f"
        "\<LL> q M \<subseteq>\<^sub>N \<LL> p M"
        "space\<^sub>N (\<LL> q M) \<subseteq> space\<^sub>N (\<LL> p M)"
        "\<And>f. f \<in> space\<^sub>N (\<LL> q M) \<Longrightarrow> Norm (\<LL> p M) f \<le> Norm (\<LL> q M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>f. eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f) &&& \<LL> q M \<subseteq>\<^sub>N \<LL> p M) &&& space\<^sub>N (\<LL> q M) \<subseteq> space\<^sub>N (\<LL> p M) &&& (\<And>f. f \<in> space\<^sub>N (\<LL> q M) \<Longrightarrow> Norm (\<LL> p M) f \<le> Norm (\<LL> q M) f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>f. eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. \<LL> q M \<subseteq>\<^sub>N \<LL> p M
 3. space\<^sub>N (\<LL> q M) \<subseteq> space\<^sub>N (\<LL> p M)
 4. \<And>f. f \<in> space\<^sub>N (\<LL> q M) \<Longrightarrow> Norm (\<LL> p M) f \<le> Norm (\<LL> q M) f
[PROOF STEP]
show "eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f" for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
proof (cases "eNorm (\<LL> q M) f < \<infinity>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eNorm (\<LL> q M) f < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. \<not> eNorm (\<LL> q M) f < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> q M) f < \<infinity>

goal (2 subgoals):
 1. eNorm (\<LL> q M) f < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. \<not> eNorm (\<LL> q M) f < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> q M) f < \<infinity>
[PROOF STEP]
have "f \<in> space\<^sub>N (\<LL> q M)"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> q M) f < \<infinity>

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> q M)
[PROOF STEP]
using spaceN_iff
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> q M) f < \<infinity>
(?x \<in> space\<^sub>N ?N) = (eNorm ?N ?x < \<infinity>)

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> q M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> space\<^sub>N (\<LL> q M)

goal (2 subgoals):
 1. eNorm (\<LL> q M) f < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. \<not> eNorm (\<LL> q M) f < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> space\<^sub>N (\<LL> q M)
[PROOF STEP]
have f_meas [measurable]: "f \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> q M)

goal (1 subgoal):
 1. random_variable borel f
[PROOF STEP]
using Lp_measurable
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> q M)
?f \<in> space\<^sub>N (\<LL> ?p ?M) \<Longrightarrow> ?f \<in> borel_measurable ?M

goal (1 subgoal):
 1. random_variable borel f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
random_variable borel f

goal (2 subgoals):
 1. eNorm (\<LL> q M) f < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. \<not> eNorm (\<LL> q M) f < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
consider "p = 0" | "p = q" | "p > 0 \<and> p < \<infinity> \<and> q = \<infinity>" | "p > 0 \<and> p < q \<and> q < \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = 0 \<Longrightarrow> thesis; p = q \<Longrightarrow> thesis; 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> thesis; 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using \<open>p \<le> q\<close>
[PROOF STATE]
proof (prove)
using this:
p \<le> q

goal (1 subgoal):
 1. \<lbrakk>p = 0 \<Longrightarrow> thesis; p = q \<Longrightarrow> thesis; 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> thesis; 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (simp add: top.not_eq_extremum)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = 0 \<Longrightarrow> thesis; p = q \<Longrightarrow> thesis; 0 < p \<and> p < \<top> \<and> q = \<top> \<Longrightarrow> thesis; 0 < p \<and> p < q \<and> q < \<top> \<Longrightarrow> thesis; p \<le> q\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using not_less_iff_gr_or_eq order.order_iff_strict
[PROOF STATE]
proof (prove)
using this:
(\<not> ?x < ?y) = (?y < ?x \<or> ?x = ?y)
(?a \<le> ?b) = (?a < ?b \<or> ?a = ?b)

goal (1 subgoal):
 1. \<lbrakk>p = 0 \<Longrightarrow> thesis; p = q \<Longrightarrow> thesis; 0 < p \<and> p < \<top> \<and> q = \<top> \<Longrightarrow> thesis; 0 < p \<and> p < q \<and> q < \<top> \<Longrightarrow> thesis; p \<le> q\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>p = 0 \<Longrightarrow> ?thesis12; p = q \<Longrightarrow> ?thesis12; 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> ?thesis12; 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> ?thesis12\<rbrakk> \<Longrightarrow> ?thesis12

goal (2 subgoals):
 1. eNorm (\<LL> q M) f < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. \<not> eNorm (\<LL> q M) f < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>p = 0 \<Longrightarrow> ?thesis12; p = q \<Longrightarrow> ?thesis12; 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> ?thesis12; 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> ?thesis12\<rbrakk> \<Longrightarrow> ?thesis12
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p = 0 \<Longrightarrow> ?thesis12; p = q \<Longrightarrow> ?thesis12; 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> ?thesis12; 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> ?thesis12\<rbrakk> \<Longrightarrow> ?thesis12

goal (1 subgoal):
 1. eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. p = 0 \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. p = q \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 3. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 4. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
p = 0

goal (4 subgoals):
 1. p = 0 \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. p = q \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 3. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 4. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = 0

goal (1 subgoal):
 1. eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
by (simp add: L_zero(1))
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f

goal (3 subgoals):
 1. p = q \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 3. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. p = q \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 3. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
p = q

goal (3 subgoals):
 1. p = q \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 3. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = q

goal (1 subgoal):
 1. eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f

goal (2 subgoals):
 1. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
0 < p \<and> p < \<infinity> \<and> q = \<infinity>

goal (2 subgoals):
 1. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < p \<and> p < \<infinity> \<and> q = \<infinity>
[PROOF STEP]
have "q = \<infinity>"
[PROOF STATE]
proof (prove)
using this:
0 < p \<and> p < \<infinity> \<and> q = \<infinity>

goal (1 subgoal):
 1. q = \<infinity>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q = \<infinity>

goal (2 subgoals):
 1. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
obtain p2 where "p = ennreal p2" "p2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p2. \<lbrakk>p = ennreal p2; 0 < p2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 3 enn2real_positive_iff[of p]
[PROOF STATE]
proof (prove)
using this:
0 < p \<and> p < \<infinity> \<and> q = \<infinity>
(0 < enn2real p) = (0 < p \<and> p < \<top>)

goal (1 subgoal):
 1. (\<And>p2. \<lbrakk>p = ennreal p2; 0 < p2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases p) auto
[PROOF STATE]
proof (state)
this:
p = ennreal p2
0 < p2

goal (2 subgoals):
 1. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
have *: "AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f
[PROOF STEP]
using L_infinity_AE_bound \<open>f \<in> space\<^sub>N (\<LL> q M)\<close> \<open>q = \<infinity>\<close>
[PROOF STATE]
proof (prove)
using this:
?f \<in> space\<^sub>N (\<LL> \<infinity> ?M) \<Longrightarrow> AE x in ?M. \<bar>?f x\<bar> \<le> Norm (\<LL> \<infinity> ?M) ?f
f \<in> space\<^sub>N (\<LL> q M)
q = \<infinity>

goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f

goal (2 subgoals):
 1. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
have **: "integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)
[PROOF STEP]
apply (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. (Norm (\<LL> \<infinity> M) f) powr p2"], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> powr p2 \<le> Norm (\<LL> \<top> M) f powr p2
[PROOF STEP]
using * powr_mono2 \<open>p2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f
\<lbrakk>0 \<le> ?a; 0 \<le> ?x; ?x \<le> ?y\<rbrakk> \<Longrightarrow> ?x powr ?a \<le> ?y powr ?a
0 < p2

goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> powr p2 \<le> Norm (\<LL> \<top> M) f powr p2
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)

goal (2 subgoals):
 1. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)
[PROOF STEP]
have "eNorm (\<LL> p2 M) f = (\<integral>x. \<bar>f x\<bar> powr p2 \<partial>M) powr (1/p2)"
[PROOF STATE]
proof (prove)
using this:
integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)

goal (1 subgoal):
 1. eNorm (\<LL> (ennreal p2) M) f = ennreal (expectation (\<lambda>x. \<bar>f x\<bar> powr p2) powr (1 / p2))
[PROOF STEP]
using Lp_I(3)[OF \<open>p2 > 0\<close> f_meas]
[PROOF STATE]
proof (prove)
using this:
integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)
integrable M (\<lambda>x. \<bar>f x\<bar> powr p2) \<Longrightarrow> eNorm (\<LL> (ennreal p2) M) f = ennreal (expectation (\<lambda>x. \<bar>f x\<bar> powr p2) powr (1 / p2))

goal (1 subgoal):
 1. eNorm (\<LL> (ennreal p2) M) f = ennreal (expectation (\<lambda>x. \<bar>f x\<bar> powr p2) powr (1 / p2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> (ennreal p2) M) f = ennreal (expectation (\<lambda>x. \<bar>f x\<bar> powr p2) powr (1 / p2))

goal (2 subgoals):
 1. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> (ennreal p2) M) f = ennreal (expectation (\<lambda>x. \<bar>f x\<bar> powr p2) powr (1 / p2))

goal (2 subgoals):
 1. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
have "... \<le> (\<integral>x. (Norm (\<LL> \<infinity> M) f) powr p2 \<partial>M) powr (1/p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (expectation (\<lambda>x. \<bar>f x\<bar> powr p2) powr (1 / p2)) \<le> ennreal (expectation (\<lambda>x. Norm (\<LL> \<infinity> M) f powr p2) powr (1 / p2))
[PROOF STEP]
apply (rule ennreal_leI, rule powr_mono2, simp add: \<open>p2 > 0\<close> less_imp_le, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation (\<lambda>x. \<bar>f x\<bar> powr p2) \<le> expectation (\<lambda>x. Norm (\<LL> \<infinity> M) f powr p2)
[PROOF STEP]
apply (rule integral_mono_AE, auto simp add: **)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> powr p2 \<le> Norm (\<LL> \<top> M) f powr p2
[PROOF STEP]
using * powr_mono2 \<open>p2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f
\<lbrakk>0 \<le> ?a; 0 \<le> ?x; ?x \<le> ?y\<rbrakk> \<Longrightarrow> ?x powr ?a \<le> ?y powr ?a
0 < p2

goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> powr p2 \<le> Norm (\<LL> \<top> M) f powr p2
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ennreal (expectation (\<lambda>x. \<bar>f x\<bar> powr p2) powr (1 / p2)) \<le> ennreal (expectation (\<lambda>x. Norm (\<LL> \<infinity> M) f powr p2) powr (1 / p2))

goal (2 subgoals):
 1. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ennreal (expectation (\<lambda>x. \<bar>f x\<bar> powr p2) powr (1 / p2)) \<le> ennreal (expectation (\<lambda>x. Norm (\<LL> \<infinity> M) f powr p2) powr (1 / p2))

goal (2 subgoals):
 1. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
have "... = Norm (\<LL> \<infinity> M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (expectation (\<lambda>x. Norm (\<LL> \<infinity> M) f powr p2) powr (1 / p2)) = ennreal (Norm (\<LL> \<infinity> M) f)
[PROOF STEP]
using \<open>p2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < p2

goal (1 subgoal):
 1. ennreal (expectation (\<lambda>x. Norm (\<LL> \<infinity> M) f powr p2) powr (1 / p2)) = ennreal (Norm (\<LL> \<infinity> M) f)
[PROOF STEP]
by (auto simp add: prob_space powr_powr)
[PROOF STATE]
proof (state)
this:
ennreal (expectation (\<lambda>x. Norm (\<LL> \<infinity> M) f powr p2) powr (1 / p2)) = ennreal (Norm (\<LL> \<infinity> M) f)

goal (2 subgoals):
 1. 0 < p \<and> p < \<infinity> \<and> q = \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
 2. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> (ennreal p2) M) f \<le> ennreal (Norm (\<LL> \<infinity> M) f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> (ennreal p2) M) f \<le> ennreal (Norm (\<LL> \<infinity> M) f)

goal (1 subgoal):
 1. eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
using \<open>p = ennreal p2\<close> \<open>q = \<infinity>\<close> eNorm_Norm[OF \<open>f \<in> space\<^sub>N (\<LL> q M)\<close>]
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> (ennreal p2) M) f \<le> ennreal (Norm (\<LL> \<infinity> M) f)
p = ennreal p2
q = \<infinity>
eNorm (\<LL> q M) f = ennreal (Norm (\<LL> q M) f)

goal (1 subgoal):
 1. eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
0 < p \<and> p < q \<and> q < \<infinity>

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < p \<and> p < q \<and> q < \<infinity>
[PROOF STEP]
have "0 < p" "p < \<infinity>"
[PROOF STATE]
proof (prove)
using this:
0 < p \<and> p < q \<and> q < \<infinity>

goal (1 subgoal):
 1. 0 < p &&& p < \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < p
p < \<infinity>

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < p
p < \<infinity>
[PROOF STEP]
obtain p2 where "p = ennreal p2" "p2 > 0"
[PROOF STATE]
proof (prove)
using this:
0 < p
p < \<infinity>

goal (1 subgoal):
 1. (\<And>p2. \<lbrakk>p = ennreal p2; 0 < p2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using enn2real_positive_iff[of p]
[PROOF STATE]
proof (prove)
using this:
0 < p
p < \<infinity>
(0 < enn2real p) = (0 < p \<and> p < \<top>)

goal (1 subgoal):
 1. (\<And>p2. \<lbrakk>p = ennreal p2; 0 < p2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases p) auto
[PROOF STATE]
proof (state)
this:
p = ennreal p2
0 < p2

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
have "0 < q" "q < \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < q &&& q < \<infinity>
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
0 < p \<and> p < q \<and> q < \<infinity>

goal (1 subgoal):
 1. 0 < q &&& q < \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < q
q < \<infinity>

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < q
q < \<infinity>
[PROOF STEP]
obtain q2 where "q = ennreal q2" "q2 > 0"
[PROOF STATE]
proof (prove)
using this:
0 < q
q < \<infinity>

goal (1 subgoal):
 1. (\<And>q2. \<lbrakk>q = ennreal q2; 0 < q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using enn2real_positive_iff[of q]
[PROOF STATE]
proof (prove)
using this:
0 < q
q < \<infinity>
(0 < enn2real q) = (0 < q \<and> q < \<top>)

goal (1 subgoal):
 1. (\<And>q2. \<lbrakk>q = ennreal q2; 0 < q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases q) auto
[PROOF STATE]
proof (state)
this:
q = ennreal q2
0 < q2

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
have "p2 < q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p2 < q2
[PROOF STEP]
using 4 \<open>p = ennreal p2\<close> \<open>q = ennreal q2\<close>
[PROOF STATE]
proof (prove)
using this:
0 < p \<and> p < q \<and> q < \<infinity>
p = ennreal p2
q = ennreal q2

goal (1 subgoal):
 1. p2 < q2
[PROOF STEP]
using ennreal_less_iff
[PROOF STATE]
proof (prove)
using this:
0 < p \<and> p < q \<and> q < \<infinity>
p = ennreal p2
q = ennreal q2
0 \<le> ?r \<Longrightarrow> (ennreal ?r < ennreal ?q) = (?r < ?q)

goal (1 subgoal):
 1. p2 < q2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p2 < q2

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
define r2 where "r2 = q2 / p2"
[PROOF STATE]
proof (state)
this:
r2 = q2 / p2

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
have "r2 \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> r2
[PROOF STEP]
unfolding r2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> q2 / p2
[PROOF STEP]
using \<open>p2 < q2\<close> \<open>p2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
p2 < q2
0 < p2

goal (1 subgoal):
 1. 1 \<le> q2 / p2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> r2

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
have *: "abs (\<bar>z\<bar> powr p2) powr r2 = \<bar>z\<bar> powr q2" for z::real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>\<bar>z\<bar> powr p2\<bar> powr r2 = \<bar>z\<bar> powr q2
[PROOF STEP]
unfolding r2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>\<bar>z\<bar> powr p2\<bar> powr (q2 / p2) = \<bar>z\<bar> powr q2
[PROOF STEP]
using \<open>p2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < p2

goal (1 subgoal):
 1. \<bar>\<bar>z\<bar> powr p2\<bar> powr (q2 / p2) = \<bar>z\<bar> powr q2
[PROOF STEP]
by (simp add: powr_powr)
[PROOF STATE]
proof (state)
this:
\<bar>\<bar>?z12\<bar> powr p2\<bar> powr r2 = \<bar>?z12\<bar> powr q2

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
have I: "integrable M (\<lambda>x. abs(\<bar>f x\<bar> powr p2) powr r2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>\<bar>f x\<bar> powr p2\<bar> powr r2)
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr q2)
[PROOF STEP]
using \<open>f \<in> space\<^sub>N (\<LL> q M)\<close> \<open>q = ennreal q2\<close> Lp_D(2)[OF \<open>q2 > 0\<close>]
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> q M)
q = ennreal q2
?f \<in> space\<^sub>N (\<LL> (ennreal q2) ?M) \<Longrightarrow> integrable ?M (\<lambda>x. \<bar>?f x\<bar> powr q2)

goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr q2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. \<bar>\<bar>f x\<bar> powr p2\<bar> powr r2)

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
have J: "integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)
[PROOF STEP]
by (rule bound_L1_Lp(1)[OF \<open>r2 \<ge> 1\<close> _ I], auto)
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
have "f \<in> space\<^sub>N (\<LL> p2 M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> (ennreal p2) M)
[PROOF STEP]
by (rule Lp_I(1)[OF \<open>p2 > 0\<close> _ J], simp)
[PROOF STATE]
proof (state)
this:
f \<in> space\<^sub>N (\<LL> (ennreal p2) M)

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
have "(\<integral>x. \<bar>f x\<bar> powr p2 \<partial>M) powr (1/p2) = abs(\<integral>x. \<bar>f x\<bar> powr p2 \<partial>M) powr (1/p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation (\<lambda>x. \<bar>f x\<bar> powr p2) powr (1 / p2) = \<bar>expectation (\<lambda>x. \<bar>f x\<bar> powr p2)\<bar> powr (1 / p2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
expectation (\<lambda>x. \<bar>f x\<bar> powr p2) powr (1 / p2) = \<bar>expectation (\<lambda>x. \<bar>f x\<bar> powr p2)\<bar> powr (1 / p2)

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
expectation (\<lambda>x. \<bar>f x\<bar> powr p2) powr (1 / p2) = \<bar>expectation (\<lambda>x. \<bar>f x\<bar> powr p2)\<bar> powr (1 / p2)

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
have "... \<le> ((\<integral>x. abs (\<bar>f x\<bar> powr p2) powr r2 \<partial>M) powr (1/r2)) powr (1/p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>expectation (\<lambda>x. \<bar>f x\<bar> powr p2)\<bar> powr (1 / p2) \<le> (expectation (\<lambda>x. \<bar>\<bar>f x\<bar> powr p2\<bar> powr r2) powr (1 / r2)) powr (1 / p2)
[PROOF STEP]
apply (subst powr_mono2, simp add: \<open>p2 > 0\<close> less_imp_le, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<bar>expectation (\<lambda>x. \<bar>f x\<bar> powr p2)\<bar> \<le> expectation (\<lambda>x. \<bar>\<bar>f x\<bar> powr p2\<bar> powr r2) powr (1 / r2)
 2. True
[PROOF STEP]
apply (rule bound_L1_Lp, simp add: \<open>r2 \<ge> 1\<close>, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>\<bar>f x\<bar> powr p2\<bar> powr r2)
 2. True
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr q2)
 2. True
[PROOF STEP]
using \<open>f \<in> space\<^sub>N (\<LL> q M)\<close> \<open>q = ennreal q2\<close> Lp_D(2)[OF \<open>q2 > 0\<close>]
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> q M)
q = ennreal q2
?f \<in> space\<^sub>N (\<LL> (ennreal q2) ?M) \<Longrightarrow> integrable ?M (\<lambda>x. \<bar>?f x\<bar> powr q2)

goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr q2)
 2. True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>expectation (\<lambda>x. \<bar>f x\<bar> powr p2)\<bar> powr (1 / p2) \<le> (expectation (\<lambda>x. \<bar>\<bar>f x\<bar> powr p2\<bar> powr r2) powr (1 / r2)) powr (1 / p2)

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>expectation (\<lambda>x. \<bar>f x\<bar> powr p2)\<bar> powr (1 / p2) \<le> (expectation (\<lambda>x. \<bar>\<bar>f x\<bar> powr p2\<bar> powr r2) powr (1 / r2)) powr (1 / p2)

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
have "... = (\<integral>x. \<bar>f x\<bar> powr q2 \<partial>M) powr (1/q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (expectation (\<lambda>x. \<bar>\<bar>f x\<bar> powr p2\<bar> powr r2) powr (1 / r2)) powr (1 / p2) = expectation (\<lambda>x. \<bar>f x\<bar> powr q2) powr (1 / q2)
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (expectation (\<lambda>x. \<bar>f x\<bar> powr q2) powr (1 / r2)) powr (1 / p2) = expectation (\<lambda>x. \<bar>f x\<bar> powr q2) powr (1 / q2)
[PROOF STEP]
using \<open>p2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < p2

goal (1 subgoal):
 1. (expectation (\<lambda>x. \<bar>f x\<bar> powr q2) powr (1 / r2)) powr (1 / p2) = expectation (\<lambda>x. \<bar>f x\<bar> powr q2) powr (1 / q2)
[PROOF STEP]
by (simp add: powr_powr r2_def)
[PROOF STATE]
proof (state)
this:
(expectation (\<lambda>x. \<bar>\<bar>f x\<bar> powr p2\<bar> powr r2) powr (1 / r2)) powr (1 / p2) = expectation (\<lambda>x. \<bar>f x\<bar> powr q2) powr (1 / q2)

goal (1 subgoal):
 1. 0 < p \<and> p < q \<and> q < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
expectation (\<lambda>x. \<bar>f x\<bar> powr p2) powr (1 / p2) \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr q2) powr (1 / q2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
expectation (\<lambda>x. \<bar>f x\<bar> powr p2) powr (1 / p2) \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr q2) powr (1 / q2)

goal (1 subgoal):
 1. eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
using \<open>f \<in> space\<^sub>N (\<LL> q M)\<close> Lp_D(4)[OF \<open>q2 > 0\<close>] ennreal_leI
[PROOF STATE]
proof (prove)
using this:
expectation (\<lambda>x. \<bar>f x\<bar> powr p2) powr (1 / p2) \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr q2) powr (1 / q2)
f \<in> space\<^sub>N (\<LL> q M)
?f \<in> space\<^sub>N (\<LL> (ennreal q2) ?M) \<Longrightarrow> eNorm (\<LL> (ennreal q2) ?M) ?f = ennreal ((LINT x|?M. \<bar>?f x\<bar> powr q2) powr (1 / q2))
?x \<le> ?y \<Longrightarrow> ennreal ?x \<le> ennreal ?y

goal (1 subgoal):
 1. eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
unfolding \<open>p = ennreal p2\<close> \<open>q = ennreal q2\<close> Lp_D(4)[OF \<open>p2 > 0\<close> \<open>f \<in> space\<^sub>N (\<LL> p2 M)\<close>]
[PROOF STATE]
proof (prove)
using this:
expectation (\<lambda>x. \<bar>f x\<bar> powr p2) powr (1 / p2) \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr q2) powr (1 / q2)
f \<in> space\<^sub>N (\<LL> (ennreal q2) M)
?f \<in> space\<^sub>N (\<LL> (ennreal q2) ?M) \<Longrightarrow> eNorm (\<LL> (ennreal q2) ?M) ?f = ennreal ((LINT x|?M. \<bar>?f x\<bar> powr q2) powr (1 / q2))
?x \<le> ?y \<Longrightarrow> ennreal ?x \<le> ennreal ?y

goal (1 subgoal):
 1. ennreal (expectation (\<lambda>x. \<bar>f x\<bar> powr p2) powr (1 / p2)) \<le> eNorm (\<LL> (ennreal q2) M) f
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f

goal (1 subgoal):
 1. \<not> eNorm (\<LL> q M) f < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> eNorm (\<LL> q M) f < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> eNorm (\<LL> q M) f < \<infinity>

goal (1 subgoal):
 1. \<not> eNorm (\<LL> q M) f < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> eNorm (\<LL> q M) f < \<infinity>
[PROOF STEP]
have "eNorm (\<LL> q M) f = \<infinity>"
[PROOF STATE]
proof (prove)
using this:
\<not> eNorm (\<LL> q M) f < \<infinity>

goal (1 subgoal):
 1. eNorm (\<LL> q M) f = \<infinity>
[PROOF STEP]
using top.not_eq_extremum
[PROOF STATE]
proof (prove)
using this:
\<not> eNorm (\<LL> q M) f < \<infinity>
(?a \<noteq> \<top>) = (?a < \<top>)

goal (1 subgoal):
 1. eNorm (\<LL> q M) f = \<infinity>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> q M) f = \<infinity>

goal (1 subgoal):
 1. \<not> eNorm (\<LL> q M) f < \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> q M) f = \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> q M) f = \<infinity>

goal (1 subgoal):
 1. eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) ?f12 \<le> eNorm (\<LL> q M) ?f12

goal (3 subgoals):
 1. \<LL> q M \<subseteq>\<^sub>N \<LL> p M
 2. space\<^sub>N (\<LL> q M) \<subseteq> space\<^sub>N (\<LL> p M)
 3. \<And>f. f \<in> space\<^sub>N (\<LL> q M) \<Longrightarrow> Norm (\<LL> p M) f \<le> Norm (\<LL> q M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> p M) ?f12 \<le> eNorm (\<LL> q M) ?f12
[PROOF STEP]
show "\<LL> q M \<subseteq>\<^sub>N \<LL> p M"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) ?f12 \<le> eNorm (\<LL> q M) ?f12

goal (1 subgoal):
 1. \<LL> q M \<subseteq>\<^sub>N \<LL> p M
[PROOF STEP]
using quasinorm_subsetI[of _ _ 1]
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) ?f12 \<le> eNorm (\<LL> q M) ?f12
(\<And>f. f \<in> space\<^sub>N ?N1.0 \<Longrightarrow> eNorm ?N2.0 f \<le> ennreal 1 * eNorm ?N1.0 f) \<Longrightarrow> ?N1.0 \<subseteq>\<^sub>N ?N2.0

goal (1 subgoal):
 1. \<LL> q M \<subseteq>\<^sub>N \<LL> p M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<LL> q M \<subseteq>\<^sub>N \<LL> p M

goal (2 subgoals):
 1. space\<^sub>N (\<LL> q M) \<subseteq> space\<^sub>N (\<LL> p M)
 2. \<And>f. f \<in> space\<^sub>N (\<LL> q M) \<Longrightarrow> Norm (\<LL> p M) f \<le> Norm (\<LL> q M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<LL> q M \<subseteq>\<^sub>N \<LL> p M
[PROOF STEP]
show "space\<^sub>N (\<LL> q M) \<subseteq> space\<^sub>N (\<LL> p M)"
[PROOF STATE]
proof (prove)
using this:
\<LL> q M \<subseteq>\<^sub>N \<LL> p M

goal (1 subgoal):
 1. space\<^sub>N (\<LL> q M) \<subseteq> space\<^sub>N (\<LL> p M)
[PROOF STEP]
using quasinorm_subset_space
[PROOF STATE]
proof (prove)
using this:
\<LL> q M \<subseteq>\<^sub>N \<LL> p M
?N1.0 \<subseteq>\<^sub>N ?N2.0 \<Longrightarrow> space\<^sub>N ?N1.0 \<subseteq> space\<^sub>N ?N2.0

goal (1 subgoal):
 1. space\<^sub>N (\<LL> q M) \<subseteq> space\<^sub>N (\<LL> p M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
space\<^sub>N (\<LL> q M) \<subseteq> space\<^sub>N (\<LL> p M)

goal (1 subgoal):
 1. \<And>f. f \<in> space\<^sub>N (\<LL> q M) \<Longrightarrow> Norm (\<LL> p M) f \<le> Norm (\<LL> q M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
space\<^sub>N (\<LL> q M) \<subseteq> space\<^sub>N (\<LL> p M)
[PROOF STEP]
show "Norm (\<LL> p M) f \<le> Norm (\<LL> q M) f" if "f \<in> space\<^sub>N (\<LL> q M)" for f
[PROOF STATE]
proof (prove)
using this:
space\<^sub>N (\<LL> q M) \<subseteq> space\<^sub>N (\<LL> p M)

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<le> Norm (\<LL> q M) f
[PROOF STEP]
using eNorm_Norm that \<open>eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f\<close> ennreal_le_iff Norm_nonneg
[PROOF STATE]
proof (prove)
using this:
space\<^sub>N (\<LL> q M) \<subseteq> space\<^sub>N (\<LL> p M)
?x \<in> space\<^sub>N ?N \<Longrightarrow> eNorm ?N ?x = ennreal (Norm ?N ?x)
f \<in> space\<^sub>N (\<LL> q M)
eNorm (\<LL> p M) f \<le> eNorm (\<LL> q M) f
0 \<le> ?y \<Longrightarrow> (ennreal ?x \<le> ennreal ?y) = (?x \<le> ?y)
0 \<le> Norm ?N ?x

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<le> Norm (\<LL> q M) f
[PROOF STEP]
by (metis rev_subsetD)
[PROOF STATE]
proof (state)
this:
?f12 \<in> space\<^sub>N (\<LL> q M) \<Longrightarrow> Norm (\<LL> p M) ?f12 \<le> Norm (\<LL> q M) ?f12

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Lp_Banach_lattice:
  assumes "f \<in> space\<^sub>N (\<LL> p M)"
  shows "(\<lambda>x. \<bar>f x\<bar>) \<in> space\<^sub>N (\<LL> p M)"
        "Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) = Norm (\<LL> p M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<bar>f x\<bar>) \<in> space\<^sub>N (\<LL> p M) &&& Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) = Norm (\<LL> p M) f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>x. \<bar>f x\<bar>) \<in> space\<^sub>N (\<LL> p M)
 2. Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) = Norm (\<LL> p M) f
[PROOF STEP]
have [measurable]: "f \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> borel_measurable M
[PROOF STEP]
using Lp_measurable[OF assms]
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M

goal (1 subgoal):
 1. f \<in> borel_measurable M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f \<in> borel_measurable M

goal (2 subgoals):
 1. (\<lambda>x. \<bar>f x\<bar>) \<in> space\<^sub>N (\<LL> p M)
 2. Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) = Norm (\<LL> p M) f
[PROOF STEP]
show "(\<lambda>x. \<bar>f x\<bar>) \<in> space\<^sub>N (\<LL> p M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<bar>f x\<bar>) \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
by (rule Lp_domination(1)[OF _ assms], auto)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<bar>f x\<bar>) \<in> space\<^sub>N (\<LL> p M)

goal (1 subgoal):
 1. Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) = Norm (\<LL> p M) f
[PROOF STEP]
have "Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) \<le> Norm (\<LL> p M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) \<le> Norm (\<LL> p M) f
[PROOF STEP]
by (rule Lp_domination[OF _ assms], auto)
[PROOF STATE]
proof (state)
this:
Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) \<le> Norm (\<LL> p M) f

goal (1 subgoal):
 1. Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) = Norm (\<LL> p M) f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) \<le> Norm (\<LL> p M) f

goal (1 subgoal):
 1. Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) = Norm (\<LL> p M) f
[PROOF STEP]
have "Norm (\<LL> p M) f \<le> Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> p M) f \<le> Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>)
[PROOF STEP]
by (rule Lp_domination[OF _ \<open>(\<lambda>x. \<bar>f x\<bar>) \<in> space\<^sub>N (\<LL> p M)\<close>], auto)
[PROOF STATE]
proof (state)
this:
Norm (\<LL> p M) f \<le> Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>)

goal (1 subgoal):
 1. Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) = Norm (\<LL> p M) f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) = Norm (\<LL> p M) f
[PROOF STEP]
show "Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) = Norm (\<LL> p M) f"
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) = Norm (\<LL> p M) f

goal (1 subgoal):
 1. Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) = Norm (\<LL> p M) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Norm (\<LL> p M) (\<lambda>x. \<bar>f x\<bar>) = Norm (\<LL> p M) f

goal:
No subgoals!
[PROOF STEP]
qed