[STATEMENT]
theorem Lp_Lq_mult:
  fixes p q r::ennreal
  assumes "1/p + 1/q = 1/r"
      and "f \<in> space\<^sub>N (\<LL> p M)" "g \<in> space\<^sub>N (\<LL> q M)"
  shows "(\<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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<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
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)
 2. Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> borel_measurable M &&& g \<in> borel_measurable M
[PROOF STEP]
using Lp_measurable assms
[PROOF STATE]
proof (prove)
using this:
?f \<in> space\<^sub>N (\<LL> ?p ?M) \<Longrightarrow> ?f \<in> borel_measurable ?M
1 / p + 1 / q = 1 / r
f \<in> space\<^sub>N (\<LL> p M)
g \<in> space\<^sub>N (\<LL> q M)

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

goal (2 subgoals):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)
 2. Norm (\<LL> r M) (\<lambda>x. f x * g x) \<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> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
proof (cases rule: Lp_cases[of r])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p2. \<lbrakk>r = ennreal p2; 0 < p2; 0 < r\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 2. r = 0 \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 3. r = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
case zero
[PROOF STATE]
proof (state)
this:
r = 0

goal (3 subgoals):
 1. \<And>p2. \<lbrakk>r = ennreal p2; 0 < p2; 0 < r\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 2. r = 0 \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 3. r = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have *: "(\<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]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * g x) \<in> borel_measurable M

goal (3 subgoals):
 1. \<And>p2. \<lbrakk>r = ennreal p2; 0 < p2; 0 < r\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 2. r = 0 \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 3. r = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<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> borel_measurable M
[PROOF STEP]
have "Norm (\<LL> r M) (\<lambda>x. f x * g x) = 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x * g x) \<in> borel_measurable M

goal (1 subgoal):
 1. Norm (\<LL> r M) (\<lambda>x. f x * g x) = 0
[PROOF STEP]
using L_zero[of M]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x * g x) \<in> borel_measurable M
eNorm (\<LL> 0 M) ?f = (if ?f \<in> borel_measurable M then 0 else \<infinity>)
defect (\<LL> 0 M) = 1

goal (1 subgoal):
 1. Norm (\<LL> r M) (\<lambda>x. f x * g x) = 0
[PROOF STEP]
unfolding Norm_def zero
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x * g x) \<in> borel_measurable M
eNorm (\<LL> 0 M) ?f = (if ?f \<in> borel_measurable M then 0 else \<infinity>)
defect (\<LL> 0 M) = 1

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

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

goal (1 subgoal):
 1. Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
using Norm_nonneg
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (\<lambda>x. f x * g x) = 0
0 \<le> Norm ?N ?x

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

goal (3 subgoals):
 1. \<And>p2. \<lbrakk>r = ennreal p2; 0 < p2; 0 < r\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 2. r = 0 \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 3. r = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
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. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
unfolding zero
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> 0 M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> 0 M) \<and> Norm (\<LL> 0 M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
using * L_zero_space[of M]
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> 0 M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
(\<lambda>x. f x * g x) \<in> borel_measurable M
space\<^sub>N (\<LL> 0 M) = borel_measurable M
zero_space\<^sub>N (\<LL> 0 M) = borel_measurable M

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

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>r = ennreal p2; 0 < p2; 0 < r\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 2. r = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p2. \<lbrakk>r = ennreal p2; 0 < p2; 0 < r\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 2. r = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
case (real_pos r2)
[PROOF STATE]
proof (state)
this:
r = ennreal r2
0 < r2
0 < r

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>r = ennreal p2; 0 < p2; 0 < r\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 2. r = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have "p > 0" "q > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < p &&& 0 < q
[PROOF STEP]
using \<open>1/p + 1/q = 1/r\<close> \<open>r > 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 / p + 1 / q = 1 / r
0 < 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 (2 subgoals):
 1. \<And>p2. \<lbrakk>r = ennreal p2; 0 < p2; 0 < r\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 2. r = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
consider "p = \<infinity>" | "q = \<infinity>" | "p < \<infinity> \<and> q < \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = \<infinity> \<Longrightarrow> thesis; q = \<infinity> \<Longrightarrow> thesis; p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using top.not_eq_extremum
[PROOF STATE]
proof (prove)
using this:
(?a \<noteq> \<top>) = (?a < \<top>)

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

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

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

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

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

goal (1 subgoal):
 1. q = r
[PROOF STEP]
by (metis ennreal_divide_top infinity_ennreal_def one_divide_one_divide_ennreal semiring_normalization_rules(5))
[PROOF STATE]
proof (state)
this:
q = r

goal (3 subgoals):
 1. p = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 2. q = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 3. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have "AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> p M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> p M) f
[PROOF STEP]
using \<open>f \<in> space\<^sub>N (\<LL> p M)\<close> L_infinity_AE_bound
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> p M)
?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> p M) f
[PROOF STEP]
unfolding \<open>p = \<infinity>\<close>
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> \<infinity> M)
?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> p M) f

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

goal (1 subgoal):
 1. AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> p M) f * g x\<bar>
[PROOF STEP]
unfolding abs_mult
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> p M) f

goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> * \<bar>g x\<bar> \<le> \<bar>Norm (\<LL> p M) f\<bar> * \<bar>g x\<bar>
[PROOF STEP]
using Norm_nonneg[of "\<LL> p M" f] mult_right_mono
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> p M) f
0 \<le> Norm (\<LL> p M) f
\<lbrakk>?a \<le> ?b; (0::?'a) \<le> ?c\<rbrakk> \<Longrightarrow> ?a * ?c \<le> ?b * ?c

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

goal (3 subgoals):
 1. p = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 2. q = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 3. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have **: "(\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M)
[PROOF STEP]
using spaceN_cmult[OF \<open>g \<in> space\<^sub>N (\<LL> q M)\<close>]
[PROOF STATE]
proof (prove)
using this:
?c *\<^sub>R g \<in> space\<^sub>N (\<LL> q M)

goal (1 subgoal):
 1. (\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M)
[PROOF STEP]
unfolding \<open>q = r\<close> scaleR_fun_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. ?c *\<^sub>R g x) \<in> space\<^sub>N (\<LL> r M)

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

goal (3 subgoals):
 1. p = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 2. q = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 3. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have ***: "Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x) = Norm (\<LL> p M) f * Norm (\<LL> q M) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x) = Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
using Norm_cmult[of "\<LL> r M"]
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (?c *\<^sub>R ?x) = \<bar>?c\<bar> * Norm (\<LL> r M) ?x

goal (1 subgoal):
 1. Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x) = Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
unfolding \<open>q = r\<close> scaleR_fun_def
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (\<lambda>x. ?c *\<^sub>R ?x x) = \<bar>?c\<bar> * Norm (\<LL> r M) ?x

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

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

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
using Lp_domination[of "\<lambda>x. f x * g x" M "\<lambda>x. Norm (\<LL> p M) f * g x" r]
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x) = Norm (\<LL> p M) f * Norm (\<LL> q M) g
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> p M) f * g x\<bar>\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> p M) f * g x\<bar>\<rbrakk> \<Longrightarrow> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x)

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
unfolding \<open>q = r\<close>
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x) = Norm (\<LL> p M) f * Norm (\<LL> r M) g
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> p M) f * g x\<bar>\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> p M) f * g x\<bar>\<rbrakk> \<Longrightarrow> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x)

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> r M) g
[PROOF STEP]
using * ** ***
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x) = Norm (\<LL> p M) f * Norm (\<LL> r M) g
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> p M) f * g x\<bar>\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> p M) f * g x\<bar>\<rbrakk> \<Longrightarrow> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x)
AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> p M) f * g x\<bar>
(\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M)
Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x) = Norm (\<LL> p M) f * Norm (\<LL> q M) g

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

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

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

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

goal (1 subgoal):
 1. p = r
[PROOF STEP]
by (metis add.right_neutral ennreal_divide_top infinity_ennreal_def one_divide_one_divide_ennreal)
[PROOF STATE]
proof (state)
this:
p = r

goal (2 subgoals):
 1. q = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 2. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have "AE x in M. \<bar>g x\<bar> \<le> Norm (\<LL> q M) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. \<bar>g x\<bar> \<le> Norm (\<LL> q M) g
[PROOF STEP]
using \<open>g \<in> space\<^sub>N (\<LL> q M)\<close> L_infinity_AE_bound
[PROOF STATE]
proof (prove)
using this:
g \<in> space\<^sub>N (\<LL> q M)
?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>g x\<bar> \<le> Norm (\<LL> q M) g
[PROOF STEP]
unfolding \<open>q = \<infinity>\<close>
[PROOF STATE]
proof (prove)
using this:
g \<in> space\<^sub>N (\<LL> \<infinity> M)
?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>g x\<bar> \<le> Norm (\<LL> \<infinity> M) g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. \<bar>g x\<bar> \<le> Norm (\<LL> q M) g

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

goal (1 subgoal):
 1. AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> q M) g * f x\<bar>
[PROOF STEP]
apply (simp only: mult.commute[of "Norm (\<LL> q M) g" _])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. \<bar>g x\<bar> \<le> Norm (\<LL> q M) g \<Longrightarrow> AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>f x * Norm (\<LL> q M) g\<bar>
[PROOF STEP]
unfolding abs_mult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. \<bar>g x\<bar> \<le> Norm (\<LL> q M) g \<Longrightarrow> AE x in M. \<bar>f x\<bar> * \<bar>g x\<bar> \<le> \<bar>f x\<bar> * \<bar>Norm (\<LL> q M) g\<bar>
[PROOF STEP]
using mult_left_mono Norm_nonneg[of "\<LL> q M" g]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<le> ?b; (0::?'a) \<le> ?c\<rbrakk> \<Longrightarrow> ?c * ?a \<le> ?c * ?b
0 \<le> Norm (\<LL> q M) g

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

goal (2 subgoals):
 1. q = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 2. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have **: "(\<lambda>x. Norm (\<LL> q M) g * f x) \<in> space\<^sub>N (\<LL> r M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. Norm (\<LL> q M) g * f x) \<in> space\<^sub>N (\<LL> r M)
[PROOF STEP]
using spaceN_cmult[OF \<open>f \<in> space\<^sub>N (\<LL> p M)\<close>]
[PROOF STATE]
proof (prove)
using this:
?c *\<^sub>R f \<in> space\<^sub>N (\<LL> p M)

goal (1 subgoal):
 1. (\<lambda>x. Norm (\<LL> q M) g * f x) \<in> space\<^sub>N (\<LL> r M)
[PROOF STEP]
unfolding \<open>p = r\<close> scaleR_fun_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. ?c *\<^sub>R f x) \<in> space\<^sub>N (\<LL> r M)

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

goal (2 subgoals):
 1. q = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
 2. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have ***: "Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> q M) g * f x) = Norm (\<LL> p M) f * Norm (\<LL> q M) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> q M) g * f x) = Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
using Norm_cmult[of "\<LL> r M"]
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (?c *\<^sub>R ?x) = \<bar>?c\<bar> * Norm (\<LL> r M) ?x

goal (1 subgoal):
 1. Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> q M) g * f x) = Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
unfolding \<open>p = r\<close> scaleR_fun_def
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (\<lambda>x. ?c *\<^sub>R ?x x) = \<bar>?c\<bar> * Norm (\<LL> r M) ?x

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

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

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
using Lp_domination[of "\<lambda>x. f x * g x" M "\<lambda>x. Norm (\<LL> q M) g * f x" r]
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> q M) g * f x) = Norm (\<LL> p M) f * Norm (\<LL> q M) g
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> q M) g * f x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> q M) g * f x\<bar>\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> q M) g * f x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> q M) g * f x\<bar>\<rbrakk> \<Longrightarrow> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> q M) g * f x)

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
unfolding \<open>p = r\<close>
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> q M) g * f x) = Norm (\<LL> r M) f * Norm (\<LL> q M) g
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> q M) g * f x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> q M) g * f x\<bar>\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> q M) g * f x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> q M) g * f x\<bar>\<rbrakk> \<Longrightarrow> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> q M) g * f x)

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> r M) f * Norm (\<LL> q M) g
[PROOF STEP]
using * ** ***
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> q M) g * f x) = Norm (\<LL> r M) f * Norm (\<LL> q M) g
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> q M) g * f x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> q M) g * f x\<bar>\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> q M) g * f x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> q M) g * f x\<bar>\<rbrakk> \<Longrightarrow> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> q M) g * f x)
AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> q M) g * f x\<bar>
(\<lambda>x. Norm (\<LL> q M) g * f x) \<in> space\<^sub>N (\<LL> r M)
Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> q M) g * f x) = Norm (\<LL> p M) f * Norm (\<LL> q M) g

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> r M) f * Norm (\<LL> q M) g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> 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. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
p < \<infinity> \<and> q < \<infinity>

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
obtain p2 where "p = ennreal p2" "p2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p2. \<lbrakk>p = ennreal p2; 0 < p2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using enn2real_positive_iff[of p] 3 \<open>p > 0\<close>
[PROOF STATE]
proof (prove)
using this:
(0 < enn2real p) = (0 < p \<and> p < \<top>)
p < \<infinity> \<and> q < \<infinity>
0 < p

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

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
obtain q2 where "q = ennreal q2" "q2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q2. \<lbrakk>q = ennreal q2; 0 < q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using enn2real_positive_iff[of q] 3 \<open>q > 0\<close>
[PROOF STATE]
proof (prove)
using this:
(0 < enn2real q) = (0 < q \<and> q < \<top>)
p < \<infinity> \<and> q < \<infinity>
0 < q

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

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have "ennreal(1/r2) = 1/r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (1 / r2) = 1 / r
[PROOF STEP]
using \<open>r = ennreal r2\<close> \<open>r2 > 0\<close> divide_ennreal zero_le_one
[PROOF STATE]
proof (prove)
using this:
r = ennreal r2
0 < r2
\<lbrakk>0 \<le> ?r; 0 < ?q\<rbrakk> \<Longrightarrow> ennreal ?r / ennreal ?q = ennreal (?r / ?q)
(0::?'a) \<le> (1::?'a)

goal (1 subgoal):
 1. ennreal (1 / r2) = 1 / r
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ennreal (1 / r2) = 1 / r

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ennreal (1 / r2) = 1 / r

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

goal (1 subgoal):
 1. 1 / r = 1 / p + 1 / q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / r = 1 / p + 1 / q

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 / r = 1 / p + 1 / q

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have "... = ennreal(1/p2 + 1/q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / p + 1 / q = ennreal (1 / p2 + 1 / q2)
[PROOF STEP]
using \<open>p = ennreal p2\<close> \<open>p2 > 0\<close> \<open>q = ennreal q2\<close> \<open>q2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
p = ennreal p2
0 < p2
q = ennreal q2
0 < q2

goal (1 subgoal):
 1. 1 / p + 1 / q = ennreal (1 / p2 + 1 / q2)
[PROOF STEP]
apply (simp only: divide_ennreal ennreal_1[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = ennreal p2; 0 < p2; q = ennreal q2; 0 < q2\<rbrakk> \<Longrightarrow> ennreal (1 / p2) + ennreal (1 / q2) = ennreal (1 / p2 + 1 / q2)
[PROOF STEP]
using ennreal_plus[of "1/p2" "1/q2", symmetric]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> 1 / p2; 0 \<le> 1 / q2\<rbrakk> \<Longrightarrow> ennreal (1 / p2) + ennreal (1 / q2) = ennreal (1 / p2 + 1 / q2)

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

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ennreal (1 / r2) = ennreal (1 / p2 + 1 / q2)
[PROOF STEP]
have *: "1/r2 = 1/p2 + 1/q2"
[PROOF STATE]
proof (prove)
using this:
ennreal (1 / r2) = ennreal (1 / p2 + 1 / q2)

goal (1 subgoal):
 1. 1 / r2 = 1 / p2 + 1 / q2
[PROOF STEP]
using ennreal_inj \<open>p2 > 0\<close> \<open>q2 > 0\<close> \<open>r2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
ennreal (1 / r2) = ennreal (1 / p2 + 1 / q2)
\<lbrakk>0 \<le> ?a; 0 \<le> ?b\<rbrakk> \<Longrightarrow> (ennreal ?a = ennreal ?b) = (?a = ?b)
0 < p2
0 < q2
0 < r2

goal (1 subgoal):
 1. 1 / r2 = 1 / p2 + 1 / q2
[PROOF STEP]
by (metis divide_pos_pos ennreal_less_zero_iff le_less zero_less_one)
[PROOF STATE]
proof (state)
this:
1 / r2 = 1 / p2 + 1 / q2

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
define P where "P = p2 / r2"
[PROOF STATE]
proof (state)
this:
P = p2 / r2

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
define Q where "Q = q2 / r2"
[PROOF STATE]
proof (state)
this:
Q = q2 / r2

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have [simp]: "P > 0" "Q > 0" and "1/P + 1/Q = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < P &&& 0 < Q) &&& 1 / P + 1 / Q = 1
[PROOF STEP]
using \<open>p2 > 0\<close> \<open>q2 > 0\<close> \<open>r2 > 0\<close> *
[PROOF STATE]
proof (prove)
using this:
0 < p2
0 < q2
0 < r2
1 / r2 = 1 / p2 + 1 / q2

goal (1 subgoal):
 1. (0 < P &&& 0 < Q) &&& 1 / P + 1 / Q = 1
[PROOF STEP]
unfolding P_def Q_def
[PROOF STATE]
proof (prove)
using this:
0 < p2
0 < q2
0 < r2
1 / r2 = 1 / p2 + 1 / q2

goal (1 subgoal):
 1. (0 < p2 / r2 &&& 0 < q2 / r2) &&& 1 / (p2 / r2) + 1 / (q2 / r2) = 1
[PROOF STEP]
by (auto simp add: divide_simps algebra_simps)
[PROOF STATE]
proof (state)
this:
0 < P
0 < Q
1 / P + 1 / Q = 1

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have Pa: "(\<bar>z\<bar> powr r2) powr P = \<bar>z\<bar> powr p2" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<bar>z\<bar> powr r2) powr P = \<bar>z\<bar> powr p2
[PROOF STEP]
unfolding P_def powr_powr
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>z\<bar> powr (r2 * (p2 / r2)) = \<bar>z\<bar> powr p2
[PROOF STEP]
using \<open>r2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < r2

goal (1 subgoal):
 1. \<bar>z\<bar> powr (r2 * (p2 / r2)) = \<bar>z\<bar> powr p2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<bar>?z\<bar> powr r2) powr P = \<bar>?z\<bar> powr p2

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have Qa: "(\<bar>z\<bar> powr r2) powr Q = \<bar>z\<bar> powr q2" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<bar>z\<bar> powr r2) powr Q = \<bar>z\<bar> powr q2
[PROOF STEP]
unfolding Q_def powr_powr
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>z\<bar> powr (r2 * (q2 / r2)) = \<bar>z\<bar> powr q2
[PROOF STEP]
using \<open>r2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < r2

goal (1 subgoal):
 1. \<bar>z\<bar> powr (r2 * (q2 / r2)) = \<bar>z\<bar> powr q2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<bar>?z\<bar> powr r2) powr Q = \<bar>?z\<bar> powr q2

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have *: "integrable M (\<lambda>x. \<bar>f x\<bar> powr r2 * \<bar>g x\<bar> powr r2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr r2 * \<bar>g x\<bar> powr r2)
[PROOF STEP]
apply (rule Holder_inequality[OF \<open>P>0\<close> \<open>Q>0\<close> \<open>1/P + 1/Q = 1\<close>], auto simp add: Pa Qa)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)
 2. integrable M (\<lambda>x. \<bar>g x\<bar> powr q2)
[PROOF STEP]
using \<open>f \<in> space\<^sub>N (\<LL> p M)\<close>
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> p M)

goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)
 2. integrable M (\<lambda>x. \<bar>g x\<bar> powr q2)
[PROOF STEP]
unfolding \<open>p = ennreal p2\<close>
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> (ennreal p2) M)

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

goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)
 2. integrable M (\<lambda>x. \<bar>g x\<bar> powr q2)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<And>M. space\<^sub>N (\<LL> (ennreal p2) M) = {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)}\<rbrakk> \<Longrightarrow> integrable M (\<lambda>x. \<bar>g x\<bar> powr q2)
[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 (1 subgoal):
 1. \<lbrakk>f \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<And>M. space\<^sub>N (\<LL> (ennreal p2) M) = {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)}\<rbrakk> \<Longrightarrow> integrable M (\<lambda>x. \<bar>g x\<bar> powr q2)
[PROOF STEP]
unfolding \<open>q = ennreal q2\<close>
[PROOF STATE]
proof (prove)
using this:
g \<in> space\<^sub>N (\<LL> (ennreal q2) M)

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

goal (1 subgoal):
 1. \<lbrakk>f \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<And>M. space\<^sub>N (\<LL> (ennreal p2) M) = {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)}\<rbrakk> \<Longrightarrow> integrable M (\<lambda>x. \<bar>g x\<bar> powr q2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. \<bar>f x\<bar> powr r2 * \<bar>g x\<bar> powr r2)

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<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> r M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)
[PROOF STEP]
unfolding \<open>r = ennreal r2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> (ennreal r2) M)
[PROOF STEP]
using Lp_space[OF \<open>r2 > 0\<close>, of M]
[PROOF STATE]
proof (prove)
using this:
space\<^sub>N (\<LL> (ennreal r2) M) = {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr r2)}

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

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have "Norm (\<LL> r M) (\<lambda>x. f x * g x) = (\<integral>x. \<bar>f x * g x\<bar> powr r2 \<partial>M) powr (1/r2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> r M) (\<lambda>x. f x * g x) = (LINT x|M. \<bar>f x * g x\<bar> powr r2) powr (1 / r2)
[PROOF STEP]
unfolding \<open>r = ennreal r2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> (ennreal r2) M) (\<lambda>x. f x * g x) = (LINT x|M. \<bar>f x * g x\<bar> powr r2) powr (1 / r2)
[PROOF STEP]
using Lp_Norm[OF \<open>r2 > 0\<close>, of _ M]
[PROOF STATE]
proof (prove)
using this:
?f \<in> borel_measurable M \<Longrightarrow> Norm (\<LL> (ennreal r2) M) ?f = (LINT x|M. \<bar>?f x\<bar> powr r2) powr (1 / r2)
?f \<in> borel_measurable M \<Longrightarrow> Norm (\<LL> (ennreal r2) M) ?f powr r2 = LINT x|M. \<bar>?f x\<bar> powr r2

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

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Norm (\<LL> r M) (\<lambda>x. f x * g x) = (LINT x|M. \<bar>f x * g x\<bar> powr r2) powr (1 / r2)

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have "... = abs (\<integral>x. \<bar>f x\<bar> powr r2 * \<bar>g x\<bar> powr r2 \<partial>M) powr (1/r2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x * g x\<bar> powr r2) powr (1 / r2) = \<bar>LINT x|M. \<bar>f x\<bar> powr r2 * \<bar>g x\<bar> powr r2\<bar> powr (1 / r2)
[PROOF STEP]
by (auto simp add: powr_mult abs_mult)
[PROOF STATE]
proof (state)
this:
(LINT x|M. \<bar>f x * g x\<bar> powr r2) powr (1 / r2) = \<bar>LINT x|M. \<bar>f x\<bar> powr r2 * \<bar>g x\<bar> powr r2\<bar> powr (1 / r2)

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(LINT x|M. \<bar>f x * g x\<bar> powr r2) powr (1 / r2) = \<bar>LINT x|M. \<bar>f x\<bar> powr r2 * \<bar>g x\<bar> powr r2\<bar> powr (1 / r2)

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have "... \<le> ((\<integral>x. \<bar> \<bar>f x\<bar> powr r2 \<bar> powr P \<partial>M) powr (1/P) * (\<integral>x. \<bar> \<bar>g x\<bar> powr r2 \<bar> powr Q \<partial>M) powr (1/Q)) powr (1/r2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>LINT x|M. \<bar>f x\<bar> powr r2 * \<bar>g x\<bar> powr r2\<bar> powr (1 / r2) \<le> ((LINT x|M. \<bar>\<bar>f x\<bar> powr r2\<bar> powr P) powr (1 / P) * (LINT x|M. \<bar>\<bar>g x\<bar> powr r2\<bar> powr Q) powr (1 / Q)) powr (1 / r2)
[PROOF STEP]
apply (rule powr_mono2, simp add: \<open>r2 > 0\<close> less_imp_le, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>LINT x|M. \<bar>f x\<bar> powr r2 * \<bar>g x\<bar> powr r2\<bar> \<le> (LINT x|M. \<bar>\<bar>f x\<bar> powr r2\<bar> powr P) powr (1 / P) * (LINT x|M. \<bar>\<bar>g x\<bar> powr r2\<bar> powr Q) powr (1 / Q)
[PROOF STEP]
apply (rule Holder_inequality[OF \<open>P>0\<close> \<open>Q>0\<close> \<open>1/P + 1/Q = 1\<close>], auto simp add: Pa Qa)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)
 2. integrable M (\<lambda>x. \<bar>g x\<bar> powr q2)
[PROOF STEP]
using \<open>f \<in> space\<^sub>N (\<LL> p M)\<close>
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> p M)

goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)
 2. integrable M (\<lambda>x. \<bar>g x\<bar> powr q2)
[PROOF STEP]
unfolding \<open>p = ennreal p2\<close>
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> (ennreal p2) M)

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

goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)
 2. integrable M (\<lambda>x. \<bar>g x\<bar> powr q2)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<And>M. space\<^sub>N (\<LL> (ennreal p2) M) = {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)}\<rbrakk> \<Longrightarrow> integrable M (\<lambda>x. \<bar>g x\<bar> powr q2)
[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 (1 subgoal):
 1. \<lbrakk>f \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<And>M. space\<^sub>N (\<LL> (ennreal p2) M) = {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)}\<rbrakk> \<Longrightarrow> integrable M (\<lambda>x. \<bar>g x\<bar> powr q2)
[PROOF STEP]
unfolding \<open>q = ennreal q2\<close>
[PROOF STATE]
proof (prove)
using this:
g \<in> space\<^sub>N (\<LL> (ennreal q2) M)

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

goal (1 subgoal):
 1. \<lbrakk>f \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<And>M. space\<^sub>N (\<LL> (ennreal p2) M) = {f \<in> borel_measurable M. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)}\<rbrakk> \<Longrightarrow> integrable M (\<lambda>x. \<bar>g x\<bar> powr q2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>LINT x|M. \<bar>f x\<bar> powr r2 * \<bar>g x\<bar> powr r2\<bar> powr (1 / r2) \<le> ((LINT x|M. \<bar>\<bar>f x\<bar> powr r2\<bar> powr P) powr (1 / P) * (LINT x|M. \<bar>\<bar>g x\<bar> powr r2\<bar> powr Q) powr (1 / Q)) powr (1 / r2)

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>LINT x|M. \<bar>f x\<bar> powr r2 * \<bar>g x\<bar> powr r2\<bar> powr (1 / r2) \<le> ((LINT x|M. \<bar>\<bar>f x\<bar> powr r2\<bar> powr P) powr (1 / P) * (LINT x|M. \<bar>\<bar>g x\<bar> powr r2\<bar> powr Q) powr (1 / Q)) powr (1 / r2)

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have "... = (\<integral>x. \<bar>f x\<bar> powr p2 \<partial>M) powr (1/p2) * (\<integral>x. \<bar>g x\<bar> powr q2 \<partial>M) powr (1/q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((LINT x|M. \<bar>\<bar>f x\<bar> powr r2\<bar> powr P) powr (1 / P) * (LINT x|M. \<bar>\<bar>g x\<bar> powr r2\<bar> powr Q) powr (1 / Q)) powr (1 / r2) = (LINT x|M. \<bar>f x\<bar> powr p2) powr (1 / p2) * (LINT x|M. \<bar>g x\<bar> powr q2) powr (1 / q2)
[PROOF STEP]
apply (auto simp add: powr_mult powr_powr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x\<bar> powr (r2 * P)) powr (1 / (P * r2)) * (LINT x|M. \<bar>g x\<bar> powr (r2 * Q)) powr (1 / (Q * r2)) = (LINT x|M. \<bar>f x\<bar> powr p2) powr (1 / p2) * (LINT x|M. \<bar>g x\<bar> powr q2) powr (1 / q2)
[PROOF STEP]
unfolding P_def Q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x\<bar> powr (r2 * (p2 / r2))) powr (1 / (p2 / r2 * r2)) * (LINT x|M. \<bar>g x\<bar> powr (r2 * (q2 / r2))) powr (1 / (q2 / r2 * r2)) = (LINT x|M. \<bar>f x\<bar> powr p2) powr (1 / p2) * (LINT x|M. \<bar>g x\<bar> powr q2) powr (1 / q2)
[PROOF STEP]
using \<open>r2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < r2

goal (1 subgoal):
 1. (LINT x|M. \<bar>f x\<bar> powr (r2 * (p2 / r2))) powr (1 / (p2 / r2 * r2)) * (LINT x|M. \<bar>g x\<bar> powr (r2 * (q2 / r2))) powr (1 / (q2 / r2 * r2)) = (LINT x|M. \<bar>f x\<bar> powr p2) powr (1 / p2) * (LINT x|M. \<bar>g x\<bar> powr q2) powr (1 / q2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((LINT x|M. \<bar>\<bar>f x\<bar> powr r2\<bar> powr P) powr (1 / P) * (LINT x|M. \<bar>\<bar>g x\<bar> powr r2\<bar> powr Q) powr (1 / Q)) powr (1 / r2) = (LINT x|M. \<bar>f x\<bar> powr p2) powr (1 / p2) * (LINT x|M. \<bar>g x\<bar> powr q2) powr (1 / q2)

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((LINT x|M. \<bar>\<bar>f x\<bar> powr r2\<bar> powr P) powr (1 / P) * (LINT x|M. \<bar>\<bar>g x\<bar> powr r2\<bar> powr Q) powr (1 / Q)) powr (1 / r2) = (LINT x|M. \<bar>f x\<bar> powr p2) powr (1 / p2) * (LINT x|M. \<bar>g x\<bar> powr q2) powr (1 / q2)

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have "... = Norm (\<LL> p M) f * Norm (\<LL> q M) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x\<bar> powr p2) powr (1 / p2) * (LINT x|M. \<bar>g x\<bar> powr q2) powr (1 / q2) = Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
unfolding \<open>p = ennreal p2\<close> \<open>q = ennreal q2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x\<bar> powr p2) powr (1 / p2) * (LINT x|M. \<bar>g x\<bar> powr q2) powr (1 / q2) = Norm (\<LL> (ennreal p2) M) f * Norm (\<LL> (ennreal q2) M) g
[PROOF STEP]
using Lp_Norm[OF \<open>p2 > 0\<close>, of _ M] Lp_Norm[OF \<open>q2 > 0\<close>, of _ M]
[PROOF STATE]
proof (prove)
using this:
?f \<in> borel_measurable M \<Longrightarrow> Norm (\<LL> (ennreal p2) M) ?f = (LINT x|M. \<bar>?f x\<bar> powr p2) powr (1 / p2)
?f \<in> borel_measurable M \<Longrightarrow> Norm (\<LL> (ennreal p2) M) ?f powr p2 = LINT x|M. \<bar>?f x\<bar> powr p2
?f \<in> borel_measurable M \<Longrightarrow> Norm (\<LL> (ennreal q2) M) ?f = (LINT x|M. \<bar>?f x\<bar> powr q2) powr (1 / q2)
?f \<in> borel_measurable M \<Longrightarrow> Norm (\<LL> (ennreal q2) M) ?f powr q2 = LINT x|M. \<bar>?f x\<bar> powr q2

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

goal (1 subgoal):
 1. p < \<infinity> \<and> q < \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
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. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
using \<open>(\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)\<close>
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
(\<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) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> 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. r = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
case PInf
[PROOF STATE]
proof (state)
this:
r = \<infinity>

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

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

goal (1 subgoal):
 1. p = \<infinity> &&& q = r
[PROOF STEP]
by (metis add_eq_0_iff_both_eq_0 ennreal_divide_eq_0_iff infinity_ennreal_def not_one_le_zero order.order_iff_strict)+
[PROOF STATE]
proof (state)
this:
p = \<infinity>
q = r

goal (1 subgoal):
 1. r = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have "AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> p M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> p M) f
[PROOF STEP]
using \<open>f \<in> space\<^sub>N (\<LL> p M)\<close> L_infinity_AE_bound
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> p M)
?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> p M) f
[PROOF STEP]
unfolding \<open>p = \<infinity>\<close>
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> \<infinity> M)
?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> p M) f

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

goal (1 subgoal):
 1. AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> p M) f * g x\<bar>
[PROOF STEP]
unfolding abs_mult
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> p M) f

goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> * \<bar>g x\<bar> \<le> \<bar>Norm (\<LL> p M) f\<bar> * \<bar>g x\<bar>
[PROOF STEP]
using Norm_nonneg[of "\<LL> p M" f] mult_right_mono
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> p M) f
0 \<le> Norm (\<LL> p M) f
\<lbrakk>?a \<le> ?b; (0::?'a) \<le> ?c\<rbrakk> \<Longrightarrow> ?a * ?c \<le> ?b * ?c

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

goal (1 subgoal):
 1. r = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have **: "(\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M)
[PROOF STEP]
using spaceN_cmult[OF \<open>g \<in> space\<^sub>N (\<LL> q M)\<close>]
[PROOF STATE]
proof (prove)
using this:
?c *\<^sub>R g \<in> space\<^sub>N (\<LL> q M)

goal (1 subgoal):
 1. (\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M)
[PROOF STEP]
unfolding \<open>q = r\<close> scaleR_fun_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. ?c *\<^sub>R g x) \<in> space\<^sub>N (\<LL> r M)

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

goal (1 subgoal):
 1. r = \<infinity> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
have ***: "Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x) = Norm (\<LL> p M) f * Norm (\<LL> q M) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x) = Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
using Norm_cmult[of "\<LL> r M"]
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (?c *\<^sub>R ?x) = \<bar>?c\<bar> * Norm (\<LL> r M) ?x

goal (1 subgoal):
 1. Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x) = Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
unfolding \<open>q = r\<close> scaleR_fun_def
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (\<lambda>x. ?c *\<^sub>R ?x x) = \<bar>?c\<bar> * Norm (\<LL> r M) ?x

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

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

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
using Lp_domination[of "\<lambda>x. f x * g x" M "\<lambda>x. Norm (\<LL> p M) f * g x" r]
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x) = Norm (\<LL> p M) f * Norm (\<LL> q M) g
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> p M) f * g x\<bar>\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> p M) f * g x\<bar>\<rbrakk> \<Longrightarrow> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x)

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
unfolding \<open>q = r\<close>
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x) = Norm (\<LL> p M) f * Norm (\<LL> r M) g
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> p M) f * g x\<bar>\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> p M) f * g x\<bar>\<rbrakk> \<Longrightarrow> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x)

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> r M) g
[PROOF STEP]
using * ** ***
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x) = Norm (\<LL> p M) f * Norm (\<LL> r M) g
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> p M) f * g x\<bar>\<rbrakk> \<Longrightarrow> (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)
\<lbrakk>(\<lambda>x. f x * g x) \<in> borel_measurable M; (\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M); AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> p M) f * g x\<bar>\<rbrakk> \<Longrightarrow> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x)
AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>Norm (\<LL> p M) f * g x\<bar>
(\<lambda>x. Norm (\<LL> p M) f * g x) \<in> space\<^sub>N (\<LL> r M)
Norm (\<LL> r M) (\<lambda>x. Norm (\<LL> p M) f * g x) = Norm (\<LL> p M) f * Norm (\<LL> q M) g

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g

goal (2 subgoals):
 1. (\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M)
 2. Norm (\<LL> r M) (\<lambda>x. f x * g x) \<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> r M) \<and> Norm (\<LL> r M) (\<lambda>x. f x * g x) \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g
[PROOF STEP]
show "(\<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"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x * g x) \<in> space\<^sub>N (\<LL> r M) \<and> 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. (\<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
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
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:
No subgoals!
[PROOF STEP]
qed