Skip to content

convex_function generalized #1887

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mkerjean wants to merge 6 commits into
base: master
Choose a base branch
from
+76 −37
Open

convex_function generalized #1887

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
65e2002
generalization
affeldt-aist Mar 11, 2026
3932450
fix
affeldt-aist Mar 11, 2026
c7d9ec4
convex_function generalized
mkerjean Mar 6, 2026
640b0ca
mv convex
affeldt-aist Mar 6, 2026
3e26e7b
simplification
affeldt-aist Mar 11, 2026
f790135
fix CI
affeldt-aist Mar 11, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,9 @@
- in `derive.v`:
+ lemmas `compact_EVT_max`, `compact_EVT_min`, `EVT_max_rV`, `EVT_min_rV`

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

### Changed

- in `constructive_ereal.v`: fixed the infamous `%E` scope bug.
Expand Down Expand Up @@ -229,6 +232,9 @@
+ lemma `cvg_comp_shift`
+ lemma `ball_open_nbhs`

- moved from `tvs.v` to `convex.v`
+ definition `convex`

### Renamed

- in `topology_structure.v`
Expand Down Expand Up @@ -273,6 +279,9 @@
+ lemmas `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd`,
`integral_itv_bndoo`

- in `convex.v`:
+ definition `convex_function` (from a realType as domain to a convex_lmodType as domain)

### Deprecated

- in `lebesgue_integral_nonneg.v`:
Expand Down
21 changes: 19 additions & 2 deletions theories/convex.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -220,7 +220,24 @@ Proof. by move=> ab; rewrite in_itv/= -lerN2 convN convC !conv_le ?lerN2. Qed.

End conv_numDomainType.

Definition convex_function (R : realType) (D : set R) (f : R -> R^o) :=
Definition convex (R : numDomainType) (M : lmodType R)
(A : set (convex_lmodType M)) :=
forall x y lambda, x \in A -> y \in A -> x <| lambda |> y \in A.

Lemma convexW (R : numDomainType) (M : lmodType R) (A : set (convex_lmodType M)) :
convex A <->
{in A &, forall x y (k : {i01 R}), 0 < k%:num -> k%:num < 1 -> x <| k |> y \in A}.
Proof.
split => [cA x y xA yA k k0 k1|cA x y l xA yA].
by have /(_ k) := cA _ _ _ xA yA.
have [->|l0] := eqVneq l 0%:i01; first by rewrite conv0.
have [->|l1] := eqVneq l 1%:i01; first by rewrite conv1.
apply: cA => //.
- by rewrite lt_neqAle eq_sym l0 ge0.
- by rewrite lt_neqAle l1 le1.
Qed.

Definition convex_function (R : numFieldType) (E : lmodType R) (E' := convex_lmodType E) (D : set E') (f : E' -> R^o) :=
forall (t : {i01 R}),
{in D &, forall (x y : R^o), (f (x <| t |> y) <= f x <| t |> f y)%R}.
{in D &, forall (x y : E'), (f (x <| t |> y) <= f x <| t |> f y)%R}.
(* TODO: generalize to convTypes once we have ordered convTypes (mathcomp 2) *)
7 changes: 4 additions & 3 deletions theories/hoelder.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -532,13 +532,14 @@ End hoelder2.
Section convex_powR.
Context {R : realType}.
Local Open Scope ring_scope.
Local Open Scope convex_scope.

Lemma convex_powR p : 1 <= p ->
convex_function `[0, +oo[%classic (@powR R ^~ p).
convex_function (`[0, +oo[%classic : set R) (@powR R ^~ p).
Proof.
move=> p1 t x y /[!inE] /= /[!in_itv] /= /[!andbT] x_ge0 y_ge0.
have p0 : 0 < p by rewrite (lt_le_trans _ p1).
rewrite !convRE; set w1 := t%:num; set w2 := t%:inum.~.
have p0 : 0 < p by rewrite (lt_le_trans _ p1).
rewrite convRE [X in X `^ _ <= _]convRE; set w1 := t%:num; set w2 := t%:inum.~.
have [->|w20] := eqVneq w2 0.
rewrite !mul0r !addr0; have [->|w10] := eqVneq w1 0.
by rewrite !mul0r powR0// gt_eqF.
Expand Down
34 changes: 20 additions & 14 deletions theories/normedtype_theory/normed_module.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ From mathcomp Require Import interval_inference fieldext falgebra.
From mathcomp Require Import unstable.
From mathcomp Require Import boolp classical_sets filter functions cardinality.
From mathcomp Require Import set_interval ereal reals topology real_interval.
From mathcomp Require Import prodnormedzmodule tvs num_normedtype.
From mathcomp Require Import convex prodnormedzmodule tvs num_normedtype.
From mathcomp Require Import ereal_normedtype pseudometric_normed_Zmodule.

(**md**************************************************************************)
Expand Down Expand Up @@ -111,21 +111,27 @@ rewrite (@le_lt_trans _ _ (`|k - l| * M)) ?ler_wpM2l -?ltr_pdivlMr//.
by near: l; apply: cvgr_dist_lt; rewrite // divr_gt0.
Unshelve. all: by end_near. Qed.

Local Open Scope convex_scope.

Let ball_convex (x : convex_lmodType V) (r : K) : convex (ball x r).
Proof.
apply/convexW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
rewrite inE/=.
rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |>
(x - y : convex_lmodType _)); last first.
by rewrite opprD -[in LHS](convmm l x) addrACA -scalerBr -scalerBr.
rewrite (le_lt_trans (ler_normD _ _))// !normrZ.
rewrite (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~) ?onem_ge0//.
rewrite -[ltRHS]mul1r -(add_onemK l%:num) [ltRHS]mulrDl.
by rewrite ltrD// ltr_pM2l// onem_gt0.
Qed.

(** NB: we have almost the same proof in `tvs.v` *)
Let locally_convex :
exists2 B : set (set V), (forall b, b \in B -> convex b) & basis B.
Proof.
exists [set B | exists x r, B = ball x r].
move=> b; rewrite inE /= => [[x]] [r] -> z y l.
rewrite !inE -!ball_normE /= => zx yx l0; rewrite -subr_gt0 => l1.
have -> : x = l *: x + (1 - l) *: x by rewrite addrC scalerBl subrK scale1r.
rewrite [X in `|X|](_ : _ = l *: (x - z) + (1 - l) *: (x - y)); last first.
by rewrite opprD addrACA -scalerBr -scalerBr.
rewrite (@le_lt_trans _ _ (`|l| * `|x - z| + `|1 - l| * `|x - y|))//.
by rewrite -!normrZ ler_normD.
rewrite (@lt_le_trans _ _ (`|l| * r + `|1 - l| * r ))//.
by rewrite ltr_leD// lter_pM2l// ?normrE ?gt_eqF// ltW.
by rewrite !gtr0_norm// -mulrDl addrC subrK mul1r.
exists2 B : set (set (convex_lmodType V)), (forall b, b \in B -> convex b) & basis B.
Proof.
exists [set B | exists (x : convex_lmodType V) r, B = ball x r].
by move=> b; rewrite inE => [[x]] [r] ->; exact: ball_convex.
split; first by move=> B [x] [r] ->; exact: ball_open.
move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=.
by exists (ball x r) => //; split; [exists x, r|exact: ballxx].
Expand Down
42 changes: 24 additions & 18 deletions theories/normedtype_theory/tvs.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,10 @@
From HB Require Import structures.
From mathcomp Require Import all_ssreflect_compat ssralg ssrnum vector.
From mathcomp Require Import interval_inference.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp classical_sets functions cardinality.
From mathcomp Require Import set_interval reals topology num_normedtype.
From mathcomp Require Import convex set_interval reals topology num_normedtype.
From mathcomp Require Import pseudometric_normed_Zmodule.

(**md**************************************************************************)
Expand Down Expand Up @@ -306,10 +308,6 @@ HB.instance Definition _ :=

HB.end.

Definition convex (R : numDomainType) (M : lmodType R) (A : set M) :=
forall x y (lambda : R), x \in A -> y \in A ->
0 < lambda -> lambda < 1 -> lambda *: x + (1 - lambda) *: y \in A.

HB.mixin Record Uniform_isTvs (R : numDomainType) E
& Uniform E & GRing.Lmodule R E := {
locally_convex : exists2 B : set (set E),
Expand Down Expand Up @@ -511,23 +509,29 @@ rewrite (@le_lt_trans _ _ (`|k - l| * M)) ?ler_wpM2l -?ltr_pdivlMr//.
by near: l; apply: cvgr_dist_lt; rewrite // divr_gt0.
Unshelve. all: by end_near. Qed.

Local Open Scope convex_scope.

Let standard_ball_convex (x : R^o) (r : R) : convex (ball x r).
Copy link
Member

@t6s t6s Mar 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't this an instance of ball_convex above?

Copy link
Member

@affeldt-aist affeldt-aist Mar 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes but ball_convex is proved inside an HB builder where the carrier is an lmodType and has a norm,
but outside the builder we do not have such a structure, making it impossible to factorize. :-(

Proof.
apply/convexW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
rewrite inE/=.
rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |>
(x - y : convex_lmodType _)); last first.
by rewrite opprD -[in LHS](convmm l x) addrACA -scalerBr -scalerBr.
rewrite (le_lt_trans (ler_normD _ _))// !normrM.
rewrite (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~) ?onem_ge0//.
rewrite -[ltRHS]mul1r -(add_onemK l%:num) [ltRHS]mulrDl.
by rewrite ltrD// ltr_pM2l// onem_gt0.
Qed.

Let standard_locally_convex :
exists2 B : set (set R^o), (forall b, b \in B -> convex b) & basis B.
Proof.
exists [set B | exists x r, B = ball x r].
move=> b; rewrite inE /= => [[x]] [r] -> z y l.
rewrite !inE -!ball_normE /= => zx yx l0; rewrite -subr_gt0 => l1.
have -> : x = l *: x + (1 - l) *: x by rewrite addrC scalerBl subrK scale1r.
rewrite [X in `|X|](_ : _ = l *: (x - z) + (1 - l) *: (x - y)); last first.
by rewrite opprD addrACA -scalerBr -scalerBr.
rewrite (@le_lt_trans _ _ (`|l| * `|x - z| + `|1 - l| * `|x - y|))//.
by rewrite -!normrM ler_normD.
rewrite (@lt_le_trans _ _ (`|l| * r + `|1 - l| * r ))//.
by rewrite ltr_leD// lter_pM2l// ?normrE ?gt_eqF// ltW.
by rewrite !gtr0_norm// -mulrDl addrC subrK mul1r.
by move=> B/= /[!inE]/= [[x]] [r] ->; exact: standard_ball_convex.
split; first by move=> B [x] [r] ->; exact: ball_open.
move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=.
by exists (ball x r) => //; split; [exists x, r|exact: ballxx].
by exists (ball x r) => //=; split; [exists x, r|exact: ballxx].
Qed.

HB.instance Definition _ :=
Expand Down Expand Up @@ -582,8 +586,10 @@ have : basis B.
rewrite !nbhsE /=; split; first by exists a => //; split => //; exact: Beo.
by exists b => //; split => // []; exact: Bfo.
exists B => // => b; rewrite inE /= => [[]] bo [] be [] bf Bee [] Bff <-.
move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2] l0 l1.
by split; rewrite -inE; [apply: Bcb; rewrite ?inE|apply: Bcf; rewrite ?inE].
move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2].
split.
by apply/set_mem/Bcb; [exact/mem_set|exact/mem_set|exact/mem_set].
by apply/set_mem/Bcf; [exact/mem_set|exact/mem_set|exact/mem_set].
Qed.

HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build
Expand Down
Loading