From 218da9b303deb5a1b91884da5ea4f1318447249d Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 27 Jul 2023 11:11:34 +0900
Subject: [PATCH] ln is concave, conjugate/powR

---
 CHANGELOG_UNRELEASED.md |  5 +++++
 theories/convex.v       | 17 +++++++++++++++++
 theories/exp.v          | 31 +++++++++++++++++++++++++++++++
 3 files changed, 53 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 43180e3eb8..82bd0bef57 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -17,6 +17,11 @@
 - in `lebesgue_measure.v`:
   + declare `lebesgue_measure` as a `SigmaFinite` instance
   + lemma `lebesgue_regularity_inner_sup`
+- in `convex.v`:
+  + lemmas `conv_gt0`, `convRE`
+
+- in `exp.v`:
+  + lemmas `concave_ln`, `conjugate_powR`
 
 ### Changed
 
diff --git a/theories/convex.v b/theories/convex.v
index a7d3050925..5eff17447a 100644
--- a/theories/convex.v
+++ b/theories/convex.v
@@ -132,6 +132,23 @@ HB.instance Definition _ := @isConvexSpace.Build R R^o
 
 End realDomainType_convex_space.
 
+Section conv_realDomainType.
+Context {R : realDomainType}.
+
+Lemma conv_gt0 (a b : R^o) (t : {i01 R}) : 0 < a -> 0 < b -> 0 < a <| t |> b.
+Proof.
+move=> a0 b0.
+have [->|t0] := eqVneq t 0%:i01; first by rewrite conv0.
+have [->|t1] := eqVneq t 1%:i01; first by rewrite conv1.
+rewrite addr_gt0// mulr_gt0//; last by rewrite lt_neqAle eq_sym t0/=.
+by rewrite onem_gt0// lt_neqAle t1/=.
+Qed.
+
+Lemma convRE (a b : R^o) (t : {i01 R}) : a <| t |> b = `1-(t%:inum) * a + t%:inum * b.
+Proof. by []. Qed.
+
+End conv_realDomainType.
+
 (* ref: http://www.math.wisc.edu/~nagel/convexity.pdf *)
 Section twice_derivable_convex.
 Context {R : realType}.
diff --git a/theories/exp.v b/theories/exp.v
index e48b50696e..4861a0862e 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -601,6 +601,15 @@ apply: (@is_derive_inverse R expR); first by near=> z; apply: expRK.
 by rewrite lnK // lt0r_neq0.
 Unshelve. all: by end_near. Qed.
 
+Local Open Scope convex_scope.
+Lemma concave_ln (t : {i01 R}) (a b : R^o) : a \is Num.pos -> b \is Num.pos ->
+  (ln a : R^o) <| t |> (ln b : R^o) <= ln (a <| t |> b).
+Proof.
+move=> a0 b0; have := convex_expR t (ln a) (ln b).
+by rewrite !lnK// -(@ler_ln) ?posrE ?expR_gt0 ?conv_gt0// expRK.
+Qed.
+Local Close Scope convex_scope.
+
 End Ln.
 
 Section PowR.
@@ -752,6 +761,28 @@ move=> a0; rewrite /powR lt_eqF// gtr0_norm ?expR_gt0//.
 by rewrite ln0 ?mulr0 ?expR0// ltW.
 Qed.
 
+Lemma conjugate_powR a b p q : 0 <= a -> 0 <= b ->
+  0 < p -> 0 < q -> p^-1 + q^-1 = 1 ->
+  a * b <= a `^ p / p + b `^ q / q.
+Proof.
+rewrite le_eqVlt => /predU1P[<- b0 p0 q0 _|a0].
+  by rewrite mul0r powR0 ?gt_eqF// mul0r add0r divr_ge0 ?powR_ge0 ?ltW.
+rewrite le_eqVlt => /predU1P[<-|b0] p0 q0 pq.
+  by rewrite mulr0 powR0 ?gt_eqF// mul0r addr0 divr_ge0 ?powR_ge0 ?ltW.
+have q01 : (q^-1 \in `[0, 1])%R.
+  by rewrite in_itv/= invr_ge0 (ltW q0)/= -pq ler_paddl// invr_ge0 ltW.
+have ap0 : (0 < a `^ p)%R by rewrite powR_gt0.
+have bq0 : (0 < b `^ q)%R by rewrite powR_gt0.
+have := @concave_ln _ (@Itv.mk _ `[0, 1] _ q01)%R _ _ ap0 bq0.
+have pq' : (p^-1 = 1 - q^-1)%R by rewrite -pq addrK.
+rewrite !convE/= /onem -pq' -ler_expR expRD (mulrC p^-1).
+rewrite ln_powR mulrAC divff ?mul1r ?gt_eqF// (mulrC q^-1).
+rewrite ln_powR mulrAC divff ?mul1r ?gt_eqF//.
+rewrite lnK ?posrE// lnK ?posrE// => /le_trans; apply.
+rewrite lnK//; last by rewrite posrE addr_gt0// mulr_gt0// ?invr_gt0.
+by rewrite (mulrC _ p^-1) (mulrC _ q^-1).
+Qed.
+
 End PowR.
 Notation "a `^ x" := (powR a x) : ring_scope.