proposition: Theorem source_coding' : exists sc : scode_fl A k n, SrcRate sc = r /\ esrc(P , sc) <= epsilon.
proof: Proof. move: (proj2_sig (source_direct_bound den delta)) => Hdelta. have Hk : aep_bound P (lambda / 2) <= INR k by exact/(leR_trans _ Hdelta)/leR_maxl. set S := `TS P k (lambda / 2). set def := TS_0 lambda2_gt0 lambda2_lt1 Hk. set F := f n S. set PHI := @phi _ n _ S def. exists (mkScode F PHI); split. rewrite /SrcRate /r /n /k 2!natRM; field. by split; exact/INR_eq0. set lhs := esrc(_, _). suff -> : lhs = (1 - Pr (P `^ k) (`TS P k (lambda / 2)))%R. rewrite leR_subl_addr addRC -leR_subl_addr. apply (@leR_trans (1 - lambda / 2)%R). by apply leR_add2l; rewrite leR_oppr oppRK; exact: lambda2_epsilon. exact: (Pr_TS_1 lambda2_gt0). rewrite /lhs {lhs} /SrcErrRate /Pr /=. set lhs := \sum_(_ | _ ) _. suff -> : lhs = \sum_(x in 'rV[A]_k | x \notin S) P `^ k x. have : forall a b : R, (a + b = 1 -> b = 1 - a)%R by move=> ? ? <-; field. apply. rewrite -[X in _ = X](Pr_cplt (P `^ k) (`TS P k (lambda / 2))). congr (_ + _)%R. by apply: eq_bigl => ta /=; rewrite !inE. rewrite {}/lhs; apply eq_bigl => //= i. rewrite inE /=; apply/negPn/negPn. - suff H : def \in S by move/eqP/phi_f; tauto. exact: (TS_0_is_typ_seq lambda2_gt0 lambda2_lt1 Hk). - suff S_2n : (#| S | < expn 2 n)%nat by move/(f_phi def S_2n)/eqP. suff card_S_bound : #| S |%:R < exp2 (k%:R * r). apply/ltP/INR_lt; rewrite -natRexp2. suff : n%:R = (k%:R * r)%R by move=> ->. rewrite /n /k /r (natRM _ den.+1) /Rdiv -mulRA. by rewrite (mulRCA den.+1%:R) mulRV ?INR_eq0' // mulR1 natRM. suff card_S_bound : 1 + #| S |%:R <= exp2 (k%:R * r) by lra. suff card_S_bound : 1 + #| S |%:R <= exp2 (k%:R * (`H P + lambda)). apply: leR_trans; first exact: card_S_bound. by apply Exp_le_increasing => //; apply leR_wpmul2l; [exact/leR0n | exact/Hlambdar]. apply (@leR_trans (exp2 (k%:R * (lambda / 2) + k%:R * (`H P + lambda / 2)))); last first. rewrite -mulRDr addRC -addRA. rewrite (_ : forall a, a / 2 + a / 2 = a)%R; last by move=> ?; field. by apply/RleP; rewrite Order.POrderTheory.lexx. apply (@leR_trans (exp2 (1 + INR k * (`H P + lambda / 2)))); last first. apply Exp_le_increasing => //; apply leR_add2r. move/leR_max : Hdelta => [_ Hlambda]. apply (@leR_pmul2r (2 / lambda)%R); first by apply/divR_gt0 => //; exact: lambda_gt0. rewrite mul1R -mulRA -{2}(Rinv_div lambda 2). by rewrite mulRV ?mulR1 //; exact/gtR_eqF/lambda2_gt0. apply: leR_trans; first exact/leR_add2l/TS_sup. apply (@leR_trans (exp2 (INR k* (`H P + lambda / 2)) + exp2 (INR k * (`H P + lambda / 2)))%R). + apply/leR_add2r. rewrite -exp2_0; apply Exp_le_increasing => //. apply mulR_ge0; first exact: leR0n. apply addR_ge0; first exact: entropy_ge0. apply Rlt_le; exact: lambda2_gt0. + rewrite addRR -{1}(logK Rlt_0_2) -ExpD {1}/log Log_n //. by apply/RleP; rewrite Order.POrderTheory.lexx. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrZ ssrR Reals_ext ssr_ext ssralg_ext logb natbin fdist proba entropy aep typ_seq source_code