Skip to content

fix for mca #1850 #206

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
Feb 18, 2026
Merged

fix for mca #1850 #206

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
f7eeca0
fix for mca #1850
t6s Feb 18, 2026
ec20f60
fix entropy_convex again
t6s Feb 18, 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: 2 additions & 2 deletions information_theory/entropy_convex.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ From mathcomp Require boolp.
From mathcomp Require Import unstable mathcomp_extra reals.
From mathcomp Require Import interval_inference set_interval.
From mathcomp Require Import functions topology normedtype realfun derive exp.
From mathcomp Require convex.
From mathcomp Require Import -(notations)convex.
Require Import ssr_ext ssralg_ext bigop_ext realType_ext realType_ln.
Require Import derive_ext fdist jfdist_cond entropy convex.
Require Import binary_entropy_function log_sum divergence.
Expand Down Expand Up @@ -244,7 +244,7 @@ have cnH2: {within `[x, y], continuous (- H2)}%classic.
apply/RNconcave_function_at.
rewrite /convex_function_at /=.
rewrite -!mc_convRE.
apply: (@analysis.convex.second_derivative_convex _ (fun z => - (H2 z))).
apply: (@second_derivative_convex _ (fun z => - (H2 z))).
- move=> z xzy.
have/zxyoo01 z01: z \in `]x, y[%classic by rewrite inE.
by rewrite DDnH2E// DDnH2_nonneg.
Expand Down
1 change: 1 addition & 0 deletions probability/convex.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg fingroup perm matrix interval.
From mathcomp Require Import unstable mathcomp_extra boolp classical_sets.
From mathcomp Require Import ssrnum archimedean ereal interval_inference.
From mathcomp Require Import realfun.
From mathcomp Require Import ring lra reals.
Require Import ssr_ext ssralg_ext realType_ext realType_ln fdist.
From mathcomp Require vector.
Expand Down
Loading