Commit 8dd2a768 authored by haftmann's avatar haftmann
Browse files

simplified definition

parent 63ca4e334ffc
......@@ -51,8 +51,8 @@ shows "emeasure (lborel_f (Suc n)) A = \<integral>\<^sup>+ y. emeasure (lborel_f
proof -
{
fix x y assume "x\<in>space (lborel_f n)"
then have "(indicator A) (x(n := y)) = (indicator {x\<in>space (lborel_f n). x(n := y) \<in> A}) x" using indicator_def
by (metis (no_types, lifting) mem_Collect_eq)
then have "(indicator A) (x(n := y)) = (indicator {x\<in>space (lborel_f n). x(n := y) \<in> A}) x"
by (simp add: indicator_def)
}
then show ?thesis
unfolding nn_integral_indicator[OF assms(1), symmetric] nn_integral_indicator[OF assms(2), symmetric]
......
......@@ -1846,7 +1846,7 @@ proof -
also have "... = (\<integral>\<^sup>+y \<in> V \<union> U. e y \<partial>count_space UNIV)"
by (rule nn_integral_disjoint_pair_countspace[symmetric], auto simp add: U_def V_def)
also have "... = (\<integral>\<^sup>+(i, n). e (i, n) * indicator {..n} i \<partial>count_space UNIV)"
by (rule nn_integral_cong, auto simp add: indicator_def V_def U_def pos, meson)
by (rule nn_integral_cong, auto simp add: indicator_def of_bool_def V_def U_def pos, meson)
also have "... = (\<integral>\<^sup>+n. (\<integral>\<^sup>+i. e (i, n) * indicator {..n} i \<partial>count_space UNIV)\<partial>count_space UNIV)"
using nn_integral_snd_count_space[of "\<lambda>(i,n). e(i,n) * indicator {..n} i"] by auto
also have "... = (\<Sum>n. (\<Sum>i. e (i, n) * indicator {..n} i))"
......
......@@ -607,6 +607,9 @@ lemma sum_indicator_eq_card2:
using sum_mult_indicator [OF assms, of "\<lambda>y. 1::nat" P "\<lambda>y. x"]
unfolding card_eq_sum by auto
subclass (in zero_less_one) zero_neq_one
by standard (use zero_less_one in blast)
lemma disjoint_family_indicator_le_1:
assumes "disjoint_family_on A I"
shows "(\<Sum> i\<in> I. indicator (A i) x) \<le> (1::'a:: {comm_monoid_add,zero_less_one})"
......
......@@ -142,7 +142,7 @@ next
using add_scale_img assms by auto
qed
definition analytically_valid:: "'a::euclidean_space set \<Rightarrow> ('a \<Rightarrow> 'b::{euclidean_space,times,one}) \<Rightarrow> 'a \<Rightarrow> bool" where
definition analytically_valid:: "'a::euclidean_space set \<Rightarrow> ('a \<Rightarrow> 'b::{euclidean_space,times,zero_neq_one}) \<Rightarrow> 'a \<Rightarrow> bool" where
"analytically_valid s F i \<equiv>
(\<forall>a \<in> s. partially_vector_differentiable F i a) \<and>
continuous_on s F \<and> \<comment> \<open>TODO: should we replace this with saying that \<open>F\<close> is partially diffrerentiable on \<open>Dy\<close>,\<close>
......
......@@ -389,7 +389,7 @@ next
proof -
let ?w = "\<lambda>y. if (x, y) \<in> \<^bold>E then weight \<Gamma> y else 0"
have sum_w: "(\<Sum>\<^sup>+ y. if edge \<Gamma> x y then weight \<Gamma> y else 0) = (\<Sum>\<^sup>+ y \<in> \<^bold>E `` {x}. weight \<Gamma> y)"
by(simp add: nn_integral_count_space_indicator indicator_def if_distrib cong: if_cong)
by(simp add: nn_integral_count_space_indicator indicator_def of_bool_def if_distrib cong: if_cong)
have "(\<lambda>n. d_OUT (h (k n)) x) \<longlonglongrightarrow> d_OUT H x" unfolding d_OUT_def
by(rule nn_integral_dominated_convergence[where w="?w"])(use bounded_B x in \<open>simp_all add: AE_count_space H h_outside_E h_le_weight2 sum_w\<close>)
moreover define n_x where "n_x = to_nat_on (A \<Gamma>) x"
......
......@@ -1156,7 +1156,7 @@ proof -
by (auto dest: completion_ex_borel_measurable_real)
from I have "((\<lambda>x. abs (indicator \<Omega> x * f x)) has_integral I) UNIV"
using nonneg by (simp add: indicator_def if_distrib[of "\<lambda>x. x * f y" for y] cong: if_cong)
using nonneg by (simp add: indicator_def of_bool_def if_distrib[of "\<lambda>x. x * f y" for y] cong: if_cong)
also have "((\<lambda>x. abs (indicator \<Omega> x * f x)) has_integral I) UNIV \<longleftrightarrow> ((\<lambda>x. abs (f' x)) has_integral I) UNIV"
using eq by (intro has_integral_AE) auto
finally have "integral\<^sup>N lborel (\<lambda>x. abs (f' x)) = I"
......
......@@ -256,7 +256,8 @@ proof -
by (intro product_nn_integral_pair) auto
also have "\<dots> = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+y. (if x = y then 1 else 0) \<partial>M) \<partial>M)"
by (subst M.nn_integral_fst [symmetric]) simp_all
also have "\<dots> = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+y. indicator {x} y \<partial>M) \<partial>M)" by (simp add: indicator_def eq_commute)
also have "\<dots> = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+y. indicator {x} y \<partial>M) \<partial>M)"
by (simp add: indicator_def of_bool_def eq_commute)
also have "\<dots> = (\<integral>\<^sup>+ x. emeasure M {x} \<partial>M)" by (subst nn_integral_indicator) (simp_all add: M_def)
also have "\<dots> = (\<integral>\<^sup>+ x. 0 \<partial>M)" unfolding M_def
by (intro nn_integral_cong_AE refl AE_uniform_measureI) auto
......
......@@ -228,7 +228,7 @@ proof -
have "set_lebesgue_integral M A f = enn2real (set_nn_integral M A f)"
unfolding set_lebesgue_integral_def using assms(1,4) * eq
by (subst integral_eq_nn_integral)
(auto intro!: nn_integral_cong simp: indicator_def set_integrable_def mult_ac)
(auto intro!: nn_integral_cong simp: indicator_def of_bool_def set_integrable_def mult_ac)
also have "\<dots> = x" using assms by simp
finally show "set_lebesgue_integral M A f = x" .
qed
......
......@@ -256,7 +256,7 @@ proof -
by (auto dest: completion_ex_borel_measurable_real)
from I have "((\<lambda>x. abs (indicator \<Omega> x * f x)) has_integral I) UNIV"
using nonneg by (simp add: indicator_def if_distrib[of "\<lambda>x. x * f y" for y] cong: if_cong)
using nonneg by (simp add: indicator_def of_bool_def if_distrib[of "\<lambda>x. x * f y" for y] cong: if_cong)
also have "((\<lambda>x. abs (indicator \<Omega> x * f x)) has_integral I) UNIV \<longleftrightarrow> ((\<lambda>x. abs (f' x)) has_integral I) UNIV"
using eq by (intro has_integral_AE) auto
finally have "integral\<^sup>N lborel (\<lambda>x. abs (f' x)) = I"
......@@ -302,7 +302,8 @@ proof -
using assms eq by (intro nn_integral_lborel_eq_integral)
(auto simp: indicator_def set_borel_measurable_def)
also have "integral UNIV (\<lambda>x. indicator A x * f x) = integral A (\<lambda>x. indicator A x * f x)"
by (rule integral_spike_set) (auto simp: indicator_def)
by (rule integral_spike_set) (auto intro: empty_imp_negligible)
also have "\<dots> = integral A f"
by (rule integral_cong) (auto simp: indicator_def)
finally show ?thesis .
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment