[STATEMENT]
theorem Lp_Lq_duality:
  fixes p q::ennreal
  assumes "f \<in> space\<^sub>N (\<LL> p M)"
          "1/p + 1/q = 1"
          "p = \<infinity> \<Longrightarrow> sigma_finite_measure M"
  shows "bdd_above ((\<lambda>g. (\<integral>x. f x * g x \<partial>M))`{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1})"
        "Norm (\<LL> p M) f = (SUP g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. (\<integral>x. f x * g x \<partial>M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>g. LINT x|M. f x * g x) ` {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}) &&& Norm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bdd_above ((\<lambda>g. LINT x|M. f x * g x) ` {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1})
 2. Norm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have [measurable]: "f \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> borel_measurable M
[PROOF STEP]
using Lp_measurable[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M

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

goal (2 subgoals):
 1. bdd_above ((\<lambda>g. LINT x|M. f x * g x) ` {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1})
 2. Norm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have B: "(\<integral>x. f x * g x \<partial>M) \<le> Norm (\<LL> p M) f" if "g \<in> {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}" for g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * g x \<le> Norm (\<LL> p M) f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. LINT x|M. f x * g x \<le> Norm (\<LL> p M) f
[PROOF STEP]
have g: "g \<in> space\<^sub>N (\<LL> q M)" "Norm (\<LL> q M) g \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<in> space\<^sub>N (\<LL> q M) &&& Norm (\<LL> q M) g \<le> 1
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
g \<in> {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}

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

goal (1 subgoal):
 1. LINT x|M. f x * g x \<le> Norm (\<LL> p M) f
[PROOF STEP]
have "(\<integral>x. f x * g x \<partial>M) \<le> abs(\<integral>x. f x * g x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * g x \<le> \<bar>LINT x|M. f x * g x\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * g x \<le> \<bar>LINT x|M. f x * g x\<bar>

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

goal (1 subgoal):
 1. LINT x|M. f x * g x \<le> Norm (\<LL> p M) f
[PROOF STEP]
have "... \<le> Norm (\<LL> p M) f * Norm (\<LL> q M) g"
[PROOF STATE]
proof (prove)
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]
using Lp_Lq_duality_bound(2)[OF \<open>1/p + 1/q = 1\<close> \<open>f \<in> space\<^sub>N (\<LL> p M)\<close> g(1)]
[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 auto
[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 (1 subgoal):
 1. LINT x|M. f x * g x \<le> Norm (\<LL> p M) f
[PROOF STEP]
also
[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 (1 subgoal):
 1. LINT x|M. f x * g x \<le> Norm (\<LL> p M) f
[PROOF STEP]
have "... \<le> Norm (\<LL> p M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> p M) f * Norm (\<LL> q M) g \<le> Norm (\<LL> p M) f
[PROOF STEP]
using g(2) Norm_nonneg[of "\<LL> p M" f] mult_left_le
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> q M) g \<le> 1
0 \<le> Norm (\<LL> p M) f
\<lbrakk>?c \<le> (1::?'a); (0::?'a) \<le> ?a\<rbrakk> \<Longrightarrow> ?a * ?c \<le> ?a

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

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

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

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

goal (2 subgoals):
 1. bdd_above ((\<lambda>g. LINT x|M. f x * g x) ` {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1})
 2. Norm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?g \<in> {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1} \<Longrightarrow> LINT x|M. f x * ?g x \<le> Norm (\<LL> p M) f
[PROOF STEP]
show "bdd_above ((\<lambda>g. (\<integral>x. f x * g x \<partial>M))`{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1})"
[PROOF STATE]
proof (prove)
using this:
?g \<in> {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1} \<Longrightarrow> LINT x|M. f x * ?g x \<le> Norm (\<LL> p M) f

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

goal (1 subgoal):
 1. Norm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
show "Norm (\<LL> p M) f = (SUP g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. (\<integral>x. f x * g x \<partial>M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> p M) f = (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x) \<le> Norm (\<LL> p M) f
[PROOF STEP]
show "(SUP g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. \<integral>x. f x * g x \<partial>M) \<le> Norm (\<LL> p M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x) \<le> Norm (\<LL> p M) f
[PROOF STEP]
by (rule cSUP_least, auto, rule exI[of _ 0], auto simp add: B)
[PROOF STATE]
proof (state)
this:
(\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x) \<le> Norm (\<LL> p M) f

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

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

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
show "Norm (\<LL> p M) f \<le> (SUP g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. (\<integral>x. f x * g x \<partial>M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
using \<open>p \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> p

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
proof (cases rule: Lp_cases_1_PInf)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. p = 1 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 3. p = \<infinity> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
case PInf
[PROOF STATE]
proof (state)
this:
p = \<infinity>

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

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

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

goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. p = 1 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 3. p = \<infinity> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "q = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q = 1
[PROOF STEP]
using \<open>1/p + 1/q = 1\<close> \<open>p = \<infinity>\<close>
[PROOF STATE]
proof (prove)
using this:
1 / p + 1 / q = 1
p = \<infinity>

goal (1 subgoal):
 1. q = 1
[PROOF STEP]
by (simp add: divide_eq_1_ennreal)
[PROOF STATE]
proof (state)
this:
q = 1

goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. p = 1 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 3. p = \<infinity> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "c \<le> (SUP g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. (\<integral>x. f x * g x \<partial>M))" if "c < Norm (\<LL> p M) f" for c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
proof (cases "c < 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
c < 0

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

goal (1 subgoal):
 1. c \<le> LINT x|M. f x * 0 x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<le> LINT x|M. f x * 0 x

goal (2 subgoals):
 1. c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c \<le> LINT x|M. f x * 0 x

goal (2 subgoals):
 1. c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... \<le> (SUP g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. (\<integral>x. f x * g x \<partial>M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * 0 x \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
apply (rule cSUP_upper, auto simp add: zero_fun_def[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>g. LINT x|M. f x * g x) ` {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1})
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
?g \<in> {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1} \<Longrightarrow> LINT x|M. f x * ?g x \<le> Norm (\<LL> p M) f

goal (1 subgoal):
 1. bdd_above ((\<lambda>g. LINT x|M. f x * g x) ` {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1})
[PROOF STEP]
by (meson bdd_aboveI2)
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * 0 x \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)

goal (2 subgoals):
 1. c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)

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

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

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

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

goal (1 subgoal):
 1. ennreal c < eNorm (\<LL> \<infinity> M) f
[PROOF STEP]
unfolding \<open>p = \<infinity>\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> c < 0
eNorm (\<LL> \<infinity> M) f = ennreal (Norm (\<LL> \<infinity> M) f)
c < Norm (\<LL> \<infinity> M) f
0 \<le> ?r \<Longrightarrow> (ennreal ?r < ennreal ?q) = (?r < ?q)

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

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

goal (1 subgoal):
 1. 0 < emeasure M {x \<in> space M. c < \<bar>f x\<bar>}
[PROOF STEP]
using L_infinity_pos_measure[of f M c]
[PROOF STATE]
proof (prove)
using this:
ennreal c < eNorm (\<LL> \<infinity> M) f
\<lbrakk>f \<in> borel_measurable M; ennreal c < eNorm (\<LL> \<infinity> M) f\<rbrakk> \<Longrightarrow> 0 < emeasure M {x \<in> space M. c < \<bar>f x\<bar>}

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

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

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

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

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have [measurable]: "Y n \<in> sets M" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y n \<in> sets M
[PROOF STEP]
unfolding Y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> A n. c < \<bar>f x\<bar>} \<in> sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y ?n \<in> sets M

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "{x \<in> space M. \<bar>f x\<bar> > c} = (\<Union>n. Y n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> space M. c < \<bar>f x\<bar>} = \<Union> (range Y)
[PROOF STEP]
unfolding Y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> space M. c < \<bar>f x\<bar>} = (\<Union>n. {x \<in> A n. c < \<bar>f x\<bar>})
[PROOF STEP]
using \<open>(\<Union>i. A i) = space M\<close>
[PROOF STATE]
proof (prove)
using this:
\<Union> (range A) = space M

goal (1 subgoal):
 1. {x \<in> space M. c < \<bar>f x\<bar>} = (\<Union>n. {x \<in> A n. c < \<bar>f x\<bar>})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x \<in> space M. c < \<bar>f x\<bar>} = \<Union> (range Y)

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{x \<in> space M. c < \<bar>f x\<bar>} = \<Union> (range Y)
[PROOF STEP]
have "emeasure M (\<Union>n. Y n) > 0"
[PROOF STATE]
proof (prove)
using this:
{x \<in> space M. c < \<bar>f x\<bar>} = \<Union> (range Y)

goal (1 subgoal):
 1. 0 < emeasure M (\<Union> (range Y))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
{x \<in> space M. c < \<bar>f x\<bar>} = \<Union> (range Y)
0 < emeasure M {x \<in> space M. c < \<bar>f x\<bar>}

goal (1 subgoal):
 1. 0 < emeasure M (\<Union> (range Y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < emeasure M (\<Union> (range Y))

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < emeasure M (\<Union> (range Y))
[PROOF STEP]
obtain n where "emeasure M (Y n) > 0"
[PROOF STATE]
proof (prove)
using this:
0 < emeasure M (\<Union> (range Y))

goal (1 subgoal):
 1. (\<And>n. 0 < emeasure M (Y n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using emeasure_pos_unionE[of Y, OF \<open>\<And>n. Y n \<in> sets M\<close>]
[PROOF STATE]
proof (prove)
using this:
0 < emeasure M (\<Union> (range Y))
0 < emeasure M (\<Union> (range Y)) \<Longrightarrow> \<exists>N. 0 < emeasure M (Y N)

goal (1 subgoal):
 1. (\<And>n. 0 < emeasure M (Y n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < emeasure M (Y n)

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "emeasure M (Y n) \<le> emeasure M (A n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure M (Y n) \<le> emeasure M (A n)
[PROOF STEP]
apply (rule emeasure_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Y n \<subseteq> A n
 2. A n \<in> sets M
[PROOF STEP]
unfolding Y_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {x \<in> A n. c < \<bar>f x\<bar>} \<subseteq> A n
 2. A n \<in> sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
emeasure M (Y n) \<le> emeasure M (A n)

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
emeasure M (Y n) \<le> emeasure M (A n)
[PROOF STEP]
have "emeasure M (Y n) \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
using this:
emeasure M (Y n) \<le> emeasure M (A n)

goal (1 subgoal):
 1. emeasure M (Y n) \<noteq> \<infinity>
[PROOF STEP]
using \<open>emeasure M (A n) \<noteq> \<infinity>\<close>
[PROOF STATE]
proof (prove)
using this:
emeasure M (Y n) \<le> emeasure M (A n)
emeasure M (A n) \<noteq> \<infinity>

goal (1 subgoal):
 1. emeasure M (Y n) \<noteq> \<infinity>
[PROOF STEP]
by (metis infinity_ennreal_def neq_top_trans)
[PROOF STATE]
proof (state)
this:
emeasure M (Y n) \<noteq> \<infinity>

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
emeasure M (Y n) \<noteq> \<infinity>
[PROOF STEP]
have "measure M (Y n) > 0"
[PROOF STATE]
proof (prove)
using this:
emeasure M (Y n) \<noteq> \<infinity>

goal (1 subgoal):
 1. 0 < Sigma_Algebra.measure M (Y n)
[PROOF STEP]
using \<open>emeasure M (Y n) > 0\<close>
[PROOF STATE]
proof (prove)
using this:
emeasure M (Y n) \<noteq> \<infinity>
0 < emeasure M (Y n)

goal (1 subgoal):
 1. 0 < Sigma_Algebra.measure M (Y n)
[PROOF STEP]
unfolding measure_def
[PROOF STATE]
proof (prove)
using this:
emeasure M (Y n) \<noteq> \<infinity>
0 < emeasure M (Y n)

goal (1 subgoal):
 1. 0 < enn2real (emeasure M (Y n))
[PROOF STEP]
by (simp add: enn2real_positive_iff top.not_eq_extremum)
[PROOF STATE]
proof (state)
this:
0 < Sigma_Algebra.measure M (Y n)

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "\<bar>f x\<bar> \<ge> c" if "x \<in> Y n" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<le> \<bar>f x\<bar>
[PROOF STEP]
using that less_imp_le
[PROOF STATE]
proof (prove)
using this:
x \<in> Y n
?x < ?y \<Longrightarrow> ?x \<le> ?y

goal (1 subgoal):
 1. c \<le> \<bar>f x\<bar>
[PROOF STEP]
unfolding Y_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {x \<in> A n. c < \<bar>f x\<bar>}
?x < ?y \<Longrightarrow> ?x \<le> ?y

goal (1 subgoal):
 1. c \<le> \<bar>f x\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> Y n \<Longrightarrow> c \<le> \<bar>f ?x\<bar>

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
define g where "g = (\<lambda>x. indicator (Y n) x * sgn(f x)) /\<^sub>R measure M (Y n)"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>x. indicat_real (Y n) x * sgn (f x)) /\<^sub>R Sigma_Algebra.measure M (Y n)

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "g \<in> space\<^sub>N (\<LL> 1 M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<in> space\<^sub>N (\<LL> 1 M)
[PROOF STEP]
apply (rule Lp_domination[of _ _ "indicator (Y n) /\<^sub>R measure M (Y n)"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. g \<in> borel_measurable M
 2. indicat_real (Y n) /\<^sub>R Sigma_Algebra.measure M (Y n) \<in> space\<^sub>N (\<LL> 1 M)
 3. AE x in M. \<bar>g x\<bar> \<le> \<bar>(indicat_real (Y n) /\<^sub>R Sigma_Algebra.measure M (Y n)) x\<bar>
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>x. indicat_real (Y n) x * sgn (f x)) /\<^sub>R Sigma_Algebra.measure M (Y n) \<in> borel_measurable M
 2. indicat_real (Y n) /\<^sub>R Sigma_Algebra.measure M (Y n) \<in> space\<^sub>N (\<LL> 1 M)
 3. AE x in M. \<bar>((\<lambda>x. indicat_real (Y n) x * sgn (f x)) /\<^sub>R Sigma_Algebra.measure M (Y n)) x\<bar> \<le> \<bar>(indicat_real (Y n) /\<^sub>R Sigma_Algebra.measure M (Y n)) x\<bar>
[PROOF STEP]
using L1_indicator'[OF \<open>Y n \<in> sets M\<close> \<open>emeasure M (Y n) \<noteq> \<infinity>\<close>]
[PROOF STATE]
proof (prove)
using this:
indicat_real (Y n) \<in> space\<^sub>N (\<LL> 1 M)
Norm (\<LL> 1 M) (indicat_real (Y n)) = Sigma_Algebra.measure M (Y n)

goal (3 subgoals):
 1. (\<lambda>x. indicat_real (Y n) x * sgn (f x)) /\<^sub>R Sigma_Algebra.measure M (Y n) \<in> borel_measurable M
 2. indicat_real (Y n) /\<^sub>R Sigma_Algebra.measure M (Y n) \<in> space\<^sub>N (\<LL> 1 M)
 3. AE x in M. \<bar>((\<lambda>x. indicat_real (Y n) x * sgn (f x)) /\<^sub>R Sigma_Algebra.measure M (Y n)) x\<bar> \<le> \<bar>(indicat_real (Y n) /\<^sub>R Sigma_Algebra.measure M (Y n)) x\<bar>
[PROOF STEP]
by (auto simp add: abs_mult indicator_def abs_sgn_eq)
[PROOF STATE]
proof (state)
this:
g \<in> space\<^sub>N (\<LL> 1 M)

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "Norm (\<LL> 1 M) g = Norm (\<LL> 1 M) (\<lambda>x. indicator (Y n) x * sgn(f x)) / abs(measure M (Y n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> 1 M) g = Norm (\<LL> 1 M) (\<lambda>x. indicat_real (Y n) x * sgn (f x)) / \<bar>Sigma_Algebra.measure M (Y n)\<bar>
[PROOF STEP]
unfolding g_def Norm_cmult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>inverse (Sigma_Algebra.measure M (Y n))\<bar> * Norm (\<LL> 1 M) (\<lambda>x. indicat_real (Y n) x * sgn (f x)) = Norm (\<LL> 1 M) (\<lambda>x. indicat_real (Y n) x * sgn (f x)) / \<bar>Sigma_Algebra.measure M (Y n)\<bar>
[PROOF STEP]
by (simp add: divide_inverse)
[PROOF STATE]
proof (state)
this:
Norm (\<LL> 1 M) g = Norm (\<LL> 1 M) (\<lambda>x. indicat_real (Y n) x * sgn (f x)) / \<bar>Sigma_Algebra.measure M (Y n)\<bar>

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Norm (\<LL> 1 M) g = Norm (\<LL> 1 M) (\<lambda>x. indicat_real (Y n) x * sgn (f x)) / \<bar>Sigma_Algebra.measure M (Y n)\<bar>

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... \<le> Norm (\<LL> 1 M) (indicator (Y n)) / abs(measure M (Y n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> 1 M) (\<lambda>x. indicat_real (Y n) x * sgn (f x)) / \<bar>Sigma_Algebra.measure M (Y n)\<bar> \<le> Norm (\<LL> 1 M) (indicat_real (Y n)) / \<bar>Sigma_Algebra.measure M (Y n)\<bar>
[PROOF STEP]
using \<open>measure M (Y n) > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < Sigma_Algebra.measure M (Y n)

goal (1 subgoal):
 1. Norm (\<LL> 1 M) (\<lambda>x. indicat_real (Y n) x * sgn (f x)) / \<bar>Sigma_Algebra.measure M (Y n)\<bar> \<le> Norm (\<LL> 1 M) (indicat_real (Y n)) / \<bar>Sigma_Algebra.measure M (Y n)\<bar>
[PROOF STEP]
apply (auto simp add: divide_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < Sigma_Algebra.measure M (Y n) \<Longrightarrow> Norm (\<LL> 1 M) (\<lambda>x. indicat_real (Y n) x * sgn (f x)) \<le> Norm (\<LL> 1 M) (indicat_real (Y n))
[PROOF STEP]
apply (rule Lp_domination)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 0 < Sigma_Algebra.measure M (Y n) \<Longrightarrow> (\<lambda>x. indicat_real (Y n) x * sgn (f x)) \<in> borel_measurable M
 2. 0 < Sigma_Algebra.measure M (Y n) \<Longrightarrow> indicat_real (Y n) \<in> space\<^sub>N (\<LL> 1 M)
 3. 0 < Sigma_Algebra.measure M (Y n) \<Longrightarrow> AE x in M. \<bar>indicat_real (Y n) x * sgn (f x)\<bar> \<le> \<bar>indicat_real (Y n) x\<bar>
[PROOF STEP]
using L1_indicator'[OF \<open>Y n \<in> sets M\<close> \<open>emeasure M (Y n) \<noteq> \<infinity>\<close>]
[PROOF STATE]
proof (prove)
using this:
indicat_real (Y n) \<in> space\<^sub>N (\<LL> 1 M)
Norm (\<LL> 1 M) (indicat_real (Y n)) = Sigma_Algebra.measure M (Y n)

goal (3 subgoals):
 1. 0 < Sigma_Algebra.measure M (Y n) \<Longrightarrow> (\<lambda>x. indicat_real (Y n) x * sgn (f x)) \<in> borel_measurable M
 2. 0 < Sigma_Algebra.measure M (Y n) \<Longrightarrow> indicat_real (Y n) \<in> space\<^sub>N (\<LL> 1 M)
 3. 0 < Sigma_Algebra.measure M (Y n) \<Longrightarrow> AE x in M. \<bar>indicat_real (Y n) x * sgn (f x)\<bar> \<le> \<bar>indicat_real (Y n) x\<bar>
[PROOF STEP]
by (auto simp add: abs_mult indicator_def abs_sgn_eq)
[PROOF STATE]
proof (state)
this:
Norm (\<LL> 1 M) (\<lambda>x. indicat_real (Y n) x * sgn (f x)) / \<bar>Sigma_Algebra.measure M (Y n)\<bar> \<le> Norm (\<LL> 1 M) (indicat_real (Y n)) / \<bar>Sigma_Algebra.measure M (Y n)\<bar>

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Norm (\<LL> 1 M) (\<lambda>x. indicat_real (Y n) x * sgn (f x)) / \<bar>Sigma_Algebra.measure M (Y n)\<bar> \<le> Norm (\<LL> 1 M) (indicat_real (Y n)) / \<bar>Sigma_Algebra.measure M (Y n)\<bar>

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... = measure M (Y n) / abs(measure M (Y n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> 1 M) (indicat_real (Y n)) / \<bar>Sigma_Algebra.measure M (Y n)\<bar> = Sigma_Algebra.measure M (Y n) / \<bar>Sigma_Algebra.measure M (Y n)\<bar>
[PROOF STEP]
using L1_indicator'[OF \<open>Y n \<in> sets M\<close> \<open>emeasure M (Y n) \<noteq> \<infinity>\<close>]
[PROOF STATE]
proof (prove)
using this:
indicat_real (Y n) \<in> space\<^sub>N (\<LL> 1 M)
Norm (\<LL> 1 M) (indicat_real (Y n)) = Sigma_Algebra.measure M (Y n)

goal (1 subgoal):
 1. Norm (\<LL> 1 M) (indicat_real (Y n)) / \<bar>Sigma_Algebra.measure M (Y n)\<bar> = Sigma_Algebra.measure M (Y n) / \<bar>Sigma_Algebra.measure M (Y n)\<bar>
[PROOF STEP]
by (auto simp add: abs_mult indicator_def abs_sgn_eq)
[PROOF STATE]
proof (state)
this:
Norm (\<LL> 1 M) (indicat_real (Y n)) / \<bar>Sigma_Algebra.measure M (Y n)\<bar> = Sigma_Algebra.measure M (Y n) / \<bar>Sigma_Algebra.measure M (Y n)\<bar>

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Norm (\<LL> 1 M) (indicat_real (Y n)) / \<bar>Sigma_Algebra.measure M (Y n)\<bar> = Sigma_Algebra.measure M (Y n) / \<bar>Sigma_Algebra.measure M (Y n)\<bar>

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma_Algebra.measure M (Y n) / \<bar>Sigma_Algebra.measure M (Y n)\<bar> = 1
[PROOF STEP]
using \<open>measure M (Y n) > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < Sigma_Algebra.measure M (Y n)

goal (1 subgoal):
 1. Sigma_Algebra.measure M (Y n) / \<bar>Sigma_Algebra.measure M (Y n)\<bar> = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Sigma_Algebra.measure M (Y n) / \<bar>Sigma_Algebra.measure M (Y n)\<bar> = 1

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Norm (\<LL> 1 M) g \<le> 1
[PROOF STEP]
have "Norm (\<LL> 1 M) g \<le> 1"
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> 1 M) g \<le> 1

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

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "c * measure M (Y n) = (\<integral>x. c * indicator (Y n) x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * Sigma_Algebra.measure M (Y n) = LINT x|M. c * indicat_real (Y n) x
[PROOF STEP]
using \<open>measure M (Y n) > 0\<close> \<open>emeasure M (Y n) \<noteq> \<infinity>\<close>
[PROOF STATE]
proof (prove)
using this:
0 < Sigma_Algebra.measure M (Y n)
emeasure M (Y n) \<noteq> \<infinity>

goal (1 subgoal):
 1. c * Sigma_Algebra.measure M (Y n) = LINT x|M. c * indicat_real (Y n) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c * Sigma_Algebra.measure M (Y n) = LINT x|M. c * indicat_real (Y n) x

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c * Sigma_Algebra.measure M (Y n) = LINT x|M. c * indicat_real (Y n) x

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... \<le> (\<integral>x. \<bar>f x\<bar> * indicator (Y n) x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. c * indicat_real (Y n) x \<le> LINT x|M. \<bar>f x\<bar> * indicat_real (Y n) x
[PROOF STEP]
apply (rule integral_mono)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. integrable M (\<lambda>x. c * indicat_real (Y n) x)
 2. integrable M (\<lambda>x. \<bar>f x\<bar> * indicat_real (Y n) x)
 3. \<And>x. x \<in> space M \<Longrightarrow> c * indicat_real (Y n) x \<le> \<bar>f x\<bar> * indicat_real (Y n) x
[PROOF STEP]
using \<open>emeasure M (Y n) \<noteq> \<infinity>\<close> \<open>0 < Sigma_Algebra.measure M (Y n)\<close> not_integrable_integral_eq
[PROOF STATE]
proof (prove)
using this:
emeasure M (Y n) \<noteq> \<infinity>
0 < Sigma_Algebra.measure M (Y n)
\<not> integrable ?M ?f \<Longrightarrow> integral\<^sup>L ?M ?f = (0::?'b)

goal (3 subgoals):
 1. integrable M (\<lambda>x. c * indicat_real (Y n) x)
 2. integrable M (\<lambda>x. \<bar>f x\<bar> * indicat_real (Y n) x)
 3. \<And>x. x \<in> space M \<Longrightarrow> c * indicat_real (Y n) x \<le> \<bar>f x\<bar> * indicat_real (Y n) x
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> * indicat_real (Y n) x)
 2. \<And>x. x \<in> space M \<Longrightarrow> c * indicat_real (Y n) x \<le> \<bar>f x\<bar> * indicat_real (Y n) x
[PROOF STEP]
apply (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. Norm (\<LL> \<infinity> M) f * indicator (Y n) x"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. integrable M (\<lambda>x. Norm (\<LL> \<infinity> M) f * indicat_real (Y n) x)
 2. (\<lambda>x. \<bar>f x\<bar> * indicat_real (Y n) x) \<in> borel_measurable M
 3. AE x in M. norm (\<bar>f x\<bar> * indicat_real (Y n) x) \<le> norm (Norm (\<LL> \<infinity> M) f * indicat_real (Y n) x)
 4. \<And>x. x \<in> space M \<Longrightarrow> c * indicat_real (Y n) x \<le> \<bar>f x\<bar> * indicat_real (Y n) x
[PROOF STEP]
using \<open>emeasure M (Y n) \<noteq> \<infinity>\<close> \<open>0 < Sigma_Algebra.measure M (Y n)\<close> not_integrable_integral_eq
[PROOF STATE]
proof (prove)
using this:
emeasure M (Y n) \<noteq> \<infinity>
0 < Sigma_Algebra.measure M (Y n)
\<not> integrable ?M ?f \<Longrightarrow> integral\<^sup>L ?M ?f = (0::?'b)

goal (4 subgoals):
 1. integrable M (\<lambda>x. Norm (\<LL> \<infinity> M) f * indicat_real (Y n) x)
 2. (\<lambda>x. \<bar>f x\<bar> * indicat_real (Y n) x) \<in> borel_measurable M
 3. AE x in M. norm (\<bar>f x\<bar> * indicat_real (Y n) x) \<le> norm (Norm (\<LL> \<infinity> M) f * indicat_real (Y n) x)
 4. \<And>x. x \<in> space M \<Longrightarrow> c * indicat_real (Y n) x \<le> \<bar>f x\<bar> * indicat_real (Y n) x
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>x. \<bar>f x\<bar> * indicat_real (Y n) x) \<in> borel_measurable M
 2. AE x in M. norm (\<bar>f x\<bar> * indicat_real (Y n) x) \<le> norm (Norm (\<LL> \<infinity> M) f * indicat_real (Y n) x)
 3. \<And>x. x \<in> space M \<Longrightarrow> c * indicat_real (Y n) x \<le> \<bar>f x\<bar> * indicat_real (Y n) x
[PROOF STEP]
using L_infinity_AE_bound[OF \<open>f \<in> space\<^sub>N (\<LL> \<infinity> M)\<close>]
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f

goal (3 subgoals):
 1. (\<lambda>x. \<bar>f x\<bar> * indicat_real (Y n) x) \<in> borel_measurable M
 2. AE x in M. norm (\<bar>f x\<bar> * indicat_real (Y n) x) \<le> norm (Norm (\<LL> \<infinity> M) f * indicat_real (Y n) x)
 3. \<And>x. x \<in> space M \<Longrightarrow> c * indicat_real (Y n) x \<le> \<bar>f x\<bar> * indicat_real (Y n) x
[PROOF STEP]
by (auto simp add: indicator_def Y_def)
[PROOF STATE]
proof (state)
this:
LINT x|M. c * indicat_real (Y n) x \<le> LINT x|M. \<bar>f x\<bar> * indicat_real (Y n) x

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
c * Sigma_Algebra.measure M (Y n) \<le> LINT x|M. \<bar>f x\<bar> * indicat_real (Y n) x
[PROOF STEP]
have "c \<le> (\<integral>x. \<bar>f x\<bar> * indicator (Y n) x \<partial>M) / measure M (Y n)"
[PROOF STATE]
proof (prove)
using this:
c * Sigma_Algebra.measure M (Y n) \<le> LINT x|M. \<bar>f x\<bar> * indicat_real (Y n) x

goal (1 subgoal):
 1. c \<le> (LINT x|M. \<bar>f x\<bar> * indicat_real (Y n) x) / Sigma_Algebra.measure M (Y n)
[PROOF STEP]
using \<open>measure M (Y n) > 0\<close>
[PROOF STATE]
proof (prove)
using this:
c * Sigma_Algebra.measure M (Y n) \<le> LINT x|M. \<bar>f x\<bar> * indicat_real (Y n) x
0 < Sigma_Algebra.measure M (Y n)

goal (1 subgoal):
 1. c \<le> (LINT x|M. \<bar>f x\<bar> * indicat_real (Y n) x) / Sigma_Algebra.measure M (Y n)
[PROOF STEP]
by (auto simp add: divide_simps)
[PROOF STATE]
proof (state)
this:
c \<le> (LINT x|M. \<bar>f x\<bar> * indicat_real (Y n) x) / Sigma_Algebra.measure M (Y n)

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c \<le> (LINT x|M. \<bar>f x\<bar> * indicat_real (Y n) x) / Sigma_Algebra.measure M (Y n)

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... = (\<integral>x. f x * indicator (Y n) x * sgn(f x) / measure M (Y n) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x\<bar> * indicat_real (Y n) x) / Sigma_Algebra.measure M (Y n) = LINT x|M. f x * indicat_real (Y n) x * sgn (f x) / Sigma_Algebra.measure M (Y n)
[PROOF STEP]
using \<open>measure M (Y n) > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < Sigma_Algebra.measure M (Y n)

goal (1 subgoal):
 1. (LINT x|M. \<bar>f x\<bar> * indicat_real (Y n) x) / Sigma_Algebra.measure M (Y n) = LINT x|M. f x * indicat_real (Y n) x * sgn (f x) / Sigma_Algebra.measure M (Y n)
[PROOF STEP]
by (simp add: abs_sgn mult.commute mult.left_commute)
[PROOF STATE]
proof (state)
this:
(LINT x|M. \<bar>f x\<bar> * indicat_real (Y n) x) / Sigma_Algebra.measure M (Y n) = LINT x|M. f x * indicat_real (Y n) x * sgn (f x) / Sigma_Algebra.measure M (Y n)

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(LINT x|M. \<bar>f x\<bar> * indicat_real (Y n) x) / Sigma_Algebra.measure M (Y n) = LINT x|M. f x * indicat_real (Y n) x * sgn (f x) / Sigma_Algebra.measure M (Y n)

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... = (\<integral>x. f x * g x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * indicat_real (Y n) x * sgn (f x) / Sigma_Algebra.measure M (Y n) = LINT x|M. f x * g x
[PROOF STEP]
unfolding divide_inverse g_def divideR_apply
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * indicat_real (Y n) x * sgn (f x) * inverse (Sigma_Algebra.measure M (Y n)) = LINT x|M. f x * (indicat_real (Y n) x * sgn (f x) /\<^sub>R Sigma_Algebra.measure M (Y n))
[PROOF STEP]
by (auto simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * indicat_real (Y n) x * sgn (f x) / Sigma_Algebra.measure M (Y n) = LINT x|M. f x * g x

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * indicat_real (Y n) x * sgn (f x) / Sigma_Algebra.measure M (Y n) = LINT x|M. f x * g x

goal (1 subgoal):
 1. \<not> c < 0 \<Longrightarrow> c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... \<le> (SUP g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. (\<integral>x. f x * g x \<partial>M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * g x \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
unfolding \<open>q = 1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * g x \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> 1 M). Norm (\<LL> 1 M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
apply (rule cSUP_upper, auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. g \<in> space\<^sub>N (\<LL> 1 M)
 2. Norm (\<LL> 1 M) g \<le> 1
 3. bdd_above ((\<lambda>g. LINT x|M. f x * g x) ` {g \<in> space\<^sub>N (\<LL> 1 M). Norm (\<LL> 1 M) g \<le> 1})
[PROOF STEP]
using \<open>g \<in> space\<^sub>N (\<LL> 1 M)\<close> \<open>Norm (\<LL> 1 M) g \<le> 1\<close>
[PROOF STATE]
proof (prove)
using this:
g \<in> space\<^sub>N (\<LL> 1 M)
Norm (\<LL> 1 M) g \<le> 1

goal (3 subgoals):
 1. g \<in> space\<^sub>N (\<LL> 1 M)
 2. Norm (\<LL> 1 M) g \<le> 1
 3. bdd_above ((\<lambda>g. LINT x|M. f x * g x) ` {g \<in> space\<^sub>N (\<LL> 1 M). Norm (\<LL> 1 M) g \<le> 1})
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g \<in> space\<^sub>N (\<LL> 1 M); Norm (\<LL> 1 M) g \<le> 1\<rbrakk> \<Longrightarrow> bdd_above ((\<lambda>g. LINT x|M. f x * g x) ` {g \<in> space\<^sub>N (\<LL> 1 M). Norm (\<LL> 1 M) g \<le> 1})
[PROOF STEP]
using B \<open>p = \<infinity>\<close> \<open>q = 1\<close>
[PROOF STATE]
proof (prove)
using this:
?g \<in> {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1} \<Longrightarrow> LINT x|M. f x * ?g x \<le> Norm (\<LL> p M) f
p = \<infinity>
q = 1

goal (1 subgoal):
 1. \<lbrakk>g \<in> space\<^sub>N (\<LL> 1 M); Norm (\<LL> 1 M) g \<le> 1\<rbrakk> \<Longrightarrow> bdd_above ((\<lambda>g. LINT x|M. f x * g x) ` {g \<in> space\<^sub>N (\<LL> 1 M). Norm (\<LL> 1 M) g \<le> 1})
[PROOF STEP]
by (meson bdd_aboveI2)
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * g x \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)

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

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

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

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

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
using dense_le
[PROOF STATE]
proof (prove)
using this:
?c < Norm (\<LL> p M) f \<Longrightarrow> ?c \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
(\<And>x. x < ?y \<Longrightarrow> x \<le> ?z) \<Longrightarrow> ?y \<le> ?z

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

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. p = 1 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. p = 1 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
case one
[PROOF STATE]
proof (state)
this:
p = 1

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

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

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

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. p = 1 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
define g where "g = (\<lambda>x. sgn (f x))"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>x. sgn (f x))

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. p = 1 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have [measurable]: "g \<in> space\<^sub>N (\<LL> \<infinity> M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
apply (rule L_infinity_I[of g M 1])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. g \<in> borel_measurable M
 2. AE x in M. \<bar>g x\<bar> \<le> 1
 3. 0 \<le> 1
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>x. sgn (f x)) \<in> borel_measurable M
 2. AE x in M. \<bar>sgn (f x)\<bar> \<le> 1
 3. 0 \<le> 1
[PROOF STEP]
by (auto simp add: abs_sgn_eq)
[PROOF STATE]
proof (state)
this:
g \<in> space\<^sub>N (\<LL> \<infinity> M)

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. p = 1 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "Norm (\<LL> \<infinity> M) g \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> \<infinity> M) g \<le> 1
[PROOF STEP]
apply (rule L_infinity_I[of g M 1])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. g \<in> borel_measurable M
 2. AE x in M. \<bar>g x\<bar> \<le> 1
 3. 0 \<le> 1
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>x. sgn (f x)) \<in> borel_measurable M
 2. AE x in M. \<bar>sgn (f x)\<bar> \<le> 1
 3. 0 \<le> 1
[PROOF STEP]
by (auto simp add: abs_sgn_eq)
[PROOF STATE]
proof (state)
this:
Norm (\<LL> \<infinity> M) g \<le> 1

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. p = 1 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "Norm (\<LL> p M) f = (\<integral>x. \<bar>f x\<bar> \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> p M) f = LINT x|M. \<bar>f x\<bar>
[PROOF STEP]
unfolding \<open>p = 1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> 1 M) f = LINT x|M. \<bar>f x\<bar>
[PROOF STEP]
apply (rule L1_D(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> 1 M)
[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 (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> 1 M)
[PROOF STEP]
unfolding \<open>p = 1\<close>
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> 1 M)

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

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. p = 1 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Norm (\<LL> p M) f = LINT x|M. \<bar>f x\<bar>

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. p = 1 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... = (\<integral>x. f x * g x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. \<bar>f x\<bar> = LINT x|M. f x * g x
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. \<bar>f x\<bar> = LINT x|M. f x * sgn (f x)
[PROOF STEP]
by (simp add: abs_sgn)
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>f x\<bar> = LINT x|M. f x * g x

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. p = 1 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>f x\<bar> = LINT x|M. f x * g x

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. p = 1 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... \<le> (SUP g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. (\<integral>x. f x * g x \<partial>M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * g x \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
unfolding \<open>q = \<infinity>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * g x \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> \<infinity> M). Norm (\<LL> \<infinity> M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
apply (rule cSUP_upper, auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. g \<in> space\<^sub>N (\<LL> \<top> M)
 2. Norm (\<LL> \<top> M) g \<le> 1
 3. bdd_above ((\<lambda>x. LINT xa|M. f xa * x xa) ` {g \<in> space\<^sub>N (\<LL> \<top> M). Norm (\<LL> \<top> M) g \<le> 1})
[PROOF STEP]
using \<open>g \<in> space\<^sub>N (\<LL> \<infinity> M)\<close> \<open>Norm (\<LL> \<infinity> M) g \<le> 1\<close>
[PROOF STATE]
proof (prove)
using this:
g \<in> space\<^sub>N (\<LL> \<infinity> M)
Norm (\<LL> \<infinity> M) g \<le> 1

goal (3 subgoals):
 1. g \<in> space\<^sub>N (\<LL> \<top> M)
 2. Norm (\<LL> \<top> M) g \<le> 1
 3. bdd_above ((\<lambda>x. LINT xa|M. f xa * x xa) ` {g \<in> space\<^sub>N (\<LL> \<top> M). Norm (\<LL> \<top> M) g \<le> 1})
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g \<in> space\<^sub>N (\<LL> \<top> M); Norm (\<LL> \<top> M) g \<le> 1\<rbrakk> \<Longrightarrow> bdd_above ((\<lambda>x. LINT xa|M. f xa * x xa) ` {g \<in> space\<^sub>N (\<LL> \<top> M). Norm (\<LL> \<top> M) g \<le> 1})
[PROOF STEP]
using B \<open>q = \<infinity>\<close>
[PROOF STATE]
proof (prove)
using this:
?g \<in> {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1} \<Longrightarrow> LINT x|M. f x * ?g x \<le> Norm (\<LL> p M) f
q = \<infinity>

goal (1 subgoal):
 1. \<lbrakk>g \<in> space\<^sub>N (\<LL> \<top> M); Norm (\<LL> \<top> M) g \<le> 1\<rbrakk> \<Longrightarrow> bdd_above ((\<lambda>x. LINT xa|M. f xa * x xa) ` {g \<in> space\<^sub>N (\<LL> \<top> M). Norm (\<LL> \<top> M) g \<le> 1})
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * g x \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)

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

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

goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
case (gr p2)
[PROOF STATE]
proof (state)
this:
p = ennreal p2
1 < p2
1 < p

goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = ennreal p2
1 < p2
1 < p
[PROOF STEP]
have "p2 > 0"
[PROOF STATE]
proof (prove)
using this:
p = ennreal p2
1 < p2
1 < p

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

goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "f \<in> space\<^sub>N (\<LL> p2 M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> (ennreal p2) M)
[PROOF STEP]
using \<open>f \<in> space\<^sub>N (\<LL> p M)\<close> \<open>p = ennreal p2\<close>
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> p M)
p = ennreal p2

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

goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
define q2 where "q2 = conjugate_exponent p2"
[PROOF STATE]
proof (state)
this:
q2 = conjugate_exponent p2

goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "q2 > 1" "q2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < q2 &&& 0 < q2
[PROOF STEP]
using conjugate_exponent_real(2)[OF \<open>p2 > 1\<close>]
[PROOF STATE]
proof (prove)
using this:
1 < conjugate_exponent p2

goal (1 subgoal):
 1. 1 < q2 &&& 0 < q2
[PROOF STEP]
unfolding q2_def
[PROOF STATE]
proof (prove)
using this:
1 < conjugate_exponent p2

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

goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "q = ennreal q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q = ennreal q2
[PROOF STEP]
unfolding q2_def conjugate_exponent_real_ennreal[OF \<open>p2 > 1\<close>, symmetric] \<open>p = ennreal p2\<close>[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q = conjugate_exponent p
[PROOF STEP]
using conjugate_exponent_ennreal_iff[OF \<open>p \<ge> 1\<close>] \<open>1/p + 1/q = 1\<close>
[PROOF STATE]
proof (prove)
using this:
(?q = conjugate_exponent p) = (1 / p + 1 / ?q = 1)
1 / p + 1 / q = 1

goal (1 subgoal):
 1. q = conjugate_exponent p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q = ennreal q2

goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
proof (cases "Norm (\<LL> p M) f = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Norm (\<LL> p M) f = 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Norm (\<LL> p M) f = 0

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

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

goal (2 subgoals):
 1. Norm (\<LL> p M) f = 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Norm (\<LL> p M) f \<le> LINT x|M. f x * 0 x

goal (2 subgoals):
 1. Norm (\<LL> p M) f = 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
 2. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... \<le> (SUP g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. (\<integral>x. f x * g x \<partial>M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * 0 x \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
apply (rule cSUP_upper, auto simp add: zero_fun_def[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>g. LINT x|M. f x * g x) ` {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1})
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
?g \<in> {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1} \<Longrightarrow> LINT x|M. f x * ?g x \<le> Norm (\<LL> p M) f

goal (1 subgoal):
 1. bdd_above ((\<lambda>g. LINT x|M. f x * g x) ` {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1})
[PROOF STEP]
by (meson bdd_aboveI2)
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * 0 x \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)

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

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

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

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

goal (1 subgoal):
 1. 0 < Norm (\<LL> (ennreal p2) M) f
[PROOF STEP]
unfolding \<open>p = ennreal p2\<close>
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> (ennreal p2) M) f \<noteq> 0

goal (1 subgoal):
 1. 0 < Norm (\<LL> (ennreal p2) M) f
[PROOF STEP]
using Norm_nonneg[of "\<LL> p2 M" f]
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> (ennreal p2) M) f \<noteq> 0
0 \<le> Norm (\<LL> (ennreal p2) M) f

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

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
define h where "h = (\<lambda>x. sgn(f x) * \<bar>f x\<bar> powr (p2 - 1))"
[PROOF STATE]
proof (state)
this:
h = (\<lambda>x. sgn (f x) * \<bar>f x\<bar> powr (p2 - 1))

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have [measurable]: "h \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<in> borel_measurable M
[PROOF STEP]
unfolding h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. sgn (f x) * \<bar>f x\<bar> powr (p2 - 1)) \<in> borel_measurable M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h \<in> borel_measurable M

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "(\<integral>\<^sup>+x. \<bar>h x\<bar> powr q2 \<partial>M) = (\<integral>\<^sup>+x. (\<bar>f x\<bar> powr (p2 - 1)) powr q2 \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (\<bar>h x\<bar> powr q2) \<partial>M = \<integral>\<^sup>+ x. ennreal ((\<bar>f x\<bar> powr (p2 - 1)) powr q2) \<partial>M
[PROOF STEP]
unfolding h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (\<bar>sgn (f x) * \<bar>f x\<bar> powr (p2 - 1)\<bar> powr q2) \<partial>M = \<integral>\<^sup>+ x. ennreal ((\<bar>f x\<bar> powr (p2 - 1)) powr q2) \<partial>M
[PROOF STEP]
by (rule nn_integral_cong, auto simp add: abs_mult abs_sgn_eq)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (\<bar>h x\<bar> powr q2) \<partial>M = \<integral>\<^sup>+ x. ennreal ((\<bar>f x\<bar> powr (p2 - 1)) powr q2) \<partial>M

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (\<bar>h x\<bar> powr q2) \<partial>M = \<integral>\<^sup>+ x. ennreal ((\<bar>f x\<bar> powr (p2 - 1)) powr q2) \<partial>M

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... = (\<integral>\<^sup>+x. \<bar>f x\<bar> powr p2 \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal ((\<bar>f x\<bar> powr (p2 - 1)) powr q2) \<partial>M = \<integral>\<^sup>+ x. ennreal (\<bar>f x\<bar> powr p2) \<partial>M
[PROOF STEP]
unfolding powr_powr q2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (\<bar>f x\<bar> powr ((p2 - 1) * conjugate_exponent p2)) \<partial>M = \<integral>\<^sup>+ x. ennreal (\<bar>f x\<bar> powr p2) \<partial>M
[PROOF STEP]
using conjugate_exponent_real(4)[OF \<open>p2 > 1\<close>]
[PROOF STATE]
proof (prove)
using this:
(p2 - 1) * conjugate_exponent p2 = p2

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (\<bar>f x\<bar> powr ((p2 - 1) * conjugate_exponent p2)) \<partial>M = \<integral>\<^sup>+ x. ennreal (\<bar>f x\<bar> powr p2) \<partial>M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal ((\<bar>f x\<bar> powr (p2 - 1)) powr q2) \<partial>M = \<integral>\<^sup>+ x. ennreal (\<bar>f x\<bar> powr p2) \<partial>M

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal ((\<bar>f x\<bar> powr (p2 - 1)) powr q2) \<partial>M = \<integral>\<^sup>+ x. ennreal (\<bar>f x\<bar> powr p2) \<partial>M

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... = (Norm (\<LL> p2 M) f) powr p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (\<bar>f x\<bar> powr p2) \<partial>M = ennreal (Norm (\<LL> (ennreal p2) M) f powr p2)
[PROOF STEP]
apply (subst Lp_Norm(2), auto simp add: \<open>p2 > 0\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (\<bar>f x\<bar> powr p2) \<partial>M = ennreal (LINT x|M. \<bar>f x\<bar> powr p2)
[PROOF STEP]
by (rule nn_integral_eq_integral, auto simp add: Lp_D(2)[OF \<open>p2 > 0\<close> \<open>f \<in> space\<^sub>N (\<LL> p2 M)\<close>])
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (\<bar>f x\<bar> powr p2) \<partial>M = ennreal (Norm (\<LL> (ennreal p2) M) f powr p2)

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (\<bar>h x\<bar> powr q2) \<partial>M = ennreal (Norm (\<LL> (ennreal p2) M) f powr p2)
[PROOF STEP]
have *: "(\<integral>\<^sup>+x. \<bar>h x\<bar> powr q2 \<partial>M) = (Norm (\<LL> p2 M) f) powr p2"
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (\<bar>h x\<bar> powr q2) \<partial>M = ennreal (Norm (\<LL> (ennreal p2) M) f powr p2)

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

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "integrable M (\<lambda>x. \<bar>h x\<bar> powr q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>h x\<bar> powr q2)
[PROOF STEP]
apply (rule integrableI_bounded, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (\<bar>h x\<bar> powr q2) \<partial>M < \<top>
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (\<bar>h x\<bar> powr q2) \<partial>M = ennreal (Norm (\<LL> (ennreal p2) M) f powr p2)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (\<bar>h x\<bar> powr q2) \<partial>M < \<top>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. \<bar>h x\<bar> powr q2)

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
integrable M (\<lambda>x. \<bar>h x\<bar> powr q2)
[PROOF STEP]
have "(\<integral>x. \<bar>h x\<bar> powr q2 \<partial>M) = (\<integral>\<^sup>+x. \<bar>h x\<bar> powr q2 \<partial>M)"
[PROOF STATE]
proof (prove)
using this:
integrable M (\<lambda>x. \<bar>h x\<bar> powr q2)

goal (1 subgoal):
 1. ennreal (LINT x|M. \<bar>h x\<bar> powr q2) = \<integral>\<^sup>+ x. ennreal (\<bar>h x\<bar> powr q2) \<partial>M
[PROOF STEP]
by (rule nn_integral_eq_integral[symmetric], auto)
[PROOF STATE]
proof (state)
this:
ennreal (LINT x|M. \<bar>h x\<bar> powr q2) = \<integral>\<^sup>+ x. ennreal (\<bar>h x\<bar> powr q2) \<partial>M

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ennreal (LINT x|M. \<bar>h x\<bar> powr q2) = \<integral>\<^sup>+ x. ennreal (\<bar>h x\<bar> powr q2) \<partial>M
[PROOF STEP]
have **: "(\<integral>x. \<bar>h x\<bar> powr q2 \<partial>M) = (Norm (\<LL> p2 M) f) powr p2"
[PROOF STATE]
proof (prove)
using this:
ennreal (LINT x|M. \<bar>h x\<bar> powr q2) = \<integral>\<^sup>+ x. ennreal (\<bar>h x\<bar> powr q2) \<partial>M

goal (1 subgoal):
 1. LINT x|M. \<bar>h x\<bar> powr q2 = Norm (\<LL> (ennreal p2) M) f powr p2
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
ennreal (LINT x|M. \<bar>h x\<bar> powr q2) = \<integral>\<^sup>+ x. ennreal (\<bar>h x\<bar> powr q2) \<partial>M
\<integral>\<^sup>+ x. ennreal (\<bar>h x\<bar> powr q2) \<partial>M = ennreal (Norm (\<LL> (ennreal p2) M) f powr p2)

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

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
define g where "g = (\<lambda>x. h x / (Norm (\<LL> p2 M) f) powr (p2 / q2))"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>x. h x / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2))

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have [measurable]: "g \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<in> borel_measurable M
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. h x / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)) \<in> borel_measurable M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> borel_measurable M

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have intg: "integrable M (\<lambda>x. \<bar>g x\<bar> powr q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>g x\<bar> powr q2)
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>h x / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)\<bar> powr q2)
[PROOF STEP]
using \<open>Norm (\<LL> p2 M) f > 0\<close> \<open>q2 > 1\<close>
[PROOF STATE]
proof (prove)
using this:
0 < Norm (\<LL> (ennreal p2) M) f
1 < q2

goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>h x / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)\<bar> powr q2)
[PROOF STEP]
apply (simp add: abs_mult powr_divide powr_powr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < Norm (\<LL> (ennreal p2) M) f; 1 < q2\<rbrakk> \<Longrightarrow> integrable M (\<lambda>x. \<bar>h x\<bar> powr q2 / Norm (\<LL> (ennreal p2) M) f powr p2)
[PROOF STEP]
using \<open>integrable M (\<lambda>x. \<bar>h x\<bar> powr q2)\<close> integrable_divide_zero
[PROOF STATE]
proof (prove)
using this:
integrable M (\<lambda>x. \<bar>h x\<bar> powr q2)
(?c \<noteq> (0::?'b) \<Longrightarrow> integrable ?M ?f) \<Longrightarrow> integrable ?M (\<lambda>x. ?f x / ?c)

goal (1 subgoal):
 1. \<lbrakk>0 < Norm (\<LL> (ennreal p2) M) f; 1 < q2\<rbrakk> \<Longrightarrow> integrable M (\<lambda>x. \<bar>h x\<bar> powr q2 / Norm (\<LL> (ennreal p2) M) f powr p2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. \<bar>g x\<bar> powr q2)

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "g \<in> space\<^sub>N (\<LL> q2 M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<in> space\<^sub>N (\<LL> (ennreal q2) M)
[PROOF STEP]
by (rule Lp_I(1)[OF \<open>q2 > 0\<close> _ intg], auto)
[PROOF STATE]
proof (state)
this:
g \<in> space\<^sub>N (\<LL> (ennreal q2) M)

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "(\<integral>x. \<bar>g x\<bar> powr q2 \<partial>M) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q2 = 1
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. \<bar>h x / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)\<bar> powr q2 = 1
[PROOF STEP]
using \<open>Norm (\<LL> p2 M) f > 0\<close> \<open>q2 > 1\<close>
[PROOF STATE]
proof (prove)
using this:
0 < Norm (\<LL> (ennreal p2) M) f
1 < q2

goal (1 subgoal):
 1. LINT x|M. \<bar>h x / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)\<bar> powr q2 = 1
[PROOF STEP]
by (simp add: abs_mult powr_divide powr_powr **)
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>g x\<bar> powr q2 = 1

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

goal (1 subgoal):
 1. Norm (\<LL> (ennreal q2) M) g = 1
[PROOF STEP]
apply (subst Lp_D[OF \<open>q2 > 0\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. LINT x|M. \<bar>g x\<bar> powr q2 = 1 \<Longrightarrow> g \<in> space\<^sub>N (\<LL> (ennreal q2) M)
 2. LINT x|M. \<bar>g x\<bar> powr q2 = 1 \<Longrightarrow> (LINT x|M. \<bar>g x\<bar> powr q2) powr (1 / q2) = 1
[PROOF STEP]
using \<open>g \<in> space\<^sub>N (\<LL> q2 M)\<close>
[PROOF STATE]
proof (prove)
using this:
g \<in> space\<^sub>N (\<LL> (ennreal q2) M)

goal (2 subgoals):
 1. LINT x|M. \<bar>g x\<bar> powr q2 = 1 \<Longrightarrow> g \<in> space\<^sub>N (\<LL> (ennreal q2) M)
 2. LINT x|M. \<bar>g x\<bar> powr q2 = 1 \<Longrightarrow> (LINT x|M. \<bar>g x\<bar> powr q2) powr (1 / q2) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Norm (\<LL> (ennreal q2) M) g = 1

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "(\<integral>x. f x * g x \<partial>M) = (\<integral>x. f x * sgn(f x) * \<bar>f x\<bar> powr (p2 - 1) / (Norm (\<LL> p2 M) f) powr (p2 / q2) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * g x = LINT x|M. f x * sgn (f x) * \<bar>f x\<bar> powr (p2 - 1) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)
[PROOF STEP]
unfolding g_def h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * (sgn (f x) * \<bar>f x\<bar> powr (p2 - 1) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)) = LINT x|M. f x * sgn (f x) * \<bar>f x\<bar> powr (p2 - 1) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)
[PROOF STEP]
by (simp add: mult.assoc)
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * g x = LINT x|M. f x * sgn (f x) * \<bar>f x\<bar> powr (p2 - 1) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * g x = LINT x|M. f x * sgn (f x) * \<bar>f x\<bar> powr (p2 - 1) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... = (\<integral>x. \<bar>f x\<bar> * \<bar>f x\<bar> powr (p2-1) \<partial>M) / (Norm (\<LL> p2 M) f) powr (p2 / q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * sgn (f x) * \<bar>f x\<bar> powr (p2 - 1) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2) = (LINT x|M. \<bar>f x\<bar> * \<bar>f x\<bar> powr (p2 - 1)) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)
[PROOF STEP]
by (auto simp add: abs_sgn)
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * sgn (f x) * \<bar>f x\<bar> powr (p2 - 1) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2) = (LINT x|M. \<bar>f x\<bar> * \<bar>f x\<bar> powr (p2 - 1)) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * sgn (f x) * \<bar>f x\<bar> powr (p2 - 1) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2) = (LINT x|M. \<bar>f x\<bar> * \<bar>f x\<bar> powr (p2 - 1)) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... = (\<integral>x. \<bar>f x\<bar> powr p2 \<partial>M) / (Norm (\<LL> p2 M) f) powr (p2 / q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x\<bar> * \<bar>f x\<bar> powr (p2 - 1)) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2) = (LINT x|M. \<bar>f x\<bar> powr p2) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)
[PROOF STEP]
by (subst powr_mult_base, auto)
[PROOF STATE]
proof (state)
this:
(LINT x|M. \<bar>f x\<bar> * \<bar>f x\<bar> powr (p2 - 1)) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2) = (LINT x|M. \<bar>f x\<bar> powr p2) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(LINT x|M. \<bar>f x\<bar> * \<bar>f x\<bar> powr (p2 - 1)) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2) = (LINT x|M. \<bar>f x\<bar> powr p2) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... = (Norm (\<LL> p2 M) f) powr p2 / (Norm (\<LL> p2 M) f) powr (p2 / q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x\<bar> powr p2) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2) = Norm (\<LL> (ennreal p2) M) f powr p2 / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)
[PROOF STEP]
by (subst Lp_Norm(2)[OF \<open>p2 > 0\<close>], auto)
[PROOF STATE]
proof (state)
this:
(LINT x|M. \<bar>f x\<bar> powr p2) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2) = Norm (\<LL> (ennreal p2) M) f powr p2 / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(LINT x|M. \<bar>f x\<bar> powr p2) / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2) = Norm (\<LL> (ennreal p2) M) f powr p2 / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2)

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... = (Norm (\<LL> p2 M) f) powr (p2 - p2/q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) f powr p2 / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2) = Norm (\<LL> (ennreal p2) M) f powr (p2 - p2 / q2)
[PROOF STEP]
by (simp add: powr_diff [symmetric] )
[PROOF STATE]
proof (state)
this:
Norm (\<LL> (ennreal p2) M) f powr p2 / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2) = Norm (\<LL> (ennreal p2) M) f powr (p2 - p2 / q2)

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Norm (\<LL> (ennreal p2) M) f powr p2 / Norm (\<LL> (ennreal p2) M) f powr (p2 / q2) = Norm (\<LL> (ennreal p2) M) f powr (p2 - p2 / q2)

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... = Norm (\<LL> p2 M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) f powr (p2 - p2 / q2) = Norm (\<LL> (ennreal p2) M) f
[PROOF STEP]
unfolding q2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) f powr (p2 - p2 / conjugate_exponent p2) = Norm (\<LL> (ennreal p2) M) f
[PROOF STEP]
using conjugate_exponent_real(5)[OF \<open>p2 > 1\<close>]
[PROOF STATE]
proof (prove)
using this:
p2 - p2 / conjugate_exponent p2 = 1

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) f powr (p2 - p2 / conjugate_exponent p2) = Norm (\<LL> (ennreal p2) M) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Norm (\<LL> (ennreal p2) M) f powr (p2 - p2 / q2) = Norm (\<LL> (ennreal p2) M) f

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
LINT x|M. f x * g x = Norm (\<LL> (ennreal p2) M) f
[PROOF STEP]
have "Norm (\<LL> p M) f = (\<integral>x. f x * g x \<partial>M)"
[PROOF STATE]
proof (prove)
using this:
LINT x|M. f x * g x = Norm (\<LL> (ennreal p2) M) f

goal (1 subgoal):
 1. Norm (\<LL> p M) f = LINT x|M. f x * g x
[PROOF STEP]
unfolding \<open>p = ennreal p2\<close>
[PROOF STATE]
proof (prove)
using this:
LINT x|M. f x * g x = Norm (\<LL> (ennreal p2) M) f

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

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

goal (1 subgoal):
 1. Norm (\<LL> p M) f \<noteq> 0 \<Longrightarrow> Norm (\<LL> p M) f \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
have "... \<le> (SUP g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. (\<integral>x. f x * g x \<partial>M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * g x \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
unfolding \<open>q = ennreal q2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * g x \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> (ennreal q2) M). Norm (\<LL> (ennreal q2) M) g \<le> 1}. LINT x|M. f x * g x)
[PROOF STEP]
apply (rule cSUP_upper, auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. g \<in> space\<^sub>N (\<LL> (ennreal q2) M)
 2. Norm (\<LL> (ennreal q2) M) g \<le> 1
 3. bdd_above ((\<lambda>g. LINT x|M. f x * g x) ` {g \<in> space\<^sub>N (\<LL> (ennreal q2) M). Norm (\<LL> (ennreal q2) M) g \<le> 1})
[PROOF STEP]
using \<open>g \<in> space\<^sub>N (\<LL> q2 M)\<close> \<open>Norm (\<LL> q2 M) g = 1\<close>
[PROOF STATE]
proof (prove)
using this:
g \<in> space\<^sub>N (\<LL> (ennreal q2) M)
Norm (\<LL> (ennreal q2) M) g = 1

goal (3 subgoals):
 1. g \<in> space\<^sub>N (\<LL> (ennreal q2) M)
 2. Norm (\<LL> (ennreal q2) M) g \<le> 1
 3. bdd_above ((\<lambda>g. LINT x|M. f x * g x) ` {g \<in> space\<^sub>N (\<LL> (ennreal q2) M). Norm (\<LL> (ennreal q2) M) g \<le> 1})
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g \<in> space\<^sub>N (\<LL> (ennreal q2) M); Norm (\<LL> (ennreal q2) M) g = 1\<rbrakk> \<Longrightarrow> bdd_above ((\<lambda>g. LINT x|M. f x * g x) ` {g \<in> space\<^sub>N (\<LL> (ennreal q2) M). Norm (\<LL> (ennreal q2) M) g \<le> 1})
[PROOF STEP]
using B \<open>q = ennreal q2\<close>
[PROOF STATE]
proof (prove)
using this:
?g \<in> {g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1} \<Longrightarrow> LINT x|M. f x * ?g x \<le> Norm (\<LL> p M) f
q = ennreal q2

goal (1 subgoal):
 1. \<lbrakk>g \<in> space\<^sub>N (\<LL> (ennreal q2) M); Norm (\<LL> (ennreal q2) M) g = 1\<rbrakk> \<Longrightarrow> bdd_above ((\<lambda>g. LINT x|M. f x * g x) ` {g \<in> space\<^sub>N (\<LL> (ennreal q2) M). Norm (\<LL> (ennreal q2) M) g \<le> 1})
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * g x \<le> (\<Squnion>g\<in>{g \<in> space\<^sub>N (\<LL> q M). Norm (\<LL> q M) g \<le> 1}. LINT x|M. f x * g x)

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed