changelog.txt

-------------------
from 0.3.8 to 0.4.0
-------------------
- packed classes (affine, biglub, convex, concave) redefined with HB
- added:
  + notation {Biglub_morph T -> R}
- renamed:
  + SemiCompleteSemiLattice -> SemiCompSemiLatt
  + idfun_is_biglub_affine -> idfun_is_biglubmorph
  + comp_is_biglub_affine -> comp_is_biglubmorph
  + affineP -> affine_functionP

-------------------
from 0.3.7 to 0.3.8
-------------------
compatibility release

-------------------
from 0.3.6 to 0.3.7
-------------------
compatibility release

-------------------
from 0.3.5 to 0.3.6
-------------------
compatibility release

-------------------
from 0.3.4 to 0.3.5
-------------------

* added
- in ssrR.v
  + lemma invR_ge0
- in ssrZ.v
  + lemmas addZAC, addZCA, neq_Zlt
* renamed:
- in ssrR.v
  + subr_le0 -> subR_le0
- in reals_ext.v
  + pos_ffun -> nneg_finfun
  + pos_ff_ge0 -> nneg_finfun_ge0
  + pos_fun -> nneg_fun
* changed:
- row_nth moved and renamed to bitseq_row_nth
* removed:
  + sumR_setT (use finset.big_set in MathComp)
  + eq_imagel (use classical_sets.eq_imagel in MathComp-Analysis)
  + eq_bigcup (use classical_sets.eq_bigcup in MathComp-Analysis)

-------------------
from 0.3.3 to 0.3.4
-------------------

* added:
- in ssrZ.v
  + lemmas ltZ_addl, ltZ_addr, pmulZ_rgt0
  + lemmas intRD, leZ0n
- in ssrR.v
  + lemmas expRn_gt0, ltR0n_neq0, lt0Rn_neq0', eqR_divl_mulr
- in proba.v
  + lemmas scalel_RVA, scaler_RVA, sq_RV_pow2, sq_RV_ge0, E_trans_min_RV
  + lemma Pr_lt1

* renamed:
- in necset.v
  + lemma nesetU_bigsetU -> nesetU_bigcup

* changed:
- in ssr_ext.v
  + remove eq_tcast in favor of eq_tcast2 (renamed to eq_tcast)
- in aep.v
  + a cleaner expression for aep_sigma2
- in proba.v
  + stopped importing the unused Nsatz
- in Rbigop.v
  + generalize leR_sumR

* removed:
- in convex.v:
  + definition choice_of_Object
- in aep.v:
  + lemma E_mlog (since it is equivalent to entropy.entropy_Ex)

-------------------
from 0.3.2 to 0.3.3
-------------------

* removed:

- in ldpc_algo_proof.v:
  + lemma sumn_eq0P

-------------------
from 0.3.1 to 0.3.2
-------------------

* added:

- in Reals_ext.v:
  + lemmas onem_le, onem_lt
  + module OProb for inferring values in the open unit interval
    * notation %:opr
    * technical lemmas oprob_gt0, oprobK, oprob_pdivRnnm, oprob_add_gt0, etc.
    * a canonical instance for the cplt and the multiplication of two oprob's
  + a canonical instance of Rpos for oprob
  + lemmas onem_prob, onem_oprob
  + lemmas prob_trichotomy and prob_trichotomy'
- in ssrR.v:
  + lemma ltR_subr_addr
- in convex.v:
  + lemmas convA'_oprob, convACA'
- in fdist.v:
  + technical lemmas about oprob and s_of, r_of, p_of, q_of
    * with canonical instances
- in necset.v:
  + lemmas conv_in_conv_pt_set, conv_in_conv_set, convA_pt_set, etc.
  + lemma affine_image_conv_set
  + lemma conv_pt_cset_is_convex, canonical conv_pt_cset,
    lemma conv_pt_cset, canonical conv_cset,
    lemma oplus_conv_cset_is_convex, canonical oplus_conv_cset
  + lemma conv_set1
- in classical_sets_ext.v:
  + lemma set1_inj

* changed:
  + modify the convex space structure on (convex_set _) to reuse conv_set instead of
    differently defining another convex combination operation
  + move and rename convex.{Rpos_prob_Op1, Rpos_prob, Rpos_probC}
    to Reals_ext.{prob_divRposxxy, divRposxxy, divRposxxyC}.

* moved:
  + lemma onem_div from convex.v to Reals_ext.v

-----------------
from 0.3 to 0.3.1
-----------------

- added:
  + Notations [affine of f] and [affine of f as g]
  + Notation biglub_morph
  + lemmas prob_ge0, prob_le1 (also as Hint Resolve)
  + views leR2P and ltR2P
  + constructor Prob.mk to build prob from boolean inequalities and
    Prob.mk_ to build prob from Prop inequalities
  + definition prob_invp, lemma Prob_invp
  + lemmas prob_gt0', prob_lt1', probmul_eq1
- renamed:
  + Module AffineFunction -> Affine
  + Notation AffineFunction -> Affine
  + Notation affine_function -> affine
  + affine_functionP' -> affine_conv
  + CSet.Class -> CSet.Mixin
- changed:
  + affine_function_id_proof/affine_function_id ->
      idfun_is_affine/Canonical idfun_affine
  + affine_function_comp_proof'/affine_function_comp_proof/affine_function_comp ->
      comp_is_affine/Canonical comp_affine
  + in Section with_affine_projection and Section S1_proj_Convn_finType
    * prj/prj_affine -> prj : {affine ... -> ...}
  + Convn_of_FSDist_FSDistfmap -> to use {affine ...}
  + biglub_morph, biglub_lub_morp -> to use {Biglub_morph ...}
  + multiple inheritance in Module BiglubMorph
  + biglub_affine_id_proof -> idfun_is_biglub_affine/Canonical idfun_is_biglub_affine
  + biglub_affine_comp_proof -> comp_is_biglub_affine/Canonical comp_biglub_affine
  + proof field of Prob.t now in bool
  + prob_subType declaration for Prob.t
  + generalize binary_symmetric_channel.closed to ssrR.ltR2W
- moved:
  + lemma Rpos_prob_Op1, Rpos_prob, Rpos_probC, onem_div from convex.v to Reals_ext.v
- removed:
  + affine_function_at
  + image_preserves_convex_hull', is_convex_set_image'
  + lemma Prob.ge0
  + lemma prob_ext
  + lemmas eqprob, eqprobP

-----------------
from 0.2.2 to 0.3
-----------------

- moved:
  + from convex_choice.v to fsdist.v
    * FSDist_convType
    * convn_convnfsdist
    * fsdist_orderedConvMixin
  + from necset.v to fsdist.v
    * finsupp_Conv
    * FSDist_eval_affine
    * FSDist_scalept_conv
    * Convn_of_FSDist
    * Convn_of_FSDist_affine
    * Convn_of_FSDist_FSDist1
    * Convn_of_FSDist_FSDistfmap
    * triangular_laws_left0
  + row_of_tuple_inj from types.v to ssralg_ext
  + derive_sincreasing_interv moved to Ranalysis_ext.v
  + num_occ_flatten from string_entropy.v to num_occ.v
- renamed:
  + lub_op -> biglub
  + lub_op1 -> biglub1
  + lub_op_bigsetU -> biglub_bignesetU
  + lub_op_bigcup -> biglub_bigcup
  + lub_op_setU -> biglub_setU
  + lub_of_flatten -> biglub_flatten
  + lub_binary -> lub
  + lub_binaryC -> lubC
  + lub_binaryA -> lubA
  + lub_binaryxx -> lubxx
  + lub_binaryAC -> lubAC
  + lub_binaryCA -> lubCA
  + lub_binaryACA -> lubACA
  + lub_binaryKU -> lubKU
  + lub_binaryUK -> lubUK
  + lub_binaryKUC -> lubKUC
  + lub_binaryUKC -> lubUKC
  + lub_binaryD{r,l} -> lubD{r,l}
  + lub_op_morph -> biglub_morph
  + lub_lub_binary_morph -> biglub_lub_morph
  + LubOpMorph -> BiglubMorph
  + LubOpAffine -> BiglubAffine
  + lub_op_affine_id_proof -> biglub_affine_id_proof
  + lub_op_affine_comp_proof -> biglub_affine_comp_proof
  + lub_opD{r,l} -> biglubD{r,l}
  + lub_op_conv_pt_setE -> biglub_conv_pt_setE
  + lub_op_conv_pt_setD -> biglub_conv_pt_setD
  + lub_op_conv_set -> biglub_conv_setE
  + lub_op_conv_setD -> biglub_conv_setD
  + lub_op_iter_conv_set -> biglub_iter_conv_set
  + lub_op_hull -> biglub_hull
- changed:
  + setU_bigsetU in necset.v changed to bigcupsetU2E in classical_sets.v
  + MVT_cor1_pderivable_new in ln_facts changed to MVT_cor1_pderivable_closed_continuity
    and moved to Ranalysis_ext.v
  + MVT_cor1_pderivable_new_var in ln_facts.v changed to MVT_cor1_pderivable_open_continuity
    and moved to Ranalysis_ext.v
  + sum_num_occ renamed to sum_num_occ_size from and moved from string_entropy.v to num_occ.v
  + in ssrR.v, gtR_eqF, ltR_eqF, invRK, invRM have now hypotheses in bool instead of Prop
  + in ssrR.v, oppR_lt0 and oppR_gt0 are now equivalences
- renamed:
  + derive_increasing_interv_ax_left -> pderive_increasing_ax_open_closed
  + derive_increasing_interv_ax_right -> pderive_increasing_ax_closed_open
  + derive_increasing_interv_left -> pderive_increasing_open_closed
  + derive_increasing_interv_right -> pderive_increasing_closed_open
  + derive_increasing_ad_hoc -> pderive_ad_hoc
  + ltr_subl_addl -> ltR_subl_addl
  + convex_choice.v -> convex.v
- removed:
  + from ssrR.v:
    * Reqb, eqRP, R_eqMixin, R_eqType, R_choiceType, ROrder.orderMixin,
      R_porderType, R_latticeType, R_distrLatticeType, R_orderType

-----------------
from 0.2 to 0.2.1
-----------------

- changed:
  + in ssrZ.v:
    * Z_of_nat_le -> leZ_nat, Z_of_nat_lt -> ltZ_nat
    * Z<=nat -> %:Z
- renamed:
  + in classical_sets_ext.v: 
    image_subset -> subset_image
- removed:
  + in classical_sets_ext.v:
    set1_inj
    fullimage_subset

-----------------
from 0.1.2 to 0.2
-----------------

warning: this changelog entry is not exhaustive

- renamed:
  + in Rbigop.v:
    * rsumr_ge0 -> sumR_ge0, rsumr_gt0 -> sumR_gt0
    * ler_rsum_support -> leR_sumR_support,ler_rsum -> leR_sumR, ler_rsum_l -> leR_sumRl,
      ler_rsum_l_support -> leR_sumRl_support, ltr_rsum_support -> ltR_sumR_support,
      ltr_rsum -> ltR_sumR
    * rsum_setT -> sumR_setT, rsum_ord_setT -> sumR_ord_setT
    * prsumr_seq_eq0P -> psumR_seq_eq0P, prsumr_eq0P -> psumR_eq0P
    * ler_rsum_Rabs -> leR_sumR_Rabs, ler_rsum_predU-> leR_sumR_predU
    * classify_big -> classify_sumR
    * Rle_big_eq -> leR_sumR_eq
    * sum_f_R0_rsum -> sum_f_R0_sumR
    * bigmul_eq0 -> rprod_eq0
    * rprodr_gt0 -> prodR_gt0, rprodr_ge0 -> prodR_ge0, rprodr_gt0_inv-> prodR_gt0_inv, rprodr_ge1 -> prodR_ge1
    * ler_rprod -> leR_prodR
    * log_rmul_rsum_mlog -> log_prodR_sumR_mlog
    * Rle_bigRmax -> leR_bigmaxR, Rle_0_bigRmax -> bigmaxR_ge0
    * bigrmax_undup -> bigmaxR_undup, bigrmax_cat -> bigmaxR_cat, bigrmax_perm -> bigmaxR_perm, bigrmax_eqi -> bigmaxR_eqi
    * rmax_imset -> bigmaxR_imset, rmax_imset' -> bigmaxR_imset_helper
    * Rle_bigrmax_R -> leR_bigmaxRl
    * bigrmax_max_seq -> bigmaxR_seq_eq, bigrmax_max - bigmaxR_eq
    * rmax_distrr -> bigmaxR_distrr, rmax_distrl -> bigmaxR_distrl
    * bigminn_min -> leq_bigmin, big_rmax_bigminn -> bigmaxR_bigmin, big_rmax_bigminn_vec -> bigmaxR_bigmin_vec
    * bigmul_constE -> prodR_constE, bigmul_card_constE -> prodR_card_constE, bigmul_m1pow -> prodRN
    * E_sumr -> E_sumR
    * unit_RV1 -> pr_eq_unit
    * Pr_domin_fst -> Pr_domain_setX
  + \Pr[ X = a ] -> `Pr[ X = a ], \Pr[ X >= a ] -> `Pr[ X >= a ]
  + RVar.d -> dist_of_RV
  + RVar.dE -> pr_eqE', RVar.Pr_Set -> pr_inE'
  + RVar.Pr -> RVarPr
  + p_of -> ambient_dist
  + cPr -> jcPr
  + cPr0 -> cPr
  + cPr0_Pr -> cPrET
  + cPr0_set0 - cPrE0
  + PrX_setT -> Pr_XsetT
  + bayes -> jBayes
  + law_of_total_probability -> total_prob, total_prob -> jtotal_prob_cond
  + product_rule -> jproduct_rule_cond, product_rule0 -> jproduct_rule
  + inde_drv -> inde_rv (in proba.v), cinde_drv -> jcinde_rv (in cinde.v)
  + RV_Pr_C -> pr_eq_pairC, RV_Pr_C_set -> pr_in_pairC
  + RV_Pr_A -> pr_eq_pairA, RV_Pr_A_set -> pr_in_pairA
  + RV_Pr_AC -> pr_eq_pairAC, RV_Pr_AC_set -> pr_in_pairAC
  + RV_Pr_comp_set -> pr_in_comp, RV_Pr_comp -> pr_eq_comp
  + reasoning_by_cases -> jcreasoning_by_cases
- added:
  + divRBl in ssrR.v
  + notation `d_ for RVar.d
  + notation `o for comp_RV
  + sumR_neq0
  + bigcup_set1
  + simple technical lemmas to deal with `*T, T*`, and `* (setX)
  + Pr_setTX
  + CondFDist in proba.v
  + lemmas about cPr proba.v (cPrE0, Pr_cPr_gt0, cPr_cplt, product_rule, cPr_diff, cPr_union_eq)
  + Pr_Bivarfst, Pr_Bivarsnd, Pr_Multivar, Pr_Multivar{1,2}
  + conditional version of random variables and independence in proba.v
  + pr_eq_pairCA, pr_in_pairCA
  + cpr_in_Eset1, cpr_in_set1F
  + reasoning_by_cases, creasoning_by_cases
  + cpr_in_pair* lemmas in proba.v
  + cinde.v -> graphoid.v
- changed:
  + generalize pr_geq to any porderType
  + definition of notation @^-1 now uses preim instead of finset notations
  + capacity changed from a relation to a definition using Rstruct.real_sup
  + slight generalization of bigcup_setX, bigcup_set0
  + slight generalization of RV_Pr_setXunit (renamed pr_eq_pair_setT)
- removed:
  + notations `E_, `V_
  + duplicate of E_leng_cw
  + PrX_diff, PrX_union
  + Pr_RV2C
  + RV_Pr_CA, RV_Pr_CA_set
  + Pr_domin_snd
  + RVarPr
  + most marginal_* lemmas and technical lemmas from cinde.v
  + RV_Pr_lC, etc., RV2_Pr*congr* lemmas, from cinde.v

---------------------
from 0.1.1 to 0.1.2 :
---------------------

- moved:
  + subR_onem from necset.v to Reals_ext.v
  + from necset.v to fsdist.v
    * bigfcup_fset1
    * fbig_pred1_inj
    * FSDistfmap_FSDist1
    * FSDist_finsuppD1
    * FSDist_prob
  + set1_inj from necset.v to classical_sets_ext.v

-------------------
from 0.1 to 0.1.1 :
-------------------

added:
- order canonical structures in ssrR.v
renamings:
- imageA -> image_comp (deprecated)
- image_idfun -> image_id (deprecated)
- bigcup0 -> bigcup_set0
- bigcup1 -> bigcup_set1
- bigcup_set1 -> bigcup_of_singletons
- bigcup_const -> bigcup_of_const
- altConvType -> naryConvType
added:
- <&>_ notation for the operator of naryContType
  + _ <& _ &> _ for its binary version
removed:
- Lemma to_bivar_entropy (redundant with entropy_to_bivar)
- file arg_rmax.v
replaced:
- custom arg_rmax with new order.v's [arg max_(i > i0) F]%O

-------------------
from 0.0.7 to 0.1 :
-------------------

new lemmas:
- FSDist.le1
new type:
- altConvType, together with equivalence proofs of several axiomatics
renamings:
- Joet -> lub_op
- joet -> lub_binary
- Convn_indexed_over_finType -> Convn_finType
notations:
- <$>_ for Convn__finType (on the model of <|>_)
- |_| fr lub_op (still [+] for lub_binary)
- _ <| _ |> _ lowered to level 49
- << and <<b changed to `<< and `<<b (level change)

---------------------
from 0.0.6 to 0.0.7 :
---------------------

renamings:
- Module jtype -> Module JType
  + jtype.jtype -> JType.t
  + jtype.mkJtype -> JType.mk
  + jtype.f -> JType.f
  + etc.
- MultivarPerm.entropy -> entropy_multivarperm
- head_of_nth0 -> Nth.head_ofE
- MargFDist.zero -> MargFDist.tail_ofE
- ide_swap -> swapK
notation changes:
- notation \Conv_ -> <|>_
- `NE -> %:ne (prefix to postfix)
- `Rpos -> %:pos
- `Rnneg -> %:nng
- `Pr -> %:pr
new notation:
- E `* F for setX E F
lemmas:
- (bij_inj bij_swap) instead of inj_swap 
files:
- fdist.v split into fdist.v (distributions) and proba.v (probabilities)

--------------------
from 0.0.5 to 0.0.6:
--------------------

renamings:
- Pr_big_union_disj -> Boole_eq (generalization)
- setX1' -> setX1r (direction change)
- setX0 -> setX0r
- Int_part_pos -> Int_part_ge0
- CFDist -> CJFDist
- CondFDist -> CondJFDist0
- CondFDistT -> CondJFDist
- scha moved from success_decode_bound.v to channel_code.v
new notation:
- P `(| a ) for CondFDistT.d
files:
- pinsker_fun.v has been integrated into pinsker.v
- proba.v renamed to fdist.v (proba.v kept for compatibility)
- cproba.v renamed to jfdist.v