[STATEMENT]
lemma L_infinity_pos_measure:
  assumes [measurable]: "f \<in> borel_measurable M"
      and "eNorm (\<LL> \<infinity> M) f > (C::real)"
  shows "emeasure M {x \<in> space M. \<bar>f x\<bar> > C} > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < emeasure M {x \<in> space M. C < \<bar>f x\<bar>}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < emeasure M {x \<in> space M. C < \<bar>f x\<bar>}
[PROOF STEP]
have *: "esssup M (\<lambda>x. ereal(\<bar>f x\<bar>)) > ereal C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ereal C < esssup M (\<lambda>x. ereal \<bar>f x\<bar>)
[PROOF STEP]
using \<open>eNorm (\<LL> \<infinity> M) f > C\<close>
[PROOF STATE]
proof (prove)
using this:
ennreal C < eNorm (\<LL> \<infinity> M) f

goal (1 subgoal):
 1. ereal C < esssup M (\<lambda>x. ereal \<bar>f x\<bar>)
[PROOF STEP]
unfolding L_infinity
[PROOF STATE]
proof (prove)
using this:
ennreal C < (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)

goal (1 subgoal):
 1. ereal C < esssup M (\<lambda>x. ereal \<bar>f x\<bar>)
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ennreal C < e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) \<Longrightarrow> ereal C < esssup M (\<lambda>x. ereal \<bar>f x\<bar>)
[PROOF STEP]
assume a1: "ennreal C < e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>))"
[PROOF STATE]
proof (state)
this:
ennreal C < e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>))

goal (1 subgoal):
 1. ennreal C < e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) \<Longrightarrow> ereal C < esssup M (\<lambda>x. ereal \<bar>f x\<bar>)
[PROOF STEP]
have "\<not> e2ennreal (esssup M (\<lambda>a. ereal \<bar>f a\<bar>)) \<le> e2ennreal (ereal C)" if "\<not> C < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> e2ennreal (esssup M (\<lambda>a. ereal \<bar>f a\<bar>)) \<le> e2ennreal (ereal C)
[PROOF STEP]
using a1 that
[PROOF STATE]
proof (prove)
using this:
ennreal C < e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>))
\<not> C < 0

goal (1 subgoal):
 1. \<not> e2ennreal (esssup M (\<lambda>a. ereal \<bar>f a\<bar>)) \<le> e2ennreal (ereal C)
[PROOF STEP]
by (metis (no_types) e2ennreal_enn2ereal enn2ereal_ennreal leD leI)
[PROOF STATE]
proof (state)
this:
\<not> C < 0 \<Longrightarrow> \<not> e2ennreal (esssup M (\<lambda>a. ereal \<bar>f a\<bar>)) \<le> e2ennreal (ereal C)

goal (1 subgoal):
 1. ennreal C < e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) \<Longrightarrow> ereal C < esssup M (\<lambda>x. ereal \<bar>f x\<bar>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> C < 0 \<Longrightarrow> \<not> e2ennreal (esssup M (\<lambda>a. ereal \<bar>f a\<bar>)) \<le> e2ennreal (ereal C)
[PROOF STEP]
have "e2ennreal (esssup M (\<lambda>a. ereal \<bar>f a\<bar>)) \<le> e2ennreal (ereal C) \<longrightarrow> (\<exists>e\<le>esssup M (\<lambda>a. ereal \<bar>f a\<bar>). ereal C < e)"
[PROOF STATE]
proof (prove)
using this:
\<not> C < 0 \<Longrightarrow> \<not> e2ennreal (esssup M (\<lambda>a. ereal \<bar>f a\<bar>)) \<le> e2ennreal (ereal C)

goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>a. ereal \<bar>f a\<bar>)) \<le> e2ennreal (ereal C) \<longrightarrow> (\<exists>e\<le>esssup M (\<lambda>a. ereal \<bar>f a\<bar>). ereal C < e)
[PROOF STEP]
using a1 e2ennreal_neg
[PROOF STATE]
proof (prove)
using this:
\<not> C < 0 \<Longrightarrow> \<not> e2ennreal (esssup M (\<lambda>a. ereal \<bar>f a\<bar>)) \<le> e2ennreal (ereal C)
ennreal C < e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>))
?x \<le> 0 \<Longrightarrow> e2ennreal ?x = 0

goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>a. ereal \<bar>f a\<bar>)) \<le> e2ennreal (ereal C) \<longrightarrow> (\<exists>e\<le>esssup M (\<lambda>a. ereal \<bar>f a\<bar>). ereal C < e)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
e2ennreal (esssup M (\<lambda>a. ereal \<bar>f a\<bar>)) \<le> e2ennreal (ereal C) \<longrightarrow> (\<exists>e\<le>esssup M (\<lambda>a. ereal \<bar>f a\<bar>). ereal C < e)

goal (1 subgoal):
 1. ennreal C < e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) \<Longrightarrow> ereal C < esssup M (\<lambda>x. ereal \<bar>f x\<bar>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e2ennreal (esssup M (\<lambda>a. ereal \<bar>f a\<bar>)) \<le> e2ennreal (ereal C) \<longrightarrow> (\<exists>e\<le>esssup M (\<lambda>a. ereal \<bar>f a\<bar>). ereal C < e)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
e2ennreal (esssup M (\<lambda>a. ereal \<bar>f a\<bar>)) \<le> e2ennreal (ereal C) \<longrightarrow> (\<exists>e\<le>esssup M (\<lambda>a. ereal \<bar>f a\<bar>). ereal C < e)

goal (1 subgoal):
 1. ereal C < esssup M (\<lambda>x. ereal \<bar>f x\<bar>)
[PROOF STEP]
by (meson e2ennreal_mono leI less_le_trans)
[PROOF STATE]
proof (state)
this:
ereal C < esssup M (\<lambda>x. ereal \<bar>f x\<bar>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ereal C < esssup M (\<lambda>x. ereal \<bar>f x\<bar>)

goal (1 subgoal):
 1. 0 < emeasure M {x \<in> space M. C < \<bar>f x\<bar>}
[PROOF STEP]
have "emeasure M {x \<in> space M. ereal(\<bar>f x\<bar>) > C} > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < emeasure M {x \<in> space M. ereal C < ereal \<bar>f x\<bar>}
[PROOF STEP]
by (rule esssup_pos_measure[OF _ *], auto)
[PROOF STATE]
proof (state)
this:
0 < emeasure M {x \<in> space M. ereal C < ereal \<bar>f x\<bar>}

goal (1 subgoal):
 1. 0 < emeasure M {x \<in> space M. C < \<bar>f x\<bar>}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < emeasure M {x \<in> space M. ereal C < ereal \<bar>f x\<bar>}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < emeasure M {x \<in> space M. ereal C < ereal \<bar>f x\<bar>}

goal (1 subgoal):
 1. 0 < emeasure M {x \<in> space M. C < \<bar>f x\<bar>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < emeasure M {x \<in> space M. C < \<bar>f x\<bar>}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma L_infinity_tendsto_AE:
  assumes "tendsto_in\<^sub>N (\<LL> \<infinity> M) f g"
          "\<And>n. f n \<in> space\<^sub>N (\<LL> \<infinity> M)"
          "g \<in> space\<^sub>N (\<LL> \<infinity> M)"
  shows "AE x in M. (\<lambda>n. f n x) \<longlonglongrightarrow> g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. (\<lambda>n. f n x) \<longlonglongrightarrow> g x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AE x in M. (\<lambda>n. f n x) \<longlonglongrightarrow> g x
[PROOF STEP]
have *: "AE x in M. \<bar>(f n - g) x\<bar> \<le> Norm (\<LL> \<infinity> M) (f n - g)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. \<bar>(f n - g) x\<bar> \<le> Norm (\<LL> \<infinity> M) (f n - g)
[PROOF STEP]
apply (rule L_infinity_AE_bound)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n - g \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
using assms spaceN_diff
[PROOF STATE]
proof (prove)
using this:
tendsto_in\<^sub>N (\<LL> \<infinity> M) f g
f ?n \<in> space\<^sub>N (\<LL> \<infinity> M)
g \<in> space\<^sub>N (\<LL> \<infinity> M)
\<lbrakk>?x \<in> space\<^sub>N ?N; ?y \<in> space\<^sub>N ?N\<rbrakk> \<Longrightarrow> ?x - ?y \<in> space\<^sub>N ?N

goal (1 subgoal):
 1. f n - g \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
AE x in M. \<bar>(f ?n - g) x\<bar> \<le> Norm (\<LL> \<infinity> M) (f ?n - g)

goal (1 subgoal):
 1. AE x in M. (\<lambda>n. f n x) \<longlonglongrightarrow> g x
[PROOF STEP]
have "AE x in M. \<forall>n. \<bar>(f n - g) x\<bar> \<le> Norm (\<LL> \<infinity> M) (f n - g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. \<forall>n. \<bar>(f n - g) x\<bar> \<le> Norm (\<LL> \<infinity> M) (f n - g)
[PROOF STEP]
apply (subst AE_all_countable)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. AE x in M. \<bar>(f i - g) x\<bar> \<le> Norm (\<LL> \<infinity> M) (f i - g)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<bar>(f ?n - g) x\<bar> \<le> Norm (\<LL> \<infinity> M) (f ?n - g)

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

goal (1 subgoal):
 1. AE x in M. (\<lambda>n. f n x) \<longlonglongrightarrow> g x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AE x in M. \<forall>n. \<bar>(f n - g) x\<bar> \<le> Norm (\<LL> \<infinity> M) (f n - g)

goal (1 subgoal):
 1. AE x in M. (\<lambda>n. f n x) \<longlonglongrightarrow> g x
[PROOF STEP]
have "(\<lambda>n. f n x) \<longlonglongrightarrow> g x" if "\<forall>n. \<bar>(f n - g) x\<bar> \<le> Norm (\<LL> \<infinity> M) (f n - g)" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f n x) \<longlonglongrightarrow> g x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. f n x) \<longlonglongrightarrow> g x
[PROOF STEP]
have "(\<lambda>n. \<bar>(f n - g) x\<bar>) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. \<bar>(f n - g) x\<bar>) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (rule tendsto_sandwich[of "\<lambda>n. 0" _ _ "\<lambda>n. Norm (\<LL> \<infinity> M) (f n - g)"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<forall>\<^sub>F n in sequentially. 0 \<le> \<bar>(f n - g) x\<bar>
 2. \<forall>\<^sub>F n in sequentially. \<bar>(f n - g) x\<bar> \<le> Norm (\<LL> \<infinity> M) (f n - g)
 3. (\<lambda>n. 0) \<longlonglongrightarrow> 0
 4. (\<lambda>n. Norm (\<LL> \<infinity> M) (f n - g)) \<longlonglongrightarrow> 0
[PROOF STEP]
using that \<open>tendsto_in\<^sub>N (\<LL> \<infinity> M) f g\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<bar>(f n - g) x\<bar> \<le> Norm (\<LL> \<infinity> M) (f n - g)
tendsto_in\<^sub>N (\<LL> \<infinity> M) f g

goal (4 subgoals):
 1. \<forall>\<^sub>F n in sequentially. 0 \<le> \<bar>(f n - g) x\<bar>
 2. \<forall>\<^sub>F n in sequentially. \<bar>(f n - g) x\<bar> \<le> Norm (\<LL> \<infinity> M) (f n - g)
 3. (\<lambda>n. 0) \<longlonglongrightarrow> 0
 4. (\<lambda>n. Norm (\<LL> \<infinity> M) (f n - g)) \<longlonglongrightarrow> 0
[PROOF STEP]
unfolding tendsto_in\<^sub>N_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<bar>(f n - g) x\<bar> \<le> Norm (\<LL> \<infinity> M) (f n - g)
(\<lambda>n. Norm (\<LL> \<infinity> M) (f n - g)) \<longlonglongrightarrow> 0

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

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

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

goal (1 subgoal):
 1. (\<lambda>n. f n x) \<longlonglongrightarrow> g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. \<bar>f n x - g x\<bar>) \<longlonglongrightarrow> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. \<bar>f n x - g x\<bar>) \<longlonglongrightarrow> 0

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n. \<bar>(f n - g) ?x\<bar> \<le> Norm (\<LL> \<infinity> M) (f n - g) \<Longrightarrow> (\<lambda>n. f n ?x) \<longlonglongrightarrow> g ?x

goal (1 subgoal):
 1. AE x in M. (\<lambda>n. f n x) \<longlonglongrightarrow> g x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AE x in M. \<forall>n. \<bar>(f n - g) x\<bar> \<le> Norm (\<LL> \<infinity> M) (f n - g)
\<forall>n. \<bar>(f n - g) ?x\<bar> \<le> Norm (\<LL> \<infinity> M) (f n - g) \<Longrightarrow> (\<lambda>n. f n ?x) \<longlonglongrightarrow> g ?x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<forall>n. \<bar>(f n - g) x\<bar> \<le> Norm (\<LL> \<infinity> M) (f n - g)
\<forall>n. \<bar>(f n - g) ?x\<bar> \<le> Norm (\<LL> \<infinity> M) (f n - g) \<Longrightarrow> (\<lambda>n. f n ?x) \<longlonglongrightarrow> g ?x

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bcontfun_subset_L_infinity:
  assumes "sets M = sets borel"
  shows "space\<^sub>N bcontfun\<^sub>N \<subseteq> space\<^sub>N (\<LL> \<infinity> M)"
        "\<And>f. f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> Norm (\<LL> \<infinity> M) f \<le> Norm bcontfun\<^sub>N f"
        "\<And>f. eNorm (\<LL> \<infinity> M) f \<le> eNorm bcontfun\<^sub>N f"
        "bcontfun\<^sub>N \<subseteq>\<^sub>N \<LL> \<infinity> M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (space\<^sub>N bcontfun\<^sub>N \<subseteq> space\<^sub>N (\<LL> \<infinity> M) &&& (\<And>f. f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> Norm (\<LL> \<infinity> M) f \<le> Norm bcontfun\<^sub>N f)) &&& (\<And>f. eNorm (\<LL> \<infinity> M) f \<le> eNorm bcontfun\<^sub>N f) &&& bcontfun\<^sub>N \<subseteq>\<^sub>N \<LL> \<infinity> M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. space\<^sub>N bcontfun\<^sub>N \<subseteq> space\<^sub>N (\<LL> \<infinity> M)
 2. \<And>f. f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> Norm (\<LL> \<infinity> M) f \<le> Norm bcontfun\<^sub>N f
 3. \<And>f. eNorm (\<LL> \<infinity> M) f \<le> eNorm bcontfun\<^sub>N f
 4. bcontfun\<^sub>N \<subseteq>\<^sub>N \<LL> \<infinity> M
[PROOF STEP]
have *: "f \<in> space\<^sub>N (\<LL> \<infinity> M) \<and> Norm (\<LL> \<infinity> M) f \<le> Norm bcontfun\<^sub>N f" if "f \<in> space\<^sub>N bcontfun\<^sub>N" for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> \<infinity> M) \<and> Norm (\<LL> \<infinity> M) f \<le> Norm bcontfun\<^sub>N f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> \<infinity> M) \<and> Norm (\<LL> \<infinity> M) f \<le> Norm bcontfun\<^sub>N f
[PROOF STEP]
have H: "continuous_on UNIV f" "\<And>x. abs(f x) \<le> Norm bcontfun\<^sub>N f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV f &&& (\<And>x. \<bar>f x\<bar> \<le> Norm bcontfun\<^sub>N f)
[PROOF STEP]
using bcontfun\<^sub>ND[OF \<open>f \<in> space\<^sub>N bcontfun\<^sub>N\<close>]
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV f
norm (f ?x) \<le> Norm bcontfun\<^sub>N f

goal (1 subgoal):
 1. continuous_on UNIV f &&& (\<And>x. \<bar>f x\<bar> \<le> Norm bcontfun\<^sub>N f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
continuous_on UNIV f
\<bar>f ?x\<bar> \<le> Norm bcontfun\<^sub>N f

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> \<infinity> M) \<and> Norm (\<LL> \<infinity> M) f \<le> Norm bcontfun\<^sub>N f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
continuous_on UNIV f
\<bar>f ?x\<bar> \<le> Norm bcontfun\<^sub>N f
[PROOF STEP]
have "f \<in> borel_measurable borel"
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV f
\<bar>f ?x\<bar> \<le> Norm bcontfun\<^sub>N f

goal (1 subgoal):
 1. f \<in> borel_measurable borel
[PROOF STEP]
using borel_measurable_continuous_onI
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV f
\<bar>f ?x\<bar> \<le> Norm bcontfun\<^sub>N f
continuous_on UNIV ?f \<Longrightarrow> ?f \<in> borel_measurable borel

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

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> \<infinity> M) \<and> Norm (\<LL> \<infinity> M) f \<le> Norm bcontfun\<^sub>N f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> borel_measurable borel
[PROOF STEP]
have "f \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable borel

goal (1 subgoal):
 1. f \<in> borel_measurable M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable borel
sets M = sets borel

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

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> \<infinity> M) \<and> Norm (\<LL> \<infinity> M) f \<le> Norm bcontfun\<^sub>N f
[PROOF STEP]
have *: "AE x in M. \<bar>f x\<bar> \<le> Norm bcontfun\<^sub>N f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> \<le> Norm bcontfun\<^sub>N f
[PROOF STEP]
using H(2)
[PROOF STATE]
proof (prove)
using this:
\<bar>f ?x\<bar> \<le> Norm bcontfun\<^sub>N f

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

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> \<infinity> M) \<and> Norm (\<LL> \<infinity> M) f \<le> Norm bcontfun\<^sub>N f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> \<infinity> M) \<and> Norm (\<LL> \<infinity> M) f \<le> Norm bcontfun\<^sub>N f
[PROOF STEP]
using L_infinity_I[OF \<open>f \<in> borel_measurable M\<close> * Norm_nonneg]
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> \<infinity> M)
Norm (\<LL> \<infinity> M) f \<le> Norm bcontfun\<^sub>N f

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> ?f \<in> space\<^sub>N (\<LL> \<infinity> M) \<and> Norm (\<LL> \<infinity> M) ?f \<le> Norm bcontfun\<^sub>N ?f

goal (4 subgoals):
 1. space\<^sub>N bcontfun\<^sub>N \<subseteq> space\<^sub>N (\<LL> \<infinity> M)
 2. \<And>f. f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> Norm (\<LL> \<infinity> M) f \<le> Norm bcontfun\<^sub>N f
 3. \<And>f. eNorm (\<LL> \<infinity> M) f \<le> eNorm bcontfun\<^sub>N f
 4. bcontfun\<^sub>N \<subseteq>\<^sub>N \<LL> \<infinity> M
[PROOF STEP]
show "space\<^sub>N bcontfun\<^sub>N \<subseteq> space\<^sub>N (\<LL> \<infinity> M)"
       "\<And>f. f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> Norm (\<LL> \<infinity> M) f \<le> Norm bcontfun\<^sub>N f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space\<^sub>N bcontfun\<^sub>N \<subseteq> space\<^sub>N (\<LL> \<infinity> M) &&& (\<And>f. f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> Norm (\<LL> \<infinity> M) f \<le> Norm bcontfun\<^sub>N f)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
?f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> ?f \<in> space\<^sub>N (\<LL> \<infinity> M) \<and> Norm (\<LL> \<infinity> M) ?f \<le> Norm bcontfun\<^sub>N ?f

goal (1 subgoal):
 1. space\<^sub>N bcontfun\<^sub>N \<subseteq> space\<^sub>N (\<LL> \<infinity> M) &&& (\<And>f. f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> Norm (\<LL> \<infinity> M) f \<le> Norm bcontfun\<^sub>N f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
space\<^sub>N bcontfun\<^sub>N \<subseteq> space\<^sub>N (\<LL> \<infinity> M)
?f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> Norm (\<LL> \<infinity> M) ?f \<le> Norm bcontfun\<^sub>N ?f

goal (2 subgoals):
 1. \<And>f. eNorm (\<LL> \<infinity> M) f \<le> eNorm bcontfun\<^sub>N f
 2. bcontfun\<^sub>N \<subseteq>\<^sub>N \<LL> \<infinity> M
[PROOF STEP]
show **: "bcontfun\<^sub>N \<subseteq>\<^sub>N \<LL> \<infinity> M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bcontfun\<^sub>N \<subseteq>\<^sub>N \<LL> \<infinity> M
[PROOF STEP]
apply (rule quasinorm_subsetI'[of _ _ 1])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> f \<in> space\<^sub>N (\<LL> \<infinity> M)
 2. \<And>f. f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> Norm (\<LL> \<infinity> M) f \<le> 1 * Norm bcontfun\<^sub>N f
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
?f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> ?f \<in> space\<^sub>N (\<LL> \<infinity> M) \<and> Norm (\<LL> \<infinity> M) ?f \<le> Norm bcontfun\<^sub>N ?f

goal (2 subgoals):
 1. \<And>f. f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> f \<in> space\<^sub>N (\<LL> \<infinity> M)
 2. \<And>f. f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> Norm (\<LL> \<infinity> M) f \<le> 1 * Norm bcontfun\<^sub>N f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bcontfun\<^sub>N \<subseteq>\<^sub>N \<LL> \<infinity> M

goal (1 subgoal):
 1. \<And>f. eNorm (\<LL> \<infinity> M) f \<le> eNorm bcontfun\<^sub>N f
[PROOF STEP]
have "eNorm (\<LL> \<infinity> M) f \<le> ennreal 1 * eNorm bcontfun\<^sub>N f" for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> \<infinity> M) f \<le> ennreal 1 * eNorm bcontfun\<^sub>N f
[PROOF STEP]
apply (rule quasinorm_subset_Norm_eNorm)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> Norm (\<LL> \<infinity> M) f \<le> 1 * Norm bcontfun\<^sub>N f
 2. bcontfun\<^sub>N \<subseteq>\<^sub>N \<LL> \<infinity> M
 3. 0 < 1
[PROOF STEP]
using * **
[PROOF STATE]
proof (prove)
using this:
?f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> ?f \<in> space\<^sub>N (\<LL> \<infinity> M) \<and> Norm (\<LL> \<infinity> M) ?f \<le> Norm bcontfun\<^sub>N ?f
bcontfun\<^sub>N \<subseteq>\<^sub>N \<LL> \<infinity> M

goal (3 subgoals):
 1. f \<in> space\<^sub>N bcontfun\<^sub>N \<Longrightarrow> Norm (\<LL> \<infinity> M) f \<le> 1 * Norm bcontfun\<^sub>N f
 2. bcontfun\<^sub>N \<subseteq>\<^sub>N \<LL> \<infinity> M
 3. 0 < 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> \<infinity> M) ?f \<le> ennreal 1 * eNorm bcontfun\<^sub>N ?f

goal (1 subgoal):
 1. \<And>f. eNorm (\<LL> \<infinity> M) f \<le> eNorm bcontfun\<^sub>N f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> \<infinity> M) ?f \<le> ennreal 1 * eNorm bcontfun\<^sub>N ?f
[PROOF STEP]
show "eNorm (\<LL> \<infinity> M) f \<le> eNorm bcontfun\<^sub>N f" for f
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> \<infinity> M) ?f \<le> ennreal 1 * eNorm bcontfun\<^sub>N ?f

goal (1 subgoal):
 1. eNorm (\<LL> \<infinity> M) f \<le> eNorm bcontfun\<^sub>N f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> \<infinity> M) ?f \<le> eNorm bcontfun\<^sub>N ?f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Lp:
  assumes "p \<ge> (1::real)"
  shows "eNorm (\<LL> p M) f = (if (f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p))
                            then (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)
                            else (\<infinity>::ennreal))"
        "defect (\<LL> p M) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> (ennreal p) M) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>) &&& defect (\<LL> (ennreal p) M) = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eNorm (\<LL> (ennreal p) M) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
 2. defect (\<LL> (ennreal p) M) = 1
[PROOF STEP]
define F where "F = {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}"
[PROOF STATE]
proof (state)
this:
F = {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}

goal (2 subgoals):
 1. eNorm (\<LL> (ennreal p) M) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
 2. defect (\<LL> (ennreal p) M) = 1
[PROOF STEP]
have *: "quasinorm_on F 1 (\<lambda>(f::'a\<Rightarrow>real). (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quasinorm_on F 1 (\<lambda>x. ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)))
[PROOF STEP]
proof (rule quasinorm_onI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> F; y \<in> F\<rbrakk> \<Longrightarrow> x + y \<in> F
 2. \<And>x y. \<lbrakk>x \<in> F; y \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(x + y) xa\<bar> powr p) powr (1 / p)) \<le> ennreal 1 * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)) + ennreal 1 * ennreal ((LINT x|M. \<bar>y x\<bar> powr p) powr (1 / p))
 3. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> F
 4. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 5. 0 \<in> F
 6. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 7. 1 \<le> 1
[PROOF STEP]
fix f g
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> F; y \<in> F\<rbrakk> \<Longrightarrow> x + y \<in> F
 2. \<And>x y. \<lbrakk>x \<in> F; y \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(x + y) xa\<bar> powr p) powr (1 / p)) \<le> ennreal 1 * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)) + ennreal 1 * ennreal ((LINT x|M. \<bar>y x\<bar> powr p) powr (1 / p))
 3. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> F
 4. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 5. 0 \<in> F
 6. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 7. 1 \<le> 1
[PROOF STEP]
assume "f \<in> F" "g \<in> F"
[PROOF STATE]
proof (state)
this:
f \<in> F
g \<in> F

goal (7 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> F; y \<in> F\<rbrakk> \<Longrightarrow> x + y \<in> F
 2. \<And>x y. \<lbrakk>x \<in> F; y \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(x + y) xa\<bar> powr p) powr (1 / p)) \<le> ennreal 1 * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)) + ennreal 1 * ennreal ((LINT x|M. \<bar>y x\<bar> powr p) powr (1 / p))
 3. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> F
 4. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 5. 0 \<in> F
 6. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 7. 1 \<le> 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> F
g \<in> F
[PROOF STEP]
show "f + g \<in> F"
[PROOF STATE]
proof (prove)
using this:
f \<in> F
g \<in> F

goal (1 subgoal):
 1. f + g \<in> F
[PROOF STEP]
unfolding F_def plus_fun_def
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}
g \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> borel_measurable M; integrable M (\<lambda>x. \<bar>f x\<bar> powr p); g \<in> borel_measurable M; integrable M (\<lambda>x. \<bar>g x\<bar> powr p)\<rbrakk> \<Longrightarrow> integrable M (\<lambda>x. \<bar>f x + g x\<bar> powr p)
[PROOF STEP]
by (rule Minkowski_inequality(1), auto simp add: \<open>p \<ge> 1\<close>)
[PROOF STATE]
proof (state)
this:
f + g \<in> F

goal (6 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> F; y \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(x + y) xa\<bar> powr p) powr (1 / p)) \<le> ennreal 1 * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)) + ennreal 1 * ennreal ((LINT x|M. \<bar>y x\<bar> powr p) powr (1 / p))
 2. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> F
 3. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 4. 0 \<in> F
 5. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 6. 1 \<le> 1
[PROOF STEP]
show "ennreal ((\<integral>x. \<bar>(f + g) x\<bar> powr p \<partial>M) powr (1/p))
          \<le> ennreal 1 * (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p) + ennreal 1 * (\<integral>x. \<bar>g x\<bar> powr p \<partial>M) powr (1/p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal ((LINT x|M. \<bar>(f + g) x\<bar> powr p) powr (1 / p)) \<le> ennreal 1 * ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) + ennreal 1 * ennreal ((LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p))
[PROOF STEP]
apply (auto, subst ennreal_plus[symmetric], simp, simp, rule ennreal_leI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
unfolding plus_fun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
apply (rule Minkowski_inequality(2)[of p f M g], auto simp add: \<open>p \<ge> 1\<close>)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. f \<in> borel_measurable M
 2. g \<in> borel_measurable M
 3. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
 4. integrable M (\<lambda>x. \<bar>g x\<bar> powr p)
[PROOF STEP]
using \<open>f \<in> F\<close> \<open>g \<in> F\<close>
[PROOF STATE]
proof (prove)
using this:
f \<in> F
g \<in> F

goal (4 subgoals):
 1. f \<in> borel_measurable M
 2. g \<in> borel_measurable M
 3. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
 4. integrable M (\<lambda>x. \<bar>g x\<bar> powr p)
[PROOF STEP]
unfolding F_def
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}
g \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}

goal (4 subgoals):
 1. f \<in> borel_measurable M
 2. g \<in> borel_measurable M
 3. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
 4. integrable M (\<lambda>x. \<bar>g x\<bar> powr p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ennreal ((LINT x|M. \<bar>(f + g) x\<bar> powr p) powr (1 / p)) \<le> ennreal 1 * ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) + ennreal 1 * ennreal ((LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p))

goal (5 subgoals):
 1. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> F
 2. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 3. 0 \<in> F
 4. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 5. 1 \<le> 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> F
 2. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 3. 0 \<in> F
 4. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 5. 1 \<le> 1
[PROOF STEP]
fix f and c::real
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> F
 2. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 3. 0 \<in> F
 4. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 5. 1 \<le> 1
[PROOF STEP]
assume "f \<in> F"
[PROOF STATE]
proof (state)
this:
f \<in> F

goal (5 subgoals):
 1. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> F
 2. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 3. 0 \<in> F
 4. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 5. 1 \<le> 1
[PROOF STEP]
show "c *\<^sub>R f \<in> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c *\<^sub>R f \<in> F
[PROOF STEP]
using \<open>f \<in> F\<close>
[PROOF STATE]
proof (prove)
using this:
f \<in> F

goal (1 subgoal):
 1. c *\<^sub>R f \<in> F
[PROOF STEP]
unfolding scaleR_fun_def F_def
[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. (\<lambda>x. c *\<^sub>R f x) \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}
[PROOF STEP]
by (auto simp add: abs_mult powr_mult)
[PROOF STATE]
proof (state)
this:
c *\<^sub>R f \<in> F

goal (4 subgoals):
 1. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 2. 0 \<in> F
 3. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 4. 1 \<le> 1
[PROOF STEP]
show "(\<integral>x. \<bar>(c *\<^sub>R f) x\<bar> powr p \<partial>M) powr (1/p) \<le> ennreal(abs(c)) * (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal ((LINT x|M. \<bar>(c *\<^sub>R f) x\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))
[PROOF STEP]
apply (rule eq_refl, subst ennreal_mult[symmetric], simp, simp, rule ennreal_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>(c *\<^sub>R f) x\<bar> powr p) powr (1 / p) = \<bar>c\<bar> * (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
apply (unfold scaleR_fun_def, simp add: abs_mult powr_mult powr_powr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<noteq> 0 \<longrightarrow> p = 0 \<longrightarrow> LINT x|M. (if f x = 0 then 0 else 1) = 0 \<or> \<bar>c\<bar> = 1
[PROOF STEP]
using \<open>p \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> p

goal (1 subgoal):
 1. c \<noteq> 0 \<longrightarrow> p = 0 \<longrightarrow> LINT x|M. (if f x = 0 then 0 else 1) = 0 \<or> \<bar>c\<bar> = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ennreal ((LINT x|M. \<bar>(c *\<^sub>R f) x\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))

goal (3 subgoals):
 1. 0 \<in> F
 2. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 3. 1 \<le> 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 0 \<in> F
 2. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 3. 1 \<le> 1
[PROOF STEP]
show "0 \<in> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<in> F
[PROOF STEP]
unfolding zero_fun_def F_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. 0) \<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:
0 \<in> F

goal (2 subgoals):
 1. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 2. 1 \<le> 1
[PROOF STEP]
qed (auto)
[PROOF STATE]
proof (state)
this:
quasinorm_on F 1 (\<lambda>x. ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)))

goal (2 subgoals):
 1. eNorm (\<LL> (ennreal p) M) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
 2. defect (\<LL> (ennreal p) M) = 1
[PROOF STEP]
have "p \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> p
[PROOF STEP]
using \<open>p \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> p

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

goal (2 subgoals):
 1. eNorm (\<LL> (ennreal p) M) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
 2. defect (\<LL> (ennreal p) M) = 1
[PROOF STEP]
have **: "\<LL> p M = quasinorm_of (1,
              (\<lambda>f. if (f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p))
              then (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)
              else (\<infinity>::ennreal)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<LL> (ennreal p) M = quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
[PROOF STEP]
unfolding Lp_space_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if ennreal p = 0 then quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>) else if ennreal p < \<infinity> then quasinorm_of (if ennreal p < 1 then 2 powr (1 / enn2real (ennreal p) - 1) else 1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr enn2real (ennreal p)) then ennreal ((LINT x|M. \<bar>f x\<bar> powr enn2real (ennreal p)) powr (1 / enn2real (ennreal p))) 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>)) = quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
[PROOF STEP]
using enn2real_ennreal[OF \<open>p \<ge> 0\<close>] \<open>p \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
enn2real (ennreal p) = p
1 \<le> p

goal (1 subgoal):
 1. (if ennreal p = 0 then quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>) else if ennreal p < \<infinity> then quasinorm_of (if ennreal p < 1 then 2 powr (1 / enn2real (ennreal p) - 1) else 1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr enn2real (ennreal p)) then ennreal ((LINT x|M. \<bar>f x\<bar> powr enn2real (ennreal p)) powr (1 / enn2real (ennreal p))) 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>)) = quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> p \<Longrightarrow> quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr enn2real (ennreal p)) powr (1 / enn2real (ennreal p))) else \<infinity>) = quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
[PROOF STEP]
using enn2real_ennreal[OF \<open>p \<ge> 0\<close>]
[PROOF STATE]
proof (prove)
using this:
enn2real (ennreal p) = p

goal (1 subgoal):
 1. 1 \<le> p \<Longrightarrow> quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr enn2real (ennreal p)) powr (1 / enn2real (ennreal p))) else \<infinity>) = quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<LL> (ennreal p) M = quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)

goal (2 subgoals):
 1. eNorm (\<LL> (ennreal p) M) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
 2. defect (\<LL> (ennreal p) M) = 1
[PROOF STEP]
show "eNorm (\<LL> p M) f = (if (f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p))
                            then (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)
                            else (\<infinity>::ennreal))"
      "defect (\<LL> p M) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> (ennreal p) M) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>) &&& defect (\<LL> (ennreal p) M) = 1
[PROOF STEP]
unfolding **
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>) &&& defect (quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)) = 1
[PROOF STEP]
using quasinorm_of[OF extend_quasinorm[OF *]]
[PROOF STATE]
proof (prove)
using this:
eNorm (quasinorm_of (1, \<lambda>x. if x \<in> F then ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)) else \<infinity>)) ?x = (if ?x \<in> F then ennreal ((LINT x|M. \<bar>?x x\<bar> powr p) powr (1 / p)) else \<infinity>)
defect (quasinorm_of (1, \<lambda>x. if x \<in> F then ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)) else \<infinity>)) = 1

goal (1 subgoal):
 1. eNorm (quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>) &&& defect (quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)) = 1
[PROOF STEP]
unfolding F_def
[PROOF STATE]
proof (prove)
using this:
eNorm (quasinorm_of (1, \<lambda>x. if x \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)} then ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)) else \<infinity>)) ?x = (if ?x \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)} then ennreal ((LINT x|M. \<bar>?x x\<bar> powr p) powr (1 / p)) else \<infinity>)
defect (quasinorm_of (1, \<lambda>x. if x \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)} then ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)) else \<infinity>)) = 1

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Lp_le_1:
  assumes "p > 0" "p \<le> (1::real)"
  shows "eNorm (\<LL> p M) f = (if (f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p))
                            then (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)
                            else (\<infinity>::ennreal))"
        "defect (\<LL> p M) = 2 powr (1/p - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> (ennreal p) M) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>) &&& defect (\<LL> (ennreal p) M) = 2 powr (1 / p - 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eNorm (\<LL> (ennreal p) M) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
 2. defect (\<LL> (ennreal p) M) = 2 powr (1 / p - 1)
[PROOF STEP]
define F where "F = {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}"
[PROOF STATE]
proof (state)
this:
F = {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}

goal (2 subgoals):
 1. eNorm (\<LL> (ennreal p) M) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
 2. defect (\<LL> (ennreal p) M) = 2 powr (1 / p - 1)
[PROOF STEP]
have *: "quasinorm_on F (2 powr (1/p-1)) (\<lambda>(f::'a\<Rightarrow>real). (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quasinorm_on F (2 powr (1 / p - 1)) (\<lambda>x. ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)))
[PROOF STEP]
proof (rule quasinorm_onI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> F; y \<in> F\<rbrakk> \<Longrightarrow> x + y \<in> F
 2. \<And>x y. \<lbrakk>x \<in> F; y \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(x + y) xa\<bar> powr p) powr (1 / p)) \<le> ennreal (2 powr (1 / p - 1)) * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)) + ennreal (2 powr (1 / p - 1)) * ennreal ((LINT x|M. \<bar>y x\<bar> powr p) powr (1 / p))
 3. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> F
 4. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 5. 0 \<in> F
 6. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 7. 1 \<le> 2 powr (1 / p - 1)
[PROOF STEP]
fix f g
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> F; y \<in> F\<rbrakk> \<Longrightarrow> x + y \<in> F
 2. \<And>x y. \<lbrakk>x \<in> F; y \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(x + y) xa\<bar> powr p) powr (1 / p)) \<le> ennreal (2 powr (1 / p - 1)) * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)) + ennreal (2 powr (1 / p - 1)) * ennreal ((LINT x|M. \<bar>y x\<bar> powr p) powr (1 / p))
 3. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> F
 4. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 5. 0 \<in> F
 6. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 7. 1 \<le> 2 powr (1 / p - 1)
[PROOF STEP]
assume "f \<in> F" "g \<in> F"
[PROOF STATE]
proof (state)
this:
f \<in> F
g \<in> F

goal (7 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> F; y \<in> F\<rbrakk> \<Longrightarrow> x + y \<in> F
 2. \<And>x y. \<lbrakk>x \<in> F; y \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(x + y) xa\<bar> powr p) powr (1 / p)) \<le> ennreal (2 powr (1 / p - 1)) * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)) + ennreal (2 powr (1 / p - 1)) * ennreal ((LINT x|M. \<bar>y x\<bar> powr p) powr (1 / p))
 3. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> F
 4. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 5. 0 \<in> F
 6. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 7. 1 \<le> 2 powr (1 / p - 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> F
g \<in> F
[PROOF STEP]
show "f + g \<in> F"
[PROOF STATE]
proof (prove)
using this:
f \<in> F
g \<in> F

goal (1 subgoal):
 1. f + g \<in> F
[PROOF STEP]
unfolding F_def plus_fun_def
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}
g \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> borel_measurable M; integrable M (\<lambda>x. \<bar>f x\<bar> powr p); g \<in> borel_measurable M; integrable M (\<lambda>x. \<bar>g x\<bar> powr p)\<rbrakk> \<Longrightarrow> integrable M (\<lambda>x. \<bar>f x + g x\<bar> powr p)
[PROOF STEP]
by (rule Minkowski_inequality_le_1(1), auto simp add: \<open>p > 0\<close> \<open>p \<le> 1\<close>)
[PROOF STATE]
proof (state)
this:
f + g \<in> F

goal (6 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> F; y \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(x + y) xa\<bar> powr p) powr (1 / p)) \<le> ennreal (2 powr (1 / p - 1)) * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)) + ennreal (2 powr (1 / p - 1)) * ennreal ((LINT x|M. \<bar>y x\<bar> powr p) powr (1 / p))
 2. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> F
 3. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 4. 0 \<in> F
 5. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 6. 1 \<le> 2 powr (1 / p - 1)
[PROOF STEP]
show "ennreal ((\<integral>x. \<bar>(f + g) x\<bar> powr p \<partial>M) powr (1/p))
          \<le> ennreal (2 powr (1/p-1)) * (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p) + ennreal (2 powr (1/p-1)) * (\<integral>x. \<bar>g x\<bar> powr p \<partial>M) powr (1/p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal ((LINT x|M. \<bar>(f + g) x\<bar> powr p) powr (1 / p)) \<le> ennreal (2 powr (1 / p - 1)) * ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) + ennreal (2 powr (1 / p - 1)) * ennreal ((LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p))
[PROOF STEP]
apply (subst ennreal_mult[symmetric], auto)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal ((LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p)) \<le> ennreal (2 powr (1 / p - 1) * (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) + ennreal (2 powr (1 / p - 1) * (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p))
[PROOF STEP]
apply (subst ennreal_plus[symmetric], simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal ((LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p)) \<le> ennreal (2 powr (1 / p - 1) * (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + 2 powr (1 / p - 1) * (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p))
[PROOF STEP]
apply (rule ennreal_leI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> 2 powr (1 / p - 1) * (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + 2 powr (1 / p - 1) * (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
unfolding plus_fun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> 2 powr (1 / p - 1) * (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + 2 powr (1 / p - 1) * (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
apply (rule Minkowski_inequality_le_1(2)[of p f M g], auto simp add: \<open>p > 0\<close> \<open>p \<le> 1\<close>)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. f \<in> borel_measurable M
 2. g \<in> borel_measurable M
 3. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
 4. integrable M (\<lambda>x. \<bar>g x\<bar> powr p)
[PROOF STEP]
using \<open>f \<in> F\<close> \<open>g \<in> F\<close>
[PROOF STATE]
proof (prove)
using this:
f \<in> F
g \<in> F

goal (4 subgoals):
 1. f \<in> borel_measurable M
 2. g \<in> borel_measurable M
 3. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
 4. integrable M (\<lambda>x. \<bar>g x\<bar> powr p)
[PROOF STEP]
unfolding F_def
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}
g \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}

goal (4 subgoals):
 1. f \<in> borel_measurable M
 2. g \<in> borel_measurable M
 3. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
 4. integrable M (\<lambda>x. \<bar>g x\<bar> powr p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ennreal ((LINT x|M. \<bar>(f + g) x\<bar> powr p) powr (1 / p)) \<le> ennreal (2 powr (1 / p - 1)) * ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) + ennreal (2 powr (1 / p - 1)) * ennreal ((LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p))

goal (5 subgoals):
 1. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> F
 2. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 3. 0 \<in> F
 4. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 5. 1 \<le> 2 powr (1 / p - 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> F
 2. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 3. 0 \<in> F
 4. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 5. 1 \<le> 2 powr (1 / p - 1)
[PROOF STEP]
fix f and c::real
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> F
 2. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 3. 0 \<in> F
 4. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 5. 1 \<le> 2 powr (1 / p - 1)
[PROOF STEP]
assume "f \<in> F"
[PROOF STATE]
proof (state)
this:
f \<in> F

goal (5 subgoals):
 1. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> F
 2. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 3. 0 \<in> F
 4. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 5. 1 \<le> 2 powr (1 / p - 1)
[PROOF STEP]
show "c *\<^sub>R f \<in> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c *\<^sub>R f \<in> F
[PROOF STEP]
using \<open>f \<in> F\<close>
[PROOF STATE]
proof (prove)
using this:
f \<in> F

goal (1 subgoal):
 1. c *\<^sub>R f \<in> F
[PROOF STEP]
unfolding scaleR_fun_def F_def
[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. (\<lambda>x. c *\<^sub>R f x) \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}
[PROOF STEP]
by (auto simp add: abs_mult powr_mult)
[PROOF STATE]
proof (state)
this:
c *\<^sub>R f \<in> F

goal (4 subgoals):
 1. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> F\<rbrakk> \<Longrightarrow> ennreal ((LINT xa|M. \<bar>(c *\<^sub>R x) xa\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p))
 2. 0 \<in> F
 3. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 4. 1 \<le> 2 powr (1 / p - 1)
[PROOF STEP]
show "(\<integral>x. \<bar>(c *\<^sub>R f) x\<bar> powr p \<partial>M) powr (1/p) \<le> ennreal(abs(c)) * (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal ((LINT x|M. \<bar>(c *\<^sub>R f) x\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))
[PROOF STEP]
apply (rule eq_refl, subst ennreal_mult[symmetric], simp, simp, rule ennreal_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>(c *\<^sub>R f) x\<bar> powr p) powr (1 / p) = \<bar>c\<bar> * (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
apply (unfold scaleR_fun_def, simp add: abs_mult powr_mult powr_powr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<noteq> 0 \<longrightarrow> p = 0 \<longrightarrow> LINT x|M. (if f x = 0 then 0 else 1) = 0 \<or> \<bar>c\<bar> = 1
[PROOF STEP]
using \<open>p > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < p

goal (1 subgoal):
 1. c \<noteq> 0 \<longrightarrow> p = 0 \<longrightarrow> LINT x|M. (if f x = 0 then 0 else 1) = 0 \<or> \<bar>c\<bar> = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ennreal ((LINT x|M. \<bar>(c *\<^sub>R f) x\<bar> powr p) powr (1 / p)) \<le> ennreal \<bar>c\<bar> * ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))

goal (3 subgoals):
 1. 0 \<in> F
 2. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 3. 1 \<le> 2 powr (1 / p - 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 0 \<in> F
 2. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 3. 1 \<le> 2 powr (1 / p - 1)
[PROOF STEP]
show "0 \<in> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<in> F
[PROOF STEP]
unfolding zero_fun_def F_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. 0) \<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:
0 \<in> F

goal (2 subgoals):
 1. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
 2. 1 \<le> 2 powr (1 / p - 1)
[PROOF STEP]
show "1 \<le> 2 powr (1 / p - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> 2 powr (1 / p - 1)
[PROOF STEP]
using \<open>p > 0\<close> \<open>p \<le> 1\<close>
[PROOF STATE]
proof (prove)
using this:
0 < p
p \<le> 1

goal (1 subgoal):
 1. 1 \<le> 2 powr (1 / p - 1)
[PROOF STEP]
by (auto simp add: ge_one_powr_ge_zero)
[PROOF STATE]
proof (state)
this:
1 \<le> 2 powr (1 / p - 1)

goal (1 subgoal):
 1. ennreal ((LINT x|M. \<bar>0 x\<bar> powr p) powr (1 / p)) = 0
[PROOF STEP]
qed (auto)
[PROOF STATE]
proof (state)
this:
quasinorm_on F (2 powr (1 / p - 1)) (\<lambda>x. ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)))

goal (2 subgoals):
 1. eNorm (\<LL> (ennreal p) M) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
 2. defect (\<LL> (ennreal p) M) = 2 powr (1 / p - 1)
[PROOF STEP]
have "p \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> p
[PROOF STEP]
using \<open>p > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < p

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

goal (2 subgoals):
 1. eNorm (\<LL> (ennreal p) M) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
 2. defect (\<LL> (ennreal p) M) = 2 powr (1 / p - 1)
[PROOF STEP]
have **: "\<LL> p M = quasinorm_of (2 powr (1/p-1),
              (\<lambda>f. if (f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p))
              then (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)
              else (\<infinity>::ennreal)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<LL> (ennreal p) M = quasinorm_of (2 powr (1 / p - 1), \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
[PROOF STEP]
unfolding Lp_space_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if ennreal p = 0 then quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>) else if ennreal p < \<infinity> then quasinorm_of (if ennreal p < 1 then 2 powr (1 / enn2real (ennreal p) - 1) else 1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr enn2real (ennreal p)) then ennreal ((LINT x|M. \<bar>f x\<bar> powr enn2real (ennreal p)) powr (1 / enn2real (ennreal p))) 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>)) = quasinorm_of (2 powr (1 / p - 1), \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
[PROOF STEP]
using \<open>p > 0\<close> \<open>p \<le> 1\<close>
[PROOF STATE]
proof (prove)
using this:
0 < p
p \<le> 1

goal (1 subgoal):
 1. (if ennreal p = 0 then quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>) else if ennreal p < \<infinity> then quasinorm_of (if ennreal p < 1 then 2 powr (1 / enn2real (ennreal p) - 1) else 1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr enn2real (ennreal p)) then ennreal ((LINT x|M. \<bar>f x\<bar> powr enn2real (ennreal p)) powr (1 / enn2real (ennreal p))) 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>)) = quasinorm_of (2 powr (1 / p - 1), \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
[PROOF STEP]
using enn2real_ennreal[OF \<open>p \<ge> 0\<close>]
[PROOF STATE]
proof (prove)
using this:
0 < p
p \<le> 1
enn2real (ennreal p) = p

goal (1 subgoal):
 1. (if ennreal p = 0 then quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>) else if ennreal p < \<infinity> then quasinorm_of (if ennreal p < 1 then 2 powr (1 / enn2real (ennreal p) - 1) else 1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr enn2real (ennreal p)) then ennreal ((LINT x|M. \<bar>f x\<bar> powr enn2real (ennreal p)) powr (1 / enn2real (ennreal p))) 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>)) = quasinorm_of (2 powr (1 / p - 1), \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < p; p < 1\<rbrakk> \<Longrightarrow> quasinorm_of (2 powr (1 / p - 1), \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr enn2real (ennreal p)) powr (1 / enn2real (ennreal p))) else \<infinity>) = quasinorm_of (2 powr (1 / p - 1), \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
 2. p = 1 \<Longrightarrow> quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar>) then ennreal ((LINT x|M. \<bar>f x\<bar> powr enn2real (ennreal 1)) powr (1 / enn2real (ennreal 1))) else \<infinity>) = quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar>) then ennreal ((LINT x|M. \<bar>f x\<bar> powr 1) powr (1 / 1)) else \<infinity>)
[PROOF STEP]
by (insert enn2real_ennreal[OF \<open>p \<ge> 0\<close>], presburger)+
[PROOF STATE]
proof (state)
this:
\<LL> (ennreal p) M = quasinorm_of (2 powr (1 / p - 1), \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)

goal (2 subgoals):
 1. eNorm (\<LL> (ennreal p) M) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)
 2. defect (\<LL> (ennreal p) M) = 2 powr (1 / p - 1)
[PROOF STEP]
show "eNorm (\<LL> p M) f = (if (f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p))
                            then (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)
                            else (\<infinity>::ennreal))"
      "defect (\<LL> p M) = 2 powr (1/p-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> (ennreal p) M) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>) &&& defect (\<LL> (ennreal p) M) = 2 powr (1 / p - 1)
[PROOF STEP]
unfolding **
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (quasinorm_of (2 powr (1 / p - 1), \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>) &&& defect (quasinorm_of (2 powr (1 / p - 1), \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)) = 2 powr (1 / p - 1)
[PROOF STEP]
using quasinorm_of[OF extend_quasinorm[OF *]]
[PROOF STATE]
proof (prove)
using this:
eNorm (quasinorm_of (2 powr (1 / p - 1), \<lambda>x. if x \<in> F then ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)) else \<infinity>)) ?x = (if ?x \<in> F then ennreal ((LINT x|M. \<bar>?x x\<bar> powr p) powr (1 / p)) else \<infinity>)
defect (quasinorm_of (2 powr (1 / p - 1), \<lambda>x. if x \<in> F then ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)) else \<infinity>)) = 2 powr (1 / p - 1)

goal (1 subgoal):
 1. eNorm (quasinorm_of (2 powr (1 / p - 1), \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)) f = (if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>) &&& defect (quasinorm_of (2 powr (1 / p - 1), \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) then ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)) else \<infinity>)) = 2 powr (1 / p - 1)
[PROOF STEP]
unfolding F_def
[PROOF STATE]
proof (prove)
using this:
eNorm (quasinorm_of (2 powr (1 / p - 1), \<lambda>x. if x \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)} then ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)) else \<infinity>)) ?x = (if ?x \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)} then ennreal ((LINT x|M. \<bar>?x x\<bar> powr p) powr (1 / p)) else \<infinity>)
defect (quasinorm_of (2 powr (1 / p - 1), \<lambda>x. if x \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)} then ennreal ((LINT xa|M. \<bar>x xa\<bar> powr p) powr (1 / p)) else \<infinity>)) = 2 powr (1 / p - 1)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Lp_space:
  assumes "p > (0::real)"
  shows "space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space\<^sub>N (\<LL> (ennreal p) M) = {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)}
[PROOF STEP]
apply (auto simp add: spaceN_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. eNorm (\<LL> (ennreal p) M) x < \<top> \<Longrightarrow> x \<in> borel_measurable M
 2. \<And>x. eNorm (\<LL> (ennreal p) M) x < \<top> \<Longrightarrow> integrable M (\<lambda>xa. \<bar>x xa\<bar> powr p)
 3. \<And>x. \<lbrakk>x \<in> borel_measurable M; integrable M (\<lambda>xa. \<bar>x xa\<bar> powr p)\<rbrakk> \<Longrightarrow> eNorm (\<LL> (ennreal p) M) x < \<top>
[PROOF STEP]
using Lp(1) Lp_le_1(1) \<open>p > 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?p \<Longrightarrow> eNorm (\<LL> (ennreal ?p) ?M) ?f = (if ?f \<in> borel_measurable ?M \<and> integrable ?M (\<lambda>x. \<bar>?f x\<bar> powr ?p) then ennreal ((LINT x|?M. \<bar>?f x\<bar> powr ?p) powr (1 / ?p)) else \<infinity>)
\<lbrakk>0 < ?p; ?p \<le> 1\<rbrakk> \<Longrightarrow> eNorm (\<LL> (ennreal ?p) ?M) ?f = (if ?f \<in> borel_measurable ?M \<and> integrable ?M (\<lambda>x. \<bar>?f x\<bar> powr ?p) then ennreal ((LINT x|?M. \<bar>?f x\<bar> powr ?p) powr (1 / ?p)) else \<infinity>)
0 < p

goal (3 subgoals):
 1. \<And>x. eNorm (\<LL> (ennreal p) M) x < \<top> \<Longrightarrow> x \<in> borel_measurable M
 2. \<And>x. eNorm (\<LL> (ennreal p) M) x < \<top> \<Longrightarrow> integrable M (\<lambda>xa. \<bar>x xa\<bar> powr p)
 3. \<And>x. \<lbrakk>x \<in> borel_measurable M; integrable M (\<lambda>xa. \<bar>x xa\<bar> powr p)\<rbrakk> \<Longrightarrow> eNorm (\<LL> (ennreal p) M) x < \<top>
[PROOF STEP]
apply (metis infinity_ennreal_def less_le not_less)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. eNorm (\<LL> (ennreal p) M) x < \<top> \<Longrightarrow> integrable M (\<lambda>xa. \<bar>x xa\<bar> powr p)
 2. \<And>x. \<lbrakk>x \<in> borel_measurable M; integrable M (\<lambda>xa. \<bar>x xa\<bar> powr p)\<rbrakk> \<Longrightarrow> eNorm (\<LL> (ennreal p) M) x < \<top>
[PROOF STEP]
using Lp(1) Lp_le_1(1) \<open>p > 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?p \<Longrightarrow> eNorm (\<LL> (ennreal ?p) ?M) ?f = (if ?f \<in> borel_measurable ?M \<and> integrable ?M (\<lambda>x. \<bar>?f x\<bar> powr ?p) then ennreal ((LINT x|?M. \<bar>?f x\<bar> powr ?p) powr (1 / ?p)) else \<infinity>)
\<lbrakk>0 < ?p; ?p \<le> 1\<rbrakk> \<Longrightarrow> eNorm (\<LL> (ennreal ?p) ?M) ?f = (if ?f \<in> borel_measurable ?M \<and> integrable ?M (\<lambda>x. \<bar>?f x\<bar> powr ?p) then ennreal ((LINT x|?M. \<bar>?f x\<bar> powr ?p) powr (1 / ?p)) else \<infinity>)
0 < p

goal (2 subgoals):
 1. \<And>x. eNorm (\<LL> (ennreal p) M) x < \<top> \<Longrightarrow> integrable M (\<lambda>xa. \<bar>x xa\<bar> powr p)
 2. \<And>x. \<lbrakk>x \<in> borel_measurable M; integrable M (\<lambda>xa. \<bar>x xa\<bar> powr p)\<rbrakk> \<Longrightarrow> eNorm (\<LL> (ennreal p) M) x < \<top>
[PROOF STEP]
apply (metis infinity_ennreal_def less_le not_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; integrable M (\<lambda>xa. \<bar>x xa\<bar> powr p)\<rbrakk> \<Longrightarrow> eNorm (\<LL> (ennreal p) M) x < \<top>
[PROOF STEP]
using Lp(1) Lp_le_1(1) \<open>p > 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?p \<Longrightarrow> eNorm (\<LL> (ennreal ?p) ?M) ?f = (if ?f \<in> borel_measurable ?M \<and> integrable ?M (\<lambda>x. \<bar>?f x\<bar> powr ?p) then ennreal ((LINT x|?M. \<bar>?f x\<bar> powr ?p) powr (1 / ?p)) else \<infinity>)
\<lbrakk>0 < ?p; ?p \<le> 1\<rbrakk> \<Longrightarrow> eNorm (\<LL> (ennreal ?p) ?M) ?f = (if ?f \<in> borel_measurable ?M \<and> integrable ?M (\<lambda>x. \<bar>?f x\<bar> powr ?p) then ennreal ((LINT x|?M. \<bar>?f x\<bar> powr ?p) powr (1 / ?p)) else \<infinity>)
0 < p

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; integrable M (\<lambda>xa. \<bar>x xa\<bar> powr p)\<rbrakk> \<Longrightarrow> eNorm (\<LL> (ennreal p) M) x < \<top>
[PROOF STEP]
by (metis ennreal_neq_top linear top.not_eq_extremum)


[STATEMENT]
lemma Lp_I:
  assumes "p > (0::real)"
          "f \<in> borel_measurable M" "integrable M (\<lambda>x. \<bar>f x\<bar> powr p)"
  shows "f \<in> space\<^sub>N (\<LL> p M)"
        "Norm (\<LL> p M) f = (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)"
        "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. f \<in> space\<^sub>N (\<LL> (ennreal p) M) &&& Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) &&& eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f \<in> space\<^sub>N (\<LL> (ennreal p) M)
 2. Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
 3. 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 = (\<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 assms, 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 (3 subgoals):
 1. f \<in> space\<^sub>N (\<LL> (ennreal p) M)
 2. Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
 3. eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))
[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]
show **: "f \<in> space\<^sub>N (\<LL> p M)"
[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. f \<in> space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
unfolding 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))

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

goal (2 subgoals):
 1. Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
 2. eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))
[PROOF STEP]
show "Norm (\<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. Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
[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))

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
unfolding Norm_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))

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

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]
then
[PROOF STATE]
proof (chain)
picking this:
Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
show "eNorm (\<LL> p M) f = (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)"
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)

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]
using eNorm_Norm[OF **]
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
eNorm (\<LL> (ennreal p) M) f = ennreal (Norm (\<LL> (ennreal p) M) f)

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 auto
[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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Lp_D:
  assumes "p>0" "f \<in> space\<^sub>N (\<LL> p M)"
  shows "f \<in> borel_measurable M"
        "integrable M (\<lambda>x. \<bar>f x\<bar> powr p)"
        "Norm (\<LL> p M) f = (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)"
        "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. (f \<in> borel_measurable M &&& integrable M (\<lambda>x. \<bar>f x\<bar> powr p)) &&& Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) &&& eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. f \<in> borel_measurable M
 2. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
 3. Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
 4. eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))
[PROOF STEP]
show *: "f \<in> borel_measurable M"
          "integrable M (\<lambda>x. \<bar>f x\<bar> powr p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> borel_measurable M &&& integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
[PROOF STEP]
using Lp_space[OF \<open>p > 0\<close>] assms(2)
[PROOF STATE]
proof (prove)
using this:
space\<^sub>N (\<LL> (ennreal p) ?M) = {f \<in> borel_measurable ?M. integrable ?M (\<lambda>x. \<bar>f x\<bar> powr p)}
f \<in> space\<^sub>N (\<LL> (ennreal p) M)

goal (1 subgoal):
 1. 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> borel_measurable M
integrable M (\<lambda>x. \<bar>f x\<bar> powr p)

goal (2 subgoals):
 1. Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
 2. eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> borel_measurable M
integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
[PROOF STEP]
show "Norm (\<LL> p M) f = (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)"
            "eNorm (\<LL> p M) f = (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)"
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M
integrable M (\<lambda>x. \<bar>f x\<bar> powr p)

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) &&& eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))
[PROOF STEP]
using Lp_I[OF \<open>p > 0\<close>]
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M
integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
\<lbrakk>?f \<in> borel_measurable ?M; integrable ?M (\<lambda>x. \<bar>?f x\<bar> powr p)\<rbrakk> \<Longrightarrow> ?f \<in> space\<^sub>N (\<LL> (ennreal p) ?M)
\<lbrakk>?f \<in> borel_measurable ?M; integrable ?M (\<lambda>x. \<bar>?f x\<bar> powr p)\<rbrakk> \<Longrightarrow> Norm (\<LL> (ennreal p) ?M) ?f = (LINT x|?M. \<bar>?f x\<bar> powr p) powr (1 / p)
\<lbrakk>?f \<in> borel_measurable ?M; integrable ?M (\<lambda>x. \<bar>?f x\<bar> powr p)\<rbrakk> \<Longrightarrow> eNorm (\<LL> (ennreal p) ?M) ?f = ennreal ((LINT x|?M. \<bar>?f x\<bar> powr p) powr (1 / p))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Lp_Norm:
  assumes "p > (0::real)"
          "f \<in> borel_measurable M"
  shows "Norm (\<LL> p M) f = (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)"
        "(Norm (\<LL> p M) f) powr p = (\<integral>x. \<bar>f x\<bar> powr p \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) &&& Norm (\<LL> (ennreal p) M) f powr p = LINT x|M. \<bar>f x\<bar> powr p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
 2. Norm (\<LL> (ennreal p) M) f powr p = LINT x|M. \<bar>f x\<bar> powr p
[PROOF STEP]
show *: "Norm (\<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. Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
proof (cases "integrable M (\<lambda>x. \<bar>f x\<bar> powr p)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr p) \<Longrightarrow> Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
 2. \<not> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) \<Longrightarrow> Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. \<bar>f x\<bar> powr p)

goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr p) \<Longrightarrow> Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
 2. \<not> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) \<Longrightarrow> Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
integrable M (\<lambda>x. \<bar>f x\<bar> powr p)

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
using Lp_I[OF assms True]
[PROOF STATE]
proof (prove)
using this:
integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
f \<in> space\<^sub>N (\<LL> (ennreal p) M)
Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
eNorm (\<LL> (ennreal p) M) f = ennreal ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p))

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

goal (1 subgoal):
 1. \<not> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) \<Longrightarrow> Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) \<Longrightarrow> Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> integrable M (\<lambda>x. \<bar>f x\<bar> powr p)

goal (1 subgoal):
 1. \<not> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) \<Longrightarrow> Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
[PROOF STEP]
have "f \<notin> space\<^sub>N (\<LL> p M)"
[PROOF STATE]
proof (prove)
using this:
\<not> integrable M (\<lambda>x. \<bar>f x\<bar> powr p)

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

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

goal (1 subgoal):
 1. \<not> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) \<Longrightarrow> Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<notin> space\<^sub>N (\<LL> (ennreal p) M)
[PROOF STEP]
have *: "Norm (\<LL> p M) f = 0"
[PROOF STATE]
proof (prove)
using this:
f \<notin> space\<^sub>N (\<LL> (ennreal p) M)

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

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

goal (1 subgoal):
 1. \<not> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) \<Longrightarrow> Norm (\<LL> (ennreal p) M) f = (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)
goal (1 subgoal):
 1. LINT x|M. \<bar>f x\<bar> powr p = 0
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> integrable M (\<lambda>x. \<bar>f x\<bar> powr p)

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

goal (1 subgoal):
 1. \<not> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) \<Longrightarrow> Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
LINT x|M. \<bar>f x\<bar> powr p = 0
[PROOF STEP]
have "(\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p) = 0"
[PROOF STATE]
proof (prove)
using this:
LINT x|M. \<bar>f x\<bar> powr p = 0

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

goal (1 subgoal):
 1. \<not> integrable M (\<lambda>x. \<bar>f x\<bar> powr p) \<Longrightarrow> Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) = 0

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p) M) f powr p = LINT x|M. \<bar>f x\<bar> powr p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
show "(Norm (\<LL> p M) f) powr p = (\<integral>x. \<bar>f x\<bar> powr p \<partial>M)"
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> (ennreal p) M) f = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p) M) f powr p = LINT x|M. \<bar>f x\<bar> powr p
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
(LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) = (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) powr (1 / p)) powr p = LINT x|M. \<bar>f x\<bar> powr p
[PROOF STEP]
using powr_powr \<open>p > 0\<close>
[PROOF STATE]
proof (prove)
using this:
(LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p)
(?x powr ?a) powr ?b = ?x powr (?a * ?b)
0 < p

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

goal:
No subgoals!
[PROOF STEP]
qed