Skip to content

Commit

Permalink
ln is concave (math-comp#990)
Browse files Browse the repository at this point in the history
* ln is concave, conjugate/powR
  • Loading branch information
affeldt-aist committed Aug 23, 2023
1 parent 31d29ce commit fef976b
Show file tree
Hide file tree
Showing 3 changed files with 53 additions and 0 deletions.
5 changes: 5 additions & 0 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
17 changes: 17 additions & 0 deletions theories/convex.v
Original file line number Diff line number Diff line change
Expand Up @@ -137,6 +137,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}.
Expand Down
31 changes: 31 additions & 0 deletions theories/exp.v
Original file line number Diff line number Diff line change
Expand Up @@ -607,6 +607,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) : 0 < a -> 0 < b ->
(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 Expand Up @@ -758,6 +767,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 !convRE/= /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.

Expand Down

0 comments on commit fef976b

Please sign in to comment.