Skip to content

Commit

Permalink
ln is concave
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist committed Jul 27, 2023
1 parent 7da8655 commit 966cfef
Show file tree
Hide file tree
Showing 3 changed files with 29 additions and 0 deletions.
6 changes: 6 additions & 0 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,12 @@
+ lemmas `lte_pmulr`, `lte_pmull`, `lte_nmulr`, `lte_nmull`
+ lemmas `lte0n`, `lee0n`, `lte1n`, `lee1n`

- in `convex.v`:
+ lemma `conv_gt0`

- in `exp.v`:
+ lemma `concave_ln`

### Changed

- moved from `lebesgue_measure.v` to `real_interval.v`:
Expand Down
14 changes: 14 additions & 0 deletions theories/convex.v
Original file line number Diff line number Diff line change
Expand Up @@ -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}.
Expand Down
9 changes: 9 additions & 0 deletions theories/exp.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down

0 comments on commit 966cfef

Please sign in to comment.