1.1 --- a/NEWS Wed Apr 25 11:29:55 2012 +0200
1.2 +++ b/NEWS Wed Apr 25 14:28:13 2012 +0200
1.3 @@ -693,143 +693,143 @@
1.4 product_sigma_algebra
1.5
1.6 Removed constants:
1.7 + conditional_space
1.8 distribution -> use distr measure, or distributed predicate
1.9 + image_space
1.10 joint_distribution -> use distr measure, or distributed predicate
1.11 + pair_measure_generator
1.12 product_prob_space.infprod_algebra -> use PiM
1.13 subvimage
1.14 - image_space
1.15 - conditional_space
1.16 - pair_measure_generator
1.17
1.18 Replacement theorems:
1.19 - sigma_algebra.measurable_sigma -> measurable_measure_of
1.20 + finite_additivity_sufficient -> ring_of_sets.countably_additiveI_finite
1.21 + finite_measure.empty_measure -> measure_empty
1.22 + finite_measure.finite_continuity_from_above -> finite_measure.finite_Lim_measure_decseq
1.23 + finite_measure.finite_continuity_from_below -> finite_measure.finite_Lim_measure_incseq
1.24 + finite_measure.finite_measure_countably_subadditive -> finite_measure.finite_measure_subadditive_countably
1.25 + finite_measure.finite_measure_eq -> finite_measure.emeasure_eq_measure
1.26 + finite_measure.finite_measure -> finite_measure.emeasure_finite
1.27 + finite_measure.finite_measure_finite_singleton -> finite_measure.finite_measure_eq_setsum_singleton
1.28 + finite_measure.positive_measure' -> measure_nonneg
1.29 + finite_measure.real_measure -> finite_measure.emeasure_real
1.30 + finite_product_prob_space.finite_measure_times -> finite_product_prob_space.finite_measure_PiM_emb
1.31 + finite_product_sigma_algebra.in_P -> sets_PiM_I_finite
1.32 + finite_product_sigma_algebra.P_empty -> space_PiM_empty, sets_PiM_empty
1.33 + information_space.conditional_entropy_eq -> information_space.conditional_entropy_simple_distributed
1.34 + information_space.conditional_entropy_positive -> information_space.conditional_entropy_nonneg_simple
1.35 + information_space.conditional_mutual_information_eq_mutual_information -> information_space.conditional_mutual_information_eq_mutual_information_simple
1.36 + information_space.conditional_mutual_information_generic_positive -> information_space.conditional_mutual_information_nonneg_simple
1.37 + information_space.conditional_mutual_information_positive -> information_space.conditional_mutual_information_nonneg_simple
1.38 + information_space.entropy_commute -> information_space.entropy_commute_simple
1.39 + information_space.entropy_eq -> information_space.entropy_simple_distributed
1.40 + information_space.entropy_generic_eq -> information_space.entropy_simple_distributed
1.41 + information_space.entropy_positive -> information_space.entropy_nonneg_simple
1.42 + information_space.entropy_uniform_max -> information_space.entropy_uniform
1.43 + information_space.KL_eq_0_imp -> information_space.KL_eq_0_iff_eq
1.44 + information_space.KL_eq_0 -> information_space.KL_same_eq_0
1.45 + information_space.KL_ge_0 -> information_space.KL_nonneg
1.46 + information_space.mutual_information_eq -> information_space.mutual_information_simple_distributed
1.47 + information_space.mutual_information_positive -> information_space.mutual_information_nonneg_simple
1.48 + Int_stable_cuboids -> Int_stable_atLeastAtMost
1.49 + Int_stable_product_algebra_generator -> positive_integral
1.50 + measure_preserving -> equality "distr M N f = N" "f : measurable M N"
1.51 measure_space.additive -> emeasure_additive
1.52 + measure_space.AE_iff_null_set -> AE_iff_null
1.53 + measure_space.almost_everywhere_def -> eventually_ae_filter
1.54 + measure_space.almost_everywhere_vimage -> AE_distrD
1.55 + measure_space.continuity_from_above -> INF_emeasure_decseq
1.56 + measure_space.continuity_from_above_Lim -> Lim_emeasure_decseq
1.57 + measure_space.continuity_from_below_Lim -> Lim_emeasure_incseq
1.58 + measure_space.continuity_from_below -> SUP_emeasure_incseq
1.59 + measure_space_density -> emeasure_density
1.60 + measure_space.density_is_absolutely_continuous -> absolutely_continuousI_density
1.61 + measure_space.integrable_vimage -> integrable_distr
1.62 + measure_space.integral_translated_density -> integral_density
1.63 + measure_space.integral_vimage -> integral_distr
1.64 measure_space.measure_additive -> plus_emeasure
1.65 - measure_space.measure_mono -> emeasure_mono
1.66 - measure_space.measure_top -> emeasure_space
1.67 measure_space.measure_compl -> emeasure_compl
1.68 + measure_space.measure_countable_increasing -> emeasure_countable_increasing
1.69 + measure_space.measure_countably_subadditive -> emeasure_subadditive_countably
1.70 + measure_space.measure_decseq -> decseq_emeasure
1.71 measure_space.measure_Diff -> emeasure_Diff
1.72 - measure_space.measure_countable_increasing -> emeasure_countable_increasing
1.73 - measure_space.continuity_from_below -> SUP_emeasure_incseq
1.74 - measure_space.measure_incseq -> incseq_emeasure
1.75 - measure_space.continuity_from_below_Lim -> Lim_emeasure_incseq
1.76 - measure_space.measure_decseq -> decseq_emeasure
1.77 - measure_space.continuity_from_above -> INF_emeasure_decseq
1.78 - measure_space.measure_insert -> emeasure_insert
1.79 - measure_space.measure_setsum -> setsum_emeasure
1.80 - measure_space.measure_finite_singleton -> emeasure_eq_setsum_singleton
1.81 - finite_additivity_sufficient -> ring_of_sets.countably_additiveI_finite
1.82 - measure_space.measure_setsum_split -> setsum_emeasure_cover
1.83 - measure_space.measure_subadditive -> subadditive
1.84 - measure_space.measure_subadditive_finite -> emeasure_subadditive_finite
1.85 + measure_space.measure_Diff_null_set -> emeasure_Diff_null_set
1.86 measure_space.measure_eq_0 -> emeasure_eq_0
1.87 measure_space.measure_finitely_subadditive -> emeasure_subadditive_finite
1.88 - measure_space.measure_countably_subadditive -> emeasure_subadditive_countably
1.89 + measure_space.measure_finite_singleton -> emeasure_eq_setsum_singleton
1.90 + measure_space.measure_incseq -> incseq_emeasure
1.91 + measure_space.measure_insert -> emeasure_insert
1.92 + measure_space.measure_mono -> emeasure_mono
1.93 + measure_space.measure_not_negative -> emeasure_not_MInf
1.94 + measure_space.measure_preserving_Int_stable -> measure_eqI_generator_eq
1.95 + measure_space.measure_setsum -> setsum_emeasure
1.96 + measure_space.measure_setsum_split -> setsum_emeasure_cover
1.97 + measure_space.measure_space_vimage -> emeasure_distr
1.98 + measure_space.measure_subadditive_finite -> emeasure_subadditive_finite
1.99 + measure_space.measure_subadditive -> subadditive
1.100 + measure_space.measure_top -> emeasure_space
1.101 measure_space.measure_UN_eq_0 -> emeasure_UN_eq_0
1.102 - measure_unique_Int_stable -> measure_eqI_generator_eq
1.103 - measure_space.measure_Diff_null_set -> emeasure_Diff_null_set
1.104 measure_space.measure_Un_null_set -> emeasure_Un_null_set
1.105 - measure_space.almost_everywhere_def -> eventually_ae_filter
1.106 - measure_space.almost_everywhere_vimage -> AE_distrD
1.107 - measure_space.measure_space_vimage -> emeasure_distr
1.108 - measure_space.AE_iff_null_set -> AE_iff_null
1.109 + measure_space.positive_integral_translated_density -> positive_integral_density
1.110 + measure_space.positive_integral_vimage -> positive_integral_distr
1.111 + measure_space.real_continuity_from_above -> Lim_measure_decseq
1.112 + measure_space.real_continuity_from_below -> Lim_measure_incseq
1.113 + measure_space.real_measure_countably_subadditive -> measure_subadditive_countably
1.114 + measure_space.real_measure_Diff -> measure_Diff
1.115 + measure_space.real_measure_finite_Union -> measure_finite_Union
1.116 + measure_space.real_measure_setsum_singleton -> measure_eq_setsum_singleton
1.117 + measure_space.real_measure_subadditive -> measure_subadditive
1.118 measure_space.real_measure_Union -> measure_Union
1.119 - measure_space.real_measure_finite_Union -> measure_finite_Union
1.120 - measure_space.real_measure_Diff -> measure_Diff
1.121 measure_space.real_measure_UNION -> measure_UNION
1.122 - measure_space.real_measure_subadditive -> measure_subadditive
1.123 - measure_space.real_measure_setsum_singleton -> measure_eq_setsum_singleton
1.124 - measure_space.real_continuity_from_below -> Lim_measure_incseq
1.125 - measure_space.continuity_from_above_Lim -> Lim_emeasure_decseq
1.126 - measure_space.real_continuity_from_above -> Lim_measure_decseq
1.127 - measure_space.real_measure_countably_subadditive -> measure_subadditive_countably
1.128 - finite_measure.finite_measure -> finite_measure.emeasure_finite
1.129 - finite_measure.finite_measure_eq -> finite_measure.emeasure_eq_measure
1.130 - finite_measure.positive_measure' -> measure_nonneg
1.131 - finite_measure.real_measure -> finite_measure.emeasure_real
1.132 - finite_measure.empty_measure -> measure_empty
1.133 - finite_measure.finite_measure_countably_subadditive -> finite_measure.finite_measure_subadditive_countably
1.134 - finite_measure.finite_measure_finite_singleton -> finite_measure.finite_measure_eq_setsum_singleton
1.135 - finite_measure.finite_continuity_from_below -> finite_measure.finite_Lim_measure_incseq
1.136 - finite_measure.finite_continuity_from_above -> finite_measure.finite_Lim_measure_decseq
1.137 - measure_space.simple_integral_vimage -> simple_integral_distr
1.138 - measure_space.integrable_vimage -> integrable_distr
1.139 - measure_space.positive_integral_translated_density -> positive_integral_density
1.140 - measure_space.integral_translated_density -> integral_density
1.141 - measure_space.integral_vimage -> integral_distr
1.142 - measure_space_density -> emeasure_density
1.143 - measure_space.positive_integral_vimage -> positive_integral_distr
1.144 measure_space.simple_function_vimage -> simple_function_comp
1.145 measure_space.simple_integral_vimage -> simple_integral_distr
1.146 + measure_space.simple_integral_vimage -> simple_integral_distr
1.147 + measure_unique_Int_stable -> measure_eqI_generator_eq
1.148 + measure_unique_Int_stable_vimage -> measure_eqI_generator_eq
1.149 pair_sigma_algebra.measurable_cut_fst -> sets_Pair1
1.150 pair_sigma_algebra.measurable_cut_snd -> sets_Pair2
1.151 pair_sigma_algebra.measurable_pair_image_fst -> measurable_Pair1
1.152 pair_sigma_algebra.measurable_pair_image_snd -> measurable_Pair2
1.153 pair_sigma_algebra.measurable_product_swap -> measurable_pair_swap_iff
1.154 - pair_sigma_finite.measure_cut_measurable_fst -> pair_sigma_finite.measurable_emeasure_Pair1
1.155 - pair_sigma_finite.measure_cut_measurable_snd -> pair_sigma_finite.measurable_emeasure_Pair2
1.156 - measure_space.measure_not_negative -> emeasure_not_MInf
1.157 - pair_sigma_finite.measure_preserving_swap -> pair_sigma_finite.distr_pair_swap
1.158 - pair_sigma_finite.pair_measure_alt -> pair_sigma_finite.emeasure_pair_measure_alt
1.159 - pair_sigma_finite.pair_measure_alt2 -> pair_sigma_finite.emeasure_pair_measure_alt2
1.160 - pair_sigma_finite.pair_measure_times -> pair_sigma_finite.emeasure_pair_measure_Times
1.161 pair_sigma_algebra.pair_sigma_algebra_measurable -> measurable_pair_swap
1.162 pair_sigma_algebra.pair_sigma_algebra_swap_measurable -> measurable_pair_swap'
1.163 pair_sigma_algebra.sets_swap -> sets_pair_swap
1.164 - finite_product_sigma_algebra.in_P -> sets_PiM_I_finite
1.165 - Int_stable_product_algebra_generator -> positive_integral
1.166 - product_sigma_finite.measure_fold -> product_sigma_finite.distr_merge
1.167 - product_sigma_finite.measure_preserving_component_singelton -> product_sigma_finite.distr_singleton
1.168 - product_sigma_finite.measure_preserving_merge -> product_sigma_finite.distr_merge
1.169 - finite_product_sigma_algebra.P_empty -> space_PiM_empty, sets_PiM_empty
1.170 - product_algebra_generator_der -> prod_algebra_eq_finite
1.171 - product_algebra_generator_into_space -> prod_algebra_sets_into_space
1.172 - product_sigma_algebra.product_algebra_into_space -> space_closed
1.173 - product_algebraE -> prod_algebraE_all
1.174 - product_algebraI -> sets_PiM_I_finite
1.175 - product_measure_exists -> product_sigma_finite.sigma_finite
1.176 - sets_product_algebra -> sets_PiM
1.177 - sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq
1.178 - space_product_algebra -> space_PiM
1.179 - Int_stable_cuboids -> Int_stable_atLeastAtMost
1.180 - measure_space.density_is_absolutely_continuous -> absolutely_continuousI_density
1.181 - sigma_finite_measure.RN_deriv_vimage -> sigma_finite_measure.RN_deriv_distr
1.182 - prob_space_unique_Int_stable -> measure_eqI_prob_space
1.183 - sigma_finite_measure.disjoint_sigma_finite -> sigma_finite_disjoint
1.184 + pair_sigma_finite.measure_cut_measurable_fst -> pair_sigma_finite.measurable_emeasure_Pair1
1.185 + pair_sigma_finite.measure_cut_measurable_snd -> pair_sigma_finite.measurable_emeasure_Pair2
1.186 + pair_sigma_finite.measure_preserving_swap -> pair_sigma_finite.distr_pair_swap
1.187 + pair_sigma_finite.pair_measure_alt2 -> pair_sigma_finite.emeasure_pair_measure_alt2
1.188 + pair_sigma_finite.pair_measure_alt -> pair_sigma_finite.emeasure_pair_measure_alt
1.189 + pair_sigma_finite.pair_measure_times -> pair_sigma_finite.emeasure_pair_measure_Times
1.190 + prob_space.indep_distribution_eq_measure -> prob_space.indep_vars_iff_distr_eq_PiM
1.191 + prob_space.indep_var_distributionD -> prob_space.indep_var_distribution_eq
1.192 prob_space.measure_space_1 -> prob_space.emeasure_space_1
1.193 prob_space.prob_space_vimage -> prob_space_distr
1.194 prob_space.random_variable_restrict -> measurable_restrict
1.195 - measure_preserving -> equality "distr M N f = N" "f : measurable M N"
1.196 - measure_unique_Int_stable_vimage -> measure_eqI_generator_eq
1.197 - measure_space.measure_preserving_Int_stable -> measure_eqI_generator_eq
1.198 + prob_space_unique_Int_stable -> measure_eqI_prob_space
1.199 + product_algebraE -> prod_algebraE_all
1.200 + product_algebra_generator_der -> prod_algebra_eq_finite
1.201 + product_algebra_generator_into_space -> prod_algebra_sets_into_space
1.202 + product_algebraI -> sets_PiM_I_finite
1.203 + product_measure_exists -> product_sigma_finite.sigma_finite
1.204 product_prob_space.finite_index_eq_finite_product -> product_prob_space.sets_PiM_generator
1.205 product_prob_space.finite_measure_infprod_emb_Pi -> product_prob_space.measure_PiM_emb
1.206 - finite_product_prob_space.finite_measure_times -> finite_product_prob_space.finite_measure_PiM_emb
1.207 product_prob_space.infprod_spec -> product_prob_space.emeasure_PiM_emb_not_empty
1.208 product_prob_space.measurable_component -> measurable_component_singleton
1.209 product_prob_space.measurable_emb -> measurable_prod_emb
1.210 product_prob_space.measurable_into_infprod_algebra -> measurable_PiM_single
1.211 product_prob_space.measurable_singleton_infprod -> measurable_component_singleton
1.212 product_prob_space.measure_emb -> emeasure_prod_emb
1.213 + product_prob_space.measure_preserving_restrict -> product_prob_space.distr_restrict
1.214 + product_sigma_algebra.product_algebra_into_space -> space_closed
1.215 + product_sigma_finite.measure_fold -> product_sigma_finite.distr_merge
1.216 + product_sigma_finite.measure_preserving_component_singelton -> product_sigma_finite.distr_singleton
1.217 + product_sigma_finite.measure_preserving_merge -> product_sigma_finite.distr_merge
1.218 sequence_space.measure_infprod -> sequence_space.measure_PiM_countable
1.219 - product_prob_space.measure_preserving_restrict -> product_prob_space.distr_restrict
1.220 - prob_space.indep_distribution_eq_measure -> prob_space.indep_vars_iff_distr_eq_PiM
1.221 - prob_space.indep_var_distributionD -> prob_space.indep_var_distribution_eq
1.222 - conditional_entropy_positive -> conditional_entropy_nonneg_simple
1.223 - conditional_entropy_eq -> conditional_entropy_simple_distributed
1.224 - conditional_mutual_information_eq_mutual_information -> conditional_mutual_information_eq_mutual_information_simple
1.225 - conditional_mutual_information_generic_positive -> conditional_mutual_information_nonneg_simple
1.226 - conditional_mutual_information_positive -> conditional_mutual_information_nonneg_simple
1.227 - entropy_commute -> entropy_commute_simple
1.228 - entropy_eq -> entropy_simple_distributed
1.229 - entropy_generic_eq -> entropy_simple_distributed
1.230 - entropy_positive -> entropy_nonneg_simple
1.231 - entropy_uniform_max -> entropy_uniform
1.232 - KL_eq_0 -> KL_same_eq_0
1.233 - KL_eq_0_imp -> KL_eq_0_iff_eq
1.234 - KL_ge_0 -> KL_nonneg
1.235 - mutual_information_eq -> mutual_information_simple_distributed
1.236 - mutual_information_positive -> mutual_information_nonneg_simple
1.237 + sets_product_algebra -> sets_PiM
1.238 + sigma_algebra.measurable_sigma -> measurable_measure_of
1.239 + sigma_finite_measure.disjoint_sigma_finite -> sigma_finite_disjoint
1.240 + sigma_finite_measure.RN_deriv_vimage -> sigma_finite_measure.RN_deriv_distr
1.241 + sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq
1.242 + space_product_algebra -> space_PiM
1.243
1.244 * New "case_product" attribute to generate a case rule doing multiple
1.245 case distinctions at the same time. E.g.