[STATEMENT]
theorem Lp_Lq_duality':
  fixes p q::ennreal
  assumes "1/p + 1/q = 1"
          "sigma_finite_measure M"
      and [measurable]: "f \<in> borel_measurable M"
  shows "eNorm (\<LL> p M) f = (SUP g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal(\<integral>x. f x * g x \<partial>M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
proof (cases "eNorm (\<LL> p M) f \<noteq> \<infinity>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eNorm (\<LL> p M) f \<noteq> \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
 2. \<not> eNorm (\<LL> p M) f \<noteq> \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) f \<noteq> \<infinity>

goal (2 subgoals):
 1. eNorm (\<LL> p M) f \<noteq> \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
 2. \<not> eNorm (\<LL> p M) f \<noteq> \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> p M) f \<noteq> \<infinity>
[PROOF STEP]
have "f \<in> space\<^sub>N (\<LL> p M)"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) f \<noteq> \<infinity>

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
unfolding space\<^sub>N_def
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) f \<noteq> \<infinity>

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

goal (2 subgoals):
 1. eNorm (\<LL> p M) f \<noteq> \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
 2. \<not> eNorm (\<LL> p M) f \<noteq> \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
unfolding eNorm_Norm[OF \<open>f \<in> space\<^sub>N (\<LL> p M)\<close>] Lp_Lq_duality[OF \<open>f \<in> space\<^sub>N (\<LL> p M)\<close> \<open>1/p + 1/q = 1\<close> \<open>sigma_finite_measure M\<close>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x) = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
apply (rule SUP_real_ennreal[symmetric], auto, rule exI[of _ 0], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>a. LINT x|M. f x * a x) ` {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1})
[PROOF STEP]
by (rule Lp_Lq_duality[OF \<open>f \<in> space\<^sub>N (\<LL> p M)\<close> \<open>1/p + 1/q = 1\<close> \<open>sigma_finite_measure M\<close>])
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))

goal (1 subgoal):
 1. \<not> eNorm (\<LL> p M) f \<noteq> \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> eNorm (\<LL> p M) f \<noteq> \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> eNorm (\<LL> p M) f \<noteq> \<infinity>

goal (1 subgoal):
 1. \<not> eNorm (\<LL> p M) f \<noteq> \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
have B: "\<exists>g \<in> {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. (\<integral>x. f x * g x \<partial>M) \<ge> C" if "C < \<infinity>" for C::ennreal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
obtain Cr where "C = ennreal Cr" "Cr \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Cr. \<lbrakk>C = ennreal Cr; 0 \<le> Cr\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>C < \<infinity>\<close> ennreal_cases less_irrefl
[PROOF STATE]
proof (prove)
using this:
C < \<infinity>
\<lbrakk>\<And>r. \<lbrakk>0 \<le> r; ?x = ennreal r\<rbrakk> \<Longrightarrow> ?thesis; ?x = \<top> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<not> ?x < ?x

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

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
obtain A where A: "\<And>n::nat. A n \<in> sets M" "incseq A" "(\<Union>n. A n) = space M"
            "\<And>n. emeasure M (A n) \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A. \<lbrakk>\<And>n. A n \<in> sets M; incseq A; \<Union> (range A) = space M; \<And>n. emeasure M (A n) \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using sigma_finite_measure.sigma_finite_incseq[OF \<open>sigma_finite_measure M\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>A. \<lbrakk>range A \<subseteq> sets M; \<Union> (range A) = space M; \<And>i. emeasure M (A i) \<noteq> \<infinity>; incseq A\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>\<And>n. A n \<in> sets M; incseq A; \<Union> (range A) = space M; \<And>n. emeasure M (A n) \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis range_subsetD)
[PROOF STATE]
proof (state)
this:
A ?n \<in> sets M
incseq A
\<Union> (range A) = space M
emeasure M (A ?n) \<noteq> \<infinity>

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
define Y where "Y = (\<lambda>n. {x \<in> A n. \<bar>f x\<bar> \<le> n})"
[PROOF STATE]
proof (state)
this:
Y = (\<lambda>n. {x \<in> A n. \<bar>f x\<bar> \<le> real n})

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
have [measurable]: "\<And>n. Y n \<in> sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. Y n \<in> sets M
[PROOF STEP]
unfolding Y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. {x \<in> A n. \<bar>f x\<bar> \<le> real n} \<in> sets M
[PROOF STEP]
using \<open>\<And>n::nat. A n \<in> sets M\<close>
[PROOF STATE]
proof (prove)
using this:
A ?n \<in> sets M

goal (1 subgoal):
 1. \<And>n. {x \<in> A n. \<bar>f x\<bar> \<le> real n} \<in> sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y ?n \<in> sets M

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
have "incseq Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incseq Y
[PROOF STEP]
apply (rule incseq_SucI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. Y n \<subseteq> Y (Suc n)
[PROOF STEP]
unfolding Y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. {x \<in> A n. \<bar>f x\<bar> \<le> real n} \<subseteq> {x \<in> A (Suc n). \<bar>f x\<bar> \<le> real (Suc n)}
[PROOF STEP]
using incseq_SucD[OF \<open>incseq A\<close>]
[PROOF STATE]
proof (prove)
using this:
A ?i \<subseteq> A (Suc ?i)

goal (1 subgoal):
 1. \<And>n. {x \<in> A n. \<bar>f x\<bar> \<le> real n} \<subseteq> {x \<in> A (Suc n). \<bar>f x\<bar> \<le> real (Suc n)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
incseq Y

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
have *: "\<exists>N. \<forall>n \<ge> N. f x * indicator (Y n) x = f x" if "x \<in> space M" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. f x * indicat_real (Y n) x = f x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. f x * indicat_real (Y n) x = f x
[PROOF STEP]
obtain n0 where n0: "x \<in> A n0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n0. x \<in> A n0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>x \<in> space M\<close> \<open>(\<Union>n. A n) = space M\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> space M
\<Union> (range A) = space M

goal (1 subgoal):
 1. (\<And>n0. x \<in> A n0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> A n0

goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. f x * indicat_real (Y n) x = f x
[PROOF STEP]
obtain n1::nat where n1: "\<bar>f x\<bar> \<le> n1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n1. \<bar>f x\<bar> \<le> real n1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using real_arch_simple
[PROOF STATE]
proof (prove)
using this:
\<exists>n. ?x \<le> of_nat n

goal (1 subgoal):
 1. (\<And>n1. \<bar>f x\<bar> \<le> real n1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<bar>f x\<bar> \<le> real n1

goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. f x * indicat_real (Y n) x = f x
[PROOF STEP]
have "x \<in> Y (max n0 n1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Y (max n0 n1)
[PROOF STEP]
unfolding Y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {x \<in> A (max n0 n1). \<bar>f x\<bar> \<le> real (max n0 n1)}
[PROOF STEP]
using n1
[PROOF STATE]
proof (prove)
using this:
\<bar>f x\<bar> \<le> real n1

goal (1 subgoal):
 1. x \<in> {x \<in> A (max n0 n1). \<bar>f x\<bar> \<le> real (max n0 n1)}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>f x\<bar> \<le> real n1 \<Longrightarrow> x \<in> A (max n0 n1)
[PROOF STEP]
using n0 \<open>incseq A\<close> incseq_def max.cobounded1
[PROOF STATE]
proof (prove)
using this:
x \<in> A n0
incseq A
incseq ?X = (\<forall>m n. m \<le> n \<longrightarrow> ?X m \<le> ?X n)
?a \<le> max ?a ?b

goal (1 subgoal):
 1. \<bar>f x\<bar> \<le> real n1 \<Longrightarrow> x \<in> A (max n0 n1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> Y (max n0 n1)

goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. f x * indicat_real (Y n) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> Y (max n0 n1)
[PROOF STEP]
have *: "x \<in> Y n" if "n \<ge> max n0 n1" for n
[PROOF STATE]
proof (prove)
using this:
x \<in> Y (max n0 n1)

goal (1 subgoal):
 1. x \<in> Y n
[PROOF STEP]
using \<open>incseq Y\<close> that incseq_def
[PROOF STATE]
proof (prove)
using this:
x \<in> Y (max n0 n1)
incseq Y
max n0 n1 \<le> n
incseq ?X = (\<forall>m n. m \<le> n \<longrightarrow> ?X m \<le> ?X n)

goal (1 subgoal):
 1. x \<in> Y n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
max n0 n1 \<le> ?n \<Longrightarrow> x \<in> Y ?n

goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. f x * indicat_real (Y n) x = f x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. f x * indicat_real (Y n) x = f x
[PROOF STEP]
by (rule exI[of _ "max n0 n1"], auto simp add: *)
[PROOF STATE]
proof (state)
this:
\<exists>N. \<forall>n\<ge>N. f x * indicat_real (Y n) x = f x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> space M \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. f ?x * indicat_real (Y n) ?x = f ?x

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
have *: "(\<lambda>n. f x * indicator (Y n) x) \<longlonglongrightarrow> f x" if "x \<in> space M" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f x * indicat_real (Y n) x) \<longlonglongrightarrow> f x
[PROOF STEP]
using *[OF that]
[PROOF STATE]
proof (prove)
using this:
\<exists>N. \<forall>n\<ge>N. f x * indicat_real (Y n) x = f x

goal (1 subgoal):
 1. (\<lambda>n. f x * indicat_real (Y n) x) \<longlonglongrightarrow> f x
[PROOF STEP]
unfolding eventually_sequentially[symmetric]
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. f x * indicat_real (Y n) x = f x

goal (1 subgoal):
 1. (\<lambda>n. f x * indicat_real (Y n) x) \<longlonglongrightarrow> f x
[PROOF STEP]
by (simp add: tendsto_eventually)
[PROOF STATE]
proof (state)
this:
?x \<in> space M \<Longrightarrow> (\<lambda>n. f ?x * indicat_real (Y n) ?x) \<longlonglongrightarrow> f ?x

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
have "liminf (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicator (Y n) x)) \<ge> eNorm (\<LL> p M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> p M) f \<le> liminf (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))
[PROOF STEP]
apply (rule Lp_AE_limit)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. f \<in> borel_measurable M
 2. AE x in M. (\<lambda>n. f x * indicat_real (Y n) x) \<longlonglongrightarrow> f x
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
?x \<in> space M \<Longrightarrow> (\<lambda>n. f ?x * indicat_real (Y n) ?x) \<longlonglongrightarrow> f ?x

goal (2 subgoals):
 1. f \<in> borel_measurable M
 2. AE x in M. (\<lambda>n. f x * indicat_real (Y n) x) \<longlonglongrightarrow> f x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) f \<le> liminf (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> p M) f \<le> liminf (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))
[PROOF STEP]
have "liminf (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicator (Y n) x)) > Cr"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) f \<le> liminf (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))

goal (1 subgoal):
 1. ennreal Cr < liminf (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))
[PROOF STEP]
using False neq_top_trans
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) f \<le> liminf (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))
\<not> eNorm (\<LL> p M) f \<noteq> \<infinity>
\<lbrakk>?y \<noteq> \<top>; ?x \<le> ?y\<rbrakk> \<Longrightarrow> ?x \<noteq> \<top>

goal (1 subgoal):
 1. ennreal Cr < liminf (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ennreal Cr < liminf (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ennreal Cr < liminf (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))
[PROOF STEP]
have "limsup (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicator (Y n) x)) > Cr"
[PROOF STATE]
proof (prove)
using this:
ennreal Cr < liminf (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))

goal (1 subgoal):
 1. ennreal Cr < limsup (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))
[PROOF STEP]
using Liminf_le_Limsup less_le_trans trivial_limit_sequentially
[PROOF STATE]
proof (prove)
using this:
ennreal Cr < liminf (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))
?F \<noteq> \<bottom> \<Longrightarrow> Liminf ?F ?f \<le> Limsup ?F ?f
\<lbrakk>?x < ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x < ?z
sequentially \<noteq> \<bottom>

goal (1 subgoal):
 1. ennreal Cr < limsup (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ennreal Cr < limsup (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ennreal Cr < limsup (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))
[PROOF STEP]
obtain n where n: "eNorm (\<LL> p M) (\<lambda>x. f x * indicator (Y n) x) > Cr"
[PROOF STATE]
proof (prove)
using this:
ennreal Cr < limsup (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))

goal (1 subgoal):
 1. (\<And>n. ennreal Cr < eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Limsup_obtain
[PROOF STATE]
proof (prove)
using this:
ennreal Cr < limsup (\<lambda>n. eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))
?c < Limsup ?F ?u \<Longrightarrow> \<exists>i. ?c < ?u i

goal (1 subgoal):
 1. (\<And>n. ennreal Cr < eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ennreal Cr < eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x)

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
have "(\<lambda>x. f x * indicator (Y n) x) \<in> space\<^sub>N (\<LL> p M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x * indicat_real (Y n) x) \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
apply (rule Lp_bounded_bounded_support[of _ _ n], auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. AE x in M. \<bar>f x * indicat_real (Y n) x\<bar> \<le> real n
 2. emeasure M {x \<in> space M. f x \<noteq> 0 \<and> indicat_real (Y n) x \<noteq> 0} = \<top> \<Longrightarrow> False
[PROOF STEP]
unfolding Y_def indicator_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. AE x in M. \<bar>f x * of_bool (x \<in> {x \<in> A n. \<bar>f x\<bar> \<le> real n})\<bar> \<le> real n
 2. emeasure M {x \<in> space M. f x \<noteq> 0 \<and> of_bool (x \<in> {x \<in> A n. \<bar>f x\<bar> \<le> real n}) \<noteq> 0} = \<top> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure M {x \<in> space M. f x \<noteq> 0 \<and> x \<in> A n \<and> \<bar>f x\<bar> \<le> real n} = \<top> \<Longrightarrow> False
[PROOF STEP]
by (metis (mono_tags, lifting) A(1) A(4) emeasure_mono infinity_ennreal_def mem_Collect_eq neq_top_trans subsetI)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * indicat_real (Y n) x) \<in> space\<^sub>N (\<LL> p M)

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
have "Norm (\<LL> p M) (\<lambda>x. f x * indicator (Y n) x) > Cr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cr < Norm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x)
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
ennreal Cr < eNorm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x)

goal (1 subgoal):
 1. Cr < Norm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x)
[PROOF STEP]
unfolding eNorm_Norm[OF \<open>(\<lambda>x. f x * indicator (Y n) x) \<in> space\<^sub>N (\<LL> p M)\<close>]
[PROOF STATE]
proof (prove)
using this:
ennreal Cr < ennreal (Norm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x))

goal (1 subgoal):
 1. Cr < Norm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x)
[PROOF STEP]
by (meson ennreal_leI not_le)
[PROOF STATE]
proof (state)
this:
Cr < Norm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x)

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cr < Norm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x)
[PROOF STEP]
have "(SUP g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. (\<integral>x. f x * indicator (Y n) x * g x \<partial>M)) > Cr"
[PROOF STATE]
proof (prove)
using this:
Cr < Norm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x)

goal (1 subgoal):
 1. Cr < (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * indicat_real (Y n) x * g x)
[PROOF STEP]
using Lp_Lq_duality(2)[OF \<open>(\<lambda>x. f x * indicator (Y n) x) \<in> space\<^sub>N (\<LL> p M)\<close> \<open>1/p + 1/q = 1\<close> \<open>sigma_finite_measure M\<close>]
[PROOF STATE]
proof (prove)
using this:
Cr < Norm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x)
Norm (\<LL> p M) (\<lambda>x. f x * indicat_real (Y n) x) = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * indicat_real (Y n) x * g x)

goal (1 subgoal):
 1. Cr < (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * indicat_real (Y n) x * g x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Cr < (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * indicat_real (Y n) x * g x)

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cr < (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * indicat_real (Y n) x * g x)
[PROOF STEP]
have "\<exists>g \<in> {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. (\<integral>x. f x * indicator (Y n) x * g x \<partial>M) > Cr"
[PROOF STATE]
proof (prove)
using this:
Cr < (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * indicat_real (Y n) x * g x)

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. Cr < LINT x|M. f x * indicat_real (Y n) x * g x
[PROOF STEP]
apply (subst less_cSUP_iff[symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Cr < (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * indicat_real (Y n) x * g x) \<Longrightarrow> {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1} \<noteq> {}
 2. Cr < (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * indicat_real (Y n) x * g x) \<Longrightarrow> bdd_above ((\<lambda>g. LINT x|M. f x * indicat_real (Y n) x * g x) ` {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1})
 3. Cr < (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * indicat_real (Y n) x * g x) \<Longrightarrow> Cr < (\<Squnion>i\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * indicat_real (Y n) x * i x)
[PROOF STEP]
using Lp_Lq_duality(1)[OF \<open>(\<lambda>x. f x * indicator (Y n) x) \<in> space\<^sub>N (\<LL> p M)\<close> \<open>1/p + 1/q = 1\<close> \<open>sigma_finite_measure M\<close>]
[PROOF STATE]
proof (prove)
using this:
bdd_above ((\<lambda>g. LINT x|M. f x * indicat_real (Y n) x * g x) ` {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1})

goal (3 subgoals):
 1. Cr < (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * indicat_real (Y n) x * g x) \<Longrightarrow> {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1} \<noteq> {}
 2. Cr < (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * indicat_real (Y n) x * g x) \<Longrightarrow> bdd_above ((\<lambda>g. LINT x|M. f x * indicat_real (Y n) x * g x) ` {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1})
 3. Cr < (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * indicat_real (Y n) x * g x) \<Longrightarrow> Cr < (\<Squnion>i\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * indicat_real (Y n) x * i x)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Cr < (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * indicat_real (Y n) x * g x); bdd_above ((\<lambda>g. LINT x|M. f x * indicat_real (Y n) x * g x) ` {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1})\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> space\<^sub>N (\<LL> q M) \<and> Norm (\<LL> q M) x \<le> 1
[PROOF STEP]
by (rule exI[of _ 0], auto)
[PROOF STATE]
proof (state)
this:
\<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. Cr < LINT x|M. f x * indicat_real (Y n) x * g x

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. Cr < LINT x|M. f x * indicat_real (Y n) x * g x
[PROOF STEP]
obtain g where g: "g \<in> space\<^sub>N (\<LL> q M)" "Norm (\<LL> q M) g \<le> 1" "(\<integral>x. f x * indicator (Y n) x * g x \<partial>M) > Cr"
[PROOF STATE]
proof (prove)
using this:
\<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. Cr < LINT x|M. f x * indicat_real (Y n) x * g x

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> space\<^sub>N (\<LL> q M); Norm (\<LL> q M) g \<le> 1; Cr < LINT x|M. f x * indicat_real (Y n) x * g x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> space\<^sub>N (\<LL> q M)
Norm (\<LL> q M) g \<le> 1
Cr < LINT x|M. f x * indicat_real (Y n) x * g x

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g \<in> space\<^sub>N (\<LL> q M)
Norm (\<LL> q M) g \<le> 1
Cr < LINT x|M. f x * indicat_real (Y n) x * g x
[PROOF STEP]
have [measurable]: "g \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
using this:
g \<in> space\<^sub>N (\<LL> q M)
Norm (\<LL> q M) g \<le> 1
Cr < LINT x|M. f x * indicat_real (Y n) x * g x

goal (1 subgoal):
 1. g \<in> borel_measurable M
[PROOF STEP]
using Lp_measurable
[PROOF STATE]
proof (prove)
using this:
g \<in> space\<^sub>N (\<LL> q M)
Norm (\<LL> q M) g \<le> 1
Cr < LINT x|M. f x * indicat_real (Y n) x * g x
?f \<in> space\<^sub>N (\<LL> ?p ?M) \<Longrightarrow> ?f \<in> borel_measurable ?M

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

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
define h where "h = (\<lambda>x. indicator (Y n) x * g x)"
[PROOF STATE]
proof (state)
this:
h = (\<lambda>x. indicat_real (Y n) x * g x)

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
have "Norm (\<LL> q M) h \<le> Norm (\<LL> q M) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> q M) h \<le> Norm (\<LL> q M) g
[PROOF STEP]
apply (rule Lp_domination[of _ _ g])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. h \<in> borel_measurable M
 2. g \<in> space\<^sub>N (\<LL> q M)
 3. AE x in M. \<bar>h x\<bar> \<le> \<bar>g x\<bar>
[PROOF STEP]
unfolding h_def indicator_def
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>x. of_bool (x \<in> Y n) * g x) \<in> borel_measurable M
 2. g \<in> space\<^sub>N (\<LL> q M)
 3. AE x in M. \<bar>of_bool (x \<in> Y n) * g x\<bar> \<le> \<bar>g x\<bar>
[PROOF STEP]
using \<open>g \<in> space\<^sub>N (\<LL> q M)\<close>
[PROOF STATE]
proof (prove)
using this:
g \<in> space\<^sub>N (\<LL> q M)

goal (3 subgoals):
 1. (\<lambda>x. of_bool (x \<in> Y n) * g x) \<in> borel_measurable M
 2. g \<in> space\<^sub>N (\<LL> q M)
 3. AE x in M. \<bar>of_bool (x \<in> Y n) * g x\<bar> \<le> \<bar>g x\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Norm (\<LL> q M) h \<le> Norm (\<LL> q M) g

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Norm (\<LL> q M) h \<le> Norm (\<LL> q M) g
[PROOF STEP]
have a: "Norm (\<LL> q M) h \<le> 1"
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> q M) h \<le> Norm (\<LL> q M) g

goal (1 subgoal):
 1. Norm (\<LL> q M) h \<le> 1
[PROOF STEP]
using \<open>Norm (\<LL> q M) g \<le> 1\<close>
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> q M) h \<le> Norm (\<LL> q M) g
Norm (\<LL> q M) g \<le> 1

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

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
have b: "h \<in> space\<^sub>N (\<LL> q M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<in> space\<^sub>N (\<LL> q M)
[PROOF STEP]
apply (rule Lp_domination[of _ _ g])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. h \<in> borel_measurable M
 2. g \<in> space\<^sub>N (\<LL> q M)
 3. AE x in M. \<bar>h x\<bar> \<le> \<bar>g x\<bar>
[PROOF STEP]
unfolding h_def indicator_def
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>x. of_bool (x \<in> Y n) * g x) \<in> borel_measurable M
 2. g \<in> space\<^sub>N (\<LL> q M)
 3. AE x in M. \<bar>of_bool (x \<in> Y n) * g x\<bar> \<le> \<bar>g x\<bar>
[PROOF STEP]
using \<open>g \<in> space\<^sub>N (\<LL> q M)\<close>
[PROOF STATE]
proof (prove)
using this:
g \<in> space\<^sub>N (\<LL> q M)

goal (3 subgoals):
 1. (\<lambda>x. of_bool (x \<in> Y n) * g x) \<in> borel_measurable M
 2. g \<in> space\<^sub>N (\<LL> q M)
 3. AE x in M. \<bar>of_bool (x \<in> Y n) * g x\<bar> \<le> \<bar>g x\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h \<in> space\<^sub>N (\<LL> q M)

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
have "(\<integral>x. f x * h x \<partial>M) > Cr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cr < LINT x|M. f x * h x
[PROOF STEP]
unfolding h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cr < LINT x|M. f x * (indicat_real (Y n) x * g x)
[PROOF STEP]
using g(3)
[PROOF STATE]
proof (prove)
using this:
Cr < LINT x|M. f x * indicat_real (Y n) x * g x

goal (1 subgoal):
 1. Cr < LINT x|M. f x * (indicat_real (Y n) x * g x)
[PROOF STEP]
by (auto simp add: mult.assoc)
[PROOF STATE]
proof (state)
this:
Cr < LINT x|M. f x * h x

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cr < LINT x|M. f x * h x
[PROOF STEP]
have "(\<integral>x. f x * h x \<partial>M) > C"
[PROOF STATE]
proof (prove)
using this:
Cr < LINT x|M. f x * h x

goal (1 subgoal):
 1. C < ennreal (LINT x|M. f x * h x)
[PROOF STEP]
unfolding \<open>C = ennreal Cr\<close>
[PROOF STATE]
proof (prove)
using this:
Cr < LINT x|M. f x * h x

goal (1 subgoal):
 1. ennreal Cr < ennreal (LINT x|M. f x * h x)
[PROOF STEP]
using \<open>Cr \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
Cr < LINT x|M. f x * h x
0 \<le> Cr

goal (1 subgoal):
 1. ennreal Cr < ennreal (LINT x|M. f x * h x)
[PROOF STEP]
by (simp add: ennreal_less_iff)
[PROOF STATE]
proof (state)
this:
C < ennreal (LINT x|M. f x * h x)

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C < ennreal (LINT x|M. f x * h x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C < ennreal (LINT x|M. f x * h x)

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
C < ennreal (LINT x|M. f x * h x)
Norm (\<LL> q M) h \<le> 1
h \<in> space\<^sub>N (\<LL> q M)

goal (1 subgoal):
 1. \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. C \<le> ennreal (LINT x|M. f x * g x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?C < \<infinity> \<Longrightarrow> \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ?C \<le> ennreal (LINT x|M. f x * g x)

goal (1 subgoal):
 1. \<not> eNorm (\<LL> p M) f \<noteq> \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
have "(SUP g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal(\<integral>x. f x * g x \<partial>M)) \<ge> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<infinity> \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
apply (rule dense_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x < \<infinity> \<Longrightarrow> x \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
?C < \<infinity> \<Longrightarrow> \<exists>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ?C \<le> ennreal (LINT x|M. f x * g x)

goal (1 subgoal):
 1. \<And>x. x < \<infinity> \<Longrightarrow> x \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
by (meson SUP_upper2)
[PROOF STATE]
proof (state)
this:
\<infinity> \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))

goal (1 subgoal):
 1. \<not> eNorm (\<LL> p M) f \<noteq> \<infinity> \<Longrightarrow> eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<infinity> \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<infinity> \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))

goal (1 subgoal):
 1. eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
using False neq_top_trans
[PROOF STATE]
proof (prove)
using this:
\<infinity> \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
\<not> eNorm (\<LL> p M) f \<noteq> \<infinity>
\<lbrakk>?y \<noteq> \<top>; ?x \<le> ?y\<rbrakk> \<Longrightarrow> ?x \<noteq> \<top>

goal (1 subgoal):
 1. eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. ennreal (LINT x|M. f x * g x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Lp_subalgebra:
  assumes "subalgebra M F"
  shows "\<And>f. eNorm (\<LL> p M) f \<le> eNorm (\<LL> p (restr_to_subalg M F)) f"
        "(\<LL> p (restr_to_subalg M F)) \<subseteq>\<^sub>N \<LL> p M"
        "space\<^sub>N ((\<LL> p (restr_to_subalg M F))) \<subseteq> space\<^sub>N (\<LL> p M)"
        "\<And>f. f \<in> space\<^sub>N ((\<LL> p (restr_to_subalg M F))) \<Longrightarrow> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>f. eNorm (\<LL> p M) f \<le> eNorm (\<LL> p (restr_to_subalg M F)) f) &&& \<LL> p (restr_to_subalg M F) \<subseteq>\<^sub>N \<LL> p M) &&& space\<^sub>N (\<LL> p (restr_to_subalg M F)) \<subseteq> space\<^sub>N (\<LL> p M) &&& (\<And>f. f \<in> space\<^sub>N (\<LL> p (restr_to_subalg M F)) \<Longrightarrow> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>f. eNorm (\<LL> p M) f \<le> eNorm (\<LL> p (restr_to_subalg M F)) f
 2. \<LL> p (restr_to_subalg M F) \<subseteq>\<^sub>N \<LL> p M
 3. space\<^sub>N (\<LL> p (restr_to_subalg M F)) \<subseteq> space\<^sub>N (\<LL> p M)
 4. \<And>f. f \<in> space\<^sub>N (\<LL> p (restr_to_subalg M F)) \<Longrightarrow> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
have *: "f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f"
       if "f \<in> space\<^sub>N (\<LL> p (restr_to_subalg M F))" for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
have [measurable]: "f \<in> borel_measurable (restr_to_subalg M F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> borel_measurable (restr_to_subalg M F)
[PROOF STEP]
using that Lp_measurable
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> p (restr_to_subalg M F))
?f \<in> space\<^sub>N (\<LL> ?p ?M) \<Longrightarrow> ?f \<in> borel_measurable ?M

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

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> borel_measurable (restr_to_subalg M F)
[PROOF STEP]
have [measurable]: "f \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable (restr_to_subalg M F)

goal (1 subgoal):
 1. f \<in> borel_measurable M
[PROOF STEP]
using assms measurable_from_subalg measurable_in_subalg'
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable (restr_to_subalg M F)
subalgebra M F
\<lbrakk>subalgebra ?M ?F; ?f \<in> ?F \<rightarrow>\<^sub>M ?N\<rbrakk> \<Longrightarrow> ?f \<in> ?M \<rightarrow>\<^sub>M ?N
\<lbrakk>subalgebra ?M ?F; ?f \<in> restr_to_subalg ?M ?F \<rightarrow>\<^sub>M ?N\<rbrakk> \<Longrightarrow> ?f \<in> ?F \<rightarrow>\<^sub>M ?N

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

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
proof (cases rule: Lp_cases[of p])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
 2. p = 0 \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
 3. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
case zero
[PROOF STATE]
proof (state)
this:
p = 0

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

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
p = 0
f \<in> space\<^sub>N (\<LL> p (restr_to_subalg M F))

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
unfolding \<open>p = 0\<close> L_zero_space Norm_def L_zero
[PROOF STATE]
proof (prove)
using this:
0 = 0
f \<in> borel_measurable (restr_to_subalg M F)

goal (1 subgoal):
 1. f \<in> borel_measurable M \<and> enn2real (if f \<in> borel_measurable M then 0 else \<infinity>) = enn2real (if f \<in> borel_measurable (restr_to_subalg M F) then 0 else \<infinity>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
 2. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
 2. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
case PInf
[PROOF STATE]
proof (state)
this:
p = \<infinity>

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
 2. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
have [measurable]: "f \<in> borel_measurable (restr_to_subalg M F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> borel_measurable (restr_to_subalg M F)
[PROOF STEP]
using that Lp_measurable
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> p (restr_to_subalg M F))
?f \<in> space\<^sub>N (\<LL> ?p ?M) \<Longrightarrow> ?f \<in> borel_measurable ?M

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

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
 2. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> borel_measurable (restr_to_subalg M F)
[PROOF STEP]
have [measurable]: "f \<in> borel_measurable F"
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable (restr_to_subalg M F)

goal (1 subgoal):
 1. f \<in> borel_measurable F
[PROOF STEP]
using assms measurable_in_subalg'
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable (restr_to_subalg M F)
subalgebra M F
\<lbrakk>subalgebra ?M ?F; ?f \<in> restr_to_subalg ?M ?F \<rightarrow>\<^sub>M ?N\<rbrakk> \<Longrightarrow> ?f \<in> ?F \<rightarrow>\<^sub>M ?N

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

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
 2. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> borel_measurable F
[PROOF STEP]
have [measurable]: "f \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable F

goal (1 subgoal):
 1. f \<in> borel_measurable M
[PROOF STEP]
using assms measurable_from_subalg
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable F
subalgebra M F
\<lbrakk>subalgebra ?M ?F; ?f \<in> ?F \<rightarrow>\<^sub>M ?N\<rbrakk> \<Longrightarrow> ?f \<in> ?M \<rightarrow>\<^sub>M ?N

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

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
 2. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
have "AE x in (restr_to_subalg M F). \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in restr_to_subalg M F. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f
[PROOF STEP]
using L_infinity_AE_bound that
[PROOF STATE]
proof (prove)
using this:
?f \<in> space\<^sub>N (\<LL> \<infinity> ?M) \<Longrightarrow> AE x in ?M. \<bar>?f x\<bar> \<le> Norm (\<LL> \<infinity> ?M) ?f
f \<in> space\<^sub>N (\<LL> p (restr_to_subalg M F))

goal (1 subgoal):
 1. AE x in restr_to_subalg M F. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f
[PROOF STEP]
unfolding \<open>p = \<infinity>\<close>
[PROOF STATE]
proof (prove)
using this:
?f \<in> space\<^sub>N (\<LL> \<infinity> ?M) \<Longrightarrow> AE x in ?M. \<bar>?f x\<bar> \<le> Norm (\<LL> \<infinity> ?M) ?f
f \<in> space\<^sub>N (\<LL> \<infinity> (restr_to_subalg M F))

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

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
 2. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in restr_to_subalg M F. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f
[PROOF STEP]
have a: "AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f"
[PROOF STATE]
proof (prove)
using this:
AE x in restr_to_subalg M F. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f

goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f
[PROOF STEP]
using assms AE_restr_to_subalg
[PROOF STATE]
proof (prove)
using this:
AE x in restr_to_subalg M F. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f
subalgebra M F
\<lbrakk>subalgebra ?M ?F; almost_everywhere (restr_to_subalg ?M ?F) ?P\<rbrakk> \<Longrightarrow> almost_everywhere ?M ?P

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

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
 2. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
have *: "f \<in> space\<^sub>N (\<LL> \<infinity> M)" "Norm (\<LL> \<infinity> M) f \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> \<infinity> M) &&& Norm (\<LL> \<infinity> M) f \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f
[PROOF STEP]
using L_infinity_I[OF \<open>f \<in> borel_measurable M\<close> a]
[PROOF STATE]
proof (prove)
using this:
0 \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f \<Longrightarrow> f \<in> space\<^sub>N (\<LL> \<infinity> M)
0 \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f \<Longrightarrow> Norm (\<LL> \<infinity> M) f \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f

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

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
 2. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> space\<^sub>N (\<LL> \<infinity> M)
Norm (\<LL> \<infinity> M) f \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f
[PROOF STEP]
have b: "AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f"
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> \<infinity> M)
Norm (\<LL> \<infinity> M) f \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f

goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f
[PROOF STEP]
using L_infinity_AE_bound
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> \<infinity> M)
Norm (\<LL> \<infinity> M) f \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f
?f \<in> space\<^sub>N (\<LL> \<infinity> ?M) \<Longrightarrow> AE x in ?M. \<bar>?f x\<bar> \<le> Norm (\<LL> \<infinity> ?M) ?f

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

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
 2. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
have c: "AE x in (restr_to_subalg M F). \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in restr_to_subalg M F. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f
[PROOF STEP]
apply (rule AE_restr_to_subalg2[OF assms])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f
 2. Measurable.pred F (\<lambda>x. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f)
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f

goal (2 subgoals):
 1. AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f
 2. Measurable.pred F (\<lambda>x. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in restr_to_subalg M F. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
 2. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
have "Norm (\<LL> \<infinity> (restr_to_subalg M F)) f \<le> Norm (\<LL> \<infinity> M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> \<infinity> (restr_to_subalg M F)) f \<le> Norm (\<LL> \<infinity> M) f
[PROOF STEP]
using L_infinity_I[OF \<open>f \<in> borel_measurable (restr_to_subalg M F)\<close> c]
[PROOF STATE]
proof (prove)
using this:
0 \<le> Norm (\<LL> \<infinity> M) f \<Longrightarrow> f \<in> space\<^sub>N (\<LL> \<infinity> (restr_to_subalg M F))
0 \<le> Norm (\<LL> \<infinity> M) f \<Longrightarrow> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f \<le> Norm (\<LL> \<infinity> M) f

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

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

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> \<infinity> (restr_to_subalg M F)) f \<le> Norm (\<LL> \<infinity> M) f
f \<in> space\<^sub>N (\<LL> \<infinity> M)
Norm (\<LL> \<infinity> M) f \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
unfolding \<open>p = \<infinity>\<close>
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> \<infinity> (restr_to_subalg M F)) f \<le> Norm (\<LL> \<infinity> M) f
f \<in> space\<^sub>N (\<LL> \<infinity> M)
Norm (\<LL> \<infinity> M) f \<le> Norm (\<LL> \<infinity> (restr_to_subalg M F)) f

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

goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
case (real_pos p2)
[PROOF STATE]
proof (state)
this:
p = ennreal p2
0 < p2
0 < p

goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = ennreal p2
0 < p2
0 < p
[PROOF STEP]
have a [measurable]: "f \<in> space\<^sub>N (\<LL> p2 (restr_to_subalg M F))"
[PROOF STATE]
proof (prove)
using this:
p = ennreal p2
0 < p2
0 < p

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> (ennreal p2) (restr_to_subalg M F))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
p = ennreal p2
0 < p2
0 < p
f \<in> space\<^sub>N (\<LL> p (restr_to_subalg M F))

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> (ennreal p2) (restr_to_subalg M F))
[PROOF STEP]
unfolding \<open>p = ennreal p2\<close>
[PROOF STATE]
proof (prove)
using this:
ennreal p2 = ennreal p2
0 < p2
0 < ennreal p2
f \<in> space\<^sub>N (\<LL> (ennreal p2) (restr_to_subalg M F))

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

goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> space\<^sub>N (\<LL> (ennreal p2) (restr_to_subalg M F))
[PROOF STEP]
have b [measurable]: "f \<in> space\<^sub>N (\<LL> p2 M)"
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> (ennreal p2) (restr_to_subalg M F))

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

goal (1 subgoal):
 1. f \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)}
[PROOF STEP]
using integrable_from_subalg[OF assms]
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> borel_measurable (restr_to_subalg M F). integrable (restr_to_subalg M F) (\<lambda>x. \<bar>f x\<bar> powr p2)}
integrable (restr_to_subalg M F) ?f \<Longrightarrow> integrable M ?f

goal (1 subgoal):
 1. f \<in> {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> space\<^sub>N (\<LL> (ennreal p2) M)

goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
unfolding \<open>p = ennreal p2\<close> Lp_D[OF \<open>p2 > 0\<close> a] Lp_D[OF \<open>p2 > 0\<close> b]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> (ennreal p2) M) \<and> (LINT x|M. \<bar>f x\<bar> powr p2) powr (1 / p2) = (LINT x|restr_to_subalg M F. \<bar>f x\<bar> powr p2) powr (1 / p2)
[PROOF STEP]
using integral_subalgebra2[OF assms, symmetric, of f]
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable F \<Longrightarrow> integral\<^sup>L M f = integral\<^sup>L (restr_to_subalg M F) f

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> (ennreal p2) M) \<and> (LINT x|M. \<bar>f x\<bar> powr p2) powr (1 / p2) = (LINT x|restr_to_subalg M F. \<bar>f x\<bar> powr p2) powr (1 / p2)
[PROOF STEP]
apply (auto simp add: b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<in> borel_measurable F \<Longrightarrow> integral\<^sup>L M f = integral\<^sup>L (restr_to_subalg M F) f) \<Longrightarrow> (LINT x|M. \<bar>f x\<bar> powr p2) powr (1 / p2) = (LINT x|restr_to_subalg M F. \<bar>f x\<bar> powr p2) powr (1 / p2)
[PROOF STEP]
by (metis (mono_tags, lifting) \<open>integrable (restr_to_subalg M F) (\<lambda>x. \<bar>f x\<bar> powr p2)\<close> assms integrableD(1) integral_subalgebra2 measurable_in_subalg')
[PROOF STATE]
proof (state)
this:
f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f

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

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

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

goal (3 subgoals):
 1. \<And>f. eNorm (\<LL> p M) f \<le> eNorm (\<LL> p (restr_to_subalg M F)) f
 2. \<LL> p (restr_to_subalg M F) \<subseteq>\<^sub>N \<LL> p M
 3. \<And>f. f \<in> space\<^sub>N (\<LL> p (restr_to_subalg M F)) \<Longrightarrow> Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
show "Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f" if "f \<in> space\<^sub>N ((\<LL> p (restr_to_subalg M F)))" for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> p M) f = Norm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
using * that
[PROOF STATE]
proof (prove)
using this:
?f \<in> space\<^sub>N (\<LL> p (restr_to_subalg M F)) \<Longrightarrow> ?f \<in> space\<^sub>N (\<LL> p M) \<and> Norm (\<LL> p M) ?f = Norm (\<LL> p (restr_to_subalg M F)) ?f
f \<in> space\<^sub>N (\<LL> p (restr_to_subalg M F))

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

goal (2 subgoals):
 1. \<And>f. eNorm (\<LL> p M) f \<le> eNorm (\<LL> p (restr_to_subalg M F)) f
 2. \<LL> p (restr_to_subalg M F) \<subseteq>\<^sub>N \<LL> p M
[PROOF STEP]
show "eNorm (\<LL> p M) f \<le> eNorm (\<LL> p (restr_to_subalg M F)) f" for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> p M) f \<le> eNorm (\<LL> p (restr_to_subalg M F)) f
[PROOF STEP]
by (metis "*" eNorm_Norm eq_iff infinity_ennreal_def less_imp_le spaceN_iff top.not_eq_extremum)
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) ?f \<le> eNorm (\<LL> p (restr_to_subalg M F)) ?f

goal (1 subgoal):
 1. \<LL> p (restr_to_subalg M F) \<subseteq>\<^sub>N \<LL> p M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> p M) ?f \<le> eNorm (\<LL> p (restr_to_subalg M F)) ?f
[PROOF STEP]
show "(\<LL> p (restr_to_subalg M F)) \<subseteq>\<^sub>N \<LL> p M"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) ?f \<le> eNorm (\<LL> p (restr_to_subalg M F)) ?f

goal (1 subgoal):
 1. \<LL> p (restr_to_subalg M F) \<subseteq>\<^sub>N \<LL> p M
[PROOF STEP]
by (metis ennreal_1 mult.left_neutral quasinorm_subsetI)
[PROOF STATE]
proof (state)
this:
\<LL> p (restr_to_subalg M F) \<subseteq>\<^sub>N \<LL> p M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Lp_real_cond_exp_eNorm:
  assumes [simp]: "subalgebra M F"
      and "p \<ge> (1::ennreal)"
          "sigma_finite_measure (restr_to_subalg M F)"
  shows "eNorm (\<LL> p (restr_to_subalg M F)) (real_cond_exp M F f) \<le> eNorm (\<LL> p M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> p (restr_to_subalg M F)) (real_cond_exp M F f) \<le> eNorm (\<LL> p M) f
[PROOF STEP]
proof (cases "eNorm (\<LL> p M) f = \<infinity>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eNorm (\<LL> p M) f = \<infinity> \<Longrightarrow> eNorm (\<LL> p (restr_to_subalg M F)) (real_cond_exp M F f) \<le> eNorm (\<LL> p M) f
 2. eNorm (\<LL> p M) f \<noteq> \<infinity> \<Longrightarrow> eNorm (\<LL> p (restr_to_subalg M F)) (real_cond_exp M F f) \<le> eNorm (\<LL> p M) f
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) f \<noteq> \<infinity>

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

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

goal (1 subgoal):
 1. eNorm (\<LL> p M) f < \<infinity>
[PROOF STEP]
by (simp add: top.not_eq_extremum)
[PROOF STATE]
proof (state)
this:
f \<in> space\<^sub>N (\<LL> p M)

goal (2 subgoals):
 1. eNorm (\<LL> p M) f = \<infinity> \<Longrightarrow> eNorm (\<LL> p (restr_to_subalg M F)) (real_cond_exp M F f) \<le> eNorm (\<LL> p M) f
 2. eNorm (\<LL> p M) f \<noteq> \<infinity> \<Longrightarrow> eNorm (\<LL> p (restr_to_subalg M F)) (real_cond_exp M F f) \<le> eNorm (\<LL> p M) f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> p (restr_to_subalg M F)) (real_cond_exp M F f) \<le> eNorm (\<LL> p M) f
[PROOF STEP]
using Lp_real_cond_exp[OF assms \<open>f \<in> space\<^sub>N (\<LL> p M)\<close>]
[PROOF STATE]
proof (prove)
using this:
real_cond_exp M F f \<in> space\<^sub>N (\<LL> p (restr_to_subalg M F))
Norm (\<LL> p (restr_to_subalg M F)) (real_cond_exp M F f) \<le> Norm (\<LL> p M) f

goal (1 subgoal):
 1. eNorm (\<LL> p (restr_to_subalg M F)) (real_cond_exp M F f) \<le> eNorm (\<LL> p M) f
[PROOF STEP]
by (subst eNorm_Norm, auto simp: \<open>f \<in> space\<^sub>N (\<LL> p M)\<close>)+
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p (restr_to_subalg M F)) (real_cond_exp M F f) \<le> eNorm (\<LL> p M) f

goal (1 subgoal):
 1. eNorm (\<LL> p M) f = \<infinity> \<Longrightarrow> eNorm (\<LL> p (restr_to_subalg M F)) (real_cond_exp M F f) \<le> eNorm (\<LL> p M) f
[PROOF STEP]
qed (simp)


[STATEMENT]
lemma tainting_imp_blp_cutcard: "\<forall>ts v. nP v = ts \<longrightarrow> finite ts \<Longrightarrow>
  SINVAR_Tainting.sinvar G nP \<Longrightarrow> SINVAR_BLPbasic.sinvar G ((\<lambda>ts. card (ts \<inter> X)) \<circ> nP)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ts v. nP v = ts \<longrightarrow> finite ts; SINVAR_Tainting.sinvar G nP\<rbrakk> \<Longrightarrow> SINVAR_BLPbasic.sinvar G ((\<lambda>ts. card (ts \<inter> X)) \<circ> nP)
[PROOF STEP]
apply(simp add: SINVAR_Tainting.sinvar_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; \<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2\<rbrakk> \<Longrightarrow> \<forall>x\<in>edges G. case x of (e1, e2) \<Rightarrow> card (nP e1 \<inter> X) \<le> card (nP e2 \<inter> X)
[PROOF STEP]
apply(clarify, rename_tac a b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; \<forall>(v1, v2)\<in>edges G. nP v1 \<subseteq> nP v2; (a, b) \<in> edges G\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
[PROOF STEP]
apply(erule_tac x="(a,b)" in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a, b) \<in> edges G; case (a, b) of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
 2. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a, b) \<in> edges G; (a, b) \<notin> edges G\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a, b) \<in> edges G; nP a \<subseteq> nP b\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
[PROOF STEP]
apply(subgoal_tac "finite (nP a \<inter> X)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X)\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
 2. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a, b) \<in> edges G; nP a \<subseteq> nP b\<rbrakk> \<Longrightarrow> finite (nP a \<inter> X)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a, b) \<in> edges G; nP a \<subseteq> nP b\<rbrakk> \<Longrightarrow> finite (nP a \<inter> X)
 2. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X)\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a_, b_) \<in> edges G; nP a_ \<subseteq> nP b_\<rbrakk> \<Longrightarrow> finite (nP a_ \<inter> X)
[PROOF STEP]
using finite_Int
[PROOF STATE]
proof (prove)
using this:
finite ?F \<or> finite ?G \<Longrightarrow> finite (?F \<inter> ?G)

goal (1 subgoal):
 1. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a_, b_) \<in> edges G; nP a_ \<subseteq> nP b_\<rbrakk> \<Longrightarrow> finite (nP a_ \<inter> X)
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X)\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
[PROOF STEP]
apply(subgoal_tac "finite (nP b \<inter> X)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X); finite (nP b \<inter> X)\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
 2. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X)\<rbrakk> \<Longrightarrow> finite (nP b \<inter> X)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X)\<rbrakk> \<Longrightarrow> finite (nP b \<inter> X)
 2. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X); finite (nP b \<inter> X)\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a_, b_) \<in> edges G; nP a_ \<subseteq> nP b_; finite (nP a_ \<inter> X)\<rbrakk> \<Longrightarrow> finite (nP b_ \<inter> X)
[PROOF STEP]
using finite_Int
[PROOF STATE]
proof (prove)
using this:
finite ?F \<or> finite ?G \<Longrightarrow> finite (?F \<inter> ?G)

goal (1 subgoal):
 1. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a_, b_) \<in> edges G; nP a_ \<subseteq> nP b_; finite (nP a_ \<inter> X)\<rbrakk> \<Longrightarrow> finite (nP b_ \<inter> X)
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X); finite (nP b \<inter> X)\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
[PROOF STEP]
using card_mono
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> card ?A \<le> card ?B

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>ts. (\<exists>v. nP v = ts) \<longrightarrow> finite ts; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X); finite (nP b \<inter> X)\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
[PROOF STEP]
by (metis Int_subset_iff order_refl subset_antisym)


[STATEMENT]
lemma tainting_imp_blp_cutcard2: "finite X \<Longrightarrow>
  SINVAR_Tainting.sinvar G nP \<Longrightarrow> SINVAR_BLPbasic.sinvar G ((\<lambda>ts. card (ts \<inter> X)) \<circ> nP)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite X; SINVAR_Tainting.sinvar G nP\<rbrakk> \<Longrightarrow> SINVAR_BLPbasic.sinvar G ((\<lambda>ts. card (ts \<inter> X)) \<circ> nP)
[PROOF STEP]
apply(simp add: SINVAR_Tainting.sinvar_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite X; \<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2\<rbrakk> \<Longrightarrow> \<forall>x\<in>edges G. case x of (e1, e2) \<Rightarrow> card (nP e1 \<inter> X) \<le> card (nP e2 \<inter> X)
[PROOF STEP]
apply(clarify, rename_tac a b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>finite X; \<forall>(v1, v2)\<in>edges G. nP v1 \<subseteq> nP v2; (a, b) \<in> edges G\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
[PROOF STEP]
apply(erule_tac x="(a,b)" in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>finite X; (a, b) \<in> edges G; case (a, b) of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
 2. \<And>a b. \<lbrakk>finite X; (a, b) \<in> edges G; (a, b) \<notin> edges G\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>finite X; (a, b) \<in> edges G; nP a \<subseteq> nP b\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
[PROOF STEP]
apply(subgoal_tac "finite (nP a \<inter> X)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>finite X; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X)\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
 2. \<And>a b. \<lbrakk>finite X; (a, b) \<in> edges G; nP a \<subseteq> nP b\<rbrakk> \<Longrightarrow> finite (nP a \<inter> X)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>finite X; (a, b) \<in> edges G; nP a \<subseteq> nP b\<rbrakk> \<Longrightarrow> finite (nP a \<inter> X)
 2. \<And>a b. \<lbrakk>finite X; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X)\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite X; (a_, b_) \<in> edges G; nP a_ \<subseteq> nP b_\<rbrakk> \<Longrightarrow> finite (nP a_ \<inter> X)
[PROOF STEP]
using finite_Int
[PROOF STATE]
proof (prove)
using this:
finite ?F \<or> finite ?G \<Longrightarrow> finite (?F \<inter> ?G)

goal (1 subgoal):
 1. \<lbrakk>finite X; (a_, b_) \<in> edges G; nP a_ \<subseteq> nP b_\<rbrakk> \<Longrightarrow> finite (nP a_ \<inter> X)
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>finite X; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X)\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
[PROOF STEP]
apply(subgoal_tac "finite (nP b \<inter> X)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>finite X; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X); finite (nP b \<inter> X)\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
 2. \<And>a b. \<lbrakk>finite X; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X)\<rbrakk> \<Longrightarrow> finite (nP b \<inter> X)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>finite X; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X)\<rbrakk> \<Longrightarrow> finite (nP b \<inter> X)
 2. \<And>a b. \<lbrakk>finite X; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X); finite (nP b \<inter> X)\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite X; (a_, b_) \<in> edges G; nP a_ \<subseteq> nP b_; finite (nP a_ \<inter> X)\<rbrakk> \<Longrightarrow> finite (nP b_ \<inter> X)
[PROOF STEP]
using finite_Int
[PROOF STATE]
proof (prove)
using this:
finite ?F \<or> finite ?G \<Longrightarrow> finite (?F \<inter> ?G)

goal (1 subgoal):
 1. \<lbrakk>finite X; (a_, b_) \<in> edges G; nP a_ \<subseteq> nP b_; finite (nP a_ \<inter> X)\<rbrakk> \<Longrightarrow> finite (nP b_ \<inter> X)
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>finite X; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X); finite (nP b \<inter> X)\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
[PROOF STEP]
using card_mono
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> card ?A \<le> card ?B

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>finite X; (a, b) \<in> edges G; nP a \<subseteq> nP b; finite (nP a \<inter> X); finite (nP b \<inter> X)\<rbrakk> \<Longrightarrow> card (nP a \<inter> X) \<le> card (nP b \<inter> X)
[PROOF STEP]
by (metis Int_subset_iff order_refl subset_antisym)


[STATEMENT]
lemma "\<forall>ts v. nP v = ts \<longrightarrow> finite ts \<Longrightarrow>
  SINVAR_Tainting.sinvar G nP \<Longrightarrow> SINVAR_BLPbasic.sinvar G (card \<circ> nP)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ts v. nP v = ts \<longrightarrow> finite ts; SINVAR_Tainting.sinvar G nP\<rbrakk> \<Longrightarrow> SINVAR_BLPbasic.sinvar G (card \<circ> nP)
[PROOF STEP]
apply(drule(1) tainting_imp_blp_cutcard[where X=UNIV])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>SINVAR_Tainting.sinvar G nP; SINVAR_BLPbasic.sinvar G ((\<lambda>ts. card (ts \<inter> UNIV)) \<circ> nP)\<rbrakk> \<Longrightarrow> SINVAR_BLPbasic.sinvar G (card \<circ> nP)
[PROOF STEP]
by(simp)


[STATEMENT]
lemma "\<forall>b \<in> snd ` edges G. finite (nP b) \<Longrightarrow>
  SINVAR_Tainting.sinvar G nP \<Longrightarrow> SINVAR_BLPbasic.sinvar G (card \<circ> nP)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>b\<in>snd ` edges G. finite (nP b); SINVAR_Tainting.sinvar G nP\<rbrakk> \<Longrightarrow> SINVAR_BLPbasic.sinvar G (card \<circ> nP)
[PROOF STEP]
apply(simp add: SINVAR_Tainting.sinvar_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>b\<in>edges G. finite (nP (snd b)); \<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2\<rbrakk> \<Longrightarrow> \<forall>x\<in>edges G. case x of (e1, e2) \<Rightarrow> card (nP e1) \<le> card (nP e2)
[PROOF STEP]
apply(clarify, rename_tac a b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>b\<in>edges G. finite (nP (snd b)); \<forall>(v1, v2)\<in>edges G. nP v1 \<subseteq> nP v2; (a, b) \<in> edges G\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
[PROOF STEP]
apply(erule_tac x="(a,b)" in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>(v1, v2)\<in>edges G. nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (nP (snd (a, b)))\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
 2. \<And>a b. \<lbrakk>\<forall>(v1, v2)\<in>edges G. nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; (a, b) \<notin> edges G\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (nP b)\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
[PROOF STEP]
apply(case_tac "finite (nP a)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (nP b); finite (nP a)\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
 2. \<And>a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (nP b); infinite (nP a)\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
[PROOF STEP]
apply(case_tac [!] "finite (nP b)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (nP b); finite (nP a); finite (nP b)\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
 2. \<And>a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (nP b); finite (nP a); infinite (nP b)\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
 3. \<And>a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (nP b); infinite (nP a); finite (nP b)\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
 4. \<And>a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (nP b); infinite (nP a); infinite (nP b)\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
[PROOF STEP]
using card_mono
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> card ?A \<le> card ?B

goal (4 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (nP b); finite (nP a); finite (nP b)\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
 2. \<And>a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (nP b); finite (nP a); infinite (nP b)\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
 3. \<And>a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (nP b); infinite (nP a); finite (nP b)\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
 4. \<And>a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (nP b); infinite (nP a); infinite (nP b)\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (nP b); finite (nP a); infinite (nP b)\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
 2. \<And>a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (nP b); infinite (nP a); finite (nP b)\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
 3. \<And>a b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (a, b) \<in> edges G; finite (nP b); infinite (nP a); infinite (nP b)\<rbrakk> \<Longrightarrow> card (nP a) \<le> card (nP b)
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma tainting_iff_blp:
  defines "extract \<equiv> \<lambda>a ts. if a \<in> ts then 1::security_level else 0::security_level"
  shows "SINVAR_Tainting.sinvar G nP \<longleftrightarrow> (\<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SINVAR_Tainting.sinvar G nP = (\<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. SINVAR_Tainting.sinvar G nP \<Longrightarrow> \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP)
 2. \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
show"SINVAR_Tainting.sinvar G nP \<Longrightarrow> \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SINVAR_Tainting.sinvar G nP \<Longrightarrow> \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP)
[PROOF STEP]
apply(simp add: extract_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SINVAR_Tainting.sinvar G nP \<Longrightarrow> \<forall>a. \<forall>x\<in>edges G. case x of (e1, e2) \<Rightarrow> (a \<in> nP e2 \<longrightarrow> (if a \<in> nP e1 then 1 else 0) \<le> Suc 0) \<and> (a \<notin> nP e2 \<longrightarrow> (if a \<in> nP e1 then 1 else 0) = 0)
[PROOF STEP]
apply(safe)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. \<lbrakk>SINVAR_Tainting.sinvar G nP; (aa, b) \<in> edges G; a \<in> nP b\<rbrakk> \<Longrightarrow> (if a \<in> nP aa then 1 else 0) \<le> Suc 0
 2. \<And>a aa b. \<lbrakk>SINVAR_Tainting.sinvar G nP; (aa, b) \<in> edges G; a \<notin> nP b\<rbrakk> \<Longrightarrow> (if a \<in> nP aa then 1 else 0) = 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>SINVAR_Tainting.sinvar G nP; (aa, b) \<in> edges G; a \<notin> nP b\<rbrakk> \<Longrightarrow> (if a \<in> nP aa then 1 else 0) = 0
[PROOF STEP]
apply(simp add: SINVAR_Tainting.sinvar_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>\<forall>x\<in>edges G. case x of (v1, v2) \<Rightarrow> nP v1 \<subseteq> nP v2; (aa, b) \<in> edges G; a \<notin> nP b\<rbrakk> \<Longrightarrow> a \<notin> nP aa
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
SINVAR_Tainting.sinvar G nP \<Longrightarrow> \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP)

goal (1 subgoal):
 1. \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
assume blp: "\<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP)"
[PROOF STATE]
proof (state)
this:
\<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP)

goal (1 subgoal):
 1. \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP)

goal (1 subgoal):
 1. \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
fix v1 v2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
assume *: "(v1,v2)\<in>edges G"
[PROOF STATE]
proof (state)
this:
(v1, v2) \<in> edges G

goal (1 subgoal):
 1. \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(v1, v2) \<in> edges G

goal (1 subgoal):
 1. \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
from blp *
[PROOF STATE]
proof (chain)
picking this:
\<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP)
(v1, v2) \<in> edges G
[PROOF STEP]
have "(if a \<in> nP v1 then 1::security_level else 0) \<le> (if a \<in> nP v2 then 1 else 0)"
[PROOF STATE]
proof (prove)
using this:
\<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP)
(v1, v2) \<in> edges G

goal (1 subgoal):
 1. (if a \<in> nP v1 then 1 else 0) \<le> (if a \<in> nP v2 then 1 else 0)
[PROOF STEP]
unfolding extract_def
[PROOF STATE]
proof (prove)
using this:
\<forall>a. SINVAR_BLPbasic.sinvar G ((\<lambda>ts. if a \<in> ts then 1 else 0) \<circ> nP)
(v1, v2) \<in> edges G

goal (1 subgoal):
 1. (if a \<in> nP v1 then 1 else 0) \<le> (if a \<in> nP v2 then 1 else 0)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a. \<forall>x\<in>edges G. case x of (e1, e2) \<Rightarrow> (if a \<in> nP e1 then 1 else 0) \<le> (if a \<in> nP e2 then 1 else 0); (v1, v2) \<in> edges G\<rbrakk> \<Longrightarrow> a \<in> nP v1 \<longrightarrow> a \<in> nP v2
[PROOF STEP]
apply(erule_tac x=a in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(v1, v2) \<in> edges G; \<forall>x\<in>edges G. case x of (e1, e2) \<Rightarrow> (if a \<in> nP e1 then 1 else 0) \<le> (if a \<in> nP e2 then 1 else 0)\<rbrakk> \<Longrightarrow> a \<in> nP v1 \<longrightarrow> a \<in> nP v2
[PROOF STEP]
apply(erule_tac x="(v1, v2)" in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(v1, v2) \<in> edges G; case (v1, v2) of (e1, e2) \<Rightarrow> (if a \<in> nP e1 then 1 else 0) \<le> (if a \<in> nP e2 then 1 else 0)\<rbrakk> \<Longrightarrow> a \<in> nP v1 \<longrightarrow> a \<in> nP v2
 2. \<lbrakk>(v1, v2) \<in> edges G; (v1, v2) \<notin> edges G\<rbrakk> \<Longrightarrow> a \<in> nP v1 \<longrightarrow> a \<in> nP v2
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(v1, v2) \<in> edges G; (if a \<in> nP v1 then 1 else 0) \<le> (if a \<in> nP v2 then 1 else 0)\<rbrakk> \<Longrightarrow> a \<in> nP v1 \<longrightarrow> a \<in> nP v2
[PROOF STEP]
apply(simp split: if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(if a \<in> nP v1 then 1 else 0) \<le> (if a \<in> nP v2 then 1 else 0)

goal (1 subgoal):
 1. \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
hence "a \<in> nP v1 \<Longrightarrow> a \<in> nP v2"
[PROOF STATE]
proof (prove)
using this:
(if a \<in> nP v1 then 1 else 0) \<le> (if a \<in> nP v2 then 1 else 0)

goal (1 subgoal):
 1. a \<in> nP v1 \<Longrightarrow> a \<in> nP v2
[PROOF STEP]
by(simp split: if_split_asm)
[PROOF STATE]
proof (state)
this:
a \<in> nP v1 \<Longrightarrow> a \<in> nP v2

goal (1 subgoal):
 1. \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?a2 \<in> nP v1 \<Longrightarrow> ?a2 \<in> nP v2

goal (1 subgoal):
 1. \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
?a2 \<in> nP v1 \<Longrightarrow> ?a2 \<in> nP v2
[PROOF STEP]
have "nP v1 \<subseteq> nP v2"
[PROOF STATE]
proof (prove)
using this:
?a2 \<in> nP v1 \<Longrightarrow> ?a2 \<in> nP v2

goal (1 subgoal):
 1. nP v1 \<subseteq> nP v2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nP v1 \<subseteq> nP v2

goal (1 subgoal):
 1. \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?v1.2, ?v2.2) \<in> edges G \<Longrightarrow> nP ?v1.2 \<subseteq> nP ?v2.2

goal (1 subgoal):
 1. \<forall>a. SINVAR_BLPbasic.sinvar G (extract a \<circ> nP) \<Longrightarrow> SINVAR_Tainting.sinvar G nP
[PROOF STEP]
thus "SINVAR_Tainting.sinvar G nP"
[PROOF STATE]
proof (prove)
using this:
(?v1.2, ?v2.2) \<in> edges G \<Longrightarrow> nP ?v1.2 \<subseteq> nP ?v2.2

goal (1 subgoal):
 1. SINVAR_Tainting.sinvar G nP
[PROOF STEP]
unfolding SINVAR_Tainting.sinvar_def
[PROOF STATE]
proof (prove)
using this:
(?v1.2, ?v2.2) \<in> edges G \<Longrightarrow> nP ?v1.2 \<subseteq> nP ?v2.2

goal (1 subgoal):
 1. \<forall>(v1, v2)\<in>edges G. nP v1 \<subseteq> nP v2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
SINVAR_Tainting.sinvar G nP

goal:
No subgoals!
[PROOF STEP]
qed