[STATEMENT]
theorem Lp_Lq_emult:
  fixes p q r::ennreal
  assumes "1/p + 1/q = 1/r"
          "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  shows "eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
[PROOF STEP]
proof (cases "r = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r = 0 \<Longrightarrow> eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
 2. r \<noteq> 0 \<Longrightarrow> eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
r = 0

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

goal (1 subgoal):
 1. eNorm (\<LL> r M) (\<lambda>x. f x * g x) = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
r = 0
1 / p + 1 / q = 1 / r
f \<in> borel_measurable M
g \<in> borel_measurable M

goal (1 subgoal):
 1. eNorm (\<LL> r M) (\<lambda>x. f x * g x) = 0
[PROOF STEP]
by (simp add: L_zero(1))
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> r M) (\<lambda>x. f x * g x) = 0

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

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

goal (1 subgoal):
 1. r \<noteq> 0 \<Longrightarrow> eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<noteq> 0 \<Longrightarrow> eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
r \<noteq> 0

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

goal (1 subgoal):
 1. 0 < r
[PROOF STEP]
using not_gr_zero
[PROOF STATE]
proof (prove)
using this:
r \<noteq> 0
(\<not> (0::?'a) < ?n) = (?n = (0::?'a))

goal (1 subgoal):
 1. 0 < r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < r

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

goal (1 subgoal):
 1. 0 < p &&& 0 < q
[PROOF STEP]
using \<open>1/p + 1/q = 1/r\<close>
[PROOF STATE]
proof (prove)
using this:
0 < r
1 / p + 1 / q = 1 / r

goal (1 subgoal):
 1. 0 < p &&& 0 < q
[PROOF STEP]
by (metis ennreal_add_eq_top ennreal_divide_eq_top_iff ennreal_top_neq_one gr_zeroI zero_neq_one)+
[PROOF STATE]
proof (state)
this:
0 < p
0 < q

goal (1 subgoal):
 1. r \<noteq> 0 \<Longrightarrow> eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < p
0 < q
[PROOF STEP]
have Z: "zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}"
               "zero_space\<^sub>N (\<LL> q M) = {f \<in> borel_measurable M. AE x in M. f x = 0}"
               "zero_space\<^sub>N (\<LL> r M) = {f \<in> borel_measurable M. AE x in M. f x = 0}"
[PROOF STATE]
proof (prove)
using this:
0 < p
0 < q

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

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

goal (1 subgoal):
 1. r \<noteq> 0 \<Longrightarrow> eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
[PROOF STEP]
have [measurable]: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> borel_measurable M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 / p + 1 / q = 1 / r
f \<in> borel_measurable M
g \<in> borel_measurable M

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

goal (1 subgoal):
 1. r \<noteq> 0 \<Longrightarrow> eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
[PROOF STEP]
consider "eNorm (\<LL> p M) f = 0 \<or> eNorm (\<LL> q M) g = 0"
         | "(eNorm (\<LL> p M) f > 0 \<and> eNorm (\<LL> q M) g = \<infinity>) \<or> (eNorm (\<LL> p M) f = \<infinity> \<and> eNorm (\<LL> q M) g > 0)"
         | "eNorm (\<LL> p M) f < \<infinity> \<and> eNorm (\<LL> q M) g < \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eNorm (\<LL> p M) f = 0 \<or> eNorm (\<LL> q M) g = 0 \<Longrightarrow> thesis; 0 < eNorm (\<LL> p M) f \<and> eNorm (\<LL> q M) g = \<infinity> \<or> eNorm (\<LL> p M) f = \<infinity> \<and> 0 < eNorm (\<LL> q M) g \<Longrightarrow> thesis; eNorm (\<LL> p M) f < \<infinity> \<and> eNorm (\<LL> q M) g < \<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using less_top
[PROOF STATE]
proof (prove)
using this:
(?a \<noteq> \<top>) = (?a < \<top>)

goal (1 subgoal):
 1. \<lbrakk>eNorm (\<LL> p M) f = 0 \<or> eNorm (\<LL> q M) g = 0 \<Longrightarrow> thesis; 0 < eNorm (\<LL> p M) f \<and> eNorm (\<LL> q M) g = \<infinity> \<or> eNorm (\<LL> p M) f = \<infinity> \<and> 0 < eNorm (\<LL> q M) g \<Longrightarrow> thesis; eNorm (\<LL> p M) f < \<infinity> \<and> eNorm (\<LL> q M) g < \<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>eNorm (\<LL> p M) f = 0 \<or> eNorm (\<LL> q M) g = 0 \<Longrightarrow> ?thesis; 0 < eNorm (\<LL> p M) f \<and> eNorm (\<LL> q M) g = \<infinity> \<or> eNorm (\<LL> p M) f = \<infinity> \<and> 0 < eNorm (\<LL> q M) g \<Longrightarrow> ?thesis; eNorm (\<LL> p M) f < \<infinity> \<and> eNorm (\<LL> q M) g < \<infinity> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. r \<noteq> 0 \<Longrightarrow> eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>eNorm (\<LL> p M) f = 0 \<or> eNorm (\<LL> q M) g = 0 \<Longrightarrow> ?thesis; 0 < eNorm (\<LL> p M) f \<and> eNorm (\<LL> q M) g = \<infinity> \<or> eNorm (\<LL> p M) f = \<infinity> \<and> 0 < eNorm (\<LL> q M) g \<Longrightarrow> ?thesis; eNorm (\<LL> p M) f < \<infinity> \<and> eNorm (\<LL> q M) g < \<infinity> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>eNorm (\<LL> p M) f = 0 \<or> eNorm (\<LL> q M) g = 0 \<Longrightarrow> ?thesis; 0 < eNorm (\<LL> p M) f \<and> eNorm (\<LL> q M) g = \<infinity> \<or> eNorm (\<LL> p M) f = \<infinity> \<and> 0 < eNorm (\<LL> q M) g \<Longrightarrow> ?thesis; eNorm (\<LL> p M) f < \<infinity> \<and> eNorm (\<LL> q M) g < \<infinity> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

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

goal (1 subgoal):
 1. (AE x in M. f x = 0) \<or> (AE x in M. g x = 0)
[PROOF STEP]
using Z
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) f = 0 \<or> eNorm (\<LL> q M) g = 0
zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
zero_space\<^sub>N (\<LL> q M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
zero_space\<^sub>N (\<LL> r M) = {f \<in> borel_measurable M. AE x in M. f x = 0}

goal (1 subgoal):
 1. (AE x in M. f x = 0) \<or> (AE x in M. g x = 0)
[PROOF STEP]
unfolding zero_space\<^sub>N_def
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) f = 0 \<or> eNorm (\<LL> q M) g = 0
{f. eNorm (\<LL> p M) f = 0} = {f \<in> borel_measurable M. AE x in M. f x = 0}
{f. eNorm (\<LL> q M) f = 0} = {f \<in> borel_measurable M. AE x in M. f x = 0}
{f. eNorm (\<LL> r M) f = 0} = {f \<in> borel_measurable M. AE x in M. f x = 0}

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

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

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

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

goal (1 subgoal):
 1. eNorm (\<LL> r M) (\<lambda>x. f x * g x) = 0
[PROOF STEP]
using Z
[PROOF STATE]
proof (prove)
using this:
AE x in M. f x * g x = 0
zero_space\<^sub>N (\<LL> p M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
zero_space\<^sub>N (\<LL> q M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
zero_space\<^sub>N (\<LL> r M) = {f \<in> borel_measurable M. AE x in M. f x = 0}

goal (1 subgoal):
 1. eNorm (\<LL> r M) (\<lambda>x. f x * g x) = 0
[PROOF STEP]
unfolding zero_space\<^sub>N_def
[PROOF STATE]
proof (prove)
using this:
AE x in M. f x * g x = 0
{f. eNorm (\<LL> p M) f = 0} = {f \<in> borel_measurable M. AE x in M. f x = 0}
{f. eNorm (\<LL> q M) f = 0} = {f \<in> borel_measurable M. AE x in M. f x = 0}
{f. eNorm (\<LL> r M) f = 0} = {f \<in> borel_measurable M. AE x in M. f x = 0}

goal (1 subgoal):
 1. eNorm (\<LL> r M) (\<lambda>x. f x * g x) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> r M) (\<lambda>x. f x * g x) = 0

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

goal (1 subgoal):
 1. eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g

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

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

goal (1 subgoal):
 1. eNorm (\<LL> p M) f * eNorm (\<LL> q M) g = \<infinity>
[PROOF STEP]
using ennreal_mult_eq_top_iff
[PROOF STATE]
proof (prove)
using this:
0 < eNorm (\<LL> p M) f \<and> eNorm (\<LL> q M) g = \<infinity> \<or> eNorm (\<LL> p M) f = \<infinity> \<and> 0 < eNorm (\<LL> q M) g
(?a * ?b = \<top>) = (?a = \<top> \<and> ?b \<noteq> 0 \<or> ?b = \<top> \<and> ?a \<noteq> 0)

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

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

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

goal (1 subgoal):
 1. eNorm (\<LL> p M) f < \<infinity> \<and> eNorm (\<LL> q M) g < \<infinity> \<Longrightarrow> eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eNorm (\<LL> p M) f < \<infinity> \<and> eNorm (\<LL> q M) g < \<infinity> \<Longrightarrow> eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) f < \<infinity> \<and> eNorm (\<LL> q M) g < \<infinity>

goal (1 subgoal):
 1. eNorm (\<LL> p M) f < \<infinity> \<and> eNorm (\<LL> q M) g < \<infinity> \<Longrightarrow> eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> p M) f < \<infinity> \<and> eNorm (\<LL> q M) g < \<infinity>
[PROOF STEP]
have *: "f \<in> space\<^sub>N (\<LL> p M)" "g \<in> space\<^sub>N (\<LL> q M)"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) f < \<infinity> \<and> eNorm (\<LL> q M) g < \<infinity>

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

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

goal (1 subgoal):
 1. eNorm (\<LL> p M) f < \<infinity> \<and> eNorm (\<LL> q M) g < \<infinity> \<Longrightarrow> eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> space\<^sub>N (\<LL> p M)
g \<in> space\<^sub>N (\<LL> q M)
[PROOF STEP]
have "(\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)"
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> p M)
g \<in> space\<^sub>N (\<LL> q M)

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)
[PROOF STEP]
using Lp_Lq_mult(1)[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> p M)
g \<in> space\<^sub>N (\<LL> q M)
\<lbrakk>?f \<in> space\<^sub>N (\<LL> p ?M); ?g \<in> space\<^sub>N (\<LL> q ?M)\<rbrakk> \<Longrightarrow> (\<lambda>x. ?f x * ?g x) \<in> space\<^sub>N (\<LL> r ?M)

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

goal (1 subgoal):
 1. eNorm (\<LL> p M) f < \<infinity> \<and> eNorm (\<LL> q M) g < \<infinity> \<Longrightarrow> eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)

goal (1 subgoal):
 1. eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
[PROOF STEP]
using Lp_Lq_mult(2)[OF assms(1) *]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)
Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g

goal (1 subgoal):
 1. eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g
[PROOF STEP]
by (simp add: eNorm_Norm * ennreal_mult'[symmetric])
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> r M) (\<lambda>x. f x * g x) \<le> eNorm (\<LL> p M) f * eNorm (\<LL> q M) g

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Lp_Lq_duality_bound:
  fixes p q::ennreal
  assumes "1/p + 1/q = 1"
          "f \<in> space\<^sub>N (\<LL> p M)"
          "g \<in> space\<^sub>N (\<LL> q M)"
  shows "integrable M (\<lambda>x. f x * g x)"
        "abs(\<integral>x. f x * g x \<partial>M) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. f x * g x) &&& \<bar>LINT x|M. f x * g x\<bar> \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * g x)
 2. \<bar>LINT x|M. f x * g x\<bar> \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have "(\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> 1 M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> 1 M)
[PROOF STEP]
apply (rule Lp_Lq_mult[OF _ \<open>f \<in> space\<^sub>N (\<LL> p M)\<close> \<open>g \<in> space\<^sub>N (\<LL> q M)\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / p + 1 / q = 1 / 1
[PROOF STEP]
using \<open>1/p + 1/q = 1\<close>
[PROOF STATE]
proof (prove)
using this:
1 / p + 1 / q = 1

goal (1 subgoal):
 1. 1 / p + 1 / q = 1 / 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> 1 M)

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * g x)
 2. \<bar>LINT x|M. f x * g x\<bar> \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> 1 M)
[PROOF STEP]
show "integrable M (\<lambda>x. f x * g x)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> 1 M)

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

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

goal (1 subgoal):
 1. \<bar>LINT x|M. f x * g x\<bar> \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have "abs(\<integral>x. f x * g x \<partial>M) \<le> Norm (\<LL> 1 M) (\<lambda>x. f x * g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>LINT x|M. f x * g x\<bar> \<le> Norm (\<LL> 1 M) (\<lambda>x. f x * g x)
[PROOF STEP]
using L1_int_ineq
[PROOF STATE]
proof (prove)
using this:
\<bar>integral\<^sup>L ?M ?f\<bar> \<le> Norm (\<LL> 1 ?M) ?f

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

goal (1 subgoal):
 1. \<bar>LINT x|M. f x * g x\<bar> \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>LINT x|M. f x * g x\<bar> \<le> Norm (\<LL> 1 M) (\<lambda>x. f x * g x)

goal (1 subgoal):
 1. \<bar>LINT x|M. f x * g x\<bar> \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have "... \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> 1 M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
apply (rule Lp_Lq_mult[OF _ \<open>f \<in> space\<^sub>N (\<LL> p M)\<close> \<open>g \<in> space\<^sub>N (\<LL> q M)\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / p + 1 / q = 1 / 1
[PROOF STEP]
using \<open>1/p + 1/q = 1\<close>
[PROOF STATE]
proof (prove)
using this:
1 / p + 1 / q = 1

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

goal (1 subgoal):
 1. \<bar>LINT x|M. f x * g x\<bar> \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>LINT x|M. f x * g x\<bar> \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
show "abs(\<integral>x. f x * g x \<partial>M) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g"
[PROOF STATE]
proof (prove)
using this:
\<bar>LINT x|M. f x * g x\<bar> \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g

goal (1 subgoal):
 1. \<bar>LINT x|M. f x * g x\<bar> \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>LINT x|M. f x * g x\<bar> \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g

goal:
No subgoals!
[PROOF STEP]
qed