From f7eeca0b890c140c3a536114275ea699d7523128 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Wed, 18 Feb 2026 11:27:29 +0900 Subject: [PATCH 1/2] fix for mca #1850 --- information_theory/entropy_convex.v | 2 +- probability/convex.v | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/information_theory/entropy_convex.v b/information_theory/entropy_convex.v index 35197dab..9b6534cb 100644 --- a/information_theory/entropy_convex.v +++ b/information_theory/entropy_convex.v @@ -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. diff --git a/probability/convex.v b/probability/convex.v index a1345b68..ea343fe8 100644 --- a/probability/convex.v +++ b/probability/convex.v @@ -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. From ec20f604e99368127c651b581e245638a8a2d72e Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Wed, 18 Feb 2026 11:42:54 +0900 Subject: [PATCH 2/2] fix entropy_convex again --- information_theory/entropy_convex.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/information_theory/entropy_convex.v b/information_theory/entropy_convex.v index 9b6534cb..0c8370ee 100644 --- a/information_theory/entropy_convex.v +++ b/information_theory/entropy_convex.v @@ -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.