# HG changeset patch
# User hoelzl
# Date 1430830337 -7200
# Node ID 831ddb69db9b70917576c5ab96082a9356a7a0be
# Parent  70d8f7abde8f5a1bcf5d344a9c880a3a560bcad6
add lfp/gfp rule for nn_integral

diff -r 70d8f7abde8f -r 831ddb69db9b src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon May 04 18:49:51 2015 +0200
+++ b/src/HOL/Nat.thy	Tue May 05 14:52:17 2015 +0200
@@ -1877,6 +1877,11 @@
   shows "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)"
   by (auto intro!: funpow_decreasing simp: mono_def)
 
+lemma antimono_funpow:
+  fixes Q :: "('i \<Rightarrow> 'a::{lattice, order_top}) \<Rightarrow> ('i \<Rightarrow> 'a)"
+  shows "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)"
+  by (auto intro!: funpow_increasing simp: antimono_def)
+
 subsection {* The divides relation on @{typ nat} *}
 
 lemma dvd_1_left [iff]: "Suc 0 dvd k"
diff -r 70d8f7abde8f -r 831ddb69db9b src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon May 04 18:49:51 2015 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Tue May 05 14:52:17 2015 +0200
@@ -838,6 +838,9 @@
   "(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^sup>N M u \<le> integral\<^sup>N M v"
   by (auto intro: nn_integral_mono_AE)
 
+lemma mono_nn_integral: "mono F \<Longrightarrow> mono (\<lambda>x. integral\<^sup>N M (F x))"
+  by (auto simp add: mono_def le_fun_def intro!: nn_integral_mono)
+
 lemma nn_integral_cong_AE:
   "AE x in M. u x = v x \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N M v"
   by (auto simp: eq_iff intro!: nn_integral_mono_AE)
@@ -1081,6 +1084,9 @@
   "0 \<le> c \<Longrightarrow> (\<integral>\<^sup>+ x. c \<partial>M) = c * (emeasure M) (space M)"
   by (subst nn_integral_eq_simple_integral) auto
 
+lemma nn_integral_const_nonpos: "c \<le> 0 \<Longrightarrow> nn_integral M (\<lambda>x. c) = 0"
+  using nn_integral_max_0[of M "\<lambda>x. c"] by (simp add: max_def split: split_if_asm)
+
 lemma nn_integral_linear:
   assumes f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" and "0 \<le> a"
   and g: "g \<in> borel_measurable M" "\<And>x. 0 \<le> g x"
@@ -1482,6 +1488,89 @@
     by (intro Liminf_eq_Limsup) auto
 qed
 
+lemma nn_integral_monotone_convergence_INF':
+  assumes f: "decseq f" and [measurable]: "\<And>i. f i \<in> borel_measurable M"
+  assumes "(\<integral>\<^sup>+ x. f 0 x \<partial>M) < \<infinity>" and nn: "\<And>x i. 0 \<le> f i x"
+  shows "(\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = (INF i. integral\<^sup>N M (f i))"
+proof (rule LIMSEQ_unique)
+  show "(\<lambda>i. integral\<^sup>N M (f i)) ----> (INF i. integral\<^sup>N M (f i))"
+    using f by (intro LIMSEQ_INF) (auto intro!: nn_integral_mono simp: decseq_def le_fun_def)
+  show "(\<lambda>i. integral\<^sup>N M (f i)) ----> \<integral>\<^sup>+ x. (INF i. f i x) \<partial>M"
+  proof (rule nn_integral_dominated_convergence)
+    show "(\<integral>\<^sup>+ x. f 0 x \<partial>M) < \<infinity>" "\<And>i. f i \<in> borel_measurable M" "f 0 \<in> borel_measurable M"
+      by fact+
+    show "\<And>j. AE x in M. 0 \<le> f j x"
+      using nn by auto
+    show "\<And>j. AE x in M. f j x \<le> f 0 x"
+      using f by (auto simp: decseq_def le_fun_def)
+    show "AE x in M. (\<lambda>i. f i x) ----> (INF i. f i x)"
+      using f by (auto intro!: LIMSEQ_INF simp: decseq_def le_fun_def)
+    show "(\<lambda>x. INF i. f i x) \<in> borel_measurable M"
+      by auto
+  qed
+qed
+
+lemma nn_integral_monotone_convergence_INF:
+  assumes f: "decseq f" and [measurable]: "\<And>i. f i \<in> borel_measurable M"
+  assumes fin: "(\<integral>\<^sup>+ x. f i x \<partial>M) < \<infinity>"
+  shows "(\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = (INF i. integral\<^sup>N M (f i))"
+proof -
+  { fix f :: "nat \<Rightarrow> ereal" and j assume "decseq f"
+    then have "(INF i. f i) = (INF i. f (i + j))"
+      apply (intro INF_eq)
+      apply (rule_tac x="i" in bexI)
+      apply (auto simp: decseq_def le_fun_def)
+      done }
+  note INF_shift = this
+
+  have dec: "\<And>f::nat \<Rightarrow> 'a \<Rightarrow> ereal. decseq f \<Longrightarrow> decseq (\<lambda>j x. max 0 (f (j + i) x))"
+    by (intro antimonoI le_funI max.mono) (auto simp: decseq_def le_fun_def)
+
+  have "(\<integral>\<^sup>+ x. max 0 (INF i. f i x) \<partial>M) = (\<integral>\<^sup>+ x. (INF i. max 0 (f i x)) \<partial>M)"
+    by (intro nn_integral_cong)
+       (simp add: sup_ereal_def[symmetric] sup_INF del: sup_ereal_def)
+  also have "\<dots> = (\<integral>\<^sup>+ x. (INF j. max 0 (f (j + i) x)) \<partial>M)"
+    using f by (intro nn_integral_cong INF_shift antimonoI le_funI max.mono) 
+               (auto simp: decseq_def le_fun_def)
+  also have "\<dots> = (INF j. (\<integral>\<^sup>+ x. max 0 (f (j + i) x) \<partial>M))"
+  proof (rule nn_integral_monotone_convergence_INF')
+    show "\<And>j. (\<lambda>x. max 0 (f (j + i) x)) \<in> borel_measurable M"
+      by measurable
+    show "(\<integral>\<^sup>+ x. max 0 (f (0 + i) x) \<partial>M) < \<infinity>"
+      using fin by (simp add: nn_integral_max_0)
+  qed (intro max.cobounded1 dec f)+
+  also have "\<dots> = (INF j. (\<integral>\<^sup>+ x. max 0 (f j x) \<partial>M))"
+    using f by (intro INF_shift[symmetric] nn_integral_mono antimonoI le_funI max.mono) 
+               (auto simp: decseq_def le_fun_def)
+  finally show ?thesis unfolding nn_integral_max_0 .
+qed
+
+lemma sup_continuous_nn_integral:
+  assumes f: "\<And>y. sup_continuous (f y)"
+  assumes [measurable]: "\<And>F x. (\<lambda>y. f y F x) \<in> borel_measurable (M x)"
+  shows "sup_continuous (\<lambda>F x. (\<integral>\<^sup>+y. f y F x \<partial>M x))"
+  unfolding sup_continuous_def
+proof safe
+  fix C :: "nat \<Rightarrow> 'b \<Rightarrow> ereal" assume C: "incseq C"
+  then show "(\<lambda>x. \<integral>\<^sup>+ y. f y (SUPREMUM UNIV C) x \<partial>M x) = (SUP i. (\<lambda>x. \<integral>\<^sup>+ y. f y (C i) x \<partial>M x))"
+    using sup_continuous_mono[OF f]
+    by (simp add: sup_continuousD[OF f C] fun_eq_iff nn_integral_monotone_convergence_SUP mono_def le_fun_def)
+qed
+
+lemma inf_continuous_nn_integral:
+  assumes f: "\<And>y. inf_continuous (f y)"
+  assumes [measurable]: "\<And>F x. (\<lambda>y. f y F x) \<in> borel_measurable (M x)"
+  assumes bnd: "\<And>x F. (\<integral>\<^sup>+ y. f y F x \<partial>M x) \<noteq> \<infinity>"
+  shows "inf_continuous (\<lambda>F x. (\<integral>\<^sup>+y. f y F x \<partial>M x))"
+  unfolding inf_continuous_def
+proof safe
+  fix C :: "nat \<Rightarrow> 'b \<Rightarrow> ereal" assume C: "decseq C"
+  then show "(\<lambda>x. \<integral>\<^sup>+ y. f y (INFIMUM UNIV C) x \<partial>M x) = (INF i. (\<lambda>x. \<integral>\<^sup>+ y. f y (C i) x \<partial>M x))"
+    using inf_continuous_mono[OF f]
+    by (auto simp add: inf_continuousD[OF f C] fun_eq_iff antimono_def mono_def le_fun_def bnd
+             intro!:  nn_integral_monotone_convergence_INF)
+qed
+
 lemma nn_integral_null_set:
   assumes "N \<in> null_sets M" shows "(\<integral>\<^sup>+ x. u x * indicator N x \<partial>M) = 0"
 proof -
@@ -1649,6 +1738,124 @@
     by (simp add: F_def)
 qed
 
+lemma nn_integral_lfp:
+  assumes sets: "\<And>s. sets (M s) = sets N"
+  assumes f: "sup_continuous f"
+  assumes meas: "\<And>F. F \<in> borel_measurable N \<Longrightarrow> f F \<in> borel_measurable N"
+  assumes nonneg: "\<And>F s. 0 \<le> g F s"
+  assumes g: "sup_continuous g"
+  assumes step: "\<And>F s. F \<in> borel_measurable N \<Longrightarrow> integral\<^sup>N (M s) (f F) = g (\<lambda>s. integral\<^sup>N (M s) F) s"
+  shows "(\<integral>\<^sup>+\<omega>. lfp f \<omega> \<partial>M s) = lfp g s"
+proof (rule antisym)
+  show "lfp g s \<le> (\<integral>\<^sup>+\<omega>. lfp f \<omega> \<partial>M s)"
+  proof (induction arbitrary: s rule: lfp_ordinal_induct[OF sup_continuous_mono[OF g]])
+    case (1 F) then show ?case
+      apply (subst lfp_unfold[OF sup_continuous_mono[OF f]])
+      apply (subst step)
+      apply (rule borel_measurable_lfp[OF f])
+      apply (rule meas)
+      apply assumption+
+      apply (rule monoD[OF sup_continuous_mono[OF g], THEN le_funD])
+      apply (simp add: le_fun_def)
+      done
+  qed (auto intro: SUP_least)
+
+  have lfp_nonneg: "\<And>s. 0 \<le> lfp g s"
+    by (subst lfp_unfold[OF sup_continuous_mono[OF g]]) (rule nonneg)
+
+  { fix i have "((f ^^ i) bot) \<in> borel_measurable N"
+      by (induction i) (simp_all add: meas) }
+
+  have "(\<integral>\<^sup>+\<omega>. lfp f \<omega> \<partial>M s) = (\<integral>\<^sup>+\<omega>. (SUP i. (f ^^ i) bot \<omega>) \<partial>M s)"
+    by (simp add: sup_continuous_lfp f)
+  also have "\<dots> = (SUP i. \<integral>\<^sup>+\<omega>. (f ^^ i) bot \<omega> \<partial>M s)"
+  proof (rule nn_integral_monotone_convergence_SUP)
+    show "incseq (\<lambda>i. (f ^^ i) bot)"
+      using f[THEN sup_continuous_mono] by (rule mono_funpow)
+    show "\<And>i. ((f ^^ i) bot) \<in> borel_measurable (M s)"
+      unfolding measurable_cong_sets[OF sets refl] by fact
+  qed
+  also have "\<dots> \<le> lfp g s"
+  proof (rule SUP_least)
+    fix i show "integral\<^sup>N (M s) ((f ^^ i) bot) \<le> lfp g s"
+    proof (induction i arbitrary: s)
+      case 0 then show ?case
+        by (simp add: nn_integral_const_nonpos lfp_nonneg)
+    next
+      case (Suc n)
+      show ?case
+        apply (simp del: bot_apply)
+        apply (subst step)
+        apply fact
+        apply (subst lfp_unfold[OF sup_continuous_mono[OF g]])
+        apply (rule monoD[OF sup_continuous_mono[OF g], THEN le_funD])
+        apply (rule le_funI)
+        apply (rule Suc)
+        done
+    qed
+  qed
+  finally show "(\<integral>\<^sup>+\<omega>. lfp f \<omega> \<partial>M s) \<le> lfp g s" .
+qed
+
+lemma nn_integral_gfp:
+  assumes sets: "\<And>s. sets (M s) = sets N"
+  assumes f: "inf_continuous f"
+  assumes meas: "\<And>F. F \<in> borel_measurable N \<Longrightarrow> f F \<in> borel_measurable N"
+  assumes bound: "\<And>F s. (\<integral>\<^sup>+x. f F x \<partial>M s) < \<infinity>"
+  assumes non_zero: "\<And>s. emeasure (M s) (space (M s)) \<noteq> 0"
+  assumes g: "inf_continuous g"
+  assumes step: "\<And>F s. F \<in> borel_measurable N \<Longrightarrow> integral\<^sup>N (M s) (f F) = g (\<lambda>s. integral\<^sup>N (M s) F) s"
+  shows "(\<integral>\<^sup>+\<omega>. gfp f \<omega> \<partial>M s) = gfp g s"
+proof (rule antisym)
+  show "(\<integral>\<^sup>+\<omega>. gfp f \<omega> \<partial>M s) \<le> gfp g s"
+  proof (induction arbitrary: s rule: gfp_ordinal_induct[OF inf_continuous_mono[OF g]])
+    case (1 F) then show ?case
+      apply (subst gfp_unfold[OF inf_continuous_mono[OF f]])
+      apply (subst step)
+      apply (rule borel_measurable_gfp[OF f])
+      apply (rule meas)
+      apply assumption+
+      apply (rule monoD[OF inf_continuous_mono[OF g], THEN le_funD])
+      apply (simp add: le_fun_def)
+      done
+  qed (auto intro: INF_greatest)
+
+  { fix i have "((f ^^ i) top) \<in> borel_measurable N"
+      by (induction i) (simp_all add: meas) }
+
+  have "(\<integral>\<^sup>+\<omega>. gfp f \<omega> \<partial>M s) = (\<integral>\<^sup>+\<omega>. (INF i. (f ^^ i) top \<omega>) \<partial>M s)"
+    by (simp add: inf_continuous_gfp f)
+  also have "\<dots> = (INF i. \<integral>\<^sup>+\<omega>. (f ^^ i) top \<omega> \<partial>M s)"
+  proof (rule nn_integral_monotone_convergence_INF)
+    show "decseq (\<lambda>i. (f ^^ i) top)"
+      using f[THEN inf_continuous_mono] by (rule antimono_funpow)
+    show "\<And>i. ((f ^^ i) top) \<in> borel_measurable (M s)"
+      unfolding measurable_cong_sets[OF sets refl] by fact
+    show "integral\<^sup>N (M s) ((f ^^ 1) top) < \<infinity>"
+      using bound[of s top] by simp
+  qed
+  also have "\<dots> \<ge> gfp g s"
+  proof (rule INF_greatest)
+    fix i show "gfp g s \<le> integral\<^sup>N (M s) ((f ^^ i) top)"
+    proof (induction i arbitrary: s)
+      case 0 with non_zero[of s] show ?case
+        by (simp add: top_ereal_def less_le emeasure_nonneg)
+    next
+      case (Suc n)
+      show ?case
+        apply (simp del: top_apply)
+        apply (subst step)
+        apply fact
+        apply (subst gfp_unfold[OF inf_continuous_mono[OF g]])
+        apply (rule monoD[OF inf_continuous_mono[OF g], THEN le_funD])
+        apply (rule le_funI)
+        apply (rule Suc)
+        done
+    qed
+  qed
+  finally show "gfp g s \<le> (\<integral>\<^sup>+\<omega>. gfp f \<omega> \<partial>M s)" .
+qed
+
 subsection {* Integral under concrete measures *}
 
 lemma nn_integral_empty: