Skip to content

Commit

Permalink
Merge branch 'math-comp:master' into master
Browse files Browse the repository at this point in the history
  • Loading branch information
jmmarulang authored Nov 21, 2024
2 parents efd64b5 + 71b1296 commit e3309d0
Show file tree
Hide file tree
Showing 22 changed files with 1,100 additions and 75 deletions.
54 changes: 53 additions & 1 deletion CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -88,11 +88,37 @@
`wedge_compact`, `wedge_connected`.

- in `boolp.`:
+ lemma `existT_inj`
+ lemma `existT_inj2`
- in file `order_topology.v`
+ new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and
`max_fun_continuous`.

- in file `boolp.v`,
+ new lemmas `uncurryK`, and `curryK`
- in file `weak_topology.v`,
+ new lemma `continuous_comp_weak`
- in file `function_spaces.v`,
+ new definition `eval`
+ new lemmas `continuous_curry_fun`, `continuous_curry_cvg`,
`eval_continuous`, and `compose_continuous`

- in file `wedge_sigT.v`,
+ new definitions `wedge_fun`, and `wedge_prod`.
+ new lemmas `wedge_fun_continuous`, `wedge_lift_funE`,
`wedge_fun_comp`, `wedge_prod_pointE`, `wedge_prod_inj`,
`wedge_prod_continuous`, `wedge_prod_open`, `wedge_hausdorff`, and
`wedge_fun_joint_continuous`.

- in `boolp.v`:
+ lemmas `existT_inj1`, `surjective_existT`

- in file `homotopy_theory/path.v`,
+ new definitions `reparameterize`, `mk_path`, and `chain_path`.
+ new lemmas `path_eqP`, and `chain_path_cts_point`.
- in file `homotopy_theory/wedge_sigT.v`,
+ new definition `bpwedge_shared_pt`.
+ new notations `bpwedge`, and `bpwedge_lift`.

### Changed

- in file `normedtype.v`,
Expand Down Expand Up @@ -144,13 +170,39 @@
`subspace_valL_continuousP'`, `subspace_valL_continuousP`, `sigT_of_setXK`,
`setX_of_sigTK`, `setX_of_sigT_continuous`, and `sigT_of_setX_continuous`.

- in `tvs.v`:
+ HB structures `NbhsNmodule`, `NbhsZmodule`, `NbhsLmodule`, `TopologicalNmodule`,
`TopologicalZmodule`
+ notation `topologicalLmoduleType`, HB structure `TopologicalLmodule`
+ HB structures `UniformZmodule`, `UniformLmodule`
+ definition `convex`
+ mixin `Uniform_isTvs`
+ type `tvsType`, HB.structure `Tvs`
+ HB.factory `TopologicalLmod_isTvs`
+ lemma `nbhs0N`
+ lemma `nbhsN`
+ lemma `nbhsT`
+ lemma `nbhsB`
+ lemma `nbhs0Z`
+ lemma `nbhZ`

### Changed

- in normedtype.v
+ HB structure `normedModule` now depends on a Tvs
instead of a Lmodule
+ Factory `PseudoMetricNormedZmod_Lmodule_isNormedModule` becomes
`PseudoMetricNormedZmod_Tvs_isNormedModule`
+ Section `prod_NormedModule` now depends on a `numFieldType`

### Renamed

- in `normedtype.v`:
+ `near_in_itv` -> `near_in_itvoo`

- in normedtype.v
+ Section `regular_topology` to `standard_topology`

### Generalized

- in `lebesgue_integral.v`:
Expand Down
2 changes: 2 additions & 0 deletions _CoqProject
Original file line number Diff line number Diff line change
Expand Up @@ -63,11 +63,13 @@ theories/topology_theory/sigT_topology.v

theories/homotopy_theory/homotopy.v
theories/homotopy_theory/wedge_sigT.v
theories/homotopy_theory/path.v

theories/separation_axioms.v
theories/function_spaces.v
theories/ereal.v
theories/cantor.v
theories/tvs.v
theories/normedtype.v
theories/realfun.v
theories/sequences.v
Expand Down
22 changes: 18 additions & 4 deletions classical/boolp.v
Original file line number Diff line number Diff line change
Expand Up @@ -88,13 +88,21 @@ move=> PQA; suff: {x | P x /\ Q x} by move=> [a [*]]; exists a.
by apply: cid; case: PQA => x; exists x.
Qed.

Lemma existT_inj (A : eqType) (P : A -> Type) (p : A) (x y : P p) :
existT P p x = existT P p y -> x = y.
Lemma existT_inj1 (T : Type) (P : T -> Type) (x y : T) (Px : P x) (Py : P y) :
existT P x Px = existT P y Py -> x = y.
Proof. by case. Qed.

Lemma existT_inj2 (T : eqType) (P : T -> Type) (x : T) (Px1 Px2 : P x) :
existT P x Px1 = existT P x Px2 -> Px1 = Px2.
Proof.
apply: Eqdep_dec.inj_pair2_eq_dec => a b.
by have [|/eqP] := eqVneq a b; [left|right].
apply: Eqdep_dec.inj_pair2_eq_dec => y z.
by have [|/eqP] := eqVneq y z; [left|right].
Qed.

Lemma surjective_existT (T : Type) (P : T -> Type) (p : {x : T & P x}):
existT [eta P] (projT1 p) (projT2 p) = p.
Proof. by case: p. Qed.

Record mextensionality := {
_ : forall (P Q : Prop), (P <-> Q) -> (P = Q);
_ : forall {T U : Type} (f g : T -> U),
Expand Down Expand Up @@ -969,3 +977,9 @@ Lemma inhabited_witness: inhabited T -> T.
Proof. by rewrite inhabitedE => /cid[]. Qed.

End Inhabited.

Lemma uncurryK {X Y Z : Type} : cancel (@uncurry X Y Z) curry.
Proof. by move=> f; rewrite funeq2E. Qed.

Lemma curryK {X Y Z : Type} : cancel curry (@uncurry X Y Z).
Proof. by move=> f; rewrite funeqE=> -[]. Qed.
10 changes: 10 additions & 0 deletions classical/classical_sets.v
Original file line number Diff line number Diff line change
Expand Up @@ -2485,6 +2485,16 @@ Proof. by apply/eqP => /seteqP[] /(_ point) /(_ Logic.I). Qed.

End PointedTheory.

HB.mixin Record isBiPointed (X : Type) of Equality X := {
zero : X;
one : X;
zero_one_neq : zero != one;
}.

#[short(type="biPointedType")]
HB.structure Definition BiPointed :=
{ X of Choice X & isBiPointed X }.

Variant squashed T : Prop := squash (x : T).
Arguments squash {T} x.
Notation "$| T |" := (squashed T) : form_scope.
Expand Down
2 changes: 2 additions & 0 deletions theories/Make
Original file line number Diff line number Diff line change
Expand Up @@ -31,10 +31,12 @@ topology_theory/sigT_topology.v

homotopy_theory/homotopy.v
homotopy_theory/wedge_sigT.v
homotopy_theory/path.v

separation_axioms.v
function_spaces.v
cantor.v
tvs.v
normedtype.v
realfun.v
sequences.v
Expand Down
2 changes: 1 addition & 1 deletion theories/charge.v
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,7 @@ Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Import numFieldNormedType.Exports.

Local Open Scope ring_scope.
Local Open Scope classical_set_scope.
Expand Down
11 changes: 6 additions & 5 deletions theories/derive.v
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import reals signed topology prodnormedzmodule normedtype.
From mathcomp Require Import landau forms.
From mathcomp Require Import reals signed topology prodnormedzmodule tvs.
From mathcomp Require Import normedtype landau forms.

(**md**************************************************************************)
(* # Differentiation *)
Expand Down Expand Up @@ -788,13 +788,14 @@ by rewrite prod_normE/= !normrZ !normfV !normr_id !mulVf ?gt_eqF// maxxx ltr1n.
Qed.

Lemma bilinear_eqo (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) :
continuous (fun p => f p.1 p.2) -> (fun p => f p.1 p.2) =o_ 0 id.
continuous (fun p => f p.1 p.2) -> (fun p => f p.1 p.2) =o_ (0 : U * V') id.
Proof.
move=> fc; have [_ /posnumP[k] fschwarz] := bilinear_schwarz fc.
apply/eqoP=> _ /posnumP[e]; near=> x; rewrite (le_trans (fschwarz _ _))//.
rewrite ler_pM ?pmulr_rge0 //; last by rewrite num_le_max /= lexx orbT.
rewrite -ler_pdivlMl //.
suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite num_le_max /= lexx.
suff : `|x| <= k%:num ^-1 * e%:num.
by apply: le_trans; rewrite num_le_max /= lexx.
near: x; rewrite !near_simpl; apply/nbhs_le_nbhs_norm.
by exists (k%:num ^-1 * e%:num) => //= ? /=; rewrite /= distrC subr0 => /ltW.
Unshelve. all: by end_near. Qed.
Expand All @@ -803,7 +804,7 @@ Fact dbilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p :
continuous (fun p => f p.1 p.2) ->
continuous (fun q => (f p.1 q.2 + f q.1 p.2)) /\
(fun q => f q.1 q.2) \o shift p = cst (f p.1 p.2) +
(fun q => f p.1 q.2 + f q.1 p.2) +o_ 0 id.
(fun q => f p.1 q.2 + f q.1 p.2) +o_ (0 : U * V') id.
Proof.
move=> fc; split=> [q|].
by apply: (@continuousD _ _ _ (fun q => f p.1 q.2) (fun q => f q.1 p.2));
Expand Down
4 changes: 2 additions & 2 deletions theories/exp.v
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
From mathcomp Require Import interval rat.
From mathcomp Require Import boolp classical_sets functions.
From mathcomp Require Import mathcomp_extra reals ereal signed.
From mathcomp Require Import topology normedtype landau sequences derive.
From mathcomp Require Import topology tvs normedtype landau sequences derive.
From mathcomp Require Import realfun itv convex.

(**md**************************************************************************)
Expand Down Expand Up @@ -228,7 +228,7 @@ suff Cc : limn (h^-1 *: (series (shx h - sx))) @[h --> 0^'] --> limn (series s).
apply: cvg_zero => /=.
suff Cc : limn
(series (fun n => c n * (((h + x) ^+ n - x ^+ n) / h - n%:R * x ^+ n.-1)))
@[h --> 0^'] --> (0 : R).
@[h --> 0^'] --> 0.
apply: cvg_sub0 Cc.
apply/cvgrPdist_lt => eps eps_gt0 /=.
near=> h; rewrite sub0r normrN /=.
Expand Down
19 changes: 9 additions & 10 deletions theories/ftc.v
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop signed reals ereal.
From mathcomp Require Import topology normedtype sequences real_interval.
From mathcomp Require Import topology tvs normedtype sequences real_interval.
From mathcomp Require Import esum measure lebesgue_measure numfun realfun.
From mathcomp Require Import lebesgue_integral derive charge.

Expand All @@ -24,7 +24,7 @@ Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Import numFieldNormedType.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Expand Down Expand Up @@ -358,7 +358,7 @@ Proof.
move=> ab intf; pose fab := f \_ `[a, b].
have intfab : mu.-integrable `[a, b] (EFin \o fab).
by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr.
apply/cvgrPdist_le => /= e e0; rewrite near_simpl; near=> x.
apply/cvgrPdist_le => /= e e0; near=> x.
rewrite {1}/int /parameterized_integral sub0r normrN.
have [|xa] := leP a x.
move=> ax; apply/ltW; move: ax.
Expand Down Expand Up @@ -423,7 +423,6 @@ have intfab : mu.-integrable `[a, b] (EFin \o fab).
by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr.
rewrite /int /parameterized_integral => z; rewrite in_itv/= => /andP[az zb].
apply/cvgrPdist_le => /= e e0.
rewrite near_simpl.
have [d [d0 /= {}int_normr_cont]] := int_normr_cont _ e0.
near=> x.
have [xz|xz|->] := ltgtP x z; last by rewrite subrr normr0 ltW.
Expand Down Expand Up @@ -501,7 +500,7 @@ Corollary continuous_FTC2 f F a b : (a < b)%R ->
Proof.
move=> ab cf dF F'f.
pose fab := f \_ `[a, b].
pose G x : R := (\int[mu]_(t in `[a, x]) fab t)%R.
pose G x := (\int[mu]_(t in `[a, x]) fab t)%R.
have iabf : mu.-integrable `[a, b] (EFin \o f).
by apply: continuous_compact_integrable => //; exact: segment_compact.
have G'f : {in `]a, b[, forall x, G^`() x = fab x /\ derivable G x 1}.
Expand Down Expand Up @@ -730,7 +729,7 @@ Lemma increasing_cvg_at_left_comp F G a b (l : R) : (a < b)%R ->
Proof.
move=> ab incrF cFb GFb.
apply/cvgrPdist_le => /= e e0.
have/cvgrPdist_le /(_ e e0) [d /= d0 {}GFb] := GFb.
have /cvgrPdist_le /(_ e e0) [d /= d0 {}GFb] := GFb.
have := cvg_at_left_within cFb.
move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFb].
near=> t.
Expand All @@ -748,7 +747,7 @@ Lemma decreasing_cvg_at_right_comp F G a b (l : R) : (a < b)%R ->
Proof.
move=> ab decrF cFa GFa.
apply/cvgrPdist_le => /= e e0.
have/cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFa] := GFa.
have /cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFa] := GFa.
have := cvg_at_right_within cFa.
move/cvgrPdist_lt/(_ _ d'0) => [d'' /= d''0 {}cFa].
near=> t.
Expand All @@ -766,7 +765,7 @@ Lemma decreasing_cvg_at_left_comp F G a b (l : R) : (a < b)%R ->
Proof.
move=> ab decrF cFb GFb.
apply/cvgrPdist_le => /= e e0.
have/cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFb] := GFb.
have /cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFb] := GFb.
have := cvg_at_left_within cFb. (* different point from gt0 version *)
move/cvgrPdist_lt/(_ _ d'0) => [d'' /= d''0 {}cFb].
near=> t.
Expand Down Expand Up @@ -863,7 +862,7 @@ rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE); last 2 first.
exact: decreasing_image_oo.
* have : -%R F^`() @ x --> (- f x)%R.
by rewrite -fE//; apply: cvgN; exact: cF'.
apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl.
apply: cvg_trans; apply: near_eq_cvg.
apply: (@open_in_nearW _ _ `]a, b[) ; last by rewrite inE.
exact: interval_open.
by move=> z; rewrite inE/= => zab; rewrite fctE fE.
Expand Down Expand Up @@ -978,7 +977,7 @@ rewrite (@integration_by_substitution_decreasing (- F)%R); first last.
by case: Fab => + _ _; exact.
rewrite -derive1E.
have /cvgN := cF' _ xab; apply: cvg_trans; apply: near_eq_cvg.
rewrite near_simpl; near=> y; rewrite fctE !derive1E deriveN//.
near=> y; rewrite fctE !derive1E deriveN//.
by case: Fab => + _ _; apply; near: y; exact: near_in_itvoo.
- by move=> x y xab yab yx; rewrite ltrN2 incrF.
- by [].
Expand Down
55 changes: 55 additions & 0 deletions theories/function_spaces.v
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,7 @@ From mathcomp Require Import reals signed topology separation_axioms.
(* {family fam, F --> f} == F converges to f in {family fam, U -> V} *)
(* {compact_open, U -> V} == compact-open topology *)
(* {compact_open, F --> f} == F converges to f in {compact_open, U -> V} *)
(* eval == the evaluation map for continuous functions *)
(* ``` *)
(* *)
(* ## Ascoli's theorem notations *)
Expand Down Expand Up @@ -1436,6 +1437,17 @@ move=> v Kv; have [[P Q] [Px Qv] PQfO] : nbhs (x, v) (f @^-1` O).
by exists (Q, P) => // -[b a] /= [Qb Pa] Kb; exact: PQfO.
Unshelve. all: by end_near. Qed.

Lemma continuous_curry_fun (f : U * V -> W) :
continuous f -> continuous (curry f).
Proof. by case/continuous_curry. Qed.

Lemma continuous_curry_cvg (f : U * V -> W) (u : U) (v : V) :
continuous f -> curry f z.1 z.2 @[z --> (u, v)] --> curry f u v.
Proof.
move=> cf D /cf; rewrite !nbhs_simpl /curry /=; apply: filterS => z ? /=.
by rewrite -surjective_pairing.
Qed.

Lemma continuous_uncurry_regular (f : U -> V -> W) :
locally_compact [set: V] -> @regular_space V -> continuous f ->
(forall u, continuous (f u)) -> continuous (uncurry f).
Expand Down Expand Up @@ -1544,3 +1556,46 @@ Unshelve. all: by end_near. Qed.
End cartesian_closed.

End currying.

Definition eval {X Y : topologicalType} : continuousType X Y * X -> Y :=
uncurry (id : continuousType X Y -> (X -> Y)).

Section composition.

Local Import ArrowAsCompactOpen.

Lemma eval_continuous {X Y : topologicalType} :
locally_compact [set: X] -> regular_space X -> continuous (@eval X Y).
Proof.
move=> lcX rsX; apply: continuous_uncurry_regular => //.
exact: weak_continuous.
by move=> ?; exact: cts_fun.
Qed.

Lemma compose_continuous {X Y Z : topologicalType} :
locally_compact [set: X] -> @regular_space X ->
locally_compact [set: Y] -> @regular_space Y ->
continuous (uncurry
(comp : continuousType Y Z -> continuousType X Y -> continuousType X Z)).
Proof.
move=> lX rX lY rY; apply: continuous_comp_weak.
set F := _ \o _.
rewrite -[F]uncurryK; apply: continuous_curry_fun.
pose g := uncurry F \o prodAr \o swap; rewrite /= in g *.
have -> : uncurry F = uncurry F \o prodAr \o prodA by rewrite funeqE => -[[]].
move=> z; apply: continuous_comp; first exact: prodA_continuous.
have -> : uncurry F \o prodAr = uncurry F \o prodAr \o swap \o swap.
by rewrite funeqE => -[[]].
apply: continuous_comp; first exact: swap_continuous.
pose h (fxg : continuousType X Y * X * continuousType Y Z) : Z :=
eval (fxg.2, (eval fxg.1)).
have <- : h = uncurry F \o prodAr \o swap.
by rewrite /h/g/uncurry/swap/F funeqE => -[[]].
rewrite /h.
apply: (@continuous2_cvg _ _ _ _ _ _ snd (eval \o fst) (curry eval)).
- by apply: continuous_curry_cvg; exact: eval_continuous.
- exact: cvg_snd.
- by apply: cvg_comp; [exact: cvg_fst | exact: eval_continuous].
Qed.

End composition.
1 change: 1 addition & 0 deletions theories/homotopy_theory/homotopy.v
Original file line number Diff line number Diff line change
@@ -1,2 +1,3 @@
(* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Export wedge_sigT.
From mathcomp Require Export path.
Loading

0 comments on commit e3309d0

Please sign in to comment.