Skip to content

fix for mathcomp analysis 1.15 #205

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
affeldt-aist merged 2 commits into from
Jan 16, 2026
Merged

fix for mathcomp analysis 1.15 #205

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d123716
workaround for intrD1
t6s Jan 16, 2026
87c2eb2
more tweaks
t6s Jan 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion information_theory/joint_typ_seq.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,9 @@ Definition Nup (x : R) := `| Num.floor x |.+1.
Lemma Nup_gt x : x < (Nup x)%:R.
Proof.
apply: (lt_le_trans (floorD1_gt x)).
by rewrite /Nup -intrD1 -natr1 lerD // natr_absz ler_int ler_norm.
rewrite /Nup.
rewrite [leLHS](_ : _ = (Num.Def.floor x)%:~R + 1%:~R); last by rewrite intrD1.
by rewrite -natr1 lerD // natr_absz ler_int ler_norm.
Qed.

Definition JTS_1_bound :=
Expand Down
6 changes: 4 additions & 2 deletions information_theory/source_coding_vl_converse.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
(* Copyright (C) 2025 infotheo authors, license: LGPL-2.1-or-later *)
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint matrix.
From mathcomp Require Import archimedean lra ring.
From mathcomp Require Import mathcomp_extra.
From mathcomp Require Import unstable contra reals normedtype sequences exp.
Require Import ssr_ext ssralg_ext bigop_ext realType_ext realType_ln.
Require Import fdist proba entropy divergence log_sum source_code.
Expand Down Expand Up @@ -779,8 +780,9 @@ apply: (@le_trans _ _ ((x ^ 2 / 2 - 1) * eps * n%:R)); last first.
rewrite /m /x.
rewrite lerBlDr.
rewrite (le_trans (ltW (floorD1_gt _)))//.
rewrite natr_absz intrD1 ler_int.
by rewrite lerD2r ler_norm.
rewrite natr_absz.
rewrite [leRHS](_ : _ = (`|floor (expR (m' eps))| + 1)%:~R); last by rewrite intrD1.
by rewrite ler_int lerD2r ler_norm.
rewrite logM//; last exact: mpos.
rewrite -(ler_pM2r ln2_gt0).
rewrite mulrDl -(mulrA (ln alp)) (mulVf ln2_neq0).
Expand Down
Loading