NEWS
changeset 47751 f98bbb445c06
parent 47706 3eef88e8496b
child 47806 7e009f4e9f47
     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.measure_additive -> plus_emeasure
    1.53 -  measure_space.measure_mono -> emeasure_mono
    1.54 -  measure_space.measure_top -> emeasure_space
    1.55 -  measure_space.measure_compl -> emeasure_compl
    1.56 -  measure_space.measure_Diff -> emeasure_Diff
    1.57 -  measure_space.measure_countable_increasing -> emeasure_countable_increasing
    1.58 +  measure_space.AE_iff_null_set -> AE_iff_null
    1.59 +  measure_space.almost_everywhere_def -> eventually_ae_filter
    1.60 +  measure_space.almost_everywhere_vimage -> AE_distrD
    1.61 +  measure_space.continuity_from_above -> INF_emeasure_decseq
    1.62 +  measure_space.continuity_from_above_Lim -> Lim_emeasure_decseq
    1.63 +  measure_space.continuity_from_below_Lim -> Lim_emeasure_incseq
    1.64    measure_space.continuity_from_below -> SUP_emeasure_incseq
    1.65 -  measure_space.measure_incseq -> incseq_emeasure
    1.66 -  measure_space.continuity_from_below_Lim -> Lim_emeasure_incseq
    1.67 +  measure_space_density -> emeasure_density
    1.68 +  measure_space.density_is_absolutely_continuous -> absolutely_continuousI_density
    1.69 +  measure_space.integrable_vimage -> integrable_distr
    1.70 +  measure_space.integral_translated_density -> integral_density
    1.71 +  measure_space.integral_vimage -> integral_distr
    1.72 +  measure_space.measure_additive -> plus_emeasure
    1.73 +  measure_space.measure_compl -> emeasure_compl
    1.74 +  measure_space.measure_countable_increasing -> emeasure_countable_increasing
    1.75 +  measure_space.measure_countably_subadditive -> emeasure_subadditive_countably
    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 -> emeasure_Diff
    1.86 +  measure_space.measure_Diff_null_set -> emeasure_Diff_null_set
    1.87    measure_space.measure_eq_0 -> emeasure_eq_0
    1.88    measure_space.measure_finitely_subadditive -> emeasure_subadditive_finite
    1.89 -  measure_space.measure_countably_subadditive -> emeasure_subadditive_countably
    1.90 -  measure_space.measure_UN_eq_0 -> emeasure_UN_eq_0
    1.91 -  measure_unique_Int_stable -> measure_eqI_generator_eq
    1.92 -  measure_space.measure_Diff_null_set -> emeasure_Diff_null_set
    1.93 -  measure_space.measure_Un_null_set -> emeasure_Un_null_set
    1.94 -  measure_space.almost_everywhere_def -> eventually_ae_filter
    1.95 -  measure_space.almost_everywhere_vimage -> AE_distrD
    1.96 +  measure_space.measure_finite_singleton -> emeasure_eq_setsum_singleton
    1.97 +  measure_space.measure_incseq -> incseq_emeasure
    1.98 +  measure_space.measure_insert -> emeasure_insert
    1.99 +  measure_space.measure_mono -> emeasure_mono
   1.100 +  measure_space.measure_not_negative -> emeasure_not_MInf
   1.101 +  measure_space.measure_preserving_Int_stable -> measure_eqI_generator_eq
   1.102 +  measure_space.measure_setsum -> setsum_emeasure
   1.103 +  measure_space.measure_setsum_split -> setsum_emeasure_cover
   1.104    measure_space.measure_space_vimage -> emeasure_distr
   1.105 -  measure_space.AE_iff_null_set -> AE_iff_null
   1.106 -  measure_space.real_measure_Union -> measure_Union
   1.107 -  measure_space.real_measure_finite_Union -> measure_finite_Union
   1.108 -  measure_space.real_measure_Diff -> measure_Diff
   1.109 -  measure_space.real_measure_UNION -> measure_UNION
   1.110 -  measure_space.real_measure_subadditive -> measure_subadditive
   1.111 -  measure_space.real_measure_setsum_singleton -> measure_eq_setsum_singleton
   1.112 -  measure_space.real_continuity_from_below -> Lim_measure_incseq
   1.113 -  measure_space.continuity_from_above_Lim -> Lim_emeasure_decseq
   1.114 +  measure_space.measure_subadditive_finite -> emeasure_subadditive_finite
   1.115 +  measure_space.measure_subadditive -> subadditive
   1.116 +  measure_space.measure_top -> emeasure_space
   1.117 +  measure_space.measure_UN_eq_0 -> emeasure_UN_eq_0
   1.118 +  measure_space.measure_Un_null_set -> emeasure_Un_null_set
   1.119 +  measure_space.positive_integral_translated_density -> positive_integral_density
   1.120 +  measure_space.positive_integral_vimage -> positive_integral_distr
   1.121    measure_space.real_continuity_from_above -> Lim_measure_decseq
   1.122 +  measure_space.real_continuity_from_below -> Lim_measure_incseq
   1.123    measure_space.real_measure_countably_subadditive -> measure_subadditive_countably
   1.124 -  finite_measure.finite_measure -> finite_measure.emeasure_finite
   1.125 -  finite_measure.finite_measure_eq -> finite_measure.emeasure_eq_measure
   1.126 -  finite_measure.positive_measure' -> measure_nonneg
   1.127 -  finite_measure.real_measure -> finite_measure.emeasure_real
   1.128 -  finite_measure.empty_measure -> measure_empty
   1.129 -  finite_measure.finite_measure_countably_subadditive -> finite_measure.finite_measure_subadditive_countably
   1.130 -  finite_measure.finite_measure_finite_singleton -> finite_measure.finite_measure_eq_setsum_singleton
   1.131 -  finite_measure.finite_continuity_from_below -> finite_measure.finite_Lim_measure_incseq
   1.132 -  finite_measure.finite_continuity_from_above -> finite_measure.finite_Lim_measure_decseq
   1.133 -  measure_space.simple_integral_vimage -> simple_integral_distr
   1.134 -  measure_space.integrable_vimage -> integrable_distr
   1.135 -  measure_space.positive_integral_translated_density -> positive_integral_density
   1.136 -  measure_space.integral_translated_density -> integral_density
   1.137 -  measure_space.integral_vimage -> integral_distr
   1.138 -  measure_space_density -> emeasure_density
   1.139 -  measure_space.positive_integral_vimage -> positive_integral_distr
   1.140 +  measure_space.real_measure_Diff -> measure_Diff
   1.141 +  measure_space.real_measure_finite_Union -> measure_finite_Union
   1.142 +  measure_space.real_measure_setsum_singleton -> measure_eq_setsum_singleton
   1.143 +  measure_space.real_measure_subadditive -> measure_subadditive
   1.144 +  measure_space.real_measure_Union -> measure_Union
   1.145 +  measure_space.real_measure_UNION -> measure_UNION
   1.146    measure_space.simple_function_vimage -> simple_function_comp
   1.147    measure_space.simple_integral_vimage -> simple_integral_distr
   1.148 +  measure_space.simple_integral_vimage -> simple_integral_distr
   1.149 +  measure_unique_Int_stable -> measure_eqI_generator_eq
   1.150 +  measure_unique_Int_stable_vimage -> measure_eqI_generator_eq
   1.151    pair_sigma_algebra.measurable_cut_fst -> sets_Pair1
   1.152    pair_sigma_algebra.measurable_cut_snd -> sets_Pair2
   1.153    pair_sigma_algebra.measurable_pair_image_fst -> measurable_Pair1
   1.154    pair_sigma_algebra.measurable_pair_image_snd -> measurable_Pair2
   1.155    pair_sigma_algebra.measurable_product_swap -> measurable_pair_swap_iff
   1.156 -  pair_sigma_finite.measure_cut_measurable_fst -> pair_sigma_finite.measurable_emeasure_Pair1
   1.157 -  pair_sigma_finite.measure_cut_measurable_snd -> pair_sigma_finite.measurable_emeasure_Pair2
   1.158 -  measure_space.measure_not_negative -> emeasure_not_MInf
   1.159 -  pair_sigma_finite.measure_preserving_swap -> pair_sigma_finite.distr_pair_swap
   1.160 -  pair_sigma_finite.pair_measure_alt -> pair_sigma_finite.emeasure_pair_measure_alt
   1.161 -  pair_sigma_finite.pair_measure_alt2 -> pair_sigma_finite.emeasure_pair_measure_alt2
   1.162 -  pair_sigma_finite.pair_measure_times -> pair_sigma_finite.emeasure_pair_measure_Times
   1.163    pair_sigma_algebra.pair_sigma_algebra_measurable -> measurable_pair_swap
   1.164    pair_sigma_algebra.pair_sigma_algebra_swap_measurable -> measurable_pair_swap'
   1.165    pair_sigma_algebra.sets_swap -> sets_pair_swap
   1.166 -  finite_product_sigma_algebra.in_P -> sets_PiM_I_finite
   1.167 -  Int_stable_product_algebra_generator -> positive_integral
   1.168 -  product_sigma_finite.measure_fold -> product_sigma_finite.distr_merge
   1.169 -  product_sigma_finite.measure_preserving_component_singelton -> product_sigma_finite.distr_singleton
   1.170 -  product_sigma_finite.measure_preserving_merge -> product_sigma_finite.distr_merge
   1.171 -  finite_product_sigma_algebra.P_empty -> space_PiM_empty, sets_PiM_empty
   1.172 -  product_algebra_generator_der -> prod_algebra_eq_finite
   1.173 -  product_algebra_generator_into_space -> prod_algebra_sets_into_space
   1.174 -  product_sigma_algebra.product_algebra_into_space -> space_closed
   1.175 -  product_algebraE -> prod_algebraE_all
   1.176 -  product_algebraI -> sets_PiM_I_finite
   1.177 -  product_measure_exists -> product_sigma_finite.sigma_finite
   1.178 -  sets_product_algebra -> sets_PiM
   1.179 -  sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq
   1.180 -  space_product_algebra -> space_PiM
   1.181 -  Int_stable_cuboids -> Int_stable_atLeastAtMost
   1.182 -  measure_space.density_is_absolutely_continuous -> absolutely_continuousI_density
   1.183 -  sigma_finite_measure.RN_deriv_vimage -> sigma_finite_measure.RN_deriv_distr
   1.184 -  prob_space_unique_Int_stable -> measure_eqI_prob_space
   1.185 -  sigma_finite_measure.disjoint_sigma_finite -> sigma_finite_disjoint
   1.186 +  pair_sigma_finite.measure_cut_measurable_fst -> pair_sigma_finite.measurable_emeasure_Pair1
   1.187 +  pair_sigma_finite.measure_cut_measurable_snd -> pair_sigma_finite.measurable_emeasure_Pair2
   1.188 +  pair_sigma_finite.measure_preserving_swap -> pair_sigma_finite.distr_pair_swap
   1.189 +  pair_sigma_finite.pair_measure_alt2 -> pair_sigma_finite.emeasure_pair_measure_alt2
   1.190 +  pair_sigma_finite.pair_measure_alt -> pair_sigma_finite.emeasure_pair_measure_alt
   1.191 +  pair_sigma_finite.pair_measure_times -> pair_sigma_finite.emeasure_pair_measure_Times
   1.192 +  prob_space.indep_distribution_eq_measure -> prob_space.indep_vars_iff_distr_eq_PiM
   1.193 +  prob_space.indep_var_distributionD -> prob_space.indep_var_distribution_eq
   1.194    prob_space.measure_space_1 -> prob_space.emeasure_space_1
   1.195    prob_space.prob_space_vimage -> prob_space_distr
   1.196    prob_space.random_variable_restrict -> measurable_restrict
   1.197 -  measure_preserving -> equality "distr M N f = N" "f : measurable M N"
   1.198 -  measure_unique_Int_stable_vimage -> measure_eqI_generator_eq
   1.199 -  measure_space.measure_preserving_Int_stable -> measure_eqI_generator_eq
   1.200 +  prob_space_unique_Int_stable -> measure_eqI_prob_space
   1.201 +  product_algebraE -> prod_algebraE_all
   1.202 +  product_algebra_generator_der -> prod_algebra_eq_finite
   1.203 +  product_algebra_generator_into_space -> prod_algebra_sets_into_space
   1.204 +  product_algebraI -> sets_PiM_I_finite
   1.205 +  product_measure_exists -> product_sigma_finite.sigma_finite
   1.206    product_prob_space.finite_index_eq_finite_product -> product_prob_space.sets_PiM_generator
   1.207    product_prob_space.finite_measure_infprod_emb_Pi -> product_prob_space.measure_PiM_emb
   1.208 -  finite_product_prob_space.finite_measure_times -> finite_product_prob_space.finite_measure_PiM_emb
   1.209    product_prob_space.infprod_spec -> product_prob_space.emeasure_PiM_emb_not_empty
   1.210    product_prob_space.measurable_component -> measurable_component_singleton
   1.211    product_prob_space.measurable_emb -> measurable_prod_emb
   1.212    product_prob_space.measurable_into_infprod_algebra -> measurable_PiM_single
   1.213    product_prob_space.measurable_singleton_infprod -> measurable_component_singleton
   1.214    product_prob_space.measure_emb -> emeasure_prod_emb
   1.215 +  product_prob_space.measure_preserving_restrict -> product_prob_space.distr_restrict
   1.216 +  product_sigma_algebra.product_algebra_into_space -> space_closed
   1.217 +  product_sigma_finite.measure_fold -> product_sigma_finite.distr_merge
   1.218 +  product_sigma_finite.measure_preserving_component_singelton -> product_sigma_finite.distr_singleton
   1.219 +  product_sigma_finite.measure_preserving_merge -> product_sigma_finite.distr_merge
   1.220    sequence_space.measure_infprod -> sequence_space.measure_PiM_countable
   1.221 -  product_prob_space.measure_preserving_restrict -> product_prob_space.distr_restrict
   1.222 -  prob_space.indep_distribution_eq_measure -> prob_space.indep_vars_iff_distr_eq_PiM
   1.223 -  prob_space.indep_var_distributionD -> prob_space.indep_var_distribution_eq
   1.224 -  conditional_entropy_positive -> conditional_entropy_nonneg_simple
   1.225 -  conditional_entropy_eq -> conditional_entropy_simple_distributed
   1.226 -  conditional_mutual_information_eq_mutual_information -> conditional_mutual_information_eq_mutual_information_simple
   1.227 -  conditional_mutual_information_generic_positive -> conditional_mutual_information_nonneg_simple
   1.228 -  conditional_mutual_information_positive -> conditional_mutual_information_nonneg_simple
   1.229 -  entropy_commute -> entropy_commute_simple
   1.230 -  entropy_eq -> entropy_simple_distributed
   1.231 -  entropy_generic_eq -> entropy_simple_distributed
   1.232 -  entropy_positive -> entropy_nonneg_simple
   1.233 -  entropy_uniform_max -> entropy_uniform
   1.234 -  KL_eq_0 -> KL_same_eq_0
   1.235 -  KL_eq_0_imp -> KL_eq_0_iff_eq
   1.236 -  KL_ge_0 -> KL_nonneg
   1.237 -  mutual_information_eq -> mutual_information_simple_distributed
   1.238 -  mutual_information_positive -> mutual_information_nonneg_simple
   1.239 +  sets_product_algebra -> sets_PiM
   1.240 +  sigma_algebra.measurable_sigma -> measurable_measure_of
   1.241 +  sigma_finite_measure.disjoint_sigma_finite -> sigma_finite_disjoint
   1.242 +  sigma_finite_measure.RN_deriv_vimage -> sigma_finite_measure.RN_deriv_distr
   1.243 +  sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq
   1.244 +  space_product_algebra -> space_PiM
   1.245  
   1.246  * New "case_product" attribute to generate a case rule doing multiple
   1.247  case distinctions at the same time.  E.g.