ln is concave

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,12 @@
 
 ### Added
 
+- in `convex.v`:
+  + lemma `conv_gt0`
+
+- in `exp.v`:
+  + lemma `concave_ln`
+
 ### Changed
 
 ### Renamed

theories/convex.v

@@ -132,6 +132,20 @@ 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.
+
+End conv_realDomainType.
+
 (* ref: http://www.math.wisc.edu/~nagel/convexity.pdf *)
 Section twice_derivable_convex.
 Context {R : realType}.

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.