[STATEMENT]
theorem Minkowski_inequality:
  assumes "p \<ge> (1::real)"
      and [measurable, simp]: "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 p)"
  shows "integrable M (\<lambda>x. \<bar>f x + g x\<bar> powr p)"
        "(\<integral>x. \<bar>f x + g x\<bar> powr p \<partial>M) powr (1/p)
          \<le> (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p) + (\<integral>x. \<bar>g x\<bar> powr p \<partial>M) powr (1/p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>f x + g x\<bar> powr p) &&& (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x + g x\<bar> powr p)
 2. (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
have *: "\<bar>x + y\<bar> powr p \<le> 2 powr p * (\<bar>x\<bar> powr p + \<bar>y\<bar> powr p)" for x y::real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x + y\<bar> powr p \<le> 2 powr p * (\<bar>x\<bar> powr p + \<bar>y\<bar> powr p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>x + y\<bar> powr p \<le> 2 powr p * (\<bar>x\<bar> powr p + \<bar>y\<bar> powr p)
[PROOF STEP]
have "\<bar>x + y\<bar> \<le> \<bar>x\<bar> + \<bar>y\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x + y\<bar> \<le> \<bar>x\<bar> + \<bar>y\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>x + y\<bar> \<le> \<bar>x\<bar> + \<bar>y\<bar>

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

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

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

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

goal (1 subgoal):
 1. \<bar>x + y\<bar> powr p \<le> 2 powr p * (\<bar>x\<bar> powr p + \<bar>y\<bar> powr p)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>x + y\<bar> \<le> 2 * max \<bar>x\<bar> \<bar>y\<bar>
[PROOF STEP]
have "\<bar>x + y\<bar> powr p \<le> (2 * max \<bar>x\<bar> \<bar>y\<bar>) powr p"
[PROOF STATE]
proof (prove)
using this:
\<bar>x + y\<bar> \<le> 2 * max \<bar>x\<bar> \<bar>y\<bar>

goal (1 subgoal):
 1. \<bar>x + y\<bar> powr p \<le> (2 * max \<bar>x\<bar> \<bar>y\<bar>) powr p
[PROOF STEP]
using powr_mono2 \<open>p \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
\<bar>x + y\<bar> \<le> 2 * max \<bar>x\<bar> \<bar>y\<bar>
\<lbrakk>0 \<le> ?a; 0 \<le> ?x; ?x \<le> ?y\<rbrakk> \<Longrightarrow> ?x powr ?a \<le> ?y powr ?a
1 \<le> p

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

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

goal (1 subgoal):
 1. \<bar>x + y\<bar> powr p \<le> 2 powr p * (\<bar>x\<bar> powr p + \<bar>y\<bar> powr p)
[PROOF STEP]
have "... = 2 powr p * (max \<bar>x\<bar> \<bar>y\<bar>) powr p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 * max \<bar>x\<bar> \<bar>y\<bar>) powr p = 2 powr p * max \<bar>x\<bar> \<bar>y\<bar> powr p
[PROOF STEP]
using powr_mult
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> ?x; 0 \<le> ?y\<rbrakk> \<Longrightarrow> (?x * ?y) powr ?a = ?x powr ?a * ?y powr ?a

goal (1 subgoal):
 1. (2 * max \<bar>x\<bar> \<bar>y\<bar>) powr p = 2 powr p * max \<bar>x\<bar> \<bar>y\<bar> powr p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(2 * max \<bar>x\<bar> \<bar>y\<bar>) powr p = 2 powr p * max \<bar>x\<bar> \<bar>y\<bar> powr p

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

goal (1 subgoal):
 1. \<bar>x + y\<bar> powr p \<le> 2 powr p * (\<bar>x\<bar> powr p + \<bar>y\<bar> powr p)
[PROOF STEP]
have "... \<le> 2 powr p * (\<bar>x\<bar> powr p + \<bar>y\<bar> powr p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 powr p * max \<bar>x\<bar> \<bar>y\<bar> powr p \<le> 2 powr p * (\<bar>x\<bar> powr p + \<bar>y\<bar> powr p)
[PROOF STEP]
unfolding max_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 powr p * (if \<bar>x\<bar> \<le> \<bar>y\<bar> then \<bar>y\<bar> else \<bar>x\<bar>) powr p \<le> 2 powr p * (\<bar>x\<bar> powr p + \<bar>y\<bar> powr p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 powr p * max \<bar>x\<bar> \<bar>y\<bar> powr p \<le> 2 powr p * (\<bar>x\<bar> powr p + \<bar>y\<bar> powr p)

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>?x + ?y\<bar> powr p \<le> 2 powr p * (\<bar>?x\<bar> powr p + \<bar>?y\<bar> powr p)

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

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

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

goal (1 subgoal):
 1. (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
apply (auto, subst Bochner_Integration.integral_add[symmetric], insert assms(4) assms(5), simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = 1; p = 1; integrable M (\<lambda>x. \<bar>f x\<bar> powr p); integrable M (\<lambda>x. \<bar>g x\<bar> powr p)\<rbrakk> \<Longrightarrow> LINT x|M. \<bar>f x + g x\<bar> \<le> LINT x|M. \<bar>f x\<bar> + \<bar>g x\<bar>
[PROOF STEP]
by (rule integral_mono', auto)
[PROOF STATE]
proof (state)
this:
(LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)

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

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

goal (1 subgoal):
 1. (1 < p &&& 1 \<le> p) &&& 0 < p &&& p \<noteq> 0
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 1
1 \<le> p

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

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

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

goal (1 subgoal):
 1. (1 < conjugate_exponent p &&& 0 < conjugate_exponent p) &&& 1 / p + 1 / conjugate_exponent p = 1 &&& (p - 1) * conjugate_exponent p = p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 < q
0 < q
1 / p + 1 / q = 1
(p - 1) * q = p

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

goal (1 subgoal):
 1. (z powr (p - 1)) powr q = z powr p
[PROOF STEP]
by (simp add: powr_powr)
[PROOF STATE]
proof (state)
this:
(?z powr (p - 1)) powr q = ?z powr p

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

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

goal (1 subgoal):
 1. p \<noteq> 1 \<Longrightarrow> (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
have "... \<le> (\<integral>x. \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p-1) + \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p-1) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. \<bar>f x + g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1) \<le> LINT x|M. \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p - 1) + \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1)
[PROOF STEP]
apply (rule integral_mono', rule Bochner_Integration.integrable_add)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p - 1))
 2. integrable M (\<lambda>x. \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1))
 3. \<And>x. x \<in> space M \<Longrightarrow> \<bar>f x + g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1) \<le> \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p - 1) + \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1)
 4. \<And>x. x \<in> space M \<Longrightarrow> 0 \<le> \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p - 1) + \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1)
[PROOF STEP]
apply (rule Holder_inequality(1)[of p q], auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1))
 2. \<And>x. x \<in> space M \<Longrightarrow> \<bar>f x + g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1) \<le> \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p - 1) + \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1)
[PROOF STEP]
apply (rule Holder_inequality(1)[of p q], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> space M \<Longrightarrow> \<bar>f x + g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1) \<le> \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p - 1) + \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1)
[PROOF STEP]
by (metis abs_ge_zero abs_triangle_ineq comm_semiring_class.distrib le_less mult_mono' powr_ge_pzero)
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>f x + g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1) \<le> LINT x|M. \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p - 1) + \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1)

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

goal (1 subgoal):
 1. p \<noteq> 1 \<Longrightarrow> (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
have "... = (\<integral>x. \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p-1) \<partial>M) + (\<integral>x. \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p-1) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p - 1) + \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1) = (LINT x|M. \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p - 1)) + (LINT x|M. \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1))
[PROOF STEP]
apply (rule Bochner_Integration.integral_add)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p - 1))
 2. integrable M (\<lambda>x. \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1))
[PROOF STEP]
by (rule Holder_inequality(1)[of p q], auto)+
[PROOF STATE]
proof (state)
this:
LINT x|M. \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p - 1) + \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1) = (LINT x|M. \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p - 1)) + (LINT x|M. \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1))

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

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

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

goal (1 subgoal):
 1. p \<noteq> 1 \<Longrightarrow> (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
have "... \<le> (\<integral>x. abs(\<bar>f x\<bar>) powr p \<partial>M) powr (1/p) * (\<integral>x. abs(\<bar>f x + g x\<bar> powr (p-1)) powr q \<partial>M) powr (1/q)
                      + (\<integral>x. abs(\<bar>g x\<bar>) powr p \<partial>M) powr (1/p) * (\<integral>x. abs(\<bar>f x + g x\<bar> powr (p-1)) powr q \<partial>M) powr (1/q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>LINT x|M. \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p - 1)\<bar> + \<bar>LINT x|M. \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1)\<bar> \<le> (LINT x|M. \<bar>\<bar>f x\<bar>\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>\<bar>f x + g x\<bar> powr (p - 1)\<bar> powr q) powr (1 / q) + (LINT x|M. \<bar>\<bar>g x\<bar>\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>\<bar>f x + g x\<bar> powr (p - 1)\<bar> powr q) powr (1 / q)
[PROOF STEP]
apply (rule add_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<bar>LINT x|M. \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p - 1)\<bar> \<le> (LINT x|M. \<bar>\<bar>f x\<bar>\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>\<bar>f x + g x\<bar> powr (p - 1)\<bar> powr q) powr (1 / q)
 2. \<bar>LINT x|M. \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1)\<bar> \<le> (LINT x|M. \<bar>\<bar>g x\<bar>\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>\<bar>f x + g x\<bar> powr (p - 1)\<bar> powr q) powr (1 / q)
[PROOF STEP]
apply (rule Holder_inequality(3)[of p q], simp, simp, simp, simp, simp, simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>LINT x|M. \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1)\<bar> \<le> (LINT x|M. \<bar>\<bar>g x\<bar>\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>\<bar>f x + g x\<bar> powr (p - 1)\<bar> powr q) powr (1 / q)
[PROOF STEP]
apply (rule Holder_inequality(3)[of p q], simp, simp, simp, simp, simp, simp, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<bar>LINT x|M. \<bar>f x\<bar> * \<bar>f x + g x\<bar> powr (p - 1)\<bar> + \<bar>LINT x|M. \<bar>g x\<bar> * \<bar>f x + g x\<bar> powr (p - 1)\<bar> \<le> (LINT x|M. \<bar>\<bar>f x\<bar>\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>\<bar>f x + g x\<bar> powr (p - 1)\<bar> powr q) powr (1 / q) + (LINT x|M. \<bar>\<bar>g x\<bar>\<bar> powr p) powr (1 / p) * (LINT x|M. \<bar>\<bar>f x + g x\<bar> powr (p - 1)\<bar> powr q) powr (1 / q)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Minkowski_inequality_le_1:
  assumes "p > (0::real)" "p \<le> 1"
      and [measurable, simp]: "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 p)"
  shows "integrable M (\<lambda>x. \<bar>f x + g x\<bar> powr p)"
        "(\<integral>x. \<bar>f x + g x\<bar> powr p \<partial>M) powr (1/p)
          \<le> 2 powr (1/p-1) * (\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p) + 2 powr (1/p-1) * (\<integral>x. \<bar>g x\<bar> powr p \<partial>M) powr (1/p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>f x + g x\<bar> powr p) &&& (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> 2 powr (1 / p - 1) * (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + 2 powr (1 / p - 1) * (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. integrable M (\<lambda>x. \<bar>f x + g x\<bar> powr p)
 2. (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> 2 powr (1 / p - 1) * (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + 2 powr (1 / p - 1) * (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
have *: "\<bar>a + b\<bar> powr p \<le> \<bar>a\<bar> powr p + \<bar>b\<bar> powr p" for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>a + b\<bar> powr p \<le> \<bar>a\<bar> powr p + \<bar>b\<bar> powr p
[PROOF STEP]
using x_plus_y_p_le_xp_plus_yp[OF \<open>p > 0\<close> \<open>p \<le> 1\<close>, of "\<bar>a\<bar>" "\<bar>b\<bar>"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> \<bar>a\<bar>; 0 \<le> \<bar>b\<bar>\<rbrakk> \<Longrightarrow> (\<bar>a\<bar> + \<bar>b\<bar>) powr p \<le> \<bar>a\<bar> powr p + \<bar>b\<bar> powr p

goal (1 subgoal):
 1. \<bar>a + b\<bar> powr p \<le> \<bar>a\<bar> powr p + \<bar>b\<bar> powr p
[PROOF STEP]
by (auto, meson abs_ge_zero abs_triangle_ineq assms(1) le_less order.trans powr_mono2)
[PROOF STATE]
proof (state)
this:
\<bar>?a + ?b\<bar> powr p \<le> \<bar>?a\<bar> powr p + \<bar>?b\<bar> powr p

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

goal (1 subgoal):
 1. (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> 2 powr (1 / p - 1) * (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + 2 powr (1 / p - 1) * (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
have "(\<integral>x. \<bar>f x + g x\<bar> powr p \<partial>M) powr (1/p) \<le> (\<integral>x. \<bar>f x\<bar> powr p + \<bar>g x\<bar> powr p \<partial>M) powr (1/p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> (LINT x|M. \<bar>f x\<bar> powr p + \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
by (rule powr_mono2, simp add: \<open>p > 0\<close> less_imp_le, simp, rule integral_mono', auto simp add: *)
[PROOF STATE]
proof (state)
this:
(LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> (LINT x|M. \<bar>f x\<bar> powr p + \<bar>g x\<bar> powr p) powr (1 / p)

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

goal (1 subgoal):
 1. (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> 2 powr (1 / p - 1) * (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + 2 powr (1 / p - 1) * (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
have "... = 2 powr (1/p) * (((\<integral>x. \<bar>f x\<bar> powr p \<partial>M) + (\<integral>x. \<bar>g x\<bar> powr p \<partial>M)) / 2) powr (1/p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. \<bar>f x\<bar> powr p + \<bar>g x\<bar> powr p) powr (1 / p) = 2 powr (1 / p) * (((LINT x|M. \<bar>f x\<bar> powr p) + (LINT x|M. \<bar>g x\<bar> powr p)) / 2) powr (1 / p)
[PROOF STEP]
by (auto simp add: powr_mult[symmetric] add_divide_distrib)
[PROOF STATE]
proof (state)
this:
(LINT x|M. \<bar>f x\<bar> powr p + \<bar>g x\<bar> powr p) powr (1 / p) = 2 powr (1 / p) * (((LINT x|M. \<bar>f x\<bar> powr p) + (LINT x|M. \<bar>g x\<bar> powr p)) / 2) powr (1 / p)

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

goal (1 subgoal):
 1. (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> 2 powr (1 / p - 1) * (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + 2 powr (1 / p - 1) * (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
have "... \<le> 2 powr (1/p) * (((\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p) + (\<integral>x. \<bar>g x\<bar> powr p \<partial>M) powr (1/p)) / 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 powr (1 / p) * (((LINT x|M. \<bar>f x\<bar> powr p) + (LINT x|M. \<bar>g x\<bar> powr p)) / 2) powr (1 / p) \<le> 2 powr (1 / p) * (((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)) / 2)
[PROOF STEP]
apply (rule mult_mono, simp, rule convex_on_mean_ineq[OF convex_powr[of "1/p"]])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. 1 \<le> 1 / p
 2. LINT x|M. \<bar>f x\<bar> powr p \<in> {0..}
 3. LINT x|M. \<bar>g x\<bar> powr p \<in> {0..}
 4. 0 \<le> 2 powr (1 / p)
 5. 0 \<le> (((LINT x|M. \<bar>f x\<bar> powr p) + (LINT x|M. \<bar>g x\<bar> powr p)) / 2) powr (1 / p)
[PROOF STEP]
using \<open>p \<le> 1\<close> \<open>p > 0\<close>
[PROOF STATE]
proof (prove)
using this:
p \<le> 1
0 < p

goal (5 subgoals):
 1. 1 \<le> 1 / p
 2. LINT x|M. \<bar>f x\<bar> powr p \<in> {0..}
 3. LINT x|M. \<bar>g x\<bar> powr p \<in> {0..}
 4. 0 \<le> 2 powr (1 / p)
 5. 0 \<le> (((LINT x|M. \<bar>f x\<bar> powr p) + (LINT x|M. \<bar>g x\<bar> powr p)) / 2) powr (1 / p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 powr (1 / p) * (((LINT x|M. \<bar>f x\<bar> powr p) + (LINT x|M. \<bar>g x\<bar> powr p)) / 2) powr (1 / p) \<le> 2 powr (1 / p) * (((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)) / 2)

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

goal (1 subgoal):
 1. (LINT x|M. \<bar>f x + g x\<bar> powr p) powr (1 / p) \<le> 2 powr (1 / p - 1) * (LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + 2 powr (1 / p - 1) * (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)
[PROOF STEP]
have "... = 2 powr (1/p - 1) * ((\<integral>x. \<bar>f x\<bar> powr p \<partial>M) powr (1/p) + (\<integral>x. \<bar>g x\<bar> powr p \<partial>M) powr (1/p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 powr (1 / p) * (((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)) / 2) = 2 powr (1 / p - 1) * ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p))
[PROOF STEP]
by (simp add: powr_diff)
[PROOF STATE]
proof (state)
this:
2 powr (1 / p) * (((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p)) / 2) = 2 powr (1 / p - 1) * ((LINT x|M. \<bar>f x\<bar> powr p) powr (1 / p) + (LINT x|M. \<bar>g x\<bar> powr p) powr (1 / p))

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma L_infinity:
  "eNorm (\<LL> \<infinity> M) f = (if f \<in> borel_measurable M then esssup M (\<lambda>x. ereal \<bar>f x\<bar>) else (\<infinity>::ennreal))"
  "defect (\<LL> \<infinity> M) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> \<infinity> M) f = (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>) &&& defect (\<LL> \<infinity> M) = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eNorm (\<LL> \<infinity> M) f = (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)
 2. defect (\<LL> \<infinity> M) = 1
[PROOF STEP]
have T: "esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + esssup M (\<lambda>x. ereal \<bar>g x\<bar>)"
    if [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" for f g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
[PROOF STEP]
proof (cases "emeasure M (space M) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. emeasure M (space M) = 0 \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
 2. emeasure M (space M) \<noteq> 0 \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
emeasure M (space M) = 0

goal (2 subgoals):
 1. emeasure M (space M) = 0 \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
 2. emeasure M (space M) \<noteq> 0 \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
emeasure M (space M) = 0
[PROOF STEP]
have "e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) = 0"
[PROOF STATE]
proof (prove)
using this:
emeasure M (space M) = 0

goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) = 0
[PROOF STEP]
using esssup_zero_space[OF True]
[PROOF STATE]
proof (prove)
using this:
emeasure M (space M) = 0
?f \<in> borel_measurable M \<Longrightarrow> esssup M ?f = - \<infinity>

goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) = 0
[PROOF STEP]
by (simp add: e2ennreal_neg)
[PROOF STATE]
proof (state)
this:
e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) = 0

goal (2 subgoals):
 1. emeasure M (space M) = 0 \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
 2. emeasure M (space M) \<noteq> 0 \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) = 0

goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))

goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
emeasure M (space M) \<noteq> 0

goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
[PROOF STEP]
have *: "esssup M (\<lambda>x. \<bar>h x\<bar>) \<ge> 0" for h::"'a \<Rightarrow> real"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> esssup M (\<lambda>x. ereal \<bar>h x\<bar>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> esssup M (\<lambda>x. ereal \<bar>h x\<bar>)
[PROOF STEP]
have "esssup M (\<lambda>x. 0) \<le> esssup M (\<lambda>x. \<bar>h x\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. esssup M (\<lambda>x. 0) \<le> esssup M (\<lambda>x. ereal \<bar>h x\<bar>)
[PROOF STEP]
by (rule esssup_mono, auto)
[PROOF STATE]
proof (state)
this:
esssup M (\<lambda>x. 0) \<le> esssup M (\<lambda>x. ereal \<bar>h x\<bar>)

goal (1 subgoal):
 1. 0 \<le> esssup M (\<lambda>x. ereal \<bar>h x\<bar>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
esssup M (\<lambda>x. 0) \<le> esssup M (\<lambda>x. ereal \<bar>h x\<bar>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. 0) \<le> esssup M (\<lambda>x. ereal \<bar>h x\<bar>)

goal (1 subgoal):
 1. 0 \<le> esssup M (\<lambda>x. ereal \<bar>h x\<bar>)
[PROOF STEP]
using esssup_const[OF False, of "0::ereal"]
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. 0) \<le> esssup M (\<lambda>x. ereal \<bar>h x\<bar>)
esssup M (\<lambda>x. 0) = 0

goal (1 subgoal):
 1. 0 \<le> esssup M (\<lambda>x. ereal \<bar>h x\<bar>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> esssup M (\<lambda>x. ereal \<bar>h x\<bar>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> esssup M (\<lambda>x. ereal \<bar>?h x\<bar>)

goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
[PROOF STEP]
have "esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>) \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar> + ereal \<bar>g x\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>) \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar> + ereal \<bar>g x\<bar>)
[PROOF STEP]
by (rule esssup_mono, auto simp add: plus_fun_def)
[PROOF STATE]
proof (state)
this:
esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>) \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar> + ereal \<bar>g x\<bar>)

goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>) \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar> + ereal \<bar>g x\<bar>)

goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
[PROOF STEP]
have "... \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>) + esssup M (\<lambda>x. ereal \<bar>g x\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>f x\<bar> + ereal \<bar>g x\<bar>) \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>) + esssup M (\<lambda>x. ereal \<bar>g x\<bar>)
[PROOF STEP]
by (rule esssup_add)
[PROOF STATE]
proof (state)
this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar> + ereal \<bar>g x\<bar>) \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>) + esssup M (\<lambda>x. ereal \<bar>g x\<bar>)

goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>) \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>) + esssup M (\<lambda>x. ereal \<bar>g x\<bar>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>) \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>) + esssup M (\<lambda>x. ereal \<bar>g x\<bar>)

goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>) \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>) + esssup M (\<lambda>x. ereal \<bar>g x\<bar>)
0 \<le> esssup M (\<lambda>x. ereal \<bar>?h x\<bar>)

goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))
[PROOF STEP]
by (simp add: e2ennreal_mono eq_onp_def plus_ennreal.abs_eq)
[PROOF STATE]
proof (state)
this:
e2ennreal (esssup M (\<lambda>x. ereal \<bar>(f + g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>g x\<bar>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?f \<in> borel_measurable M; ?g \<in> borel_measurable M\<rbrakk> \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(?f + ?g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>?f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>?g x\<bar>))

goal (2 subgoals):
 1. eNorm (\<LL> \<infinity> M) f = (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)
 2. defect (\<LL> \<infinity> M) = 1
[PROOF STEP]
have H: "esssup M (\<lambda>x. ereal \<bar>(c *\<^sub>R f) x\<bar>) \<le> ennreal \<bar>c\<bar> * esssup M (\<lambda>x. ereal \<bar>f x\<bar>)" if "c \<noteq> 0" for f c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal \<bar>(c *\<^sub>R f) x\<bar>)) \<le> ennreal \<bar>c\<bar> * e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal \<bar>(c *\<^sub>R f) x\<bar>)) \<le> ennreal \<bar>c\<bar> * e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>))
[PROOF STEP]
have "abs c > 0" "ereal \<bar>c\<bar> \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < \<bar>c\<bar> &&& 0 \<le> ereal \<bar>c\<bar>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0

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

goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal \<bar>(c *\<^sub>R f) x\<bar>)) \<le> ennreal \<bar>c\<bar> * e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>))
[PROOF STEP]
have *: "esssup M (\<lambda>x. abs(c *\<^sub>R f x)) = abs c * esssup M (\<lambda>x. \<bar>f x\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>c *\<^sub>R f x\<bar>) = ereal \<bar>c\<bar> * esssup M (\<lambda>x. ereal \<bar>f x\<bar>)
[PROOF STEP]
apply (subst esssup_cmult[OF \<open>abs c > 0\<close>, of M "\<lambda>x. ereal \<bar>f x\<bar>", symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>c *\<^sub>R f x\<bar>) = esssup M (\<lambda>x. ereal \<bar>c\<bar> * ereal \<bar>f x\<bar>)
[PROOF STEP]
using times_ereal.simps(1)
[PROOF STATE]
proof (prove)
using this:
ereal ?r * ereal ?p = ereal (?r * ?p)

goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>c *\<^sub>R f x\<bar>) = esssup M (\<lambda>x. ereal \<bar>c\<bar> * ereal \<bar>f x\<bar>)
[PROOF STEP]
by (auto simp add: abs_mult)
[PROOF STATE]
proof (state)
this:
esssup M (\<lambda>x. ereal \<bar>c *\<^sub>R f x\<bar>) = ereal \<bar>c\<bar> * esssup M (\<lambda>x. ereal \<bar>f x\<bar>)

goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal \<bar>(c *\<^sub>R f) x\<bar>)) \<le> ennreal \<bar>c\<bar> * e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal \<bar>(c *\<^sub>R f) x\<bar>)) \<le> ennreal \<bar>c\<bar> * e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>))
[PROOF STEP]
unfolding e2ennreal_mult[OF \<open>ereal \<bar>c\<bar> \<ge> 0\<close>] * scaleR_fun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e2ennreal (ereal \<bar>c\<bar>) * e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) \<le> ennreal \<bar>c\<bar> * e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
e2ennreal (esssup M (\<lambda>x. ereal \<bar>(c *\<^sub>R f) x\<bar>)) \<le> ennreal \<bar>c\<bar> * e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?c \<noteq> 0 \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(?c *\<^sub>R ?f) x\<bar>)) \<le> ennreal \<bar>?c\<bar> * e2ennreal (esssup M (\<lambda>x. ereal \<bar>?f x\<bar>))

goal (2 subgoals):
 1. eNorm (\<LL> \<infinity> M) f = (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)
 2. defect (\<LL> \<infinity> M) = 1
[PROOF STEP]
have "esssup M (\<lambda>x. ereal 0) \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal 0) \<le> 0
[PROOF STEP]
using esssup_I
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?f \<in> borel_measurable ?M; AE x in ?M. ?f x \<le> ?c\<rbrakk> \<Longrightarrow> esssup ?M ?f \<le> ?c

goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal 0) \<le> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
esssup M (\<lambda>x. ereal 0) \<le> 0

goal (2 subgoals):
 1. eNorm (\<LL> \<infinity> M) f = (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)
 2. defect (\<LL> \<infinity> M) = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
esssup M (\<lambda>x. ereal 0) \<le> 0
[PROOF STEP]
have Z: "e2ennreal (esssup M (\<lambda>x. ereal 0)) = 0"
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal 0) \<le> 0

goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal 0)) = 0
[PROOF STEP]
using e2ennreal_neg
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal 0) \<le> 0
?x \<le> 0 \<Longrightarrow> e2ennreal ?x = 0

goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal 0)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e2ennreal (esssup M (\<lambda>x. ereal 0)) = 0

goal (2 subgoals):
 1. eNorm (\<LL> \<infinity> M) f = (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)
 2. defect (\<LL> \<infinity> M) = 1
[PROOF STEP]
have *: "quasinorm_on (borel_measurable M) 1 (\<lambda>(f::'a\<Rightarrow>real). e2ennreal(esssup M (\<lambda>x. ereal \<bar>f x\<bar>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quasinorm_on (borel_measurable M) 1 (\<lambda>f. e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)))
[PROOF STEP]
apply (rule quasinorm_onI)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> borel_measurable M; y \<in> borel_measurable M\<rbrakk> \<Longrightarrow> x + y \<in> borel_measurable M
 2. \<And>x y. \<lbrakk>x \<in> borel_measurable M; y \<in> borel_measurable M\<rbrakk> \<Longrightarrow> e2ennreal (esssup M (\<lambda>xa. ereal \<bar>(x + y) xa\<bar>)) \<le> ennreal 1 * e2ennreal (esssup M (\<lambda>xa. ereal \<bar>x xa\<bar>)) + ennreal 1 * e2ennreal (esssup M (\<lambda>x. ereal \<bar>y x\<bar>))
 3. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> borel_measurable M\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> borel_measurable M
 4. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> borel_measurable M\<rbrakk> \<Longrightarrow> e2ennreal (esssup M (\<lambda>xa. ereal \<bar>(c *\<^sub>R x) xa\<bar>)) \<le> ennreal \<bar>c\<bar> * e2ennreal (esssup M (\<lambda>xa. ereal \<bar>x xa\<bar>))
 5. 0 \<in> borel_measurable M
 6. e2ennreal (esssup M (\<lambda>x. ereal \<bar>0 x\<bar>)) = 0
 7. 1 \<le> 1
[PROOF STEP]
using T H Z
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?f \<in> borel_measurable M; ?g \<in> borel_measurable M\<rbrakk> \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(?f + ?g) x\<bar>)) \<le> e2ennreal (esssup M (\<lambda>x. ereal \<bar>?f x\<bar>)) + e2ennreal (esssup M (\<lambda>x. ereal \<bar>?g x\<bar>))
?c \<noteq> 0 \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>(?c *\<^sub>R ?f) x\<bar>)) \<le> ennreal \<bar>?c\<bar> * e2ennreal (esssup M (\<lambda>x. ereal \<bar>?f x\<bar>))
e2ennreal (esssup M (\<lambda>x. ereal 0)) = 0

goal (7 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> borel_measurable M; y \<in> borel_measurable M\<rbrakk> \<Longrightarrow> x + y \<in> borel_measurable M
 2. \<And>x y. \<lbrakk>x \<in> borel_measurable M; y \<in> borel_measurable M\<rbrakk> \<Longrightarrow> e2ennreal (esssup M (\<lambda>xa. ereal \<bar>(x + y) xa\<bar>)) \<le> ennreal 1 * e2ennreal (esssup M (\<lambda>xa. ereal \<bar>x xa\<bar>)) + ennreal 1 * e2ennreal (esssup M (\<lambda>x. ereal \<bar>y x\<bar>))
 3. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> borel_measurable M\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> borel_measurable M
 4. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> borel_measurable M\<rbrakk> \<Longrightarrow> e2ennreal (esssup M (\<lambda>xa. ereal \<bar>(c *\<^sub>R x) xa\<bar>)) \<le> ennreal \<bar>c\<bar> * e2ennreal (esssup M (\<lambda>xa. ereal \<bar>x xa\<bar>))
 5. 0 \<in> borel_measurable M
 6. e2ennreal (esssup M (\<lambda>x. ereal \<bar>0 x\<bar>)) = 0
 7. 1 \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
quasinorm_on (borel_measurable M) 1 (\<lambda>f. e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)))

goal (2 subgoals):
 1. eNorm (\<LL> \<infinity> M) f = (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)
 2. defect (\<LL> \<infinity> M) = 1
[PROOF STEP]
have **: "quasinorm_on UNIV 1 (\<lambda>(f::'a\<Rightarrow>real). if f \<in> borel_measurable M then e2ennreal(esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quasinorm_on UNIV 1 (\<lambda>f. if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)
[PROOF STEP]
by (rule extend_quasinorm[OF *])
[PROOF STATE]
proof (state)
this:
quasinorm_on UNIV 1 (\<lambda>f. if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)

goal (2 subgoals):
 1. eNorm (\<LL> \<infinity> M) f = (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)
 2. defect (\<LL> \<infinity> M) = 1
[PROOF STEP]
show "eNorm (\<LL> \<infinity> M) f = (if f \<in> borel_measurable M then e2ennreal(esssup M (\<lambda>x. \<bar>f x\<bar>)) else \<infinity>)"
       "defect (\<LL> \<infinity> M) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> \<infinity> M) f = (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>) &&& defect (\<LL> \<infinity> M) = 1
[PROOF STEP]
unfolding Lp_space_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (if \<infinity> = 0 then quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>) else if \<infinity> < \<infinity> then quasinorm_of (if \<infinity> < 1 then 2 powr (1 / enn2real \<infinity> - 1) else 1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr enn2real \<infinity>) then ennreal ((LINT x|M. \<bar>f x\<bar> powr enn2real \<infinity>) powr (1 / enn2real \<infinity>)) else \<infinity>) else quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)) f = (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>) &&& defect (if \<infinity> = 0 then quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>) else if \<infinity> < \<infinity> then quasinorm_of (if \<infinity> < 1 then 2 powr (1 / enn2real \<infinity> - 1) else 1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr enn2real \<infinity>) then ennreal ((LINT x|M. \<bar>f x\<bar> powr enn2real \<infinity>) powr (1 / enn2real \<infinity>)) else \<infinity>) else quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)) = 1
[PROOF STEP]
using quasinorm_of[OF **]
[PROOF STATE]
proof (prove)
using this:
eNorm (quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)) ?x = (if ?x \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>?x x\<bar>)) else \<infinity>)
defect (quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)) = 1

goal (1 subgoal):
 1. eNorm (if \<infinity> = 0 then quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>) else if \<infinity> < \<infinity> then quasinorm_of (if \<infinity> < 1 then 2 powr (1 / enn2real \<infinity> - 1) else 1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr enn2real \<infinity>) then ennreal ((LINT x|M. \<bar>f x\<bar> powr enn2real \<infinity>) powr (1 / enn2real \<infinity>)) else \<infinity>) else quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)) f = (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>) &&& defect (if \<infinity> = 0 then quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then 0 else \<infinity>) else if \<infinity> < \<infinity> then quasinorm_of (if \<infinity> < 1 then 2 powr (1 / enn2real \<infinity> - 1) else 1, \<lambda>f. if f \<in> borel_measurable M \<and> integrable M (\<lambda>x. \<bar>f x\<bar> powr enn2real \<infinity>) then ennreal ((LINT x|M. \<bar>f x\<bar> powr enn2real \<infinity>) powr (1 / enn2real \<infinity>)) else \<infinity>) else quasinorm_of (1, \<lambda>f. if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> \<infinity> M) f = (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)
defect (\<LL> \<infinity> M) = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma L_infinity_zero_space:
  "zero_space\<^sub>N (\<LL> \<infinity> M) = {f \<in> borel_measurable M. AE x in M. f x = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_space\<^sub>N (\<LL> \<infinity> M) = {f \<in> borel_measurable M. AE x in M. f x = 0}
[PROOF STEP]
proof (auto simp del: infinity_ennreal_def)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> zero_space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> x \<in> borel_measurable M
 2. \<And>x. x \<in> zero_space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> AE xa in M. x xa = 0
 3. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> zero_space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> x \<in> borel_measurable M
 2. \<And>x. x \<in> zero_space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> AE xa in M. x xa = 0
 3. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
assume H: "f \<in> zero_space\<^sub>N (\<LL> \<infinity> M)"
[PROOF STATE]
proof (state)
this:
f \<in> zero_space\<^sub>N (\<LL> \<infinity> M)

goal (3 subgoals):
 1. \<And>x. x \<in> zero_space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> x \<in> borel_measurable M
 2. \<And>x. x \<in> zero_space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> AE xa in M. x xa = 0
 3. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> zero_space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
show "f \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
using this:
f \<in> zero_space\<^sub>N (\<LL> \<infinity> M)

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

goal (1 subgoal):
 1. f \<in> borel_measurable M
[PROOF STEP]
using L_infinity(1)[of M] top.not_eq_extremum
[PROOF STATE]
proof (prove)
using this:
f \<in> {f. eNorm (\<LL> \<infinity> M) f = 0}
eNorm (\<LL> \<infinity> M) ?f = (if ?f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>?f x\<bar>)) else \<infinity>)
(?a \<noteq> \<top>) = (?a < \<top>)

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

goal (2 subgoals):
 1. \<And>x. x \<in> zero_space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> AE xa in M. x xa = 0
 2. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> borel_measurable M
[PROOF STEP]
have *: "e2ennreal(esssup M (\<lambda>x. \<bar>f x\<bar>)) = 0"
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M

goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) = 0
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M
f \<in> zero_space\<^sub>N (\<LL> \<infinity> M)

goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) = 0
[PROOF STEP]
unfolding zero_space\<^sub>N_def
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M
f \<in> {f. eNorm (\<LL> \<infinity> M) f = 0}

goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) = 0
[PROOF STEP]
using L_infinity(1)[of M] e2ennreal_infty
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M
f \<in> {f. eNorm (\<LL> \<infinity> M) f = 0}
eNorm (\<LL> \<infinity> M) ?f = (if ?f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>?f x\<bar>)) else \<infinity>)
e2ennreal \<infinity> = \<top>

goal (1 subgoal):
 1. e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) = 0

goal (2 subgoals):
 1. \<And>x. x \<in> zero_space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> AE xa in M. x xa = 0
 2. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) = 0
[PROOF STEP]
have "esssup M (\<lambda>x. \<bar>f x\<bar>) \<le> 0"
[PROOF STATE]
proof (prove)
using this:
e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) = 0

goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> 0
[PROOF STEP]
by (metis e2ennreal_infty e2ennreal_mult ennreal_top_neq_zero ereal_mult_infty leI linear mult_zero_left)
[PROOF STATE]
proof (state)
this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> 0

goal (2 subgoals):
 1. \<And>x. x \<in> zero_space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> AE xa in M. x xa = 0
 2. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> 0
[PROOF STEP]
have "f x = 0" if "ereal \<bar>f x\<bar> \<le> esssup M (\<lambda>x. \<bar>f x\<bar>)" for x
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> 0

goal (1 subgoal):
 1. f x = 0
[PROOF STEP]
using that order.trans
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> 0
ereal \<bar>f x\<bar> \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>)
\<lbrakk>?a \<le> ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a \<le> ?c

goal (1 subgoal):
 1. f x = 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ereal \<bar>f ?x\<bar> \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<Longrightarrow> f ?x = 0

goal (2 subgoals):
 1. \<And>x. x \<in> zero_space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> AE xa in M. x xa = 0
 2. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ereal \<bar>f ?x\<bar> \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<Longrightarrow> f ?x = 0
[PROOF STEP]
show "AE x in M. f x = 0"
[PROOF STATE]
proof (prove)
using this:
ereal \<bar>f ?x\<bar> \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<Longrightarrow> f ?x = 0

goal (1 subgoal):
 1. AE x in M. f x = 0
[PROOF STEP]
using esssup_AE[of "\<lambda>x. ereal \<bar>f x\<bar>" M]
[PROOF STATE]
proof (prove)
using this:
ereal \<bar>f ?x\<bar> \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<Longrightarrow> f ?x = 0
AE x in M. ereal \<bar>f x\<bar> \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>)

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
fix f::"'a \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
assume H: "f \<in> borel_measurable M" "AE x in M. f x = 0"
[PROOF STATE]
proof (state)
this:
f \<in> borel_measurable M
AE x in M. f x = 0

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> borel_measurable M
AE x in M. f x = 0
[PROOF STEP]
have "esssup M (\<lambda>x. \<bar>f x\<bar>) \<le> 0"
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M
AE x in M. f x = 0

goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> 0
[PROOF STEP]
using esssup_I
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M
AE x in M. f x = 0
\<lbrakk>?f \<in> borel_measurable ?M; AE x in ?M. ?f x \<le> ?c\<rbrakk> \<Longrightarrow> esssup ?M ?f \<le> ?c

goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> 0

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> 0
[PROOF STEP]
have "eNorm (\<LL> \<infinity> M) f = 0"
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> 0

goal (1 subgoal):
 1. eNorm (\<LL> \<infinity> M) f = 0
[PROOF STEP]
unfolding L_infinity(1)
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> 0

goal (1 subgoal):
 1. (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>) = 0
[PROOF STEP]
using H(1)
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> 0
f \<in> borel_measurable M

goal (1 subgoal):
 1. (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>) = 0
[PROOF STEP]
by (simp add: e2ennreal_neg)
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> \<infinity> M) f = 0

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> borel_measurable M; AE xa in M. x xa = 0\<rbrakk> \<Longrightarrow> x \<in> zero_space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> \<infinity> M) f = 0
[PROOF STEP]
show "f \<in> zero_space\<^sub>N (\<LL> \<infinity> M)"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> \<infinity> M) f = 0

goal (1 subgoal):
 1. f \<in> zero_space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
using zero_spaceN_iff
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> \<infinity> M) f = 0
(?x \<in> zero_space\<^sub>N ?N) = (eNorm ?N ?x = 0)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma L_infinity_AE_ebound:
  "AE x in M. ennreal \<bar>f x\<bar> \<le> eNorm (\<LL> \<infinity> M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. ennreal \<bar>f x\<bar> \<le> eNorm (\<LL> \<infinity> M) f
[PROOF STEP]
proof (cases "f \<in> borel_measurable M")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f \<in> borel_measurable M \<Longrightarrow> AE x in M. ennreal \<bar>f x\<bar> \<le> eNorm (\<LL> \<infinity> M) f
 2. f \<notin> borel_measurable M \<Longrightarrow> AE x in M. ennreal \<bar>f x\<bar> \<le> eNorm (\<LL> \<infinity> M) f
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
f \<notin> borel_measurable M

goal (2 subgoals):
 1. f \<in> borel_measurable M \<Longrightarrow> AE x in M. ennreal \<bar>f x\<bar> \<le> eNorm (\<LL> \<infinity> M) f
 2. f \<notin> borel_measurable M \<Longrightarrow> AE x in M. ennreal \<bar>f x\<bar> \<le> eNorm (\<LL> \<infinity> M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<notin> borel_measurable M
[PROOF STEP]
have "eNorm (\<LL> \<infinity> M) f = \<infinity>"
[PROOF STATE]
proof (prove)
using this:
f \<notin> borel_measurable M

goal (1 subgoal):
 1. eNorm (\<LL> \<infinity> M) f = \<infinity>
[PROOF STEP]
unfolding L_infinity(1)
[PROOF STATE]
proof (prove)
using this:
f \<notin> borel_measurable M

goal (1 subgoal):
 1. (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>) = \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> \<infinity> M) f = \<infinity>

goal (2 subgoals):
 1. f \<in> borel_measurable M \<Longrightarrow> AE x in M. ennreal \<bar>f x\<bar> \<le> eNorm (\<LL> \<infinity> M) f
 2. f \<notin> borel_measurable M \<Longrightarrow> AE x in M. ennreal \<bar>f x\<bar> \<le> eNorm (\<LL> \<infinity> M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> \<infinity> M) f = \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> \<infinity> M) f = \<infinity>

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

goal (1 subgoal):
 1. f \<in> borel_measurable M \<Longrightarrow> AE x in M. ennreal \<bar>f x\<bar> \<le> eNorm (\<LL> \<infinity> M) f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<in> borel_measurable M \<Longrightarrow> AE x in M. ennreal \<bar>f x\<bar> \<le> eNorm (\<LL> \<infinity> M) f
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
f \<in> borel_measurable M

goal (1 subgoal):
 1. f \<in> borel_measurable M \<Longrightarrow> AE x in M. ennreal \<bar>f x\<bar> \<le> eNorm (\<LL> \<infinity> M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> borel_measurable M
[PROOF STEP]
have "ennreal \<bar>f x\<bar> \<le> eNorm (\<LL> \<infinity> M) f" if "\<bar>f x\<bar> \<le> esssup M (\<lambda>x. \<bar>f x\<bar>)" for x
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M

goal (1 subgoal):
 1. ennreal \<bar>f x\<bar> \<le> eNorm (\<LL> \<infinity> M) f
[PROOF STEP]
unfolding L_infinity(1)
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M

goal (1 subgoal):
 1. ennreal \<bar>f x\<bar> \<le> (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)
[PROOF STEP]
using that e2ennreal_mono
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M
ereal \<bar>f x\<bar> \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>)
?x \<le> ?y \<Longrightarrow> e2ennreal ?x \<le> e2ennreal ?y

goal (1 subgoal):
 1. ennreal \<bar>f x\<bar> \<le> (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ereal \<bar>f ?x\<bar> \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<Longrightarrow> ennreal \<bar>f ?x\<bar> \<le> eNorm (\<LL> \<infinity> M) f

goal (1 subgoal):
 1. f \<in> borel_measurable M \<Longrightarrow> AE x in M. ennreal \<bar>f x\<bar> \<le> eNorm (\<LL> \<infinity> M) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ereal \<bar>f ?x\<bar> \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<Longrightarrow> ennreal \<bar>f ?x\<bar> \<le> eNorm (\<LL> \<infinity> M) f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ereal \<bar>f ?x\<bar> \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<Longrightarrow> ennreal \<bar>f ?x\<bar> \<le> eNorm (\<LL> \<infinity> M) f

goal (1 subgoal):
 1. AE x in M. ennreal \<bar>f x\<bar> \<le> eNorm (\<LL> \<infinity> M) f
[PROOF STEP]
using esssup_AE[of "\<lambda>x. ereal \<bar>f x\<bar>"]
[PROOF STATE]
proof (prove)
using this:
ereal \<bar>f ?x\<bar> \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<Longrightarrow> ennreal \<bar>f ?x\<bar> \<le> eNorm (\<LL> \<infinity> M) f
AE x in ?M. ereal \<bar>f x\<bar> \<le> esssup ?M (\<lambda>x. ereal \<bar>f x\<bar>)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma L_infinity_AE_bound:
  assumes "f \<in> space\<^sub>N (\<LL> \<infinity> M)"
  shows "AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f
[PROOF STEP]
using L_infinity_AE_ebound[of f M]
[PROOF STATE]
proof (prove)
using this:
AE x in M. ennreal \<bar>f x\<bar> \<le> eNorm (\<LL> \<infinity> M) f

goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> \<le> Norm (\<LL> \<infinity> M) f
[PROOF STEP]
unfolding eNorm_Norm[OF assms]
[PROOF STATE]
proof (prove)
using this:
AE x in M. ennreal \<bar>f x\<bar> \<le> ennreal (Norm (\<LL> \<infinity> M) f)

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


[STATEMENT]
lemma L_infinity_I:
  assumes "f \<in> borel_measurable M"
          "AE x in M. \<bar>f x\<bar> \<le> C"
          "C \<ge> 0"
  shows "f \<in> space\<^sub>N (\<LL> \<infinity> M)"
        "Norm (\<LL> \<infinity> M) f \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> \<infinity> M) &&& Norm (\<LL> \<infinity> M) f \<le> C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f \<in> space\<^sub>N (\<LL> \<infinity> M)
 2. Norm (\<LL> \<infinity> M) f \<le> C
[PROOF STEP]
show "f \<in> space\<^sub>N (\<LL> \<infinity> M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
using L_infinity_space assms(1) assms(2)
[PROOF STATE]
proof (prove)
using this:
space\<^sub>N (\<LL> \<infinity> ?M) = {f \<in> borel_measurable ?M. \<exists>C. AE x in ?M. \<bar>f x\<bar> \<le> C}
f \<in> borel_measurable M
AE x in M. \<bar>f x\<bar> \<le> C

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

goal (1 subgoal):
 1. Norm (\<LL> \<infinity> M) f \<le> C
[PROOF STEP]
have "esssup M (\<lambda>x. \<bar>f x\<bar>) \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> ereal C
[PROOF STEP]
using assms(1) assms(2) esssup_I
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M
AE x in M. \<bar>f x\<bar> \<le> C
\<lbrakk>?f \<in> borel_measurable ?M; AE x in ?M. ?f x \<le> ?c\<rbrakk> \<Longrightarrow> esssup ?M ?f \<le> ?c

goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> ereal C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> ereal C

goal (1 subgoal):
 1. Norm (\<LL> \<infinity> M) f \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> ereal C
[PROOF STEP]
have "eNorm (\<LL> \<infinity> M) f \<le> ereal C"
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> ereal C

goal (1 subgoal):
 1. eNorm (\<LL> \<infinity> M) f \<le> e2ennreal (ereal C)
[PROOF STEP]
unfolding L_infinity(1)
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> ereal C

goal (1 subgoal):
 1. (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>) \<le> e2ennreal (ereal C)
[PROOF STEP]
using assms(1) e2ennreal_mono
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> ereal C
f \<in> borel_measurable M
?x \<le> ?y \<Longrightarrow> e2ennreal ?x \<le> e2ennreal ?y

goal (1 subgoal):
 1. (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>) \<le> e2ennreal (ereal C)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> \<infinity> M) f \<le> e2ennreal (ereal C)

goal (1 subgoal):
 1. Norm (\<LL> \<infinity> M) f \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> \<infinity> M) f \<le> e2ennreal (ereal C)
[PROOF STEP]
have "ennreal (Norm (\<LL> \<infinity> M) f) \<le> ennreal C"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> \<infinity> M) f \<le> e2ennreal (ereal C)

goal (1 subgoal):
 1. ennreal (Norm (\<LL> \<infinity> M) f) \<le> ennreal C
[PROOF STEP]
using eNorm_Norm[OF \<open>f \<in> space\<^sub>N (\<LL> \<infinity> M)\<close>] assms(3)
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> \<infinity> M) f \<le> e2ennreal (ereal C)
eNorm (\<LL> \<infinity> M) f = ennreal (Norm (\<LL> \<infinity> M) f)
0 \<le> C

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

goal (1 subgoal):
 1. Norm (\<LL> \<infinity> M) f \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ennreal (Norm (\<LL> \<infinity> M) f) \<le> ennreal C
[PROOF STEP]
show "Norm (\<LL> \<infinity> M) f \<le> C"
[PROOF STATE]
proof (prove)
using this:
ennreal (Norm (\<LL> \<infinity> M) f) \<le> ennreal C

goal (1 subgoal):
 1. Norm (\<LL> \<infinity> M) f \<le> C
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
ennreal (Norm (\<LL> \<infinity> M) f) \<le> ennreal C
0 \<le> C

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma L_infinity_I':
  assumes [measurable]: "f \<in> borel_measurable M"
      and "AE x in M. ennreal \<bar>f x\<bar> \<le> C"
  shows "eNorm (\<LL> \<infinity> M) f \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> \<infinity> M) f \<le> C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eNorm (\<LL> \<infinity> M) f \<le> C
[PROOF STEP]
have "esssup M (\<lambda>x. \<bar>f x\<bar>) \<le> enn2ereal C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> enn2ereal C
[PROOF STEP]
apply (rule esssup_I, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. ereal \<bar>f x\<bar> \<le> enn2ereal C
[PROOF STEP]
using assms(2) less_eq_ennreal.rep_eq
[PROOF STATE]
proof (prove)
using this:
AE x in M. ennreal \<bar>f x\<bar> \<le> C
(?x \<le> ?xa) = (enn2ereal ?x \<le> enn2ereal ?xa)

goal (1 subgoal):
 1. AE x in M. ereal \<bar>f x\<bar> \<le> enn2ereal C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> enn2ereal C

goal (1 subgoal):
 1. eNorm (\<LL> \<infinity> M) f \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> enn2ereal C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> enn2ereal C

goal (1 subgoal):
 1. eNorm (\<LL> \<infinity> M) f \<le> C
[PROOF STEP]
unfolding L_infinity
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> enn2ereal C

goal (1 subgoal):
 1. (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>) \<le> C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> enn2ereal C
f \<in> borel_measurable M
AE x in M. ennreal \<bar>f x\<bar> \<le> C

goal (1 subgoal):
 1. (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>) \<le> C
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> enn2ereal C; AE x in M. ennreal \<bar>f x\<bar> \<le> C\<rbrakk> \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) \<le> C
[PROOF STEP]
using e2ennreal_mono
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> e2ennreal ?x \<le> e2ennreal ?y

goal (1 subgoal):
 1. \<lbrakk>esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> enn2ereal C; AE x in M. ennreal \<bar>f x\<bar> \<le> C\<rbrakk> \<Longrightarrow> e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) \<le> C
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> \<infinity> M) f \<le> C

goal:
No subgoals!
[PROOF STEP]
qed