From cc2e53ea72531c01f611e719a701bd463b42d412 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 4 Oct 2024 23:55:16 +0900 Subject: [PATCH] wip --- information_theory/shannon_fano.v | 6 +- information_theory/typ_seq.v | 142 +++++++++++++++--------------- lib/logb.v | 1 + lib/realType_logb.v | 52 +++++++---- 4 files changed, 113 insertions(+), 88 deletions(-) diff --git a/information_theory/shannon_fano.v b/information_theory/shannon_fano.v index 008c88d9..6ab00bdf 100644 --- a/information_theory/shannon_fano.v +++ b/information_theory/shannon_fano.v @@ -74,10 +74,10 @@ apply ler_sum => i _. rewrite H. have Pi0 : 0 < P i by rewrite lt0r Pr0/=. apply (@le_trans _ _ (Exp #|T|%:R (- Log #|T|%:R (P i)^-1))); last first. - by rewrite LogV// opprK LogK // card_ord natn. + by rewrite LogV// opprK natn LogK// card_ord. rewrite pow_Exp; last by rewrite card_ord. -rewrite Exp_oppr lef_pV2// ?posrE ?Exp_gt0//. -rewrite !card_ord natn Exp_le_increasing//. +rewrite Exp_oppr card_ord lef_pV2// ?posrE ?Exp_gt0//. +rewrite Exp_le_increasing// ?ltr1n//. rewrite (le_trans (mathcomp_extra.ceil_ge _))//. by rewrite natr_absz// ler_int ler_norm. Qed. diff --git a/information_theory/typ_seq.v b/information_theory/typ_seq.v index baeb8bdb..bb02bbc3 100644 --- a/information_theory/typ_seq.v +++ b/information_theory/typ_seq.v @@ -1,9 +1,8 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) From mathcomp Require Import all_ssreflect ssralg ssrnum matrix. -Require Import Reals Lra. -From mathcomp Require Import Rstruct. -Require Import ssrR Reals_ext realType_ext logb. +From mathcomp Require Import Rstruct reals lra exp. +Require Import ssr_ext realType_ext realType_logb. Require Import fdist proba entropy aep. (******************************************************************************) @@ -35,19 +34,19 @@ Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits. -Local Open Scope R_scope. Local Open Scope fdist_scope. Local Open Scope proba_scope. Local Open Scope entropy_scope. +Local Open Scope ring_scope. Import Order.TTheory GRing.Theory Num.Theory. Section typical_sequence_definition. -Variables (A : finType) (P : {fdist A}) (n : nat) (epsilon : R). +Variables (A : finType) (P : {fdist A}) (n : nat) (epsilon : Rdefinitions.R). Definition typ_seq (t : 'rV[A]_n) := - (exp2 (- n%:R * (`H P + epsilon)) <= P `^ n t <= exp2 (- n%:R * (`H P - epsilon)))%mcR. + (2 `^ (- n%:R * (`H P + epsilon)) <= (P `^ n)%fdist t <= 2 `^ (- n%:R * (`H P - epsilon)))%R. Definition set_typ_seq := [set ta | typ_seq ta]. @@ -57,107 +56,112 @@ Notation "'`TS'" := (set_typ_seq) : typ_seq_scope. Local Open Scope typ_seq_scope. -Lemma set_typ_seq_incl (A : finType) (P : {fdist A}) n epsilon : 0 <= epsilon -> forall r, 1 <= r -> +Lemma set_typ_seq_incl (A : finType) (P : {fdist A}) n epsilon : 0 <= epsilon -> `TS P n (epsilon / 3) \subset `TS P n epsilon. Proof. -move=> e0 r r1. +move=> e0. apply/subsetP => /= x. -rewrite !inE /typ_seq => /andP[/RleP H2 /RleP H3] [:Htmp]. -apply/andP; split; apply/RleP. -- apply/(leR_trans _ H2)/Exp_le_increasing => //. - rewrite !mulNR leR_oppr oppRK; apply leR_wpmul2l; first exact/leR0n. - apply/leR_add2l. +rewrite !inE /typ_seq => /andP[H2 H3] [:Htmp]. +apply/andP; split. +- apply/(le_trans _ H2). + rewrite ler_powR ?ler1n// !mulNr lerNr opprK; apply ler_wpM2l => //. + rewrite lerD2l//. abstract: Htmp. - rewrite leR_pdivr_mulr; [apply leR_pmulr => //|]; lra. -- apply/(leR_trans H3)/Exp_le_increasing => //. - rewrite !mulNR leR_oppr oppRK; apply leR_wpmul2l; first exact/leR0n. - apply leR_add2l; rewrite leR_oppr oppRK; exact Htmp. + by rewrite ler_pdivr_mulr// ler_peMr//; lra. +- apply/(le_trans H3); rewrite ler_powR// ?ler1n//. + rewrite !mulNr lerNr opprK; apply ler_wpM2l => //. + by rewrite lerD2l lerNr opprK; exact Htmp. Qed. Section typ_seq_prop. -Variables (A : finType) (P : {fdist A}) (epsilon : R) (n : nat). +Variables (A : finType) (P : {fdist A}) (epsilon : Rdefinitions.R) (n : nat). -Lemma TS_sup : #| `TS P n epsilon |%:R <= exp2 (n%:R * (`H P + epsilon)). +Lemma TS_sup : #| `TS P n epsilon |%:R <= 2 `^ (n%:R * (`H P + epsilon)). Proof. -suff Htmp : #| `TS P n epsilon |%:R * exp2 (- n%:R * (`H P + epsilon)) <= 1. - by rewrite -(mulR1 (exp2 _)) mulRC -leR_pdivr_mulr // /Rdiv -exp2_Ropp -mulNR. -rewrite (_ : 1 = 1%mcR)// -(FDist.f1 (P `^ n)). -rewrite (_ : _ * _ = \sum_(x in `TS P n epsilon) (exp2 (- n%:R * (`H P + epsilon)))); last first. - by rewrite big_const iter_addR. -by apply/leR_sumRl => //= i; rewrite inE; case/andP => /RleP. +suff Htmp : #| `TS P n epsilon |%:R * 2 `^ (- n%:R * (`H P + epsilon)) <= 1. + by rewrite -(mulr1 (2 `^ _)) mulrC -ler_pdivrMr // ?powR_gt0// -powRN// -mulNr. +rewrite -[leRHS](FDist.f1 (P `^ n)%fdist). +rewrite (_ : _ * _ = \sum_(x in `TS P n epsilon) (2 `^ (- n%:R * (`H P + epsilon)))); last first. + by rewrite big_const iter_addr addr0 mulr_natl. +by apply: leR_sumRl => //= i; rewrite inE; case/andP. Qed. Lemma typ_seq_definition_equiv x : x \in `TS P n epsilon -> - exp2 (- n%:R * (`H P + epsilon)) <= P `^ n x <= exp2 (- n%:R * (`H P - epsilon)). -Proof. by rewrite inE /typ_seq => /andP[? ?]; split; apply/RleP. Qed. + 2 `^ (- n%:R * (`H P + epsilon)) <= (P `^ n)%fdist x <= 2 `^ (- n%:R * (`H P - epsilon)). +Proof. by rewrite inE /typ_seq => /andP[? ?]; apply/andP; split. Qed. Lemma typ_seq_definition_equiv2 x : x \in `TS P n.+1 epsilon -> - `H P - epsilon <= - (1 / n.+1%:R) * log (P `^ n.+1 x) <= `H P + epsilon. + `H P - epsilon <= - n.+1%:R^-1 * log ((P `^ n.+1)%fdist x) <= `H P + epsilon. Proof. rewrite inE /typ_seq. -case/andP => H1 H2; split; - apply/RleP; rewrite -(@ler_pM2r _ n.+1%:R) ?ltr0n//. -- rewrite div1R -[in leRHS]RmultE mulRAC mulNR INRE mulVR; last first. - by rewrite mulrn_eq0/= oner_eq0. - rewrite mulN1R; apply/RleP. - rewrite leR_oppr. - apply/(@Exp_le_inv 2) => //. - rewrite LogK //; last by apply/(ltR_leR_trans (exp2_gt0 _)); apply/RleP: H1. - rewrite mulrC -mulNR -INRE. - exact/RleP. -- rewrite div1R -[in leLHS]RmultE mulRAC mulNR INRE mulVR; last first. - by rewrite mulrn_eq0/= oner_eq0. - rewrite mulN1R; apply/RleP. - rewrite leR_oppl. - apply/(@Exp_le_inv 2) => //. - rewrite LogK //; last by apply/(ltR_leR_trans (exp2_gt0 _)); apply/RleP: H1. - rewrite mulrC -mulNR -INRE. - exact/RleP. +case/andP => H1 H2; apply/andP; split; + rewrite -(@ler_pM2r _ n.+1%:R) ?ltr0n//. +- rewrite mulrAC mulNr mulVf; last by rewrite pnatr_eq0. + rewrite mulN1r. + rewrite lerNr. + rewrite -ler_log ?posrE// in H2; last 2 first. + by rewrite (lt_le_trans _ H1)// Exp_gt0//. + by rewrite Exp_gt0. + by rewrite mulNr powRN logV ?Exp_gt0// log_powR log2 mulr1 mulrC in H2. +- rewrite mulrAC mulNr mulVf; last by rewrite pnatr_eq0. + have := FDist.ge0 ((P `^ n.+1)%fdist) x; rewrite le_eqVlt => /predU1P[H3|H3]. + have : 0 < 2 `^ (1 *- n.+1 * (`H P + epsilon)). + by rewrite Exp_gt0//. + rewrite -H3 in H1. + by rewrite ltNge H1. + rewrite mulN1r. + rewrite lerNl. + rewrite -ler_log ?posrE// in H1; last first. + by rewrite Exp_gt0. + by rewrite mulNr powRN logV ?Exp_gt0// log_powR log2 mulr1 mulrC in H1. Qed. End typ_seq_prop. Section typ_seq_more_prop. - -Variables (A : finType) (P : {fdist A}) (epsilon : R) (n : nat). +Variables (A : finType) (P : {fdist A}) (epsilon : Rdefinitions.R) (n : nat). Hypothesis He : 0 < epsilon. Lemma Pr_TS_1 : aep_bound P epsilon <= n.+1%:R -> - 1 - epsilon <= Pr (P `^ n.+1) (`TS P n.+1 epsilon). + 1 - epsilon <= Pr (P `^ n.+1)%fdist (`TS P n.+1 epsilon). Proof. move=> k0_k. -have -> : Pr P `^ n.+1 (`TS P n.+1 epsilon) = - Pr P `^ n.+1 [set i | (i \in `TS P n.+1 epsilon) && (0 < P `^ n.+1 i)%mcR]. +have -> : Pr (P `^ n.+1)%fdist (`TS P n.+1 epsilon) = + Pr (P `^ n.+1)%fdist [set i | (i \in `TS P n.+1 epsilon) && (0 < (P `^ n.+1)%fdist i)%mcR]. congr Pr; apply/setP => /= t; rewrite !inE. apply/idP/andP => [H|]; [split => // | by case]. - case/andP : H => /RleP H _; exact/RltP/(ltR_leR_trans (exp2_gt0 _) H). + case/andP : H => H _; apply/(lt_le_trans _ H). + by rewrite Exp_gt0//. set p := [set _ | _]. -rewrite Pr_to_cplt leR_add2l leR_oppl oppRK. -have -> : Pr P `^ n.+1 (~: p) = - Pr P `^ n.+1 [set x | P `^ n.+1 x == 0] + - Pr P `^ n.+1 [set x | (0 < P `^ n.+1 x)%mcR && - (`| - (1 / n.+1%:R) * log (P `^ n.+1 x) - `H P | > epsilon)%mcR]. +rewrite Pr_to_cplt lerD2l lerNl opprK. +have -> : Pr (P `^ n.+1)%fdist (~: p) = + Pr (P `^ n.+1)%fdist [set x | (P `^ n.+1)%fdist x == 0] + + Pr (P `^ n.+1)%fdist [set x | (0 < (P `^ n.+1)%fdist x)%mcR && + (`| - n.+1%:R^-1 * log ((P `^ n.+1)%fdist x) - `H P | > epsilon)%mcR]. have -> : ~: p = - [set x | P `^ n.+1 x == 0 ] :|: - [set x | (0 < P `^ n.+1 x)%mcR && - (`| - (1 / n.+1%:R) * log (P `^ n.+1 x) - `H P | > epsilon)%mcR]. + [set x | (P `^ n.+1)%fdist x == 0 ] :|: + [set x | (0 < (P `^ n.+1)%fdist x)%mcR && + (`| - n.+1%:R^-1 * log ((P `^ n.+1)%fdist x) - `H P | > epsilon)%mcR]. apply/setP => /= i; rewrite !inE negb_and orbC. - apply/idP/idP => [/orP[/RltP|]|]. - - move/RltP => H. - have {}H : P `^ n.+1 i = 0. + apply/idP/idP => [/orP[H|]|]. + - have {}H : (P `^ n.+1)%fdist i = 0. apply/eqP. apply/negPn. apply: contra H. - by have [+ _] := fdist_gt0 (P `^ n.+1) i. + by have [+ _] := fdist_gt0 (P `^ n.+1)%fdist i. by rewrite H eqxx. - rewrite /typ_seq negb_and => /orP[|] LHS. - + have [//|H1] := eqVneq (P `^ n.+1 i) 0. - have {}H1 : 0 < P `^ n.+1 i by apply/RltP; rewrite lt0r H1/=. - apply/andP; split; first exact/RltP. - move/RleP: LHS => /ltRNge/(@Log_increasing 2 _ _ Rlt_1_2 H1). - rewrite /exp2 ExpK // mulRC mulRN -mulNR -ltR_pdivr_mulr; last exact/ltR0n. + + have [//|H1] := eqVneq ((P `^ n.+1)%fdist i) 0. + have {}H1 : 0 < (P `^ n.+1)%fdist i by rewrite lt0r H1/=. + rewrite /= H1/=. + move: LHS; rewrite -ltNge => /log_increasing => /(_ H1). + rewrite log_powR mulNr log2 mulr1. + mulN1r. mulrC. mulrN -mulNr -ltr_pdivr_mulr. + + +; last exact/ltR0n. rewrite /Rdiv mulRC ltR_oppr => /RltP; rewrite -ltrBrDl => LHS. rewrite div1r// mulNr -RinvE ger0_norm// -INRE//. by move/RltP : LHS; move/(ltR_trans He)/ltRW/RleP. diff --git a/lib/logb.v b/lib/logb.v index 88c73537..c04cd978 100644 --- a/lib/logb.v +++ b/lib/logb.v @@ -414,3 +414,4 @@ rewrite big_cons LogM//; last first. by apply/RltP/prodr_gt0 => a _; exact/RltP. by rewrite [RHS]big_cons oppRD; congr (_ + _)%coqR. Qed. + diff --git a/lib/realType_logb.v b/lib/realType_logb.v index 957d583a..ff9539ef 100644 --- a/lib/realType_logb.v +++ b/lib/realType_logb.v @@ -115,38 +115,46 @@ End Log. Section Exp. Context {R : realType}. -Definition Exp (n : nat) (x : R) := expR (x * ln n%:R). +(* TODO: rm *) +Definition Exp (n : R) (x : R) := n `^ x. -Lemma pow_Exp (x : nat) n : (0 < x)%N -> x%:R ^+ n = Exp x n%:R. -Proof. by move=> x0; rewrite /Exp expRM_natl lnK// posrE ltr0n. Qed. +Lemma pow_Exp (x : R) n : (0 <= x) -> x ^+ n = Exp x n%:R. +Proof. by move=> x0; rewrite /Exp powR_mulrn. Qed. -Lemma LogK n x : (1 < n)%N -> 0 < x -> Exp n (Log n x) = x. +Lemma LogK n x : (1 < n)%N -> 0 < x -> Exp n%:R (Log n x) = x. Proof. move=> n1 x0. -rewrite /Log /Exp prednK// 1?ltnW// -mulrA mulVf// ?mulr1 ?lnK//. -by rewrite gt_eqF// -ln1 ltr_ln// ?posrE// ?ltr1n// ltr0n ltnW. +rewrite /Exp /Log prednK// 1?ltnW//. +rewrite powRrM {1}/powR ifF; last first. + by apply/negbTE; rewrite powR_eq0 negb_and pnatr_eq0 gt_eqF// ltEnat/= ltnW. +rewrite ln_powR mulrCA mulVf//. + by rewrite mulr1 lnK ?posrE. +by rewrite gt_eqF// -ln1 ltr_ln ?posrE// ?ltr1n// ltr0n ltnW. Qed. Lemma Exp_oppr n x : Exp n (- x) = (Exp n x)^-1. -Proof. by rewrite /Exp mulNr expRN. Qed. +Proof. by rewrite /Exp -powRN. Qed. -Lemma Exp_gt0 n x : 0 < Exp n x. Proof. by rewrite /Exp expR_gt0. Qed. +Lemma Exp_gt0 n x : 0 < n -> 0 < Exp n x. Proof. by move=> ?; rewrite /Exp powR_gt0. Qed. -Lemma Exp_ge0 n x : 0 <= Exp n x. Proof. exact/ltW/Exp_gt0. Qed. +Lemma Exp_ge0 n x : 0 <= Exp n x. Proof. by rewrite /Exp powR_ge0. Qed. -Lemma Exp_increasing n x y : (1 < n)%N -> x < y -> Exp n x < Exp n y. -Proof. by move=> ? ?; rewrite ltr_expR// ltr_pM2r// ln_gt0// ltr1n. Qed. +Lemma Exp_increasing n x y : 1 < n -> x < y -> Exp n x < Exp n y. +Proof. +move=> n1 xy; rewrite /Exp /powR ifF; last first. + by apply/negbTE; rewrite gt_eqF// (lt_trans _ n1). +rewrite ifF//; last first. + by apply/negbTE; rewrite gt_eqF// (lt_trans _ n1). +by rewrite ltr_expR// ltr_pM2r// ln_gt0// ltr1n. +Qed. -Lemma Exp_le_increasing n x y : (1 < n)%N -> x <= y -> Exp n x <= Exp n y. +Lemma Exp_le_increasing n x y : 1 < n -> x <= y -> Exp n x <= Exp n y. Proof. -move=> n1; rewrite /Exp le_eqVlt => /predU1P[->//|]. -by move/Exp_increasing => x_y; exact/ltW/x_y. +by move=> n1 xy; rewrite /Exp ler_powR// ltW. Qed. End Exp. -Hint Extern 0 (0 < Exp _ _) => solve [exact/Exp_gt0] : core. - Hint Extern 0 (0 <= Exp _ _) => solve [exact/Exp_ge0] : core. Section log. @@ -188,6 +196,18 @@ move=> x0; rewrite logexp1E ler_wpM2r// ?invr_ge0//= ?(ltW (@ln2_gt0 _))//. exact/ln_id_cmp. Qed. +Lemma log_powR (a x : R) : log (a `^ x) = x * log a. +Proof. +by rewrite /log /Log ln_powR// mulrA. +Qed. + +Lemma log_increasing (a b : R) : 0 < a -> a < b -> log a < log b. +Proof. +move=> Ha a_b. +rewrite /log /Log prednK// ltr_pmul2r ?invr_gt0 ?ln2_gt0//. +by rewrite ltr_ln ?posrE// (lt_trans _ a_b). +Qed. + End log. Lemma log_prodr_sumr_mlog {R : realType} {A : finType} (f : A -> R) s :