[STATEMENT]
lemma conjugate_exponent_ennreal:
  assumes "p \<ge> (1::ennreal)"
  shows "1/p + 1/(conjugate_exponent p) = 1"
        "conjugate_exponent p \<ge> 1"
        "conjugate_exponent(conjugate_exponent p) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / p + 1 / conjugate_exponent p = 1 &&& 1 \<le> conjugate_exponent p &&& conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 1 / p + 1 / conjugate_exponent p = 1
 2. 1 \<le> conjugate_exponent p
 3. conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
have "(1/p + 1/(conjugate_exponent p) = 1) \<and> (conjugate_exponent p \<ge> 1) \<and> conjugate_exponent(conjugate_exponent p) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
using \<open>p \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> p

goal (1 subgoal):
 1. 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
[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> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
 2. p = 1 \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
 3. p = \<infinity> \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
case (gr p2)
[PROOF STATE]
proof (state)
this:
p = ennreal p2
1 < p2
1 < p

goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
 2. p = 1 \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
 3. p = \<infinity> \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = ennreal p2
1 < p2
1 < p
[PROOF STEP]
have *: "conjugate_exponent p = ennreal (conjugate_exponent p2)"
[PROOF STATE]
proof (prove)
using this:
p = ennreal p2
1 < p2
1 < p

goal (1 subgoal):
 1. conjugate_exponent p = ennreal (conjugate_exponent p2)
[PROOF STEP]
using conjugate_exponent_real_ennreal[OF \<open>p2 > 1\<close>]
[PROOF STATE]
proof (prove)
using this:
p = ennreal p2
1 < p2
1 < p
conjugate_exponent (ennreal p2) = ennreal (conjugate_exponent p2)

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

goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
 2. p = 1 \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
 3. p = \<infinity> \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
have a: "conjugate_exponent p \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> conjugate_exponent p
[PROOF STEP]
using * conjugate_exponent_real[OF \<open>p2 > 1\<close>]
[PROOF STATE]
proof (prove)
using this:
conjugate_exponent p = ennreal (conjugate_exponent p2)
1 / p2 + 1 / conjugate_exponent p2 = 1
1 < conjugate_exponent p2
conjugate_exponent (conjugate_exponent p2) = p2
(p2 - 1) * conjugate_exponent p2 = p2
p2 - p2 / conjugate_exponent p2 = 1

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

goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
 2. p = 1 \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
 3. p = \<infinity> \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
have b: "conjugate_exponent(conjugate_exponent p) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
using conjugate_exponent_real(3)[OF \<open>p2 > 1\<close>] conjugate_exponent_real_ennreal[OF \<open>p2 > 1\<close>]
      conjugate_exponent_real_ennreal[OF conjugate_exponent_real(2)[OF \<open>p2 > 1\<close>]]
[PROOF STATE]
proof (prove)
using this:
conjugate_exponent (conjugate_exponent p2) = p2
conjugate_exponent (ennreal p2) = ennreal (conjugate_exponent p2)
conjugate_exponent (ennreal (conjugate_exponent p2)) = ennreal (conjugate_exponent (conjugate_exponent p2))

goal (1 subgoal):
 1. conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
unfolding * \<open>p = ennreal p2\<close>
[PROOF STATE]
proof (prove)
using this:
conjugate_exponent (conjugate_exponent p2) = p2
conjugate_exponent (ennreal p2) = ennreal (conjugate_exponent p2)
conjugate_exponent (ennreal (conjugate_exponent p2)) = ennreal (conjugate_exponent (conjugate_exponent p2))

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

goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
 2. p = 1 \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
 3. p = \<infinity> \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
have "1 / p + 1 / conjugate_exponent p = ennreal(1/p2 + 1/(conjugate_exponent p2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / p + 1 / conjugate_exponent p = ennreal (1 / p2 + 1 / conjugate_exponent p2)
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / p + 1 / ennreal (conjugate_exponent p2) = ennreal (1 / p2 + 1 / conjugate_exponent p2)
[PROOF STEP]
unfolding \<open>p = ennreal p2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / ennreal p2 + 1 / ennreal (conjugate_exponent p2) = ennreal (1 / p2 + 1 / conjugate_exponent p2)
[PROOF STEP]
using conjugate_exponent_real(2)[OF \<open>p2 > 1\<close>] \<open>p2 > 1\<close>
[PROOF STATE]
proof (prove)
using this:
1 < conjugate_exponent p2
1 < p2

goal (1 subgoal):
 1. 1 / ennreal p2 + 1 / ennreal (conjugate_exponent p2) = ennreal (1 / p2 + 1 / conjugate_exponent p2)
[PROOF STEP]
apply (subst ennreal_plus, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 < conjugate_exponent p2; 1 < p2\<rbrakk> \<Longrightarrow> 1 / ennreal p2 + 1 / ennreal (conjugate_exponent p2) = ennreal (1 / p2) + ennreal (1 / conjugate_exponent p2)
[PROOF STEP]
apply (subst divide_ennreal[symmetric], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 < conjugate_exponent p2; 1 < p2; 1 / ennreal (conjugate_exponent p2) \<noteq> ennreal (1 / conjugate_exponent p2)\<rbrakk> \<Longrightarrow> 1 / ennreal p2 = \<top>
[PROOF STEP]
using divide_ennreal_def inverse_ennreal inverse_eq_divide
[PROOF STATE]
proof (prove)
using this:
?x / ?y = ?x * inverse ?y
0 < ?r \<Longrightarrow> inverse (ennreal ?r) = ennreal (inverse ?r)
inverse ?a = (1::?'a) / ?a

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

goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
 2. p = 1 \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
 3. p = \<infinity> \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 / p + 1 / conjugate_exponent p = ennreal (1 / p2 + 1 / conjugate_exponent p2)
[PROOF STEP]
have c: "1 / p + 1 / conjugate_exponent p = 1"
[PROOF STATE]
proof (prove)
using this:
1 / p + 1 / conjugate_exponent p = ennreal (1 / p2 + 1 / conjugate_exponent p2)

goal (1 subgoal):
 1. 1 / p + 1 / conjugate_exponent p = 1
[PROOF STEP]
using conjugate_exponent_real[OF \<open>p2 > 1\<close>]
[PROOF STATE]
proof (prove)
using this:
1 / p + 1 / conjugate_exponent p = ennreal (1 / p2 + 1 / conjugate_exponent p2)
1 / p2 + 1 / conjugate_exponent p2 = 1
1 < conjugate_exponent p2
conjugate_exponent (conjugate_exponent p2) = p2
(p2 - 1) * conjugate_exponent p2 = p2
p2 - p2 / conjugate_exponent p2 = 1

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

goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
 2. p = 1 \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
 3. p = \<infinity> \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
using a b c
[PROOF STATE]
proof (prove)
using this:
1 \<le> conjugate_exponent p
conjugate_exponent (conjugate_exponent p) = p
1 / p + 1 / conjugate_exponent p = 1

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

goal (2 subgoals):
 1. p = 1 \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
 2. p = \<infinity> \<Longrightarrow> 1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
qed (auto)
[PROOF STATE]
proof (state)
this:
1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p

goal (3 subgoals):
 1. 1 / p + 1 / conjugate_exponent p = 1
 2. 1 \<le> conjugate_exponent p
 3. conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
show "1/p + 1/(conjugate_exponent p) = 1"
            "conjugate_exponent p \<ge> 1"
            "conjugate_exponent(conjugate_exponent p) = p"
[PROOF STATE]
proof (prove)
using this:
1 / p + 1 / conjugate_exponent p = 1 \<and> 1 \<le> conjugate_exponent p \<and> conjugate_exponent (conjugate_exponent p) = p

goal (1 subgoal):
 1. 1 / p + 1 / conjugate_exponent p = 1 &&& 1 \<le> conjugate_exponent p &&& conjugate_exponent (conjugate_exponent p) = p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / p + 1 / conjugate_exponent p = 1
1 \<le> conjugate_exponent p
conjugate_exponent (conjugate_exponent p) = p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma conjugate_exponent_ennreal_iff:
  assumes "p \<ge> (1::ennreal)"
  shows "q = conjugate_exponent p \<longleftrightarrow> (1/p + 1/q = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q = conjugate_exponent p) = (1 / p + 1 / q = 1)
[PROOF STEP]
using conjugate_exponent_ennreal[OF assms]
[PROOF STATE]
proof (prove)
using this:
1 / p + 1 / conjugate_exponent p = 1
1 \<le> conjugate_exponent p
conjugate_exponent (conjugate_exponent p) = p

goal (1 subgoal):
 1. (q = conjugate_exponent p) = (1 / p + 1 / q = 1)
[PROOF STEP]
by (auto, metis ennreal_add_diff_cancel_left ennreal_add_eq_top ennreal_top_neq_one one_divide_one_divide_ennreal)


[STATEMENT]
lemma conjugate_exponent_ennrealI:
  assumes "1/p + 1/q = (1::ennreal)"
  shows "p \<ge> 1" "q \<ge> 1" "p = conjugate_exponent q" "q = conjugate_exponent p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 \<le> p &&& 1 \<le> q) &&& p = conjugate_exponent q &&& q = conjugate_exponent p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. 1 \<le> p
 2. 1 \<le> q
 3. p = conjugate_exponent q
 4. q = conjugate_exponent p
[PROOF STEP]
have "1/p \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / p \<le> 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 / p + 1 / q = 1

goal (1 subgoal):
 1. 1 / p \<le> 1
[PROOF STEP]
using le_iff_add
[PROOF STATE]
proof (prove)
using this:
1 / p + 1 / q = 1
(?a \<le> ?b) = (\<exists>c. ?b = ?a + c)

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

goal (4 subgoals):
 1. 1 \<le> p
 2. 1 \<le> q
 3. p = conjugate_exponent q
 4. q = conjugate_exponent p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 / p \<le> 1
[PROOF STEP]
show "p \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
1 / p \<le> 1

goal (1 subgoal):
 1. 1 \<le> p
[PROOF STEP]
by (metis assms divide_ennreal_def ennreal_add_eq_top ennreal_divide_self ennreal_divide_zero ennreal_le_epsilon ennreal_one_neq_top mult.left_neutral mult_left_le zero_le)
[PROOF STATE]
proof (state)
this:
1 \<le> p

goal (3 subgoals):
 1. 1 \<le> q
 2. p = conjugate_exponent q
 3. q = conjugate_exponent p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 \<le> p
[PROOF STEP]
show "q = conjugate_exponent p"
[PROOF STATE]
proof (prove)
using this:
1 \<le> p

goal (1 subgoal):
 1. q = conjugate_exponent p
[PROOF STEP]
using conjugate_exponent_ennreal_iff assms
[PROOF STATE]
proof (prove)
using this:
1 \<le> p
1 \<le> ?p \<Longrightarrow> (?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 = conjugate_exponent p

goal (2 subgoals):
 1. 1 \<le> q
 2. p = conjugate_exponent q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q = conjugate_exponent p
[PROOF STEP]
show "q \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
q = conjugate_exponent p

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

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

goal (1 subgoal):
 1. p = conjugate_exponent q
[PROOF STEP]
show "p = conjugate_exponent q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = conjugate_exponent q
[PROOF STEP]
using conjugate_exponent_ennreal_iff[OF \<open>q\<ge>1\<close>, of p] assms
[PROOF STATE]
proof (prove)
using this:
(p = conjugate_exponent q) = (1 / q + 1 / p = 1)
1 / p + 1 / q = 1

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in prob_space) bound_L1_Lp:
  assumes "p \<ge> (1::real)"
          "f \<in> borel_measurable M"
          "integrable M (\<lambda>x. \<bar>f x\<bar> powr p)"
  shows "integrable M f"
        "abs(\<integral>x. f x \<partial>M) powr p \<le> (\<integral>x. \<bar>f x\<bar> powr p \<partial>M)"
        "abs(\<integral>x. f x \<partial>M) \<le> (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M f &&& \<bar>expectation f\<bar> powr p \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p) &&& \<bar>expectation f\<bar> \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. integrable M f
 2. \<bar>expectation f\<bar> powr p \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p)
 3. \<bar>expectation f\<bar> \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
have *: "norm x \<le> 1 + (norm x) powr p" for x::real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm x \<le> 1 + norm x powr p
[PROOF STEP]
apply (cases "norm x \<le> 1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. norm x \<le> 1 \<Longrightarrow> norm x \<le> 1 + norm x powr p
 2. \<not> norm x \<le> 1 \<Longrightarrow> norm x \<le> 1 + norm x powr p
[PROOF STEP]
apply (meson le_add_same_cancel1 order.trans powr_ge_pzero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> norm x \<le> 1 \<Longrightarrow> norm x \<le> 1 + norm x powr p
[PROOF STEP]
apply (metis add_le_same_cancel2 assms(1) less_le_trans linear not_less not_one_le_zero powr_le_cancel_iff powr_one_gt_zero_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
norm ?x12 \<le> 1 + norm ?x12 powr p

goal (3 subgoals):
 1. integrable M f
 2. \<bar>expectation f\<bar> powr p \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p)
 3. \<bar>expectation f\<bar> \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
show *: "integrable M f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M f
[PROOF STEP]
apply (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. 1 + \<bar>f x\<bar> powr p"], auto simp add: assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> \<le> 1 + \<bar>f x\<bar> powr p
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
norm ?x12 \<le> 1 + norm ?x12 powr p

goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> \<le> 1 + \<bar>f x\<bar> powr p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integrable M f

goal (2 subgoals):
 1. \<bar>expectation f\<bar> powr p \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p)
 2. \<bar>expectation f\<bar> \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
show "abs(\<integral>x. f x \<partial>M) powr p \<le> (\<integral>x. \<bar>f x\<bar> powr p \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>expectation f\<bar> powr p \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p)
[PROOF STEP]
by (rule jensens_inequality[OF * _ _ assms(3) convex_abs_powr[OF \<open>p \<ge> 1\<close>]], auto)
[PROOF STATE]
proof (state)
this:
\<bar>expectation f\<bar> powr p \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p)

goal (1 subgoal):
 1. \<bar>expectation f\<bar> \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<bar>expectation f\<bar> powr p \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p)
[PROOF STEP]
have "(abs(\<integral>x. f x \<partial>M) powr p) powr (1/p) \<le> (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)"
[PROOF STATE]
proof (prove)
using this:
\<bar>expectation f\<bar> powr p \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p)

goal (1 subgoal):
 1. (\<bar>expectation f\<bar> powr p) powr (1 / p) \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
using assms(1) powr_mono2
[PROOF STATE]
proof (prove)
using this:
\<bar>expectation f\<bar> powr p \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p)
1 \<le> p
\<lbrakk>0 \<le> ?a; 0 \<le> ?x; ?x \<le> ?y\<rbrakk> \<Longrightarrow> ?x powr ?a \<le> ?y powr ?a

goal (1 subgoal):
 1. (\<bar>expectation f\<bar> powr p) powr (1 / p) \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<bar>expectation f\<bar> powr p) powr (1 / p) \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p) powr (1 / p)

goal (1 subgoal):
 1. \<bar>expectation f\<bar> \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<bar>expectation f\<bar> powr p) powr (1 / p) \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
show "abs(\<integral>x. f x \<partial>M) \<le> (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p)"
[PROOF STATE]
proof (prove)
using this:
(\<bar>expectation f\<bar> powr p) powr (1 / p) \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p) powr (1 / p)

goal (1 subgoal):
 1. \<bar>expectation f\<bar> \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
using \<open>p \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
(\<bar>expectation f\<bar> powr p) powr (1 / p) \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p) powr (1 / p)
1 \<le> p

goal (1 subgoal):
 1. \<bar>expectation f\<bar> \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p) powr (1 / p)
[PROOF STEP]
by (auto simp add: powr_powr)
[PROOF STATE]
proof (state)
this:
\<bar>expectation f\<bar> \<le> expectation (\<lambda>x. \<bar>f x\<bar> powr p) powr (1 / p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Holder_inequality:
  assumes "p > (0::real)" "q > 0" "1/p + 1/q = 1"
      and [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
          "integrable M (\<lambda>x. \<bar>f x\<bar> powr p)"
          "integrable M (\<lambda>x. \<bar>g x\<bar> powr q)"
  shows "integrable M (\<lambda>x. f x * g x)"
        "(\<integral>x. \<bar>f x * g x\<bar> \<partial>M) \<le> (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p) * (\<integral>x. \<bar>g x\<bar> powr q \<partial>M) powr (1/q)"
        "abs(\<integral>x. f x * g x \<partial>M) \<le> (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p) * (\<integral>x. \<bar>g x\<bar> powr q \<partial>M) powr (1/q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. f x * g x) &&& LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q) &&& \<bar>LINT x|M. f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. integrable M (\<lambda>x. f x * g x)
 2. LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
 3. \<bar>LINT x|M. f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "p > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < p
[PROOF STEP]
using conjugate_exponent_realI(1)[OF \<open>p>0\<close> \<open>q>0\<close> \<open>1/p+1/q=1\<close>]
[PROOF STATE]
proof (prove)
using this:
1 < p

goal (1 subgoal):
 1. 1 < p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
1 < p

goal (3 subgoals):
 1. integrable M (\<lambda>x. f x * g x)
 2. LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
 3. \<bar>LINT x|M. f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have *: "x * y \<le> x powr p + y powr q" if "x \<ge> 0" "y \<ge> 0" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<le> x powr p + y powr q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y \<le> x powr p + y powr q
[PROOF STEP]
have "x * y = (x powr p) powr (1/p) * (y powr q) powr (1/q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y = (x powr p) powr (1 / p) * (y powr q) powr (1 / q)
[PROOF STEP]
using \<open>p > 0\<close> \<open>q > 0\<close> powr_powr that(1) that(2)
[PROOF STATE]
proof (prove)
using this:
0 < p
0 < q
(?x powr ?a) powr ?b = ?x powr (?a * ?b)
0 \<le> x
0 \<le> y

goal (1 subgoal):
 1. x * y = (x powr p) powr (1 / p) * (y powr q) powr (1 / q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x * y = (x powr p) powr (1 / p) * (y powr q) powr (1 / q)

goal (1 subgoal):
 1. x * y \<le> x powr p + y powr q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * y = (x powr p) powr (1 / p) * (y powr q) powr (1 / q)

goal (1 subgoal):
 1. x * y \<le> x powr p + y powr q
[PROOF STEP]
have "... \<le> (max (x powr p) (y powr q)) powr (1/p) * (max (x powr p) (y powr q)) powr (1/q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x powr p) powr (1 / p) * (y powr q) powr (1 / q) \<le> max (x powr p) (y powr q) powr (1 / p) * max (x powr p) (y powr q) powr (1 / q)
[PROOF STEP]
apply (rule mult_mono, auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (x powr p) powr (1 / p) \<le> max (x powr p) (y powr q) powr (1 / p)
 2. (y powr q) powr (1 / q) \<le> max (x powr p) (y powr q) powr (1 / q)
[PROOF STEP]
using assms(1) assms(2) powr_mono2
[PROOF STATE]
proof (prove)
using this:
0 < p
0 < q
\<lbrakk>0 \<le> ?a; 0 \<le> ?x; ?x \<le> ?y\<rbrakk> \<Longrightarrow> ?x powr ?a \<le> ?y powr ?a

goal (2 subgoals):
 1. (x powr p) powr (1 / p) \<le> max (x powr p) (y powr q) powr (1 / p)
 2. (y powr q) powr (1 / q) \<le> max (x powr p) (y powr q) powr (1 / q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x powr p) powr (1 / p) * (y powr q) powr (1 / q) \<le> max (x powr p) (y powr q) powr (1 / p) * max (x powr p) (y powr q) powr (1 / q)

goal (1 subgoal):
 1. x * y \<le> x powr p + y powr q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x powr p) powr (1 / p) * (y powr q) powr (1 / q) \<le> max (x powr p) (y powr q) powr (1 / p) * max (x powr p) (y powr q) powr (1 / q)

goal (1 subgoal):
 1. x * y \<le> x powr p + y powr q
[PROOF STEP]
have "... = max (x powr p) (y powr q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (x powr p) (y powr q) powr (1 / p) * max (x powr p) (y powr q) powr (1 / q) = max (x powr p) (y powr q)
[PROOF STEP]
by (metis max_def mult.right_neutral powr_add powr_powr assms(3))
[PROOF STATE]
proof (state)
this:
max (x powr p) (y powr q) powr (1 / p) * max (x powr p) (y powr q) powr (1 / q) = max (x powr p) (y powr q)

goal (1 subgoal):
 1. x * y \<le> x powr p + y powr q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
max (x powr p) (y powr q) powr (1 / p) * max (x powr p) (y powr q) powr (1 / q) = max (x powr p) (y powr q)

goal (1 subgoal):
 1. x * y \<le> x powr p + y powr q
[PROOF STEP]
have "... \<le> x powr p + y powr q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (x powr p) (y powr q) \<le> x powr p + y powr q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
max (x powr p) (y powr q) \<le> x powr p + y powr q

goal (1 subgoal):
 1. x * y \<le> x powr p + y powr q
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x * y \<le> x powr p + y powr q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x * y \<le> x powr p + y powr q

goal (1 subgoal):
 1. x * y \<le> x powr p + y powr q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x * y \<le> x powr p + y powr q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?x; 0 \<le> ?y\<rbrakk> \<Longrightarrow> ?x * ?y \<le> ?x powr p + ?y powr q

goal (3 subgoals):
 1. integrable M (\<lambda>x. f x * g x)
 2. LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
 3. \<bar>LINT x|M. f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
show [simp]: "integrable M (\<lambda>x. f x * g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. f x * g x)
[PROOF STEP]
apply (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. \<bar>f x\<bar> powr p + \<bar>g x\<bar> powr q"], auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr p + \<bar>g x\<bar> powr q)
 2. AE x in M. \<bar>f x * g x\<bar> \<le> \<bar>f x\<bar> powr p + \<bar>g x\<bar> powr q
[PROOF STEP]
by (rule Bochner_Integration.integrable_add, auto simp add: assms * abs_mult)
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. f x * g x)

goal (2 subgoals):
 1. LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
 2. \<bar>LINT x|M. f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
text \<open>The proof of the main inequality is done by applying the inequality
        $(\int |h| d\mu \leq \int |h|^p d\mu)^{1/p}$ to the right function $h$ in the right
        probability space. One should take $h = f \cdot |g|^{1-q}$, and $d\mu = |g|^q dM / I$,
        where $I = \int |g|^q$. This readily gives the result.\<close>
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. f x * g x)

goal (2 subgoals):
 1. LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
 2. \<bar>LINT x|M. f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
show *: "(\<integral>x. \<bar>f x * g x\<bar> \<partial>M) \<le> (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p) * (\<integral>x. \<bar>g x\<bar> powr q \<partial>M) powr (1/q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
proof (cases "(\<integral>x. \<bar>g x\<bar> powr q \<partial>M) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. LINT x|M. \<bar>g x\<bar> powr q = 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
 2. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>g x\<bar> powr q = 0

goal (2 subgoals):
 1. LINT x|M. \<bar>g x\<bar> powr q = 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
 2. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
LINT x|M. \<bar>g x\<bar> powr q = 0
[PROOF STEP]
have "AE x in M. \<bar>g x\<bar> powr q = 0"
[PROOF STATE]
proof (prove)
using this:
LINT x|M. \<bar>g x\<bar> powr q = 0

goal (1 subgoal):
 1. AE x in M. \<bar>g x\<bar> powr q = 0
[PROOF STEP]
by (subst integral_nonneg_eq_0_iff_AE[symmetric], auto simp add: assms)
[PROOF STATE]
proof (state)
this:
AE x in M. \<bar>g x\<bar> powr q = 0

goal (2 subgoals):
 1. LINT x|M. \<bar>g x\<bar> powr q = 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
 2. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. \<bar>g x\<bar> powr q = 0
[PROOF STEP]
have *: "AE x in M. f x * g x = 0"
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<bar>g x\<bar> powr q = 0

goal (1 subgoal):
 1. AE x in M. f x * g x = 0
[PROOF STEP]
using \<open>q > 0\<close>
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<bar>g x\<bar> powr q = 0
0 < q

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

goal (2 subgoals):
 1. LINT x|M. \<bar>g x\<bar> powr q = 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
 2. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "(\<integral>x. \<bar>f x * g x\<bar> \<partial>M) = (\<integral>x. 0 \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. \<bar>f x * g x\<bar> = LINT x|M. 0
[PROOF STEP]
apply (rule integral_cong_AE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>x. \<bar>f x * g x\<bar>) \<in> borel_measurable M
 2. (\<lambda>x. 0) \<in> borel_measurable M
 3. AE x in M. \<bar>f x * g x\<bar> = 0
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
AE x in M. f x * g x = 0

goal (3 subgoals):
 1. (\<lambda>x. \<bar>f x * g x\<bar>) \<in> borel_measurable M
 2. (\<lambda>x. 0) \<in> borel_measurable M
 3. AE x in M. \<bar>f x * g x\<bar> = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>f x * g x\<bar> = LINT x|M. 0

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

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

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "(\<integral>x. \<bar>g x\<bar> powr q \<partial>M) \<ge> (\<integral>x. 0 \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. 0 \<le> LINT x|M. \<bar>g x\<bar> powr q
[PROOF STEP]
by (rule integral_mono, auto simp add: assms)
[PROOF STATE]
proof (state)
this:
LINT x|M. 0 \<le> LINT x|M. \<bar>g x\<bar> powr q

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0
LINT x|M. 0 \<le> LINT x|M. \<bar>g x\<bar> powr q
[PROOF STEP]
have *: "(\<integral>x. \<bar>g x\<bar> powr q \<partial>M) > 0"
[PROOF STATE]
proof (prove)
using this:
LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0
LINT x|M. 0 \<le> LINT x|M. \<bar>g x\<bar> powr q

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

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
define I where "I = (\<integral>x. \<bar>g x\<bar> powr q \<partial>M)"
[PROOF STATE]
proof (state)
this:
I = LINT x|M. \<bar>g x\<bar> powr q

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have [simp]: "I > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < I
[PROOF STEP]
unfolding I_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < LINT x|M. \<bar>g x\<bar> powr q
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
0 < LINT x|M. \<bar>g x\<bar> powr q

goal (1 subgoal):
 1. 0 < LINT x|M. \<bar>g x\<bar> powr q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < I

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
define M2 where "M2 = density M (\<lambda>x. \<bar>g x\<bar> powr q / I)"
[PROOF STATE]
proof (state)
this:
M2 = density M (\<lambda>x. ennreal (\<bar>g x\<bar> powr q / I))

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
interpret prob_space M2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob_space M2
[PROOF STEP]
apply (standard, unfold M2_def, auto, subst emeasure_density, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (\<bar>g x\<bar> powr q / I) \<partial>M = 1
[PROOF STEP]
apply (subst divide_ennreal[symmetric], auto, subst nn_integral_divide, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (\<bar>g x\<bar> powr q) \<partial>M / ennreal I = 1
[PROOF STEP]
apply (subst nn_integral_eq_integral, auto simp add: assms, unfold I_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (LINT x|M. \<bar>g x\<bar> powr q) / ennreal (LINT x|M. \<bar>g x\<bar> powr q) = 1
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
0 < LINT x|M. \<bar>g x\<bar> powr q

goal (1 subgoal):
 1. ennreal (LINT x|M. \<bar>g x\<bar> powr q) / ennreal (LINT x|M. \<bar>g x\<bar> powr q) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have [simp]: "p \<ge> 1" "p \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> p &&& 0 \<le> p
[PROOF STEP]
using \<open>p > 1\<close>
[PROOF STATE]
proof (prove)
using this:
1 < p

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

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have A: "q + (1 - q) * p = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q + (1 - q) * p = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < p
0 < q
1 / p + 1 / q = 1
f \<in> borel_measurable M
g \<in> borel_measurable M
integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
integrable M (\<lambda>x. \<bar>g x\<bar> powr q)

goal (1 subgoal):
 1. q + (1 - q) * p = 0
[PROOF STEP]
by (auto simp add: divide_simps algebra_simps)
[PROOF STATE]
proof (state)
this:
q + (1 - q) * p = 0

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have B: "1 - 1/p = 1/q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 - 1 / p = 1 / q
[PROOF STEP]
using \<open>1/p + 1/q = 1\<close>
[PROOF STATE]
proof (prove)
using this:
1 / p + 1 / q = 1

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

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
define f2 where "f2 = (\<lambda>x. f x * indicator {y\<in> space M. g y \<noteq> 0} x)"
[PROOF STATE]
proof (state)
this:
f2 = (\<lambda>x. f x * indicat_real {y \<in> space M. g y \<noteq> 0} x)

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have [measurable]: "f2 \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f2 \<in> borel_measurable M
[PROOF STEP]
unfolding f2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x * indicat_real {y \<in> space M. g y \<noteq> 0} x) \<in> borel_measurable M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f2 \<in> borel_measurable M

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
define h where "h = (\<lambda>x. \<bar>f2 x\<bar> * \<bar>g x\<bar> powr (1-q))"
[PROOF STATE]
proof (state)
this:
h = (\<lambda>x. \<bar>f2 x\<bar> * \<bar>g x\<bar> powr (1 - q))

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[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. \<bar>f2 x\<bar> * \<bar>g x\<bar> powr (1 - q)) \<in> borel_measurable M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h \<in> borel_measurable M

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have [measurable]: "h \<in> borel_measurable M2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. random_variable borel h
[PROOF STEP]
unfolding M2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<in> borel_measurable (density M (\<lambda>x. ennreal (\<bar>g x\<bar> powr q / I)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
random_variable borel h

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have Eq: "(\<bar>g x\<bar> powr q / I) *\<^sub>R \<bar>h x\<bar> powr p = \<bar>f2 x\<bar> powr p / I" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<bar>g x\<bar> powr q / I) *\<^sub>R \<bar>h x\<bar> powr p = \<bar>f2 x\<bar> powr p / I
[PROOF STEP]
apply (insert \<open>I>0\<close>, auto simp add: divide_simps, unfold h_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<noteq> 0 \<Longrightarrow> \<bar>g x\<bar> powr q * \<bar>\<bar>f2 x\<bar> * \<bar>g x\<bar> powr (1 - q)\<bar> powr p = \<bar>f2 x\<bar> powr p
[PROOF STEP]
apply (auto simp add: divide_nonneg_pos divide_simps powr_mult powr_powr powr_add[symmetric] A)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> 0; g x = 0\<rbrakk> \<Longrightarrow> f2 x = 0
[PROOF STEP]
unfolding f2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> 0; g x = 0\<rbrakk> \<Longrightarrow> f x * indicat_real {y \<in> space M. g y \<noteq> 0} x = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<bar>g ?x1\<bar> powr q / I) *\<^sub>R \<bar>h ?x1\<bar> powr p = \<bar>f2 ?x1\<bar> powr p / I

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "integrable M2 (\<lambda>x. \<bar>h x\<bar> powr p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M2 (\<lambda>x. \<bar>h x\<bar> powr p)
[PROOF STEP]
unfolding M2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable (density M (\<lambda>x. ennreal (\<bar>g x\<bar> powr q / I))) (\<lambda>x. \<bar>h x\<bar> powr p)
[PROOF STEP]
apply (subst integrable_density, simp, simp, simp add: divide_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. (\<bar>g x\<bar> powr q / I) *\<^sub>R \<bar>h x\<bar> powr p)
[PROOF STEP]
apply (subst Eq, rule integrable_divide, rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. \<bar>f x\<bar> powr p"], unfold f2_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr p)
 2. (\<lambda>x. \<bar>f x * indicat_real {y \<in> space M. g y \<noteq> 0} x\<bar> powr p) \<in> borel_measurable M
 3. AE x in M. norm (\<bar>f x * indicat_real {y \<in> space M. g y \<noteq> 0} x\<bar> powr p) \<le> norm (\<bar>f x\<bar> powr p)
[PROOF STEP]
by (unfold indicator_def, auto simp add: \<open>integrable M (\<lambda>x. \<bar>f x\<bar> powr p)\<close>)
[PROOF STATE]
proof (state)
this:
integrable M2 (\<lambda>x. \<bar>h x\<bar> powr p)

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
integrable M2 (\<lambda>x. \<bar>h x\<bar> powr p)
[PROOF STEP]
have "integrable M2 (\<lambda>x. \<bar>h x\<bar>)"
[PROOF STATE]
proof (prove)
using this:
integrable M2 (\<lambda>x. \<bar>h x\<bar> powr p)

goal (1 subgoal):
 1. integrable M2 (\<lambda>x. \<bar>h x\<bar>)
[PROOF STEP]
by (metis bound_L1_Lp(1) \<open>random_variable borel h\<close> \<open>p > 1\<close> integrable_abs le_less)
[PROOF STATE]
proof (state)
this:
integrable M2 (\<lambda>x. \<bar>h x\<bar>)

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "(\<integral>x. \<bar>h x\<bar> powr p \<partial>M2) = (\<integral>x. (\<bar>g x\<bar> powr q / I) *\<^sub>R (\<bar>h x\<bar> powr p) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation (\<lambda>x. \<bar>h x\<bar> powr p) = LINT x|M. (\<bar>g x\<bar> powr q / I) *\<^sub>R \<bar>h x\<bar> powr p
[PROOF STEP]
unfolding M2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|density M (\<lambda>x. ennreal (\<bar>g x\<bar> powr q / I)). \<bar>h x\<bar> powr p = LINT x|M. (\<bar>g x\<bar> powr q / I) *\<^sub>R \<bar>h x\<bar> powr p
[PROOF STEP]
by (rule integral_density[of "\<lambda>x. \<bar>h x\<bar> powr p" M "\<lambda>x. \<bar>g x\<bar> powr q / I"], auto simp add: divide_simps)
[PROOF STATE]
proof (state)
this:
expectation (\<lambda>x. \<bar>h x\<bar> powr p) = LINT x|M. (\<bar>g x\<bar> powr q / I) *\<^sub>R \<bar>h x\<bar> powr p

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
expectation (\<lambda>x. \<bar>h x\<bar> powr p) = LINT x|M. (\<bar>g x\<bar> powr q / I) *\<^sub>R \<bar>h x\<bar> powr p

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "... = (\<integral>x. \<bar>f2 x\<bar> powr p / I \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. (\<bar>g x\<bar> powr q / I) *\<^sub>R \<bar>h x\<bar> powr p = LINT x|M. \<bar>f2 x\<bar> powr p / I
[PROOF STEP]
apply (rule Bochner_Integration.integral_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. M = M
 2. \<And>x. x \<in> space M \<Longrightarrow> (\<bar>g x\<bar> powr q / I) *\<^sub>R \<bar>h x\<bar> powr p = \<bar>f2 x\<bar> powr p / I
[PROOF STEP]
using Eq
[PROOF STATE]
proof (prove)
using this:
(\<bar>g ?x1\<bar> powr q / I) *\<^sub>R \<bar>h ?x1\<bar> powr p = \<bar>f2 ?x1\<bar> powr p / I

goal (2 subgoals):
 1. M = M
 2. \<And>x. x \<in> space M \<Longrightarrow> (\<bar>g x\<bar> powr q / I) *\<^sub>R \<bar>h x\<bar> powr p = \<bar>f2 x\<bar> powr p / I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
LINT x|M. (\<bar>g x\<bar> powr q / I) *\<^sub>R \<bar>h x\<bar> powr p = LINT x|M. \<bar>f2 x\<bar> powr p / I

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LINT x|M. (\<bar>g x\<bar> powr q / I) *\<^sub>R \<bar>h x\<bar> powr p = LINT x|M. \<bar>f2 x\<bar> powr p / I

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "... \<le> (\<integral>x. \<bar>f x\<bar> powr p / I \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. \<bar>f2 x\<bar> powr p / I \<le> LINT x|M. \<bar>f x\<bar> powr p / I
[PROOF STEP]
apply (rule integral_mono', rule integrable_divide[OF \<open>integrable M (\<lambda>x. \<bar>f x\<bar> powr p)\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> space M \<Longrightarrow> \<bar>f2 x\<bar> powr p / I \<le> \<bar>f x\<bar> powr p / I
 2. \<And>x. x \<in> space M \<Longrightarrow> 0 \<le> \<bar>f x\<bar> powr p / I
[PROOF STEP]
unfolding f2_def indicator_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> space M \<Longrightarrow> \<bar>f x * of_bool (x \<in> {y \<in> space M. g y \<noteq> 0})\<bar> powr p / I \<le> \<bar>f x\<bar> powr p / I
 2. \<And>x. x \<in> space M \<Longrightarrow> 0 \<le> \<bar>f x\<bar> powr p / I
[PROOF STEP]
using \<open>I > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < I

goal (2 subgoals):
 1. \<And>x. x \<in> space M \<Longrightarrow> \<bar>f x * of_bool (x \<in> {y \<in> space M. g y \<noteq> 0})\<bar> powr p / I \<le> \<bar>f x\<bar> powr p / I
 2. \<And>x. x \<in> space M \<Longrightarrow> 0 \<le> \<bar>f x\<bar> powr p / I
[PROOF STEP]
by (auto simp add: divide_simps)
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>f2 x\<bar> powr p / I \<le> LINT x|M. \<bar>f x\<bar> powr p / I

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
expectation (\<lambda>x. \<bar>h x\<bar> powr p) \<le> LINT x|M. \<bar>f x\<bar> powr p / I
[PROOF STEP]
have C: "(\<integral>x. \<bar>h x\<bar> powr p \<partial>M2) \<le> (\<integral>x. \<bar>f x\<bar> powr p / I \<partial>M)"
[PROOF STATE]
proof (prove)
using this:
expectation (\<lambda>x. \<bar>h x\<bar> powr p) \<le> LINT x|M. \<bar>f x\<bar> powr p / I

goal (1 subgoal):
 1. expectation (\<lambda>x. \<bar>h x\<bar> powr p) \<le> LINT x|M. \<bar>f x\<bar> powr p / I
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
expectation (\<lambda>x. \<bar>h x\<bar> powr p) \<le> LINT x|M. \<bar>f x\<bar> powr p / I

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "(\<integral>x. \<bar>f x * g x\<bar> \<partial>M) / I = (\<integral>x. \<bar>f x * g x\<bar> / I \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x * g x\<bar>) / I = LINT x|M. \<bar>f x * g x\<bar> / I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(LINT x|M. \<bar>f x * g x\<bar>) / I = LINT x|M. \<bar>f x * g x\<bar> / I

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(LINT x|M. \<bar>f x * g x\<bar>) / I = LINT x|M. \<bar>f x * g x\<bar> / I

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "... = (\<integral>x. \<bar>f2 x * g x\<bar> / I \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. \<bar>f x * g x\<bar> / I = LINT x|M. \<bar>f2 x * g x\<bar> / I
[PROOF STEP]
by (auto simp add: divide_simps, rule Bochner_Integration.integral_cong, unfold f2_def indicator_def, auto)
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>f x * g x\<bar> / I = LINT x|M. \<bar>f2 x * g x\<bar> / I

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>f x * g x\<bar> / I = LINT x|M. \<bar>f2 x * g x\<bar> / I

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "... = (\<integral>x. \<bar>h x\<bar> \<partial>M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. \<bar>f2 x * g x\<bar> / I = expectation (\<lambda>x. \<bar>h x\<bar>)
[PROOF STEP]
apply (unfold M2_def, subst integral_density, simp, simp, simp add: divide_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. \<bar>f2 x * g x\<bar> / I = LINT x|M. (\<bar>g x\<bar> powr q / I) *\<^sub>R \<bar>h x\<bar>
[PROOF STEP]
by (rule Bochner_Integration.integral_cong, unfold h_def, auto simp add: divide_simps algebra_simps powr_add[symmetric] abs_mult)
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>f2 x * g x\<bar> / I = expectation (\<lambda>x. \<bar>h x\<bar>)

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>f2 x * g x\<bar> / I = expectation (\<lambda>x. \<bar>h x\<bar>)

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "... \<le> abs (\<integral>x. \<bar>h x\<bar> \<partial>M2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation (\<lambda>x. \<bar>h x\<bar>) \<le> \<bar>expectation (\<lambda>x. \<bar>h x\<bar>)\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
expectation (\<lambda>x. \<bar>h x\<bar>) \<le> \<bar>expectation (\<lambda>x. \<bar>h x\<bar>)\<bar>

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
expectation (\<lambda>x. \<bar>h x\<bar>) \<le> \<bar>expectation (\<lambda>x. \<bar>h x\<bar>)\<bar>

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "... \<le> (\<integral>x. abs(\<bar>h x\<bar>) powr p \<partial>M2) powr (1/p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>expectation (\<lambda>x. \<bar>h x\<bar>)\<bar> \<le> expectation (\<lambda>x. \<bar>\<bar>h x\<bar>\<bar> powr p) powr (1 / p)
[PROOF STEP]
apply (rule bound_L1_Lp(3)[of p "\<lambda>x. \<bar>h x\<bar>"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 1 \<le> p
 2. random_variable borel (\<lambda>x. \<bar>h x\<bar>)
 3. integrable M2 (\<lambda>x. \<bar>\<bar>h x\<bar>\<bar> powr p)
[PROOF STEP]
by (auto simp add: \<open>integrable M2 (\<lambda>x. \<bar>h x\<bar> powr p)\<close>)
[PROOF STATE]
proof (state)
this:
\<bar>expectation (\<lambda>x. \<bar>h x\<bar>)\<bar> \<le> expectation (\<lambda>x. \<bar>\<bar>h x\<bar>\<bar> powr p) powr (1 / p)

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>expectation (\<lambda>x. \<bar>h x\<bar>)\<bar> \<le> expectation (\<lambda>x. \<bar>\<bar>h x\<bar>\<bar> powr p) powr (1 / p)

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "... \<le> (\<integral>x. \<bar>f x\<bar> powr p / I \<partial>M) powr (1/p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation (\<lambda>x. \<bar>\<bar>h x\<bar>\<bar> powr p) powr (1 / p) \<le> (LINT x|M. \<bar>f x\<bar> powr p / I) powr (1 / p)
[PROOF STEP]
by (rule powr_mono2, insert C, auto)
[PROOF STATE]
proof (state)
this:
expectation (\<lambda>x. \<bar>\<bar>h x\<bar>\<bar> powr p) powr (1 / p) \<le> (LINT x|M. \<bar>f x\<bar> powr p / I) powr (1 / p)

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
expectation (\<lambda>x. \<bar>\<bar>h x\<bar>\<bar> powr p) powr (1 / p) \<le> (LINT x|M. \<bar>f x\<bar> powr p / I) powr (1 / p)

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "... \<le> ((\<integral>x. \<bar>f x\<bar> powr p \<partial>M) / I) powr (1/p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x\<bar> powr p / I) powr (1 / p) \<le> ((LINT x|M. \<bar>f x\<bar> powr p) / I) powr (1 / p)
[PROOF STEP]
apply (rule powr_mono2, auto simp add: divide_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p < 0 \<Longrightarrow> False
[PROOF STEP]
using \<open>p \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> p

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

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(LINT x|M. \<bar>f x\<bar> powr p / I) powr (1 / p) \<le> ((LINT x|M. \<bar>f x\<bar> powr p) / I) powr (1 / p)

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "... = (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p) * I powr(-1/p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((LINT x|M. \<bar>f x\<bar> powr p) / I) powr (1 / p) = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * I powr (- 1 / p)
[PROOF STEP]
by (auto simp add: less_imp_le powr_divide powr_minus_divide)
[PROOF STATE]
proof (state)
this:
((LINT x|M. \<bar>f x\<bar> powr p) / I) powr (1 / p) = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * I powr (- 1 / p)

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(LINT x|M. \<bar>f x * g x\<bar>) / I \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * I powr (- 1 / p)
[PROOF STEP]
have "(\<integral>x. \<bar>f x * g x\<bar> \<partial>M) \<le> (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p) * I * I powr(-1/p)"
[PROOF STATE]
proof (prove)
using this:
(LINT x|M. \<bar>f x * g x\<bar>) / I \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * I powr (- 1 / p)

goal (1 subgoal):
 1. LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * I * I powr (- 1 / p)
[PROOF STEP]
by (auto simp add: divide_simps algebra_simps)
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * I * I powr (- 1 / p)

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * I * I powr (- 1 / p)

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "... = (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p) * I powr (1-1/p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * I * I powr (- 1 / p) = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * I powr (1 - 1 / p)
[PROOF STEP]
by (auto simp add: powr_mult_base less_imp_le)
[PROOF STATE]
proof (state)
this:
(LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * I * I powr (- 1 / p) = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * I powr (1 - 1 / p)

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * I * I powr (- 1 / p) = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * I powr (1 - 1 / p)

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
have "... = (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p) * (\<integral>x. \<bar>g x\<bar> powr q \<partial>M) powr (1/q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * I powr (1 - 1 / p) = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
unfolding I_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 - 1 / p) = (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
1 - 1 / p = 1 / q

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

goal (1 subgoal):
 1. LINT x|M. \<bar>g x\<bar> powr q \<noteq> 0 \<Longrightarrow> LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)

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

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

goal (1 subgoal):
 1. \<bar>LINT x|M. f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<bar>LINT x|M. f x * g x\<bar> \<le> LINT x|M. \<bar>f x * g x\<bar>
LINT x|M. \<bar>f x * g x\<bar> \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>g x\<bar> powr q) powr (1 / q)

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

goal:
No subgoals!
[PROOF STEP]
qed