diff --git a/CHANGELOG.md b/CHANGELOG.md index 2dc9f65c9e..bf0a8172d5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,127 @@ # Changelog -Latest releases: [[0.6.7] - 2024-01-09](#067---2024-01-09) and [[0.6.6] - 2023-11-14](#066---2023-11-14) +Latest releases: [[0.7.0] - 2024-01-19](#070---2024-01-19) and [[0.6.7] - 2024-01-09](#067---2024-01-09) + +## [0.7.0] - 2024-01-19 + +### Added + +- in `mathcomp_extra.v`: + + lemmas `last_filterP`, + `path_lt_filter0`, `path_lt_filterT`, `path_lt_head`, `path_lt_last_filter`, + `path_lt_le_last` + +- new file `contra.v` + + lemma `assume_not` + + tactic `assume_not` + + lemma `absurd_not` + + tactics `absurd_not`, `contrapose` + + tactic notations `contra`, `contra : constr(H)`, `contra : ident(H)`, + `contra : { hyp_list(Hs) } constr(H)`, `contra : { hyp_list(Hs) } ident(H)`, + `contra : { - } constr(H)` + + lemma `absurd` + + tactic notations `absurd`, `absurd constr(P)`, `absurd : constr(H)`, + `absurd : ident(H)`, `absurd : { hyp_list(Hs) } constr(H)`, + `absurd : { hyp_list(Hs) } ident(H)` + +- in `topology.v`: + + lemma `filter_bigI_within` + + lemma `near_powerset_map` + + lemma `near_powerset_map_monoE` + + lemma `fst_open` + + lemma `snd_open` + + definition `near_covering_within` + + lemma `near_covering_withinP` + + lemma `compact_setM` + + lemma `compact_regular` + + lemma `fam_compact_nbhs` + + definition `compact_open`, notation `{compact-open, U -> V}` + + notation `{compact-open, F --> f}` + + definition `compact_openK` + + definition `compact_openK_nbhs` + + instance `compact_openK_nbhs_filter` + + definition `compact_openK_topological_mixin` + + canonicals `compact_openK_filter`, `compact_openK_topological`, + `compact_open_pointedType` + + definition `compact_open_topologicalType` + + canonicals `compact_open_filtered`, `compact_open_topological` + + lemma `compact_open_cvgP` + + lemma `compact_open_open` + + lemma `compact_closedI` + + lemma `compact_open_fam_compactP` + + lemma `compact_equicontinuous` + + lemma `uniform_regular` + + lemma `continuous_curry` + + lemma `continuous_uncurry_regular` + + lemma `continuous_uncurry` + + lemma `curry_continuous` + + lemma `uncurry_continuous` + +- in `ereal.v`: + + lemma `ereal_supy` + +- in file `normedtype.v`, + + new lemma `continuous_within_itvP`. + +- in file `realfun.v`, + + new definitions `itv_partition`, `itv_partitionL`, `itv_partitionR`, + `variation`, `variations`, `bounded_variation`, `total_variation`, + `neg_tv`, and `pos_tv`. + + + new lemmas `left_right_continuousP`, + `nondecreasing_funN`, `nonincreasing_funN` + + + new lemmas `itv_partition_nil`, `itv_partition_cons`, `itv_partition1`, + `itv_partition_size_neq0`, `itv_partitionxx`, `itv_partition_le`, + `itv_partition_cat`, `itv_partition_nth_size`, + `itv_partition_nth_ge`, `itv_partition_nth_le`, + `nondecreasing_fun_itv_partition`, `nonincreasing_fun_itv_partition`, + `itv_partitionLP`, `itv_partitionRP`, `in_itv_partition`, + `notin_itv_partition`, `itv_partition_rev`, + + + new lemmas `variation_zip`, `variation_prev`, `variation_next`, `variation_nil`, + `variation_ge0`, `variationN`, `variation_le`, `nondecreasing_variation`, + `nonincreasing_variation`, `variationD`, `variation_itv_partitionLR`, + `le_variation`, `variation_opp_rev`, `variation_rev_opp` + + + new lemmas `variations_variation`, `variations_neq0`, `variationsN`, `variationsxx` + + + new lemmas `bounded_variationxx`, `bounded_variationD`, `bounded_variationN`, + `bounded_variationl`, `bounded_variationr`, `variations_opp`, + `nondecreasing_bounded_variation` + + + new lemmas `total_variationxx`, `total_variation_ge`, `total_variation_ge0`, + `bounded_variationP`, `nondecreasing_total_variation`, `total_variationN`, + `total_variation_le`, `total_variationD`, `neg_tv_nondecreasing`, + `total_variation_pos_neg_tvE`, `fine_neg_tv_nondecreasing`, + `neg_tv_bounded_variation`, `total_variation_right_continuous`, + `neg_tv_right_continuous`, `total_variation_opp`, + `total_variation_left_continuous`, `total_variation_continuous` + +- in `lebesgue_stieltjes_measure.v`: + + `sigma_finite_measure` HB instance on `lebesgue_stieltjes_measure` + +- in `lebesgue_measure.v`: + + `sigma_finite_measure` HB instance on `lebesgue_measure` + +- in `lebesgue_integral.v`: + + `sigma_finite_measure` instance on product measure `\x` + +### Changed + +- in `topology.v`: + + lemmas `nbhsx_ballx` and `near_ball` take a parameter of type `R` instead of `{posnum R}` + + lemma `pointwise_compact_cvg` + +### Generalized + +- in `realfun.v`: + + lemmas `nonincreasing_at_right_cvgr`, `nonincreasing_at_left_cvgr` + + lemmas `nondecreasing_at_right_cvge`, `nondecreasing_at_right_is_cvge`, + `nonincreasing_at_right_cvge`, `nonincreasing_at_right_is_cvge` + +- in `realfun.v`: + + lemmas `nonincreasing_at_right_is_cvgr`, `nondecreasing_at_right_is_cvgr` ## [0.6.7] - 2024-01-09 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 89e2e400bd..2d1ba5e501 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,158 +4,14 @@ ### Added -- in file `cantor.v`, - + new definitions `cantor_space`, `cantor_like`, `pointed_discrete`, and - `tree_of`. - + new lemmas `cantor_space_compact`, `cantor_space_hausdorff`, - `cantor_zero_dimensional`, `cantor_perfect`, `cantor_like_cantor_space`, - `tree_map_props`, `homeomorphism_cantor_like`, and - `cantor_like_finite_prod`. - + new theorem `cantor_surj`. -- in file `topology.v`, - + new lemmas `perfect_set2`, and `ent_closure`. - + lemma `clopen_surj` - - in `cantor.v`: + definitions `pointed_principal_filter`, `pointed_discrete_topology` + lemma `discrete_pointed` + lemma `discrete_bool_compact` -- in `normedtype.v`: - + hints for `at_right_proper_filter` and `at_left_proper_filter` - -- in `realfun.v`: - + notations `nondecreasing_fun`, `nonincreasing_fun`, - `increasing_fun`, `decreasing_fun` - + lemmas `cvg_addrl`, `cvg_addrr`, `cvg_centerr`, `cvg_shiftr`, - `nondecreasing_cvgr`, - `nonincreasing_at_right_cvgr`, - `nondecreasing_at_right_cvgr`, - `nondecreasing_cvge`, `nondecreasing_is_cvge`, - `nondecreasing_at_right_cvge`, `nondecreasing_at_right_is_cvge`, - `nonincreasing_at_right_cvge`, `nonincreasing_at_right_is_cvge` -- in `ereal.v`: - + lemmas `ereal_sup_le`, `ereal_inf_le` - -- in `normedtype.v`: - + definition `lower_semicontinuous` - + lemma `lower_semicontinuousP` - -- in `numfun.v`: - + lemma `patch_indic` - -- in `lebesgue_measure.v` - + lemma `lower_semicontinuous_measurable` - -- in `lebesgue_integral.v`: - + definition `locally_integrable` - + lemmas `integrable_locally`, `locally_integrableN`, `locally_integrableD`, - `locally_integrableB` - + definition `iavg` - + lemmas `iavg0`, `iavg_ge0`, `iavg_restrict`, `iavgD` - + definitions `HL_maximal` - + lemmas `HL_maximal_ge0`, `HL_maximalT_ge0`, - `lower_semicontinuous_HL_maximal`, `measurable_HL_maximal`, - `maximal_inequality` - -- in file `measure.v` - + add lemmas `ae_eq_subset`, `measure_dominates_ae_eq`. - -- in `charge.v` - + definition `charge_of_finite_measure` (instance of `charge`) - + lemmas `dominates_cscalel`, `dominates_cscaler` - + definition `cpushforward` (instance of `charge`) - + lemma `dominates_pushforward` - + lemma `cjordan_posE` - + lemma `jordan_posE` - + lemma `cjordan_negE` - + lemma `jordan_negE` - + lemma `Radon_Nikodym_sigma_finite` - + lemma `Radon_Nikodym_fin_num` - + lemma `Radon_Nikodym_integral` - + lemma `ae_eq_Radon_Nikodym_SigmaFinite` - + lemma `Radon_Nikodym_change_of_variables` - + lemma `Radon_Nikodym_cscale` - + lemma `Radon_Nikodym_cadd` - + lemma `Radon_Nikodym_chain_rule` - -- in `sequences.v`: - + lemma `minr_cvg_0_cvg_0` - + lemma `mine_cvg_0_cvg_fin_num` - + lemma `mine_cvg_minr_cvg` - + lemma `mine_cvg_0_cvg_0` - + lemma `maxr_cvg_0_cvg_0` - + lemma `maxe_cvg_0_cvg_fin_num` - + lemma `maxe_cvg_maxr_cvg` - + lemma `maxe_cvg_0_cvg_0` -- in `constructive_ereal.v` - + lemma `lee_subgt0Pr` - -- in `topology.v`: - + lemma `nbhs_dnbhs_neq` - -- in `normedtype.v`: - + lemma `not_near_at_rightP` - -- in `realfun.v`: - + lemma `cvg_at_right_left_dnbhs` - + lemma `cvg_at_rightP` - + lemma `cvg_at_leftP` - + lemma `cvge_at_rightP` - + lemma `cvge_at_leftP` - + lemma `lime_sup` - + lemma `lime_inf` - + lemma `lime_supE` - + lemma `lime_infE` - + lemma `lime_infN` - + lemma `lime_supN` - + lemma `lime_sup_ge0` - + lemma `lime_inf_ge0` - + lemma `lime_supD` - + lemma `lime_sup_le` - + lemma `lime_inf_sup` - + lemma `lim_lime_inf` - + lemma `lim_lime_sup` - + lemma `lime_sup_inf_at_right` - + lemma `lime_sup_inf_at_left` - -- in `normedtype.v`: - + lemmas `withinN`, `at_rightN`, `at_leftN`, `cvg_at_leftNP`, `cvg_at_rightNP` - + lemma `dnbhsN` - + lemma `limf_esup_dnbhsN` - -- in `topology.v`: - + lemma `dnbhs_ball` - -- in `normedtype.v` - + definitions `limf_esup`, `limf_einf` - + lemmas `limf_esupE`, `limf_einfE`, `limf_esupN`, `limf_einfN` - -- in `sequences.v`: - + lemmas `limn_esup_lim`, `limn_einf_lim` - -- in `realfun.v`: - + lemmas `lime_sup_lim`, `lime_inf_lim` - -- in `boolp.v`: - + tactic `eqProp` - + variant `BoolProp` - + lemmas `PropB`, `notB`, `andB`, `orB`, `implyB`, `decide_or`, `not_andE`, - `not_orE`, `orCA`, `orAC`, `orACA`, `orNp`, `orpN`, `or3E`, `or4E`, `andCA`, - `andAC`, `andACA`, `and3E`, `and4E`, `and5E`, `implyNp`, `implypN`, - `implyNN`, `or_andr`, `or_andl`, `and_orr`, `and_orl`, `exists2E`, - `inhabitedE`, `inhabited_witness` -- in `lebesgue_stieltjes_measure.v`: - + `sigma_finite_measure` HB instance on `lebesgue_stieltjes_measure` - -- in `lebesgue_measure.v`: - + `sigma_finite_measure` HB instance on `lebesgue_measure` - -- in `lebesgue_integral.v`: - + `sigma_finite_measure` instance on product measure `\x` ### Changed - + ### Renamed ### Generalized diff --git a/INSTALL.md b/INSTALL.md index fb7ee64fb8..0885655132 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -2,11 +2,11 @@ ## Requirements -- [The Coq Proof Assistant version ≥ 8.14](https://coq.inria.fr) -- [Mathematical Components version ≥ 1.13.0](https://github.com/math-comp/math-comp) - + except `coq-mathcomp-solvable` ≥ 1.15.0 +- [The Coq Proof Assistant version ≥ 8.15](https://coq.inria.fr) +- [Mathematical Components version ≥ 1.17.0](https://github.com/math-comp/math-comp) - [Finmap library version ≥ 1.5.1](https://github.com/math-comp/finmap) - [Hierarchy builder version >= 1.2.0](https://github.com/math-comp/hierarchy-builder) +- [bigenough >= 1.0.0](https://github.com/math-comp/bigenough) These requirements can be installed in a custom way, or through [opam](https://opam.ocaml.org/) (the recommended way) using @@ -48,7 +48,7 @@ $ opam install coq-mathcomp-analysis ``` To install a precise version, type, say ``` -$ opam install coq-mathcomp-analysis.0.6.7 +$ opam install coq-mathcomp-analysis.0.7.0 ``` 4. Everytime you want to work in this same context, you need to type ``` @@ -71,20 +71,20 @@ using [proof general for emacs](https://github.com/ProofGeneral/PG) ## Break-down of phase 3 of the installation procedure step by step -With the example of Coq 8.14.0 and MathComp 1.13.0. For other versions, update the +With the example of Coq 8.15.0 and MathComp 1.17.0. For other versions, update the version numbers accordingly. -1. Install Coq 8.14.0 +1. Install Coq 8.15.0 ``` -$ opam install coq.8.14.0 +$ opam install coq.8.15.0 ``` 2. Install the Mathematical Components ``` -$ opam install coq-mathcomp-ssreflect.1.13.0 -$ opam install coq-mathcomp-fingroup.1.13.0 -$ opam install coq-mathcomp-algebra.1.13.0 -$ opam install coq-mathcomp-solvable.1.13.0 -$ opam install coq-mathcomp-field.1.13.0 +$ opam install coq-mathcomp-ssreflect.1.17.0 +$ opam install coq-mathcomp-fingroup.1.17.0 +$ opam install coq-mathcomp-algebra.1.17.0 +$ opam install coq-mathcomp-solvable.1.17.0 +$ opam install coq-mathcomp-field.1.17.0 ``` 3. Install the Finite maps library ``` diff --git a/README.md b/README.md index a7dbff5d4e..a0e4e95699 100644 --- a/README.md +++ b/README.md @@ -35,11 +35,11 @@ the Coq proof-assistant and using the Mathematical Components library. - License: [CeCILL-C](LICENSE) - Compatible Coq versions: Coq 8.14 to 8.18 (or dev) - Additional dependencies: - - [MathComp ssreflect 1.13 or later](https://math-comp.github.io) - - [MathComp fingroup 1.13 or later](https://math-comp.github.io) - - [MathComp algebra 1.13 or later](https://math-comp.github.io) - - [MathComp solvable 1.15 or later](https://math-comp.github.io) - - [MathComp field 1.13 or later](https://math-comp.github.io) + - [MathComp ssreflect 1.17 or later](https://math-comp.github.io) + - [MathComp fingroup 1.17 or later](https://math-comp.github.io) + - [MathComp algebra 1.17 or later](https://math-comp.github.io) + - [MathComp solvable 1.17 or later](https://math-comp.github.io) + - [MathComp field 1.17 or later](https://math-comp.github.io) - [MathComp finmap 1.5.1](https://github.com/math-comp/finmap) - [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough) - [Hierarchy Builder >= 1.2.0](https://github.com/math-comp/hierarchy-builder) diff --git a/_CoqProject b/_CoqProject index fcb3ccc198..45e3d6e8ba 100644 --- a/_CoqProject +++ b/_CoqProject @@ -10,6 +10,7 @@ classical/all_classical.v classical/boolp.v +classical/contra.v classical/classical_sets.v classical/mathcomp_extra.v classical/functions.v diff --git a/classical/Make b/classical/Make index 8e854b561e..4d4fe74c81 100644 --- a/classical/Make +++ b/classical/Make @@ -8,6 +8,7 @@ -arg -w -arg -projection-no-head-constant boolp.v +contra.v classical_sets.v mathcomp_extra.v functions.v diff --git a/classical/all_classical.v b/classical/all_classical.v index ae11425621..9581e05ef0 100644 --- a/classical/all_classical.v +++ b/classical/all_classical.v @@ -1,4 +1,5 @@ From mathcomp Require Export boolp. +From mathcomp Require Export contra. From mathcomp Require Export classical_sets. From mathcomp Require Export mathcomp_extra. From mathcomp Require Export functions. diff --git a/classical/contra.v b/classical/contra.v new file mode 100644 index 0000000000..6f158e4829 --- /dev/null +++ b/classical/contra.v @@ -0,0 +1,883 @@ +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +From mathcomp Require Import boolp. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(******************************************************************************) +(* Contraposition *) +(* *) +(* This file provides tactics to reason by contraposition and contradiction. *) +(* *) +(* * Tactics *) +(* assume_not == add a goal negation assumption. The tactic also works for *) +(* goals in Type, simplifies the added assumption, and *) +(* exposes its top-level constructive content. *) +(* absurd_not == proof by contradiction. Same as assume_not, but the goal is *) +(* erased and replaced by False. *) +(* Caveat: absurd_not cannot be used as a move/ view because *) +(* its conclusion is indeterminate. The more general notP can *) +(* be used instead. *) +(* contra == proof by contraposition. Change a goal of the form *) +(* assumption -> conclusion to ~ conclusion -> ~ assumption. *) +(* As with assume_not, contra allows both assumption and *) +(* conclusion to be in Type, simplifies the negation of both *) +(* assumption and conclusion, and exposes the constructive *) +(* contents of the negated conclusion. *) +(* The contra tactic also supports a limited form of the ':' *) +(* discharge pseudo tactical, whereby contra: means *) +(* move: ; contra. *) +(* The only allowed are one term, possibly preceded *) +(* by a clear switch. *) +(* absurd == proof by contradiction. The defective form of the tactic *) +(* simply replaces the entire goal with False (just as the Ltac *) +(* exfalso), leaving the user to derive a contradiction from *) +(* the assumptions. *) +(* The ':' form absurd: replaces the goal with the *) +(* negation of the (single) (as with contra:, a clear *) +(* switch is also allowed. *) +(* Finally the Ltac absurd term form is also supported. *) +(******************************************************************************) + +(* Hiding module for the internal definitions and lemmas used by the tactics + defined here. *) +Module Internals. + +(******************************************************************************) +(* A wrapper for view lemmas with an indeterminate conclusion (of the form *) +(* forall ... T ..., pattern -> T), and for which the intended view pattern *) +(* may fail to match some assumptions. This wrapper ensures that such views *) +(* are only used in the forward direction (as in move/), and only with the *) +(* appropriate move_viewP hint, preventing its application to an arbitrary *) +(* assumption A by the instatiation to A -> T' of its indeterminate *) +(* conclusion T. This is similar to the implies wrapper, except move_viewP is *) +(* NOT declared as a coercion - it must be used explicitly to apply the view *) +(* manually to an assumption (as in, move_viewP my_view some_assumption). *) +(******************************************************************************) + +Variant move_view S T := MoveView of S -> T. +Definition move_viewP {S T} mv : S -> T := let: MoveView v := mv in v. +Hint View for move/ move_viewP|2. + +(******************************************************************************) +(* A generic Forall "constructor" for the Gallina forall quantifier, i.e., *) +(* \Forall x, P := Forall (fun x => P) := forall x, P. *) +(* The main use of Forall is to apply congruence to a forall equality: *) +(* congr1 Forall : forall P Q, P = Q -> Forall P = Forall Q. *) +(* in particular in a classical setting with function extensionality, where *) +(* we can have (forall x, P x = Q x) -> (forall x, P x) = (forall x, Q x). *) +(* We use a forallSort structure to factor the ad hoc PTS product formation *) +(* rules; forallSort is keyed on the type of the entire forall expression, or *) +(* (up to subsumption) the type of the forall body - this is always a sort. *) +(* This implementation has two important limitations: *) +(* 1) It cannot handle the SProp sort and its typing rules. However, its *) +(* main application is extensionality, which is not compatible with *) +(* SProp because an (A : SProp) -> B "function" is not a generic *) +(* (A : Type) -> B function as SProp is not included in Type. *) +(* 2) The Forall constructor can't be inserted by a straightforward *) +(* unfold (as in, rewrite -[forall x, _]/(Forall _)) because of the *) +(* way Coq unification handles Type constraints. The ForallI tactic *) +(* mitigates this issue, but there are additional issues with its *) +(* implementation -- see below. *) +(******************************************************************************) + +Structure forallSort A := + ForallSort {forall_sort :> Type; _ : (A -> forall_sort) -> forall_sort}. + +Notation mkForallSort A S := (@ForallSort A S (fun T => forall x, T x)). +Polymorphic Definition TypeForall (S := Type) (A : S) := mkForallSort A S. +Canonical TypeForall. + +Canonical PropForall A := mkForallSort A Prop. + +(* This is just a special case of TypeForall, but it provides a projection *) +(* for the Set sort "constant". *) +Canonical SetForall (A : Set) := mkForallSort A Set. + +Definition Forall {A} {S : forallSort A} := + let: ForallSort _ F := S return (A -> S) -> S in F. + +Notation "\Forall x .. z , T" := + (Forall (fun x => .. (Forall (fun z => T)) ..)) + (at level 200, x binder, z binder, T at level 200, + format "'[hv' '\Forall' '[' x .. z , ']' '/ ' T ']'") : type_scope. + +(* The ForallI implementation has to work around several Coq 8.12 issues: *) +(* - Coq unification defers Type constraints so we must ensure the type *) +(* constraint for the forall term F is processed, and the resulting *) +(* sort unified with the forall_sort projection _BEFORE_ F is unified *) +(* with a Forall _ pattern, because the inferred forallSort structure *) +(* determines the actual shape of that pattern. This is done by passing *) +(* F to erefl, then constraining the type of erefl to Forall _ = _. Note *) +(* that putting a redundant F on the right hand side would break due to *) +(* incomplete handling of subtyping. *) +(* - ssr rewrite and Coq replace do not handle universe constraints. *) +(* and rewrite does not handle subsumption of the redex type. This means *) +(* we cannot use rewrite, replace or fold, and must resort to primitive *) +(* equality destruction. *) +(* - ssr case: and set do not recognize ssrpatternarg parameters, so we *) +(* must rely on ssrmatching.ssrpattern. *) +Tactic Notation "ForallI" ssrpatternarg(pat) := + let F := fresh "F" in ssrmatching.ssrpattern pat => F; + case: F / (@erefl _ F : Forall _ = _). +Tactic Notation "ForallI" := ForallI (forall x, _). + +(******************************************************************************) +(* We define specialized copies of the wrapped structure of ssrfun for Prop *) +(* and Type, as we need more than two alternative rules (indeed, 3 for Prop *) +(* and 4 for Type). We need separate copies for Prop and Type as universe *) +(* polymorphism cannot instantiate Type with Prop. *) +(******************************************************************************) + +Structure wrappedProp := WrapProp {unwrap_Prop :> Prop}. +Definition wrap4Prop := WrapProp. +Definition wrap3Prop := wrap4Prop. +Definition wrap2Prop := wrap3Prop. +Canonical wrap1Prop P := wrap2Prop P. + +Polymorphic Structure wrappedType@{i} := WrapType {unwrap_Type :> Type@{i}}. +Polymorphic Definition wrap4Type@{i} := WrapType@{i}. +Polymorphic Definition wrap3Type@{i} := wrap4Type@{i}. +Polymorphic Definition wrap2Type@{i} := wrap3Type@{i}. +Polymorphic Definition wrap1Type@{i} (T : Type@{i}) := wrap2Type T. +Canonical wrap1Type. + +Lemma generic_forall_extensionality {A} {S : forallSort A} {P Q : A -> S} : + P =1 Q -> Forall P = Forall Q. +Proof. by move/funext->. Qed. + +(******************************************************************************) +(* A set of tools (tactics, views, and rewrite rules) to facilitate the *) +(* handling of classical negation. The core functionality of these tools is *) +(* implemented by three sets of canonical structures that provide for the *) +(* simplification of negation statements (e.g., using de Morgan laws), the *) +(* conversion from constructive statements in Type to purely logical ones in *) +(* Prop (equivalently, expansion rules for the statement inhabited T), and *) +(* conversely extraction of constructive contents from logical statements. *) +(* Except for bool predicates and operators, all definitions are treated *) +(* transparently when matching statements for either simplification or *) +(* conversion; this is achieved by using the wrapper telescope pattern, first *) +(* delegating the matching of specific logical connectives, predicates, or *) +(* type constructors to an auxiliary structure that FAILS to match unknown *) +(* operators, thus triggers the expansion of defined constants. If this *) +(* ultimately fails then the wrapper is expanded, and the primary structure *) +(* instance for the expanded wrapper provides an alternative default rule: *) +(* not simplifying ~ P, not expanding inhabited T, or not extracting any *) +(* contents from a proposition P, respectively. *) +(* Additional rules, for intermediate wrapper instances, are used to handle *) +(* forall statements (for which canonical instances are not yet supported), *) +(* as well as addiitonal simplifications, such as inhabited P = P :> Prop. *) +(* Finally various tertiary structures are used to match deeper patterns, *) +(* such as bounded forall statements of the form forall x, P x -> Q x, or *) +(* inequalites x != y (i.e., is_true (~~ (x == y))). As mentioned above, *) +(* tertiary rules for bool subexpressions do not try to expand definitions, *) +(* as this would lead to the undesireable expansion of some standard *) +(* definitions. This is simply achieved by NOT using the wrapper telescope *) +(* pattern, and just having a default instance alongside those for specific *) +(* predicates and connectives. *) +(******************************************************************************) + +(******************************************************************************) +(* The negatedProp structure provides simplification of the Prop negation *) +(* (~ _) for standard connectives and predicates. The instances below cover *) +(* the pervasive and ssrbool Prop connectives, decidable equality, as well as *) +(* bool propositions (i.e., the is_true predicate), together with a few bool *) +(* connectives and predicates: negation ~~, equality ==, and nat <= and <. *) +(* Others can be added (e.g., Order.le/lt) by declaring appropriate instances *) +(* of bool_negation and bool_affirmation, while other Prop connectives and *) +(* predicates can be added by declaring instances of proper_negatedProp. *) +(******************************************************************************) + +(******************************************************************************) +(* The implementation follows the wrapper telescope pattern outlined above: *) +(* negatedProp instances match on the wrappedProp wrapper to try three *) +(* generic matching rules, in sucession: *) +(* Rule 1: match a specific connective or predicate with an instance of the *) +(* properNegatedProp secondary structure, expanding definitions *) +(* if needed, but failing if no proper match is found. *) +(* Rule 2: match a forall statement (including (T : Type) -> P statements). *) +(* Rule 3: match any Prop but return the trivial simplification. *) +(* The simplified proposition is returned as a projection parameter nP rather *) +(* than a Structure member, so that applying the corresponding views or *) +(* rewrite rules doesn't expose the inferred structures; properNegatedProp *) +(* does similarly. Also, negatedProp similarly returns a 'trivial' bool flag *) +(* that is set when Rule 3 is used, but this is actually used in the reverse *) +(* direction: views notP and rewrite rule notE force trivial := false, thus *) +(* excluding trivial instances. *) +(******************************************************************************) + +Structure negatedProp (trivial : bool) nP := + NegatedProp {negated_Prop :> wrappedProp; _ : (~ negated_Prop) = nP}. + +Structure properNegatedProp nP := ProperNegatedProp { + proper_negated_Prop :> Prop; _ : (~ proper_negated_Prop) = nP}. + +Local Notation nProp t nP P := (unwrap_Prop (@negated_Prop t nP P)). +Local Notation nPred t nP P x := (nProp t (nP x) (P x)). +Local Notation pnProp nP P := (@proper_negated_Prop nP P). + +(******************************************************************************) +(* User views and rewrite rules. The plain versions (notP, notE and notI) do *) +(* not match trivial instances; lax_XXX versions allow them. In addition, *) +(* the negation introduction rewrite rule notI does not match forall or -> *) +(* statements - lax_notI must be used for these. *) +(******************************************************************************) + +Lemma lax_notE {t nP} P : (~ nProp t nP P) = nP. Proof. by case: P. Qed. +Lemma lax_notP {t nP P} : ~ nProp t nP P -> nP. Proof. by rewrite lax_notE. Qed. +Definition lax_notI {t nP} P : nProp t nP P = (~ nP) := canRL notK (lax_notE P). + +Definition notE {nP} P : (~ nProp false nP P) = nP := lax_notE P. +Definition notP {nP P} := MoveView (@lax_notP false nP P). + +Fact proper_nPropP nP P : (~ pnProp nP P) = nP. Proof. by case: P. Qed. +Definition notI {nP} P : pnProp nP P = ~ nP := canRL notK (proper_nPropP P). + +(* Rule 1: proper negation simplification, delegated to properNegatedProp. *) +Canonical proper_nProp nP P := + @NegatedProp false nP (wrap1Prop (pnProp nP P)) (proper_nPropP P). + +(* Rule 2: forall_nProp is defined below as it uses exists_nProp. *) + +(* Rule 3: trivial negation. *) +Canonical trivial_nProp P := @NegatedProp true (~ P) (wrap3Prop P) erefl. + +(* properNegatedProp instances. *) + +Canonical True_nProp := @ProperNegatedProp False True notB.1. +Canonical False_nProp := @ProperNegatedProp True False notB.2. +Canonical not_nProp P := @ProperNegatedProp P (~ P) (notK P). + +Fact and_nPropP P tQ nQ Q : (~ (P /\ nProp tQ nQ Q)) = (P -> nQ). +Proof. by rewrite -implypN lax_notE. Qed. +Canonical and_nProp P tQ nQ Q := + ProperNegatedProp (@and_nPropP P tQ nQ Q). + +Fact and3_nPropP P Q tR nR R : (~ [/\ P, Q & nProp tR nR R]) = (P -> Q -> nR). +Proof. by hnf; rewrite and3E notE. Qed. +Canonical and3_nProp P Q tR nR R := + ProperNegatedProp (@and3_nPropP P Q tR nR R). + +Fact and4_nPropP P Q R tS nS S : + (~ [/\ P, Q, R & nProp tS nS S]) = (P -> Q -> R -> nS). +Proof. by hnf; rewrite and4E notE. Qed. +Canonical and4_nProp P Q R tS nS S := + ProperNegatedProp (@and4_nPropP P Q R tS nS S). + +Fact and5_nPropP P Q R S tT nT T : + (~ [/\ P, Q, R, S & nProp tT nT T]) = (P -> Q -> R -> S -> nT). +Proof. by hnf; rewrite and5E notE. Qed. +Canonical and5_nProp P Q R S tT nT T := + ProperNegatedProp (@and5_nPropP P Q R S tT nT T). + +Fact or_nPropP tP nP P tQ nQ Q : + (~ (nProp tP nP P \/ nProp tQ nQ Q)) = (nP /\ nQ). +Proof. by rewrite not_orE !lax_notE. Qed. +Canonical or_nProp tP nP P tQ nQ Q := + ProperNegatedProp (@or_nPropP tP nP P tQ nQ Q). + +Fact or3_nPropP tP nP P tQ nQ Q tR nR R : + (~ [\/ nProp tP nP P, nProp tQ nQ Q | nProp tR nR R]) = [/\ nP, nQ & nR]. +Proof. by rewrite or3E notE and3E. Qed. +Canonical or3_nProp tP nP P tQ nQ Q tR nR R := + ProperNegatedProp (@or3_nPropP tP nP P tQ nQ Q tR nR R). + +Fact or4_nPropP tP nP P tQ nQ Q tR nR R tS nS S : + (~ [\/ nProp tP nP P, nProp tQ nQ Q, nProp tR nR R | nProp tS nS S]) + = [/\ nP, nQ, nR & nS]. +Proof. by rewrite or4E notE and4E. Qed. +Canonical or4_nProp tP nP P tQ nQ Q tR nR R tS nS S := + ProperNegatedProp (@or4_nPropP tP nP P tQ nQ Q tR nR R tS nS S). + +(******************************************************************************) +(* The andRHS tertiary structure used to simplify (~ (P -> False)) to P, *) +(* both here for the imply_nProp instance and for bounded_forall_nProp below. *) +(* Because the andRHS instances match the Prop RETURNED by negatedProp they *) +(* do not need to expand definitions, hence do not need to use the wrapper *) +(* telescope pattern. *) +(******************************************************************************) + +Notation and_def binary P Q PQ := (PQ = if binary then P /\ Q else Q)%type. +Structure andRHS binary P Q PQ := + AndRHS {and_RHS :> Prop; _ : (P /\ and_RHS) = PQ; _ : and_def binary P Q PQ}. +Canonical unary_and_rhs P := @AndRHS false P P P True (andB.1.2 P) erefl. +Canonical binary_and_rhs P Q := @AndRHS true P Q (P /\ Q) Q erefl erefl. + +Fact imply_nPropP b P nQ PnQ tR (nR : andRHS b P nQ PnQ) R : + (~ (P -> nProp tR nR R)) = PnQ. +Proof. by rewrite -orNp {R}lax_notE; case: nR. Qed. +Canonical imply_nProp b P nQ PnQ tR nR R := + ProperNegatedProp (@imply_nPropP b P nQ PnQ tR nR R). + +Fact exists_nPropP A tP nP P : + (~ exists x : A, nPred tP nP P x) = (forall x : A, nP x). +Proof. +eqProp=> [nEP x | AnP [x]]; last by rewrite -/(~ _) lax_notE. +by rewrite -(lax_notE (P x)) => Px; case: nEP; exists x. +Qed. +Canonical exists_nProp A tP nP P := + ProperNegatedProp (@exists_nPropP A tP nP P). + +Fact exists2_nPropP A P tQ nQ Q : + (~ exists2 x : A, P x & nPred tQ nQ Q x) = (forall x : A, P x -> nQ x). +Proof. by rewrite exists2E notE. Qed. +Canonical exists2_nProp A P tQ nQ Q := + ProperNegatedProp (@exists2_nPropP A P tQ nQ Q). + +Fact inhabited_nPropP T : (~ inhabited T) = (T -> False). +Proof. by rewrite inhabitedE notE. Qed. +Canonical inhabited_nProp T := ProperNegatedProp (inhabited_nPropP T). + +(******************************************************************************) +(* Rule 2: forall negation, including (T : Type) -> P statements. *) +(* We use tertiary structures to recognize bounded foralls and simplify, *) +(* e.g., ~ forall x, P -> Q to exists2 x, P & ~ Q, or even exists x, P when *) +(* Q := False (as above for imply). *) +(* As forall_body_nProp and forall_body_proper_nProp are telescopes *) +(* over negatedProp and properNegatedProp, respectively, their instances *) +(* match instances declared above without the need to expand definitions, *) +(* hence do not need to use the wrapper telescope idiom. *) +(******************************************************************************) + +Structure negatedForallBody bounded P nQ tR nR := NegatedForallBody { + negated_forall_body :> negatedProp tR nR; _ : and_def bounded P nQ nR}. +Structure properNegatedForallBody b P nQ nR := ProperNegatedForallBody { + proper_negated_forall_body :> properNegatedProp nR; _ : and_def b P nQ nR}. +Notation nBody b P nQ t nR x := (negatedForallBody b (P x) (nQ x) t (nR x)). + +(******************************************************************************) +(* The explicit argument to fun_if is a workaround for a bug in the Coq *) +(* unification code that prevents default instances from ever matching match *) +(* constructs. Furthermore rewriting with ifE would not work here, because *) +(* the if_expr definition would be expanded by the eta expansion needed to *) +(* match the exists_nProp rule. *) +(******************************************************************************) + +Fact forall_nPropP A b P nQ tR nR (R : forall x, nBody b P nQ tR nR x) : + (~ forall x : A, R x) = if b then exists2 x, P x & nQ x else exists x, nQ x. +Proof. +rewrite exists2E -(fun_if (fun P => exists x, idfun P x)) notI /=; congr not. +apply/generic_forall_extensionality=> x; rewrite if_arg lax_notI. +by case: (R x) => _ <-. +Qed. +Canonical forall_nProp A b P nQ tR nR (R : forall x, nBody b P nQ tR nR x) := + @NegatedProp false _ (wrap2Prop (forall x : A, R x)) (forall_nPropP R). + +Fact proper_nBodyP b P nQ nR : + properNegatedForallBody b P nQ nR -> and_def b P nQ nR. +Proof. by case. Qed. +Canonical proper_nBody b P nQ nR R := + let def_nR := @proper_nBodyP b P nQ nR R in + @NegatedForallBody b P nQ false nR (proper_nProp R) def_nR. +Canonical nonproper_nBody tP nP P := + @NegatedForallBody false True nP tP nP P erefl. + +Fact andRHS_def b P Q PQ : andRHS b P Q PQ -> and_def b P Q PQ. +Proof. by case. Qed. +Canonical bounded_nBody b P nQ PnQ tR nR R := + ProperNegatedForallBody (@imply_nProp b P nQ PnQ tR nR R) (andRHS_def nR). +Canonical unbounded_nBody nQ Q := + @ProperNegatedForallBody false True nQ nQ Q erefl. + +(******************************************************************************) +(* The properNegatedProp instance that handles boolean statements. We use *) +(* two tertiary structures to handle positive and negative boolean statements *) +(* so that the contra tactic below will mostly subsume the collection of *) +(* contraXX lemmas in ssrbool and eqtype. *) +(* We only match manifest ~~ connectives, the true and false constants, *) +(* and the ==, <=%N, and <%N predicates. In particular we do not use de *) +(* Morgan laws to push boolean negation into connectives, as we did above for *) +(* Prop connectives. It will be up to the user to use rewriting to put the *) +(* negated statement in its desired shape. *) +(******************************************************************************) + +Structure negatedBool nP := + NegatedBool {negated_bool :> bool; _ : (~ negated_bool) = nP}. +Structure positedBool P := + PositedBool {posited_bool :> bool; _ : is_true posited_bool = P}. + +Local Fact is_true_nPropP nP (b : negatedBool nP) : (~ b) = nP. +Proof. by case: b. Qed. +Canonical is_true_nProp nP b := ProperNegatedProp (@is_true_nPropP nP b). + +Local Fact true_negP : (~ true) = False. Proof. by eqProp. Qed. +Local Fact true_posP : (true : Prop) = True. Proof. by eqProp. Qed. +Local Fact false_negP : (~ false) = True. Proof. by eqProp. Qed. +Local Fact false_posP : (false : Prop) = False. Proof. by eqProp. Qed. +Canonical true_neg := NegatedBool true_negP. +Canonical true_pos := PositedBool true_posP. +Canonical false_neg := NegatedBool false_negP. +Canonical false_pos := PositedBool false_posP. + +Local Fact id_negP (b : bool) : (~ b) = ~~ b. Proof. exact/reflect_eq/negP. Qed. +Canonical id_neg b := NegatedBool (id_negP b). +Canonical id_pos (b : bool) := @PositedBool b b erefl. + +Local Fact negb_negP P (b : positedBool P) : (~ ~~ b) = P. +Proof. by rewrite (reflect_eq negP) negbK; case: b. Qed. +Canonical negb_neg P b := NegatedBool (@negb_negP P b). +Local Fact negb_posP nP (b : negatedBool nP) : (~~ b = nP :> Prop). +Proof. by rewrite -(reflect_eq negP) notE. Qed. +Canonical negb_pos nP b := PositedBool (@negb_posP nP b). + +(******************************************************************************) +(* We use a tertiary structure to handle the negation of nat comparisons, and *) +(* simplify ~ m <= n to n < m, and ~ m < n to n <= m. As m < n is merely *) +(* notation for m.+1 <= n, we need to dispatch on the left hand side of the *) +(* comparison to perform the latter simplification. *) +(******************************************************************************) + +Structure negatedLeqLHS n lt_nm := + NegatedLeqLHS {negated_leq_LHS :> nat; _ : (n < negated_leq_LHS) = lt_nm}. +Canonical neg_ltn_LHS n m := @NegatedLeqLHS n (n <= m) m.+1 erefl. +Canonical neg_leq_LHS n m := @NegatedLeqLHS n (n < m) m erefl. + +Local Fact leq_negP n lt_nm (m : negatedLeqLHS n lt_nm) : (~ m <= n) = lt_nm. +Proof. by rewrite notE -ltnNge; case: m => /= m ->. Qed. +Canonical leq_neg n lt_nm m := NegatedBool (@leq_negP n lt_nm m). + +(******************************************************************************) +(* We use two tertiary structures to simplify negation of boolean constant *) +(* and decidable equalities, simplifying b <> true to ~~ b, b <> false to b, *) +(* x <> y to x != y, and ~ x != y to x = y. We do need to use the wrapper *) +(* telescope pattern here, as we want to simplify instances of x <> y when y *) +(* evaluates to true or false. Since we only need two rules (true/false RHS *) +(* or generic eqType RHS) we can use the generic wrapped type from ssrfun. *) +(* The actual matching of the true and false RHS is delegated to a fourth *) +(* level bool_eq_negation_rhs structure. Finally observe that the ~ x != y to *) +(* x = y simplification can be handled by a bool_affirmation instance. *) +(******************************************************************************) + +Structure neqRHS nP T x := + NeqRHS {neq_RHS :> wrapped T; _ : (x <> unwrap neq_RHS) = nP}. +Structure boolNeqRHS nP (x : bool) := + BoolNeqRHS {bool_neq_RHS; _ : (x <> bool_neq_RHS) = nP}. + +Local Fact eq_nPropP nP T x (y : neqRHS nP x) : (x <> unwrap y :> T) = nP. +Proof. by case: y. Qed. +Canonical eq_nProp nP T x y := ProperNegatedProp (@eq_nPropP nP T x y). + +Local Fact bool_neqP nP x y : (x <> @bool_neq_RHS nP x y) = nP. +Proof. by case: y. Qed. +Canonical bool_neq nP x y := @NeqRHS nP bool x (wrap _) (@bool_neqP nP x y). +Canonical true_neq nP b := BoolNeqRHS (@is_true_nPropP nP b). +Local Fact false_neqP P (b : positedBool P) : (b <> false :> bool) = P. +Proof. + admit. +Admitted. +Canonical false_neq P b := BoolNeqRHS (@false_neqP P b). + +Local Fact eqType_neqP (T : eqType) (x y : T) : (x <> y) = (x != y). +Proof. by rewrite (reflect_eq eqP) (reflect_eq negP). Qed. +Canonical eqType_neq (T : eqType) x y := + @NeqRHS (x != y) T x (Wrap y) (eqType_neqP x y). +Local Fact eq_op_posP (T : eqType) x y : (x == y :> T : Prop) = (x = y). +Proof. exact/esym/reflect_eq/eqP. Qed. +Canonical eq_op_pos T x y := PositedBool (@eq_op_posP T x y). + +(******************************************************************************) +(* The witnessedType structure provides conversion between Type and Prop in *) +(* goals; the conversion is mostly used in the Type-to-Prop direction, e.g., *) +(* as a preprocessing step preceding proof by contradiction (see absurd_not *) +(* below), but the Prop-to-Type direction is required for contraposition. *) +(* Thus witnessedType associates to a type T a "witness" proposition P *) +(* equivalent to the existence of an x of type T. As in a `{classical_logic} *) +(* context inhabited T is such a proposition, witnessedType can be understood *) +(* as providing simplification for inhabited T, much like negatedProp *) +(* provides simplification for ~ P for standard connectives and predicates. *) +(******************************************************************************) + +(******************************************************************************) +(* Similarly to negatedProp, witnessedType returns the witness proposition *) +(* via a projection argument P, but does not need to signal "trivial" *) +(* instances as the default value for P is nontrivial (namely, inhabited T), *) +(* while the "trivial" case where P = T is actually desireable and handled *) +(* by an extra top-priority rule. *) +(******************************************************************************) + +Structure witnessedType P := WitnessedType { + witnessed_Type :> wrappedType; _ : inhabited witnessed_Type = P}. +Structure properWitnessedType P := ProperWitnessedType { + proper_witnessed_Type :> Type; _ : inhabited proper_witnessed_Type = P}. +Local Notation wType P T := (unwrap_Type (@witnessed_Type P T)). +Local Notation wTycon P T x := (wType (P x) (T x)). + +(* User interface lemmas. *) + +Lemma witnessedType_intro {P : Prop} T : P -> wType P T. +Proof. by case: T => /= T <- /inhabited_witness. Qed. +Local Coercion witnessedType_intro : witnessedType >-> Funclass. + +Lemma witnessedType_elim {P} T : wType P T -> P. +Proof. by case: T => /= T <-. Qed. +Local Notation wTypeP := witnessedType_elim. + +(* Helper lemma and tactic. *) + +Local Fact eq_inhabited T (P : Prop) : (T -> P) -> (P -> T) -> inhabited T = P. +Proof. by move=> T_P P_T; eqProp=> [[/T_P] | /P_T]. Qed. +Ltac eqInh := apply: eq_inhabited. + +(* Rule 1: Prop goals are left as is. *) +Canonical Prop_wType P := + @WitnessedType P (wrap1Type P) (eq_inhabited (@id P) id). + +(* Rule 2: Specific type constructors (sigs, sums, and pairs) are delegated *) +(* to the secondary properWitnessedType structure. *) +Lemma proper_wTypeP P (T : properWitnessedType P) : inhabited T = P. +Proof. by case: T. Qed. +Canonical proper_wType P T := + @WitnessedType P (wrap2Type _) (@proper_wTypeP P T). + +(* Rule 3: Forall (and -> as a special case). *) +Local Fact forall_wTypeP A P T : + inhabited (forall x : A, wTycon P T x) = (forall x : A, P x) . +Proof. by do [eqInh=> allP x; have:= allP x] => [/wTypeP | /T]. Qed. +Canonical forall_wType A P T := + @WitnessedType _ (wrap3Type _) (@forall_wTypeP A P T). + +(* Rule 4: Default to inhabited if all else fails. *) +Canonical inhabited_wType T := @WitnessedType (inhabited T) (wrap4Type T) erefl. + +(* Specific proper_witnessedType instances. *) + +Local Fact void_wTypeP : inhabited void = False. Proof. by eqInh. Qed. +Canonical void_wType := ProperWitnessedType void_wTypeP. + +Local Fact unit_wTypeP : inhabited unit = True. Proof. by eqInh. Qed. +Canonical unit_wType := ProperWitnessedType unit_wTypeP. + +Local Fact pair_wTypeP P Q S T : inhabited (wType P S * wType Q T) = (P /\ Q). +Proof. by eqInh=> [[/wTypeP-isP /wTypeP] | [/S-x /T]]. Qed. +Canonical pair_wType P Q S T := ProperWitnessedType (@pair_wTypeP P Q S T). + +Local Fact sum_wTypeP P Q S T : inhabited (wType P S + wType Q T) = (P \/ Q). +Proof. by eqInh=> [[] /wTypeP | /decide_or[/S | /T]]; by [left | right]. Qed. +Canonical sum_wType P Q S T := ProperWitnessedType (@sum_wTypeP P Q S T). + +Local Fact sumbool_wTypeP P Q : inhabited ({P} + {Q}) = (P \/ Q). +Proof. by eqInh=> [[] | /decide_or[]]; by [left | right]. Qed. +Canonical sumbool_wType P Q := ProperWitnessedType (@sumbool_wTypeP P Q). + +Local Fact sumor_wTypeP P Q T : inhabited (wType P T + {Q}) = (P \/ Q). +Proof. by eqInh=> [[/wTypeP|] | /decide_or[/T|]]; by [left | right]. Qed. +Canonical sumor_wType P Q T := ProperWitnessedType (@sumor_wTypeP P Q T). + +Local Fact sig1_wTypeP T P : inhabited {x : T | P x} = (exists x : T, P x). +Proof. by eqInh=> [[x Px] | /cid//]; exists x. Qed. +Canonical sig1_wType T P := ProperWitnessedType (@sig1_wTypeP T P). + +Local Fact sig2_wTypeP T P Q : + inhabited {x : T | P x & Q x} = exists2 x : T, P x & Q x. +Proof. by eqInh=> [[x Px Qx] | /cid2//]; exists x. Qed. +Canonical sig2_wType T P Q := ProperWitnessedType (@sig2_wTypeP T P Q). + +Local Fact sigT_wTypeP A P T : + inhabited {x : A & wTycon P T x} = (exists x : A, P x). +Proof. by eqInh=> [[x /wTypeP] | /cid[x /T]]; exists x. Qed. +Canonical sigT_wType A P T := ProperWitnessedType (@sigT_wTypeP A P T). + +Local Fact sigT2_wTypeP A P Q S T : + inhabited {x : A & wTycon P S x & wTycon Q T x} = (exists2 x : A, P x & Q x). +Proof. by eqInh=> [[x /wTypeP-Px /wTypeP] | /cid2[x /S-y /T]]; exists x. Qed. +Canonical sigT2_wType A P Q S T := + ProperWitnessedType (@sigT2_wTypeP A P Q S T). + +(******************************************************************************) +(* The witnessProp structure provides for conversion of some Prop *) +(* assumptions to Type values with some constructive contents, e.g., convert *) +(* a P \/ Q assumption to a {P} + {Q} sumbool value. This is not the same as *) +(* the forward direction of witnessedType, because instances here match the *) +(* Prop statement: witness_Prop find a T such that P -> T while witnessedType *) +(* finds a P such that P -> T (and T -> P for the converse direction). *) +(******************************************************************************) + +(******************************************************************************) +(* The implementation follows the wrapper telescope pattern similarly to *) +(* negatedProp, with three rules, one for Prop constructors with proper *) +(* constructive contents, one for forall propositions (also with proper *) +(* constructive contents) and one default rule that just returns P : Prop as *) +(* is (thus, with no other contents except the provability of P). *) +(* The witnessProp structure also uses projection parameters to return the *) +(* inferred Type T together with a bool 'trivial' flag that is set when the *) +(* trivial rule is used. Here, however, this flag is used in both directions: *) +(* the 'witness' view forces it to false to prevent trivial instances, but *) +(* the flag is also used to fine tune the choice of T, selecting between *) +(* sum, sumor, and sumbool, between sig and sigT, and sig2 and sigT2. This *) +(* relies on the fact that the tactic engine will eagerly iota reduce the *) +(* returned type, so that the user will never see the conditionals specified *) +(* in the proper_witness_Prop instances. *) +(* However, it would not be possible to construct the specialised types *) +(* for trivial witnesses (e.g., {P} + {Q}) using the types returned by *) +(* witnessProp instances, since thes are in Type, and the information that *) +(* they are actully in Prop has been lost. This is solved by returning an *) +(* additional Prop P0 that is a copy of the matched Prop P when *) +(* trivial = true. (We put P0 = True when trivial = false, as we only need to *) +(* ensure P -> P0.) *) +(* Caveat: although P0 should in principle be the last parameter of *) +(* witness_Prop, and we use this order for the wProp and wPred projector *) +(* local notation, it is important to put P0 BEFORE T, to circumvent an *) +(* incompleteness in Coq's implementation of higher-order pattern unification *) +(* that would cause the trivial rule to fail for the body of an exists. *) +(* In such a case the rule needs to unify (1) ?P0 x ~ ?P and (2) ?T x ~ ?P *) +(* for some type A some x : A in the context of ?P, but not ?P0 nor ?T. This *) +(* succeeds easily if (1) is performed before (2), setting ?P := ?P0 x and *) +(* ?T := ?P0, but if (2) is attempted first Coq tries to perform ?P := ?T x, *) +(* which fails Type/Prop universe constraints, and then fails outright, *) +(* instead of using pattern unification to solve (2) as ?P := ?Q x, ?T := ?Q *) +(* for a fresh ?Q : A -> Prop. *) +(******************************************************************************) + +Structure witnessProp (trivial : bool) (P0 : Prop) (T : Type) := + WitnessProp {witness_Prop :> wrappedProp; _ : witness_Prop -> T * P0}. +Structure properWitnessProp T := + ProperWitnessProp {proper_witness_Prop :> Prop; _ : proper_witness_Prop -> T}. + +Local Notation wProp t T P0 P := (unwrap_Prop (@witness_Prop t P0 T P)). +Local Notation wPred t T P0 P x := (wProp t (T x) (P0 x) (P x)). + +Local Fact wPropP t T P0 P : wProp t T P0 P -> T * P0. Proof. by case: P. Qed. +Lemma lax_witness {t T P0 P} : move_view (wProp t T P0 P) T. +Proof. by split=> /wPropP[]. Qed. +Definition witness {T P0 P} := @lax_witness false T P0 P. + +(* Rule 1: proper instances (except forall), delegated to an auxiliary *) +(* structures. *) +Local Fact proper_wPropP T P : wrap1Prop (@proper_witness_Prop T P) -> T * True. +Proof. by case: P => _ P_T {}/P_T. Qed. +Canonical proper_wProp T P := WitnessProp false (@proper_wPropP T P). + +(* Rule 2: forall types (including implication); as only proper instances are *) +(* allowed, we set trivial = false for the recursive body instance. *) +Local Fact forall_wPropP A T P0 P : + wrap2Prop (forall x : A, wPred false T P0 P x) -> (forall x, T x) * True. +Proof. by move=> P_A; split=> // x; have /witness := P_A x. Qed. +Canonical forall_wProp A T P0 P := WitnessProp false (@forall_wPropP A T P0 P). + +(* Rule 3: trivial (proof) self-witness. *) +Canonical trivial_wProp P := + WitnessProp true (fun p : wrap3Prop P => (p, p) : P * P). + +(* Specific proper_witnesss_Prop instances. *) + +Canonical inhabited_wProp T := ProperWitnessProp (@inhabited_witness T). + +(******************************************************************************) +(* Conjunctions P /\ Q are a little delicate to handle, as we should not *) +(* produce a proper instance (and thus fail) if neither P nor Q is proper. *) +(* We use a tertiary structure for this : nand_bool b, which has instances *) +(* only for booleans b0 such that ~~ (b0 && b). We allow the witness_Prop *) +(* instance for P to return an arbitrary 'trivial' flag s, but then force the *) +(* 'trivial' flag for Q to be an instance of nand_bool s. *) +(******************************************************************************) + +Structure nandBool b := NandBool {nand_bool :> bool; _ : ~~ (nand_bool && b)}. +Canonical nand_false_bool b := @NandBool b false isT. +Canonical nand_true_bool := @NandBool false true isT. + +Local Fact and_wPropP s S P0 P (t : nandBool s) T Q0 Q : + wProp s S P0 P /\ wProp t T Q0 Q -> S * T. +Proof. by case=> /lax_witness-x /lax_witness. Qed. +Canonical and_wProp s S P0 P t T Q0 Q := + ProperWitnessProp (@and_wPropP s S P0 P t T Q0 Q). + +(* The first : Type cast ensures the return type of the inner 'if' is not *) +(* incorrectly set to 'Set', while the second merely ensures the S + T *) +(* notation is resolved correctly). *) +Local Fact or_wPropP s S P0 P t T Q0 Q : + wProp s S P0 P \/ wProp t T Q0 Q -> + if t then if s then {P0} + {Q0} : Type else S + {Q0} else S + T : Type. +Proof. +by case: s t => -[] in P Q *; (case/decide_or=> /wPropP[]; [left | right]). +Qed. +Canonical or_wProp s S P0 P t T Q0 Q := + ProperWitnessProp (@or_wPropP s S P0 P t T Q0 Q). + +Local Fact exists_wPropP A t T P0 P : + (exists x : A, wPred t T P0 P x) -> if t then {x | P0 x} else {x & T x}. +Proof. by case/cid => x /wPropP[]; case t; exists x. Qed. +Canonical exists_wProp A t T P0 P := + ProperWitnessProp (@exists_wPropP A t T P0 P). + +(* Note the expanded expression for st = s && t, which will be reduced to *) +(* true or false by iota reduction when s and t are known. *) +Local Fact exists2_wPropP A s S P0 P t T Q0 Q (st := if s then t else false) : + (exists2 x : A, wPred s S P0 P x & wPred t T Q0 Q x) -> + if st then {x | P0 x & Q0 x} else {x : A & S x & T x}. +Proof. by case/cid2=> x /wPropP[P0x y] /wPropP[]; case: ifP; exists x. Qed. +Canonical exists2_wProp A s S P0 P t T Q0 Q := + ProperWitnessProp (@exists2_wPropP A s S P0 P t T Q0 Q). + +(******************************************************************************) +(* User lemmas and tactics for proof by contradiction and contraposition. *) +(******************************************************************************) + +(******************************************************************************) +(* Helper lemmas: *) +(* push_goal_copy makes a copy of the goal that can then be matched with *) +(* witnessedType and negatedProp instances to generate a contradiction *) +(* assuption, without disturbing the original form of the goal. *) +(* assume_not_with turns the copy generated by push_identity into an *) +(* equivalent negative assumption, which can then be simplified using the *) +(* lax_notP and lax_witness views. *) +(* absurd and absurdW replace the goal with False; absurdW does this under *) +(* an assumption, and is used to weaken proof-by-assuming-negation to *) +(* proof-by-contradiction. *) +(* contra_Type converts an arbitrary function goal (with assumption and *) +(* conclusion in Type) to an equivalent contrapositive Prop implication. *) +(* contra_notP simplifies a contrapositive ~ Q -> ~ P goal using *) +(* negatedProp instances. *) +(******************************************************************************) + +Local Fact push_goal_copy {T} : ((T -> T) -> T) -> T. Proof. exact. Qed. +Local Fact assume_not_with {R P T} : (~ P -> R) -> (wType P T -> R) -> R. +Proof. by move=> nP_T T_R; have [/T|] := asboolP P. Qed. + +Local Fact absurdW {S T} : (S -> False) -> S -> T. Proof. by []. Qed. + +Local Fact contra_Type {P Q S T} : (~ Q -> ~ P) -> wType P S -> wType Q T. +Proof. by rewrite implyNN => P_Q /wTypeP/P_Q/T. Qed. + +Local Fact contra_notP tP tQ (nP nQ : Prop) P Q : + (nP -> nQ) -> (~ nProp tP nP P -> ~ nProp tQ nQ Q). +Proof. by rewrite 2!lax_notE. Qed. + +End Internals. +Import Internals. +Canonical TypeForall. +Canonical PropForall. +Canonical SetForall. +Canonical wrap1Prop. +Canonical wrap1Type. +Canonical proper_nProp. +Canonical trivial_nProp. +Canonical True_nProp. +Canonical False_nProp. +Canonical not_nProp. +Canonical and_nProp. +Canonical and3_nProp. +Canonical and4_nProp. +Canonical and5_nProp. +Canonical or_nProp. +Canonical or3_nProp. +Canonical or4_nProp. +Canonical unary_and_rhs. +Canonical binary_and_rhs. +Canonical imply_nProp. +Canonical exists_nProp. +Canonical exists2_nProp. +Canonical inhabited_nProp. +Canonical forall_nProp. +Canonical proper_nBody. +Canonical nonproper_nBody. +Canonical bounded_nBody. +Canonical unbounded_nBody. +Canonical is_true_nProp. +Canonical true_neg. +Canonical true_pos. +Canonical false_neg. +Canonical false_pos. +Canonical id_neg. +Canonical id_pos. +Canonical negb_neg. +Canonical negb_pos. +Canonical neg_ltn_LHS. +Canonical neg_leq_LHS. +Canonical leq_neg. +Canonical eq_nProp. +Canonical bool_neq. +Canonical true_neq. +Canonical false_neq. +Canonical eqType_neq. +Canonical eq_op_pos. +Canonical Prop_wType. +Canonical proper_wType. +Canonical forall_wType. +Canonical inhabited_wType. +Canonical void_wType. +Canonical unit_wType. +Canonical pair_wType. +Canonical sum_wType. +Canonical sumbool_wType. +Canonical sumor_wType. +Canonical sig1_wType. +Canonical sig2_wType. +Canonical sigT_wType. +Canonical sigT2_wType. +Canonical proper_wProp. +Canonical forall_wProp. +Canonical trivial_wProp. +Canonical inhabited_wProp. +Canonical nand_false_bool. +Canonical nand_true_bool. +Canonical and_wProp. +Canonical or_wProp. +Canonical exists_wProp. +Canonical exists2_wProp. + +(******************************************************************************) +(* Lemma and tactic assume_not: add a goal negation assumption. The tactic *) +(* also works for goals in Type, simplifies the added assumption, and *) +(* exposes its top-level constructive content. *) +(******************************************************************************) + +Lemma assume_not {P} : (~ P -> P) -> P. Proof. by rewrite implyNp orB. Qed. +Ltac assume_not := + apply: Internals.push_goal_copy; apply: Internals.assume_not_with + => /Internals.lax_notP-/Internals.lax_witness. + +(******************************************************************************) +(* Lemma and tactic absurd_not: proof by contradiction. Same as assume_not, *) +(* but the goal is erased and replaced by False. *) +(* Caveat: absurd_not cannot be used as a move/ view because its conclusion *) +(* is indeterminate. The more general notP defined above can be used instead. *) +(******************************************************************************) +Lemma absurd_not {P} : (~ P -> False) -> P. Proof. by move/Internals.notP. Qed. +Ltac absurd_not := assume_not; apply: Internals.absurdW. + +(******************************************************************************) +(* Tactic contra: proof by contraposition. Assume the negation of the goal *) +(* conclusion, and prove the negation of a given assumption. The defective *) +(* form contra (which can also be written contrapose) expects the assumption *) +(* to be pushed on the goal which thus has the form assumption -> conclusion. *) +(* As with assume_not, contra allows both assumption and conclusion to be *) +(* in Type, simplifies the negation of both assumption and conclusion, and *) +(* exposes the constructive contents of the negated conclusion. *) +(* The contra tactic also supports a limited form of the ':' discharge *) +(* pseudo tactical, whereby contra: means move: ; contra. *) +(* The only allowed are one term, possibly preceded by a clear *) +(* switch. *) +(******************************************************************************) + +Ltac contrapose := + apply: Internals.contra_Type; + apply: Internals.contra_notP => /Internals.lax_witness. +Tactic Notation "contra" := contrapose. +Tactic Notation "contra" ":" constr(H) := move: (H); contra. +Tactic Notation "contra" ":" ident(H) := move: H; contra. +Tactic Notation "contra" ":" "{" hyp_list(Hs) "}" constr(H) := + contra: (H); clear Hs. +Tactic Notation "contra" ":" "{" hyp_list(Hs) "}" ident(H) := + contra: H; clear Hs. +Tactic Notation "contra" ":" "{" "-" "}" constr(H) := contra: (H). + +(******************************************************************************) +(* Lemma and tactic absurd: proof by contradiction. The defective form of the *) +(* lemma simply replaces the entire goal with False (just as the Ltac *) +(* exfalso), leaving the user to derive a contradiction from the assumptions. *) +(* The ':' form absurd: replaces the goal with the negation of the *) +(* (single) (as with contra:, a clear switch is also allowed. *) +(* Finally the Ltac absurd term form is also supported. *) +(******************************************************************************) + +Lemma absurd T : False -> T. Proof. by []. Qed. +Tactic Notation (at level 0) "absurd" := apply absurd. +Tactic Notation (at level 0) "absurd" constr(P) := have []: ~ P. +Tactic Notation "absurd" ":" constr(H) := absurd; contra: (H) => _. +Tactic Notation "absurd" ":" ident(H) := absurd; contra: H => _. +Tactic Notation "absurd" ":" "{" hyp_list(Hs) "}" constr(H) := + absurd: (H) => _; clear Hs. +Tactic Notation "absurd" ":" "{" hyp_list(Hs) "}" ident(H) := + absurd: H => _; clear Hs. diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 59c5481c80..7e4e7091bc 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -934,3 +934,54 @@ Qed. Definition monotonous d (T : porderType d) (pT : predType T) (A : pT) (f : T -> T) := {in A &, {mono f : x y / (x <= y)%O}} \/ {in A &, {mono f : x y /~ (x <= y)%O}}. + +(* NB: these lemmas have been introduced to develop the theory of bounded variation *) +Section path_lt. +Context d {T : orderType d}. +Implicit Types (a b c : T) (s : seq T). + +Lemma last_filterP a (P : pred T) s : + P a -> P (last a [seq x <- s | P x]). +Proof. +by elim: s a => //= t1 t2 ih a Pa; case: ifPn => //= Pt1; exact: ih. +Qed. + +Lemma path_lt_filter0 a s : path <%O a s -> [seq x <- s | (x < a)%O] = [::]. +Proof. +move=> /lt_path_min/allP sa; rewrite -(filter_pred0 s). +apply: eq_in_filter => x xs. +by apply/negbTE; have := sa _ xs; rewrite ltNge; apply: contra => /ltW. +Qed. + +Lemma path_lt_filterT a s : path <%O a s -> [seq x <- s | (a < x)%O] = s. +Proof. +move=> /lt_path_min/allP sa; rewrite -[RHS](filter_predT s). +by apply: eq_in_filter => x xs; exact: sa. +Qed. + +Lemma path_lt_head a b s : (a < b)%O -> path <%O b s -> path <%O a s. +Proof. +by elim: s b => // h t ih b /= ab /andP[bh ->]; rewrite andbT (lt_trans ab). +Qed. + +(* TODO: this lemma feels a bit too technical, generalize? *) +Lemma path_lt_last_filter a b c s : + (a < c)%O -> (c < b)%O -> path <%O a s -> last a s = b -> + last c [seq x <- s | (c < x)%O] = b. +Proof. +elim/last_ind : s a b c => /= [|h t ih a b c ac cb]. + move=> a b c ac cb _ ab. + by apply/eqP; rewrite eq_le (ltW cb) -ab (ltW ac). +rewrite rcons_path => /andP[ah ht]; rewrite last_rcons => tb. +by rewrite filter_rcons tb cb last_rcons. +Qed. + +Lemma path_lt_le_last a s : path <%O a s -> (a <= last a s)%O. +Proof. +elim: s a => // a [_ c /andP[/ltW//]|b t ih i/= /and3P[ia ab bt]] /=. +have /= := ih a; rewrite ab bt => /(_ erefl). +by apply: le_trans; exact/ltW. +Qed. + +End path_lt. +Arguments last_filterP {d T a} P s. diff --git a/theories/derive.v b/theories/derive.v index 6edda28fab..e26f431037 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -682,7 +682,7 @@ Qed. Lemma linear_lipschitz (V' W' : normedModType R) (f : {linear V' -> W'}) : continuous f -> exists2 k, k > 0 & forall x, `|f x| <= k * `|x|. Proof. -move=> /(_ 0); rewrite /continuous_at linear0 => /(_ _ (nbhsx_ballx 0 1%:pos)). +move=> /(_ 0); rewrite /continuous_at linear0 => /(_ _ (nbhsx_ballx _ _ ltr01)). move=> /nbhs_ballP [_ /posnumP[e] he]; exists (2 / e%:num) => // x. have [|xn0] := real_le0P (normr_real x). by rewrite normr_le0 => /eqP->; rewrite linear0 !normr0 mulr0. @@ -751,7 +751,7 @@ Lemma bilinear_schwarz (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) : continuous (fun p => f p.1 p.2) -> exists2 k, k > 0 & forall u v, `|f u v| <= k * `|u| * `|v|. Proof. -move=> /(_ 0); rewrite /continuous_at linear0r => /(_ _ (nbhsx_ballx 0 1%:pos)). +move=> /(_ 0); rewrite /continuous_at linear0r => /(_ _ (nbhsx_ballx _ _ ltr01)). move=> /nbhs_ballP [_ /posnumP[e] he]; exists ((2 / e%:num) ^+2) => // u v. have [|un0] := real_le0P (normr_real u). by rewrite normr_le0 => /eqP->; rewrite linear0l !normr0 mulr0 mul0r. diff --git a/theories/ereal.v b/theories/ereal.v index 896c4fc7e3..1201c4ea38 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -511,6 +511,11 @@ case: xgetP => /=; first by move=> _ -> -[] /ubP geS _; apply geS. by case: (ereal_supremums_neq0 S) => /= x0 Sx0; move/(_ x0). Qed. +Lemma ereal_supy S : S +oo -> ereal_sup S = +oo. +Proof. +by move=> Soo; apply/eqP; rewrite eq_le leey/=; exact: ereal_sup_ub. +Qed. + Lemma ereal_sup_le S x : (exists2 y, S y & x <= y) -> x <= ereal_sup S. Proof. by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ub. Qed. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index a29b5398fa..a670be30e6 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1951,7 +1951,7 @@ have finDn n : mu (Dn n) \is a fin_num. by rewrite le_measure// ?inE//=; [exact: mDn|exact: subIsetl]. have finD : mu D \is a fin_num by rewrite fin_num_abs gee0_abs. rewrite -[mu D]fineK// => /fine_cvg/(_ (interior (ball (fine (mu D)) eps)))[]. - exact/nbhs_interior/(nbhsx_ballx _ (PosNum epspos)). + exact/nbhs_interior/nbhsx_ballx. move=> n _ /(_ _ (leqnn n))/interior_subset muDN. exists (-n%:R, n%:R)%R; rewrite measureD//=. move: muDN; rewrite /ball/= /ereal_ball/= -fineB//=; last exact: finDn. @@ -2090,9 +2090,7 @@ have mE k n : measurable (E k n). have nEcvg x k : exists n, A x -> (~` (E k n)) x. case : (pselect (A x)); last by move => ?; exists point. move=> Ax; have [] := fptwsg _ Ax (interior (ball (g x) (k.+1%:R^-1))). - apply: open_nbhs_nbhs; split; first exact: open_interior. - have ki0 : ((0:R) < k.+1%:R^-1)%R by rewrite invr_gt0. - rewrite (_ : k.+1%:R^-1 = (PosNum ki0)%:num ) //; exact: nbhsx_ballx. + by apply: open_nbhs_nbhs; split; [exact: open_interior|exact: nbhsx_ballx]. move=> N _ Nk; exists N.+1 => _; rewrite /E setC_bigcup => i /= /ltnW Ni. apply/not_andP; right; apply/negP; rewrite /h -real_ltNge // distrC. by case: (Nk _ Ni) => _/posnumP[?]; apply; exact: ball_norm_center. @@ -2110,8 +2108,7 @@ have badn' : forall k, exists n, mu (E k n) < ((eps/2) / (2 ^ k.+1)%:R)%:E. - by apply: bigcap_measurable => ?. rewrite measure0; case/fine_cvg/(_ (interior (ball (0:R) ek))%R). apply: open_nbhs_nbhs; split; first exact: open_interior. - have ekpos : (0 < ek)%R by rewrite divr_gt0 // divr_gt0. - by move: ek ekpos => _/posnumP[ek]; exact: nbhsx_ballx. + by apply: nbhsx_ballx; rewrite !divr_gt0. move=> N _ /(_ N (leqnn _))/interior_subset muEN; exists N; move: muEN. rewrite /ball /= distrC subr0 ger0_norm // -[x in x < _]fineK ?ge0_fin_numE//. by apply:(le_lt_trans _ finA); apply: le_measure; rewrite ?inE// => ? [? _ []]. diff --git a/theories/normedtype.v b/theories/normedtype.v index 66c9dac3e0..01ea11f428 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -1033,7 +1033,7 @@ Lemma dnbhs0_le e : 0 < e -> \forall x \near (0 : V)^', `|x| <= e. Proof. by move=> e_gt0; apply: cvg_within; apply: nbhs0_le. Qed. Lemma nbhs_norm_ball x (eps : {posnum R}) : nbhs_norm x (ball x eps%:num). -Proof. rewrite nbhs_nbhs_norm; by apply: nbhsx_ballx. Qed. +Proof. by rewrite nbhs_nbhs_norm; exact: nbhsx_ballx. Qed. Lemma nbhsDl (P : set V) (x y : V) : (\forall z \near (x + y), P z) <-> (\near x, P (x + y)). @@ -2075,6 +2075,51 @@ by apply: xe_A => //; rewrite eq_sym. Qed. Arguments cvg_at_leftE {R V} f x. +Lemma continuous_within_itvP {R : realType } a b (f : R -> R) : + a < b -> + {within `[a,b], continuous f} <-> + {in `]a,b[, continuous f} /\ f @ a^'+ --> f a /\ f @b^'- --> f b. +Proof. +move=> ab; split=> [abf|]. + split. + suff : {in `]a, b[%classic, continuous f}. + by move=> P c W; apply: P; rewrite inE. + rewrite -continuous_open_subspace; last exact: interval_open. + by move: abf; exact/continuous_subspaceW/subset_itvW. + have [aab bab] : a \in `[a, b] /\ b \in `[a, b]. + by rewrite !in_itv/= !lexx (ltW ab). + split; apply/cvgrPdist_lt => eps eps_gt0 /=. + + move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf a). + rewrite /dnbhs/= near_withinE !near_simpl// /prop_near1 /nbhs/=. + rewrite -nbhs_subspace_in// /within/= near_simpl. + apply: filter_app; exists (b - a); rewrite /= ?subr_gt0// => c cba + ac. + apply=> //; rewrite ?gt_eqF// !in_itv/= (ltW ac)/=; move: cba => /=. + by rewrite ltr0_norm ?subr_lt0// opprB ltr_add2r => /ltW. + + move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf b). + rewrite /dnbhs/= near_withinE !near_simpl /prop_near1 /nbhs/=. + rewrite -nbhs_subspace_in// /within/= near_simpl. + apply: filter_app; exists (b - a); rewrite /= ?subr_gt0// => c cba + ac. + apply=> //; rewrite ?lt_eqF// !in_itv/= (ltW ac)/= andbT; move: cba => /=. + by rewrite gtr0_norm ?subr_gt0// ltr_add2l ltr_oppr opprK => /ltW. +case=> ctsoo [ctsL ctsR]; apply/subspace_continuousP => x /andP[]. +rewrite !bnd_simp/= !le_eqVlt => /predU1P[<-{x}|ax] /predU1P[|]. +- by move/eqP; rewrite lt_eqF. +- move=> _; apply/cvgrPdist_lt => eps eps_gt0 /=. + move/cvgrPdist_lt/(_ _ eps_gt0): ctsL; rewrite /at_right !near_withinE. + apply: filter_app; exists (b - a); rewrite /= ?subr_gt0// => c cba + ac. + have : a <= c by move: ac => /andP[]. + by rewrite le_eqVlt => /predU1P[->|/[swap] /[apply]//]; rewrite subrr normr0. +- move=> ->; apply/cvgrPdist_lt => eps eps_gt0 /=. + move/cvgrPdist_lt/(_ _ eps_gt0): ctsR; rewrite /at_left !near_withinE. + apply: filter_app; exists (b - a); rewrite /= ?subr_gt0 // => c cba + ac. + have : c <= b by move: ac => /andP[]. + by rewrite le_eqVlt => /predU1P[->|/[swap] /[apply]//]; rewrite subrr normr0. +- move=> xb; have aboox : x \in `]a, b[ by rewrite !in_itv/= ax. + rewrite within_interior; first exact: ctsoo. + suff : `]a, b[ `<=` interior `[a, b] by exact. + by rewrite -open_subsetE; [exact: subset_itvW| exact: interval_open]. +Qed. + (* TODO: generalize to R : numFieldType *) Section hausdorff. @@ -3180,36 +3225,33 @@ move=> [x y]; have [pE U /= Upinf|] := eqVneq (edist (x, y)) +oo%E. rewrite -ltey -ge0_fin_numE// => efin. rewrite /continuous_at -[edist (x, y)]fineK//; apply: cvg_EFin. by have := edist_fin_open efin; apply: filter_app; near=> w. -move=> U /=; rewrite nbhs_simpl/= -nbhs_ballE. -move=> [] _/posnumP[r] distrU; rewrite nbhs_simpl /=. -have r2p : 0 < r%:num / 4%:R by rewrite divr_gt0// ltr0n. -exists (ball x (r%:num / 4%:R), ball y (r%:num / 4%:R)). - by split => //=; exact: (@nbhsx_ballx _ _ _ (@PosNum _ _ r2p)). -case => a b /= [/ball_sym xar yar]; apply: distrU => /=. -have abxy : (edist (a, b) <= edist (a, x) + edist (x, y) + edist (y, b))%E. - by rewrite -addeA (le_trans (@edist_triangle _ x _)) ?lee_add ?edist_triangle. +apply/cvgrPdist_le => _/posnumP[eps]. +suff: \forall t \near (nbhs x, nbhs y), + `|fine (edist (x, y)) - fine (edist t)| <= eps%:num by []. +rewrite -near2_pair; near=> a b => /=. +have abxy : (edist (a, b) <= edist (x, a) + edist (x, y) + edist (y, b))%E. + rewrite (edist_sym x a) -addeA. + by rewrite (le_trans (@edist_triangle _ x _)) ?lee_add ?edist_triangle. +have xyab : (edist (x, y) <= edist (x, a) + edist (a, b) + edist (y, b))%E. + rewrite (edist_sym y b) -addeA. + by rewrite (le_trans (@edist_triangle _ a _))// ?lee_add// ?edist_triangle. +have xafin : edist (x, a) \is a fin_num. + by apply/edist_finP; exists 1 =>//; near: a; exact: nbhsx_ballx. +have ybfin : edist (y, b) \is a fin_num. + by apply/edist_finP; exists 1 =>//; near: b; exact: nbhsx_ballx. have abfin : edist (a, b) \is a fin_num. - rewrite ge0_fin_numE// (le_lt_trans abxy)//. - by apply: lte_add_pinfty; [apply: lte_add_pinfty|]; - rewrite -ge0_fin_numE //; apply/edist_finP; exists (r%:num / 4%:R). -have xyabfin : `|edist (x, y) - edist (a, b)|%E \is a fin_num. - by rewrite abse_fin_num fin_numB abfin efin. -have daxr : edist (a, x) \is a fin_num by apply/edist_finP; exists (r%:num / 4). -have dybr : edist (y, b) \is a fin_num by apply/edist_finP; exists (r%:num / 4). -rewrite /ball/= -fineB// -fine_abse ?fin_numB ?abfin ?efin//. -rewrite (@le_lt_trans _ _ (fine (edist (a, x) + edist (y, b))))//. - rewrite fine_le// ?fin_numD ?daxr ?dybr//. - have [xyab|xyab] := leP (edist (a, b)) (edist (x, y)). - rewrite gee0_abs ?subre_ge0// lee_subl_addr//. - rewrite (le_trans (@edist_triangle _ a _))// (edist_sym a x) -addeA. - by rewrite lee_add// addeC (edist_sym y) edist_triangle. - rewrite lte0_abs ?subre_lt0// oppeB ?fin_num_adde_defr// addeC. - by rewrite lee_subl_addr// addeAC. -rewrite fineD // [_%:num]splitr. -have r42 : r%:num / 4 < r%:num / 2. - by rewrite ltr_pM2l// ltf_pV2 ?posrE ?ltr0n// ltr_nat. -by apply: ltrD; rewrite (le_lt_trans _ r42)// -lee_fin fineK // edist_fin. -Unshelve. end_near. Qed. + by rewrite ge0_fin_numE// (le_lt_trans abxy) ?lte_add_pinfty// -ge0_fin_numE. +have xyabfin: (edist (x, y) - edist (a, b))%E \is a fin_num + by rewrite fin_numB abfin efin. +rewrite -fineB// -fine_abse// -lee_fin fineK ?abse_fin_num//. +rewrite (@le_trans _ _ (edist (x, a) + edist (y, b))%E)//; last first. + by rewrite [eps%:num]splitr/= EFinD lee_add//; apply: edist_fin => //=; + [near: a | near: b]; exact: nbhsx_ballx. +have [ab_le_xy|/ltW xy_le_ab] := leP (edist (a, b)) (edist (x, y)). + by rewrite gee0_abs ?subre_ge0// lee_subl_addr// addeAC. +rewrite lee0_abs ?sube_le0// oppeB ?fin_num_adde_defr//. +by rewrite addeC lee_subl_addr// addeAC. +Unshelve. all: end_near. Qed. Lemma edist_closeP x y : close x y <-> edist (x, y) = 0%E. Proof. @@ -3297,7 +3339,7 @@ have fwfin : \forall w \near z, edist_inf w \is a fin_num. rewrite fin_numD fz_fin andbT; apply/edist_finP; exists 1 => //. exact/ball_sym. split => //; apply/cvgrPdist_le => _/posnumP[eps]. -have : nbhs z (ball z eps%:num) by apply: nbhsx_ballx. +have : nbhs z (ball z eps%:num) by exact: nbhsx_ballx. apply: filter_app; near_simpl; move: fwfin; apply: filter_app. near=> t => tfin /= /[dup] ?. have ztfin : edist (z, t) \is a fin_num by apply/edist_finP; exists eps%:num. @@ -4644,7 +4686,8 @@ move=> x clAx; have abx : x \in `[a, b]. by apply: interval_closed; have /closureI [] := clAx. split=> //; have /sabUf [i Di fx] := abx. have /fop := Di; rewrite openE => /(_ _ fx) [_ /posnumP[e] xe_fi]. -have /clAx [y [[aby [E sD [sayUf _]]] xe_y]] := nbhsx_ballx x e. +have /clAx [y [[aby [E sD [sayUf _]]] xe_y]] := + nbhsx_ballx x e%:num ltac:(by []). exists (i |` E)%fset; first by move=> j /fset1UP[->|/sD] //; rewrite inE. split=> [z axz|]; last first. exists i; first by rewrite /= !inE eq_refl. diff --git a/theories/realfun.v b/theories/realfun.v index 3a1cdfcc31..e4502e512c 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -14,18 +14,31 @@ From HB Require Import structures. (* numbers (e.g., the continuity of the inverse of a continuous function). *) (* *) (* ``` *) -(* nondecreasing_fun f == the function f is non-decreasing *) -(* nonincreasing_fun f == the function f is non-increasing *) -(* increasing_fun f == the function f is (strictly) increasing *) -(* decreasing_fun f == the function f is (strictly) decreasing *) +(* nondecreasing_fun f == the function f is non-decreasing *) +(* nonincreasing_fun f == the function f is non-increasing *) +(* increasing_fun f == the function f is (strictly) increasing *) +(* decreasing_fun f == the function f is (strictly) decreasing *) (* *) (* derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and *) -(* continuous up to the boundary *) +(* continuous up to the boundary *) +(* *) +(* itv_partition a b s == s is a partition of the interval `[a, b] *) +(* itv_partitionL s c == the left side of splitting a partition at c *) +(* itv_partitionR s c == the right side of splitting a partition at c *) +(* variation a b f s == the sum of f at all points in the partition s *) +(* variations a b f == the set of all variations of f between a and b *) +(* bounded_variation a b f == all variations of f are bounded *) +(* total_variation a b f == the sup over all variations of f from a to b *) +(* neg_tv a f x == the decreasing component of f *) +(* pos_tv a f x == the increasing component of f *) +(* *) (* ``` *) (* *) (* * Limit superior and inferior for functions: *) +(* ``` *) (* lime_sup f a/lime_inf f a == limit sup/inferior of the extended real- *) -(* valued function f at point a *) +(* valued function f at point a *) +(* ``` *) (* *) (******************************************************************************) @@ -50,6 +63,23 @@ Notation "'increasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n <= m)%O}) Notation "'decreasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n >= m)%O}) (at level 10). +Lemma nondecreasing_funN {R : realType} a b (f : R -> R) : + {in `[a, b] &, nondecreasing_fun f} <-> + {in `[a, b] &, nonincreasing_fun (\- f)}. +Proof. +split=> [h m n mab nab mn|h m n mab nab mn]; first by rewrite lerNr opprK h. +by rewrite -(opprK (f n)) -lerNr h. +Qed. + +Lemma nonincreasing_funN {R : realType} a b (f : R -> R) : + {in `[a, b] &, nonincreasing_fun f} <-> + {in `[a, b] &, nondecreasing_fun (\- f)}. +Proof. +apply: iff_sym; apply: (iff_trans (nondecreasing_funN a b (\- f))). +rewrite [in X in _ <-> X](_ : f = \- (\- f))//. +by apply/funext => x /=; rewrite opprK. +Qed. + Section fun_cvg. Section fun_cvg_realFieldType. @@ -88,6 +118,18 @@ apply: near_eq_cvg; near do rewrite subrK; exists M. by rewrite num_real. Unshelve. all: by end_near. Qed. +Lemma left_right_continuousP {T : topologicalType} (f : R -> T) x : + f @ x^'- --> f x /\ f @ x^'+ --> f x <-> f @ x --> f x. +Proof. +split; last by move=> cts; split; exact: cvg_within_filter. +move=> [+ +] U /= Uz => /(_ U Uz) + /(_ U Uz); near_simpl. +rewrite !near_withinE => lf rf; apply: filter_app lf; apply: filter_app rf. +near=> t => xlt xgt; have := @real_leVge R x t; rewrite !num_real. +move=> /(_ isT isT) /orP; rewrite !le_eqVlt => -[|] /predU1P[|//]. +- by move=> <-; exact: nbhs_singleton. +- by move=> ->; exact: nbhs_singleton. +Unshelve. all: by end_near. Qed. + Lemma cvg_at_right_left_dnbhs (f : R -> R) (p : R) (l : R) : f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l -> f x @[x --> p^'] --> l. @@ -106,7 +148,6 @@ rewrite neq_lt => /orP[tp|pt]. move=> z/= + _ => /lt_le_trans; apply. by rewrite ler_pdivrMr// ler_pMr// ler1n. Unshelve. all: by end_near. Qed. - End fun_cvg_realFieldType. Section cvgr_fun_cvg_seq. @@ -219,10 +260,10 @@ End cvge_fun_cvg_seq. Section fun_cvg_realType. Context {R : realType}. +Implicit Types f : R -> R. (* NB: see nondecreasing_cvgn in sequences.v *) -Lemma nondecreasing_cvgr (f : R -> R) : - nondecreasing_fun f -> has_ubound (range f) -> +Lemma nondecreasing_cvgr f : nondecreasing_fun f -> has_ubound (range f) -> f r @[r --> +oo] --> sup (range f). Proof. move=> ndf ubf; set M := sup (range f). @@ -236,49 +277,97 @@ rewrite ler_distlC (le_trans Mefp (ndf _ _ _))//= (@le_trans _ _ M) ?lerDl//. by have /ubP := sup_upper_bound supf; apply; exists n. Unshelve. all: by end_near. Qed. -Lemma nonincreasing_at_right_cvgr (f : R -> R) a : - {in `]a, +oo[, nonincreasing_fun f} -> - has_ubound (f @` `]a, +oo[) -> - f x @[x --> a ^'+] --> sup (f @` `]a, +oo[). -Proof. -move=> lef ubf; set M := sup _. -have supf : has_sup [set f x | x in `]a, +oo[]. - split => //; exists (f (a + 1)), (a + 1) => //=. - by rewrite in_itv/= ltrDl ltr01. +(***md This covers the cases where the interval is + $]a, +\infty[$, $]a, b[$, or $]a, b]$. *) +Lemma nonincreasing_at_right_cvgr f a (b : itv_bound R) : (BRight a < b)%O -> + {in Interval (BRight a) b &, nonincreasing_fun f} -> + has_ubound (f @` [set` Interval (BRight a) b]) -> + f x @[x --> a ^'+] --> sup (f @` [set` Interval (BRight a) b]). +Proof. +move=> ab lef ubf; set M := sup _. +have supf : has_sup [set f x | x in [set` Interval (BRight a) b]]. + split => //; case: b ab {lef ubf M} => [[|] t ta|[]] /=. + - exists (f ((a + t) / 2)), ((a + t) / 2) => //=. + by rewrite in_itv/= !midf_lt. + - exists (f ((a + t) / 2)), ((a + t) / 2) => //=. + by rewrite in_itv/= midf_lt// midf_le// ltW. + - by exists (f (a + 1)), (a + 1). + - by exists (f (a + 1)), (a + 1) => //=; rewrite in_itv/= ltrDl andbT. apply/cvgrPdist_le => _/posnumP[e]. -have [p ap Mefp] : exists2 p, a < p & M - e%:num <= f p. - have [_ -[p ap] <- /ltW efp] := sup_adherent (gt0 e) supf. - exists p; last by rewrite efp. - by move: ap; rewrite /= in_itv/= andbT. -near=> n. -rewrite ler_distl; apply/andP; split; last first. - rewrite -lerBlDr (le_trans Mefp)// lef//. - by rewrite in_itv/= andbT; near: n; exact: nbhs_right_gt. - by near: n; exact: nbhs_right_le. -have : f n <= M. - apply: sup_ub => //=; exists n => //; rewrite in_itv/= andbT. - by near: n; apply: nbhs_right_gt. -by apply: le_trans; rewrite lerBlDr lerDl. +have {supf} [p [ap pb]] : + exists p, [/\ a < p, (BLeft p < b)%O & M - e%:num <= f p]. + have [_ -[p apb] <- /ltW efp] := sup_adherent (gt0 e) supf. + move: apb; rewrite /= in_itv/= -[X in _ && X]/(BLeft p < b)%O => /andP[ap pb]. + by exists p; split. +rewrite lerBlDr {}/M. +move: b ab pb lef ubf => [[|] b|[//|]] ab pb lef ubf; set M := sup _ => Mefp. +- near=> r; rewrite ler_distl; apply/andP; split. + + suff: f r <= M by apply: le_trans; rewrite lerBlDr lerDl. + apply: sup_ub => //=; exists r => //; rewrite in_itv/=. + by apply/andP; split; near: r; [exact: nbhs_right_gt|exact: nbhs_right_lt]. + + rewrite (le_trans Mefp)// lerD2r lef//=; last 2 first. + by rewrite in_itv/= ap. + by near: r; exact: nbhs_right_le. + apply/andP; split; near: r; [exact: nbhs_right_gt|exact: nbhs_right_lt]. +- near=> r; rewrite ler_distl; apply/andP; split. + + suff: f r <= M by apply: le_trans; rewrite lerBlDr lerDl. + apply: sup_ub => //=; exists r => //; rewrite in_itv/=. + by apply/andP; split; near: r; [exact: nbhs_right_gt|exact: nbhs_right_le]. + + rewrite (le_trans Mefp)// lerD2r lef//=; last 2 first. + by rewrite in_itv/= ap. + by near: r; exact: nbhs_right_le. + by apply/andP; split; near: r; [exact: nbhs_right_gt|exact: nbhs_right_le]. +- near=> r; rewrite ler_distl; apply/andP; split. + suff: f r <= M by apply: le_trans; rewrite lerBlDr lerDl. + apply: sup_ub => //=; exists r => //; rewrite in_itv/= andbT. + by near: r; apply: nbhs_right_gt. + rewrite (le_trans Mefp)// lerD2r lef//. + - by rewrite in_itv/= andbT; near: r; exact: nbhs_right_gt. + - by rewrite in_itv/= ap. + - by near: r; exact: nbhs_right_le. +Unshelve. all: by end_near. Qed. + +Lemma nonincreasing_at_right_is_cvgr f a : + (\forall x \near a^'+, {in `]a, x[ &, nonincreasing_fun f}) -> + (\forall x \near a^'+, has_ubound (f @` `]a, x[)) -> + cvg (f x @[x --> a ^'+]). +Proof. +move=> nif ubf; apply/cvg_ex; near a^'+ => b. +by eexists; apply: (@nonincreasing_at_right_cvgr _ _ (BLeft b)); + [rewrite bnd_simp|near: b..]. Unshelve. all: by end_near. Qed. -Lemma nondecreasing_at_right_cvgr (f : R -> R) a : - {in `]a, +oo[, nondecreasing_fun f} -> - has_lbound (f @` `]a, +oo[) -> - f x @[x --> a ^'+] --> inf (f @` `]a, +oo[). +Lemma nondecreasing_at_right_cvgr f a (b : itv_bound R) : (BRight a < b)%O -> + {in Interval (BRight a) b &, nondecreasing_fun f} -> + has_lbound (f @` [set` Interval (BRight a) b]) -> + f x @[x --> a ^'+] --> inf (f @` [set` Interval (BRight a) b]). Proof. -move=> nif hlb. -have ndNf : {in `]a, +oo[, nonincreasing_fun (\- f)}. - by move=> r ra y /nif; rewrite lerN2; exact. -have hub : has_ubound [set (\- f) x | x in `]a, +oo[]. +move=> ab nif hlb; set M := inf _. +have ndNf : {in Interval (BRight a) b &, nonincreasing_fun (\- f)}. + by move=> r s rab sab /nif; rewrite lerN2; exact. +have hub : has_ubound [set (\- f) x | x in [set` Interval (BRight a) b]]. apply/has_ub_lbN; rewrite image_comp/=. - rewrite [X in has_lbound X](_ : _ = [set f x | x in `]a, +oo[])//. + rewrite [X in has_lbound X](_ : _ = f @` [set` Interval (BRight a) b])//. by apply: eq_imagel => y _ /=; rewrite opprK. -have /cvgN := nonincreasing_at_right_cvgr ndNf hub. -rewrite opprK [X in _ --> X -> _](_ : _ = inf [set f x | x in `]a, +oo[])//. +have /cvgN := nonincreasing_at_right_cvgr ab ndNf hub. +rewrite opprK [X in _ --> X -> _](_ : _ = + inf (f @` [set` Interval (BRight a) b]))//. by rewrite /inf; congr (- sup _); rewrite image_comp/=; exact: eq_imagel. Qed. +Lemma nondecreasing_at_right_is_cvgr f a : + (\forall x \near a^'+, {in `]a, x[ &, nondecreasing_fun f}) -> + (\forall x \near a^'+, has_lbound (f @` `]a, x[)) -> + cvg (f x @[x --> a ^'+]). +Proof. +move=> ndf lbf; apply/cvg_ex; near a^'+ => b. +by eexists; apply: (@nondecreasing_at_right_cvgr _ _ (BLeft b)); + [rewrite bnd_simp|near: b..]. +Unshelve. all: by end_near. Qed. + End fun_cvg_realType. +Arguments nondecreasing_at_right_cvgr {R f a} b. +Arguments nondecreasing_at_right_cvgr {R f a} b. Section fun_cvg_ereal. Context {R : realType}. @@ -370,100 +459,129 @@ Lemma nondecreasing_is_cvge (f : R -> \bar R) : nondecreasing_fun f -> (cvg (f r @[r --> +oo]))%R. Proof. by move=> u_nd u_ub; apply: cvgP; exact: nondecreasing_cvge. Qed. -Lemma nondecreasing_at_right_cvge (f : R -> \bar R) a : - {in `]a, +oo[, nondecreasing_fun f} -> - f x @[x --> a ^'+] --> ereal_inf (f @` `]a, +oo[). +Lemma nondecreasing_at_right_cvge (f : R -> \bar R) a (b : itv_bound R) : + (BRight a < b)%O -> + {in Interval (BRight a) b &, nondecreasing_fun f} -> + f x @[x --> a ^'+] --> ereal_inf (f @` [set` Interval (BRight a) b]). Proof. -move=> ndf; set S := (X in ereal_inf X); set l := ereal_inf S. +move=> ab ndf; set S := (X in ereal_inf X); set l := ereal_inf S. have [Snoo|Snoo] := pselect (S -oo). - case: (Snoo) => N /=; rewrite in_itv/= andbT => aN fNpoo. + case: (Snoo) => N/=. + rewrite in_itv/= -[X in _ && X]/(BLeft N < b)%O => /andP[aN Nb] fNpoo. have Nf n : (a < n <= N)%R -> f n = -oo. move=> /andP[an nN]; apply/eqP. - by rewrite eq_le leNye andbT -fNpoo ndf// in_itv/= an. + rewrite eq_le leNye andbT -fNpoo ndf//. + by rewrite in_itv/= -[X in _ && X]/(BLeft n < b)%O an (le_lt_trans _ Nb). + by rewrite in_itv/= -[X in _ && X]/(BLeft N < b)%O (lt_le_trans an nN). have -> : l = -oo. by rewrite /l /ereal_inf /ereal_sup supremum_pinfty//=; exists -oo. apply: cvg_near_cst; exists (N - a)%R => /=; first by rewrite subr_gt0. - move=> y /= + ay. - rewrite ltr0_norm ?subr_lt0// opprB => ayNa. + move=> y /= + ay; rewrite ltr0_norm ?subr_lt0// opprB => ayNa. by rewrite Nf// ay/= -(subrK a y) -lerBrDr ltW. have [lnoo|lnoo] := eqVneq l -oo. rewrite lnoo; apply/cvgeNyPle => M. - have : M%:E > l by rewrite lnoo ltNyr. - move=> /ereal_inf_lt[x [y]]. - rewrite /= in_itv/= andbT => ay <- fyM. + have /ereal_inf_lt[x [y]]/= : M%:E > l by rewrite lnoo ltNyr. + rewrite in_itv/= -[X in _ && X]/(BLeft y < b)%O/= => /andP[ay yb] <- fyM. exists (y - a)%R => /=; first by rewrite subr_gt0. move=> z /= + az. rewrite ltr0_norm ?subr_lt0// opprB ltrBlDr subrK => zy. - by rewrite (le_trans _ (ltW fyM))// ndf// ?in_itv/= ?andbT// ltW. -have [fpoo|fpoo] := pselect {in `]a, +oo[, forall x, f x = +oo}. - rewrite /l (_ : S = [set +oo]). + rewrite (le_trans _ (ltW fyM))// ndf ?ltW//. + by rewrite in_itv/= -[X in _ && X]/(BLeft z < b)%O/= az/= (lt_trans _ yb). + by rewrite in_itv/= -[X in _ && X]/(BLeft y < b)%O/= (lt_trans az zy). +have [fpoo|fpoo] := pselect {in Interval (BRight a) b, forall x, f x = +oo}. + rewrite {}/l in lnoo *; rewrite {}/S in Snoo lnoo *. + rewrite [X in ereal_inf X](_ : _ = [set +oo]). rewrite ereal_inf1; apply/cvgeyPgey; near=> M. - near=> x. - rewrite fpoo ?leey// in_itv/= andbT. - by near: x; exact: nbhs_right_gt. + move: b ab {ndf lnoo Snoo} fpoo => [[|] b|[//|]] ab fpoo. + - near=> x; rewrite fpoo ?leey// in_itv/=. + by apply/andP; split; near: x; [exact: nbhs_right_gt|exact: nbhs_right_lt]. + - near=> x; rewrite fpoo ?leey// in_itv/=. + by apply/andP; split; near: x; [exact: nbhs_right_gt|exact: nbhs_right_le]. + - near=> x; rewrite fpoo ?leey// in_itv/= andbT. + by near: x; exact: nbhs_right_gt. apply/seteqP; split => [_ [n _] <- /[!fpoo]//|_ ->]. - rewrite /S /=; exists (a + 1)%R; first by rewrite in_itv/= andbT ltrDl. - by rewrite fpoo// in_itv /= andbT ltrDl. + move: b ab ndf lnoo Snoo fpoo => [[|] s|[//|]] ab ndf lnoo Snoo fpoo /=. + - by exists ((a + s) / 2)%R; rewrite ?fpoo// in_itv/= !midf_lt. + - by exists ((a + s) / 2)%R; rewrite ?fpoo// in_itv/= !(midf_lt, midf_le)// ltW. + - by exists (a + 1)%R; rewrite ?fpoo// in_itv/= andbT ltrDl. have [/ereal_inf_pinfty lpoo|lpoo] := eqVneq l +oo. - exfalso. - apply/fpoo => n; rewrite in_itv/= andbT => an; rewrite (lpoo (f n))//. - by exists n => //=; rewrite in_itv/= andbT. + by exfalso; apply/fpoo => r rab; rewrite (lpoo (f r))//; exists r. have l_fin_num : l \is a fin_num by rewrite fin_numE lpoo lnoo. -set A := [set n | (a < n)%R /\ f n != +oo]. -set B := [set n | (a < n)%R /\ f n = +oo]. -have f_fin_num n : n \in A -> f n \is a fin_num. - move=> /[1!inE]-[an fnnoo]; rewrite fin_numE fnnoo andbT. - apply: contra_notN Snoo => /eqP unpoo. - by exists n => //=; rewrite in_itv/= andbT. -have [x [Ax fxpoo]] : A !=set0. - apply/set0P/negP => /eqP A0; apply/fpoo => x; rewrite in_itv/= andbT => ax. +set A := [set r | [/\ (a < r)%R, (BLeft r < b)%O & f r != +oo]]. +have f_fin_num r : r \in A -> f r \is a fin_num. + rewrite inE /A/= => -[ar rb] frnoo; rewrite fin_numE frnoo andbT. + apply: contra_notN Snoo => /eqP frpoo. + by exists r => //=; rewrite in_itv/= -[X in _ && X]/(BLeft r < b)%O ar rb. +have [x [ax xb fxpoo]] : A !=set0. + apply/set0P/negP => /eqP A0; apply/fpoo => x. + rewrite in_itv/= -[X in _ && X]/(BLeft x < b)%O => /andP[ax xb]. apply/eqP/negPn/negP => unnoo. by move/seteqP : A0 => [+ _] => /(_ x); apply; rewrite /A/= ax. have axA r : (a < r <= x)%R -> r \in A. move=> /andP[ar rx]; move: (rx) => /ndf rafx; rewrite /A /= inE; split => //. + by rewrite (le_lt_trans _ xb). apply/negP => /eqP urnoo. - move: rafx; rewrite urnoo in_itv/= andbT => /(_ ar). - by rewrite leye_eq (negbTE fxpoo). + move: rafx; rewrite urnoo. + rewrite in_itv/= -[X in _ && X]/(BLeft r < b)%O ar/=. + rewrite in_itv/= -[X in _ && X]/(BLeft x < b)%O ax/=. + by rewrite leye_eq (negbTE fxpoo) -falseE; apply; rewrite (le_lt_trans _ xb). rewrite -(@fineK _ l)//; apply/fine_cvgP; split. exists (x - a)%R => /=; first by rewrite subr_gt0. move=> z /= + az. rewrite ltr0_norm ?subr_lt0// opprB ltrBlDr subrK// => zx. by rewrite f_fin_num// axA// az/= ltW. set g := fun n => if (a < n < x)%R then fine (f n) else fine (f x). -have <- : inf [set g x | x in `]a, +oo[] = fine l. +have <- : inf [set g x | x in [set` Interval (BRight a) b]] = fine l. apply: EFin_inj; rewrite -ereal_inf_EFin//; last 2 first. - exists (fine l) => /= _ [m _ <-]; rewrite /g /=. case: ifPn => [/andP[am mx]|]. rewrite fine_le// ?f_fin_num//; first by rewrite axA// am (ltW mx). - by apply: ereal_inf_lb; exists m => //=; rewrite in_itv/= andbT. + apply: ereal_inf_lb; exists m => //=. + rewrite in_itv/= -[X in _ && X]/(BLeft m < b)%O am/=. + by rewrite (le_lt_trans _ xb) ?ltW. rewrite negb_and -!leNgt => /orP[ma|xm]. rewrite fine_le// ?f_fin_num ?inE//. - by apply: ereal_inf_lb; exists x => //=; rewrite in_itv/= andbT. + apply: ereal_inf_lb; exists x => //=. + by rewrite in_itv/= -[X in _ && X]/(BLeft x < b)%O ax xb. rewrite fine_le// ?f_fin_num ?inE//. - by apply: ereal_inf_lb; exists x => //=; rewrite in_itv/= andbT. - - by exists (g (a + 1)%R), (a + 1)%R => //=; rewrite in_itv/= andbT ltrDl. + apply: ereal_inf_lb; exists x => //=. + by rewrite in_itv/= -[X in _ && X]/(BLeft x < b)%O ax xb. + - rewrite {}/l in lnoo lpoo l_fin_num *. + rewrite {}/S in Snoo lnoo lpoo l_fin_num *. + rewrite {}/A in f_fin_num axA *. + move: b ab {xb ndf lnoo lpoo l_fin_num f_fin_num Snoo fpoo axA} => + [[|] s|[//|]] ab /=. + + exists (g ((a + s) / 2))%R, ((a + s) / 2)%R => //=. + by rewrite /= in_itv/= !midf_lt. + + exists (g ((a + s) / 2))%R, ((a + s) / 2)%R => //=. + by rewrite /= in_itv/= !(midf_lt, midf_le)// ltW. + + exists (g (a + 1)%R), (a + 1)%R => //=. + by rewrite in_itv/= andbT ltrDl. rewrite fineK//; apply/eqP; rewrite eq_le; apply/andP; split; last first. apply: le_ereal_inf => _ /= [_ [m _] <-] <-. rewrite /g; case: ifPn => [/andP[am mx]|]. rewrite fineK// ?f_fin_num//; last by rewrite axA// am ltW. - by exists m => //=; rewrite in_itv/= andbT. + exists m => //=. + by rewrite in_itv/= -[X in _ && X]/(BLeft m < b)%O am/= (lt_trans _ xb). rewrite negb_and -!leNgt => /orP[ma|xm]. - rewrite fineK//; first by exists x => //=; rewrite in_itv/= andbT. - by rewrite f_fin_num ?inE. - exists x => /=; first by rewrite in_itv/= andbT. + rewrite fineK//; last by rewrite f_fin_num ?inE. + exists x => //=. + by rewrite in_itv/= -[X in _ && X]/(BLeft x < b)%O ax xb. + exists x => /=. + by rewrite in_itv/= -[X in _ && X]/(BLeft x < b)%O ax xb. by rewrite fineK// f_fin_num ?inE. - apply: lb_ereal_inf => /= y [m] /=; rewrite in_itv/= andbT => am <-{y}. + apply: lb_ereal_inf => /= y [m] /=. + rewrite in_itv/= -[X in _ && X]/(BLeft m < b)%O => /andP[am mb] <-{y}. have [mx|xm] := ltP m x. apply: ereal_inf_lb => /=; exists (fine (f m)); last first. by rewrite fineK// f_fin_num// axA// am (ltW mx). - exists m; first by rewrite in_itv/= andbT. - by rewrite /g am mx. - rewrite (le_trans _ (ndf _ _ _ xm))//; last by rewrite in_itv/= andbT. + by exists m; [rewrite in_itv/= am|rewrite /g am mx]. + rewrite (@le_trans _ _ (f x))//; last first. + by apply: ndf => //; rewrite in_itv//= ?ax ?am. apply: ereal_inf_lb => /=; exists (fine (f x)); last first. by rewrite fineK// f_fin_num ?inE. - exists x; first by rewrite in_itv andbT. - by rewrite /g ltxx andbF. -suff: g x @[x --> a^'+] --> inf [set g x | x in `]a, +oo[]. + by exists x; [rewrite in_itv/= ax|rewrite /g ltxx andbF]. +suff: g x @[x --> a^'+] --> inf [set g x | x in [set` Interval (BRight a) b]]. apply: cvg_trans; apply: near_eq_cvg; near=> n. rewrite /g /=; case: ifPn => [//|]. rewrite negb_and -!leNgt => /orP[na|xn]. @@ -475,43 +593,53 @@ suff: g x @[x --> a^'+] --> inf [set g x | x in `]a, +oo[]. move=> y /= /[swap] ay. rewrite ltr0_norm// ?subr_lt0// opprB ltrBlDr => /lt_le_trans; apply. by rewrite -lerBrDr ler_pdivrMr// ler_pMr// ?ler1n// subr_gt0. -apply: nondecreasing_at_right_cvgr. -- move=> m ma n mn /=; rewrite /g /=; case: ifPn => [/andP[am mx]|]. +apply: nondecreasing_at_right_cvgr => //. +- move=> m n; rewrite !in_itv/= -[X in _ && X]/(BLeft m < b)%O. + rewrite -[X in _ -> _ && X -> _]/(BLeft n < b)%O. + move=> /andP[am mb] /andP[an nb] mn. + rewrite /g /=; case: ifPn => [/andP[_ mx]|]. rewrite (lt_le_trans am mn) /=; have [nx|nn0] := ltP n x. rewrite fine_le ?f_fin_num ?ndf//; first by rewrite axA// am (ltW mx). by rewrite axA// (ltW nx) andbT (lt_le_trans am). + by rewrite in_itv/= am. + by rewrite in_itv/= an. rewrite fine_le ?f_fin_num//. + by rewrite axA// am (ltW (lt_le_trans mx _)). + by rewrite inE. - + by rewrite ndf// ltW. - rewrite negb_and -!leNgt => /orP[ma'|xm]. - by rewrite in_itv/= andbT ltNge ma' in ma. - rewrite in_itv/= andbT in ma. - by rewrite (lt_le_trans ma mn)/= ltNge (le_trans xm mn). + + rewrite ndf//; last exact/ltW. + by rewrite !in_itv/= am. + by rewrite !in_itv/= ax. + rewrite negb_and -!leNgt => /orP[|xm]; first by rewrite leNgt am. + by rewrite (lt_le_trans am mn)/= ltNge (le_trans xm mn). - exists (fine l) => /= _ [m _ <-]; rewrite /g /=. rewrite -lee_fin (fineK l_fin_num); apply: ereal_inf_lb. case: ifPn => [/andP[am mn0]|]. - rewrite fineK//; first by exists m => //=; rewrite in_itv/= am. - by rewrite f_fin_num// axA// am (ltW mn0). + rewrite fineK//; last by rewrite f_fin_num// axA// am (ltW mn0). + exists m => //=. + by rewrite in_itv/= -[X in _ && X]/(BLeft m < b)%O am (lt_trans _ xb). rewrite negb_and -!leNgt => /orP[ma|xm]. - rewrite fineK//; first by exists x => //=; rewrite in_itv/= Ax. + rewrite fineK//; first by exists x => //=; rewrite in_itv/= ax. by rewrite f_fin_num ?inE. - by rewrite fineK// ?f_fin_num ?inE//; exists x => //=; rewrite in_itv/= andbT. + by rewrite fineK// ?f_fin_num ?inE//; exists x => //=; rewrite in_itv/= ax. Unshelve. all: by end_near. Qed. -Lemma nondecreasing_at_right_is_cvge (f : R -> \bar R) a : - {in `]a, +oo[, nondecreasing_fun f} -> +Lemma nondecreasing_at_right_is_cvge (f : R -> \bar R) (a : R) : + (\forall x \near a^'+, {in `]a, x[ &, nondecreasing_fun f}) -> cvg (f x @[x --> a ^'+]). -Proof. by move=> ndf; apply: cvgP; exact: nondecreasing_at_right_cvge. Qed. +Proof. +move=> ndf; apply/cvg_ex; near a^'+ => b. +by eexists; apply: (@nondecreasing_at_right_cvge _ _ (BLeft b)); + [rewrite bnd_simp|near: b..]. +Unshelve. all: by end_near. Qed. -Lemma nonincreasing_at_right_cvge (f : R -> \bar R) a : - {in `]a, +oo[, nonincreasing_fun f} -> - f x @[x --> a ^'+] --> ereal_sup (f @` `]a, +oo[). +Lemma nonincreasing_at_right_cvge (f : R -> \bar R) a (b : itv_bound R) : + (BRight a < b)%O -> {in Interval (BRight a) b &, nonincreasing_fun f} -> + f x @[x --> a ^'+] --> ereal_sup (f @` [set` Interval (BRight a) b]). Proof. -move=> nif. -have ndNf : {in `]a, +oo[, {homo (\- f) : n m / (n <= m)%R >-> n <= m}}. - by move=> r ra y /nif; rewrite leeN2; exact. -have /cvgeN := nondecreasing_at_right_cvge ndNf. +move=> ab nif; have ndNf : {in Interval (BRight a) b &, + {homo (\- f) : n m / (n <= m)%R >-> n <= m}}. + by move=> r s rab sab /nif; rewrite leeN2; exact. +have /cvgeN := nondecreasing_at_right_cvge ab ndNf. under eq_fun do rewrite oppeK. set lhs := (X in _ --> X -> _); set rhs := (X in _ -> _ --> X). suff : lhs = rhs by move=> ->. @@ -520,13 +648,21 @@ by rewrite image_comp/=; apply: eq_imagel => x _ /=; rewrite oppeK. Qed. Lemma nonincreasing_at_right_is_cvge (f : R -> \bar R) a : - {in `]a, +oo[, nonincreasing_fun f} -> + (\forall x \near a^'+, {in `]a, x[ &, nonincreasing_fun f}) -> cvg (f x @[x --> a ^'+]). -Proof. by move=> ndf; apply: cvgP; exact: nonincreasing_at_right_cvge. Qed. +Proof. +move=> nif; apply/cvg_ex; near a^'+ => b. +by eexists; apply: (@nonincreasing_at_right_cvge _ _ (BLeft b)); + [rewrite bnd_simp|near: b..]. +Unshelve. all: by end_near. Qed. End fun_cvg_ereal. End fun_cvg. +Arguments nondecreasing_at_right_cvge {R f a} b. +Arguments nondecreasing_at_right_is_cvge {R f a}. +Arguments nonincreasing_at_right_cvge {R f a} b. +Arguments nonincreasing_at_right_is_cvge {R f a}. Section lime_sup_inf. Variable R : realType. @@ -547,9 +683,9 @@ Qed. Let sup_ball_is_cvg f a : cvg (sup_ball f a e @[e --> 0^'+]). Proof. -apply: nondecreasing_at_right_is_cvge => x. -by rewrite in_itv/= andbT => x0 y /sup_ball_le. -Qed. +apply: nondecreasing_at_right_is_cvge; near=> e. +by move=> x y; rewrite !in_itv/= => /andP[x0 xe] /andP[y0 ye] /sup_ball_le. +Unshelve. all: by end_near. Qed. Let inf_ball f a r := - sup_ball (\- f) a r. @@ -563,9 +699,9 @@ Proof. by move=> sr; rewrite /inf_ball lee_oppl oppeK sup_ball_le. Qed. Let inf_ball_is_cvg f a : cvg (inf_ball f a e @[e --> 0^'+]). Proof. -apply: nonincreasing_at_right_is_cvge => //. -by move=> x; rewrite in_itv/= andbT => x0 y /inf_ball_le. -Qed. +apply: nonincreasing_at_right_is_cvge; near=> e. +by move=> x y; rewrite !in_itv/= => /andP[x0 xe] /andP[y0 ye] /inf_ball_le. +Unshelve. all: by end_near. Qed. Let le_sup_ball f g a : (forall r, (0 < r)%R -> forall y : R, y != a -> ball a r y -> f y <= g y) -> @@ -599,7 +735,7 @@ Lemma lime_supE f a : Proof. rewrite lime_sup_lim; apply/cvg_lim => //. apply: nondecreasing_at_right_cvge => //. -by move=> x; rewrite in_itv/= andbT => x0 y; exact: sup_ball_le. +by move=> x y; rewrite !in_itv/= !andbT => x0 y0; exact: sup_ball_le. Qed. Lemma lime_infE f a : @@ -636,8 +772,8 @@ Proof. move=> fg; rewrite !lime_sup_lim -limeD//; last first. by rewrite -!lime_sup_lim. apply: lee_lim => //. -- apply: nondecreasing_at_right_is_cvge => x. - by rewrite in_itv/= andbT => x0 y xy; rewrite lee_add//; exact: sup_ball_le. +- apply: nondecreasing_at_right_is_cvge; near=> e => x y; rewrite !in_itv/=. + by move=> /andP[? ?] /andP[? ?] xy; apply: lee_add => //; exact: sup_ball_le. - near=> a0; apply: ub_ereal_sup => _ /= [a1 [a1ae a1a]] <-. by apply: lee_add; apply: ereal_sup_ub => /=; exists a1. Unshelve. all: by end_near. Qed. @@ -1116,6 +1252,7 @@ have : f a >= f b by rewrite (itvP xfafb). by case: ltrgtP xfafb => // ->. Qed. + Lemma segment_inc_surj_continuous a b f : {in `[a, b] &, {mono f : x y / x <= y}} -> set_surj `[a, b] `[f a, f b] f -> {within `[a, b], continuous f}. @@ -1329,7 +1466,6 @@ Section is_derive_inverse. Variable R : realType. (* Attempt to prove the diff of inverse *) - Lemma is_derive1_caratheodory (f : R -> R) (x a : R) : is_derive x 1 f a <-> exists g, [/\ forall z, f z - f x = g z * (z - x), @@ -1425,3 +1561,866 @@ End is_derive_inverse. #[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) => (eapply is_deriveV; first by []) : typeclass_instances. + +Section interval_partition. +Context {R : realType}. +Implicit Type (a b : R) (s : seq R). + +(** a :: s is a partition of the interval [a, b] *) +Definition itv_partition a b s := [/\ path <%R a s & last a s == b]. + +Lemma itv_partition_nil a b : itv_partition a b [::] -> a = b. +Proof. by move=> [_ /eqP <-]. Qed. + +Lemma itv_partition_cons a b x s : + itv_partition a b (x :: s) -> itv_partition x b s. +Proof. by rewrite /itv_partition/= => -[/andP[]]. Qed. + +Lemma itv_partition1 a b : a < b -> itv_partition a b [:: b]. +Proof. by rewrite /itv_partition /= => ->. Qed. + +Lemma itv_partition_size_neq0 a b s : + (size s > 0)%N -> itv_partition a b s -> a < b. +Proof. +elim: s a => // x [_ a _|h t ih a _]; rewrite /itv_partition /=. + by rewrite andbT => -[ax /eqP <-]. +move=> [] /andP[ax /andP[xy] ht /eqP tb]. +by rewrite (lt_trans ax)// ih// /itv_partition /= xy/= tb. +Qed. + +Lemma itv_partitionxx a s : itv_partition a a s -> s = [::]. +Proof. +case: s => //= h t [/= /andP[ah /lt_path_min/allP ht] /eqP hta]. +suff : h < a by move/lt_trans => /(_ _ ah); rewrite ltxx. +apply/ht; rewrite -hta. +by have := mem_last h t; rewrite inE hta lt_eqF. +Qed. + +Lemma itv_partition_le a b s : itv_partition a b s -> a <= b. +Proof. +case: s => [/itv_partition_nil ->//|h t /itv_partition_size_neq0 - /(_ _)/ltW]. +exact. +Qed. + +Lemma itv_partition_cat a b c s t : + itv_partition a b s -> itv_partition b c t -> itv_partition a c (s ++ t). +Proof. +rewrite /itv_partition => -[sa /eqP asb] [bt btc]. +by rewrite cat_path// sa /= last_cat asb. +Qed. + +Lemma itv_partition_nth_size def a b s : itv_partition a b s -> + nth def (a :: s) (size s) = b. +Proof. +by elim: s a => [a/= /itv_partition_nil//|y t ih a /= /itv_partition_cons/ih]. +Qed. + +Lemma itv_partition_nth_ge a b s m : (m < (size s).+1)%N -> + itv_partition a b s -> a <= nth b (a :: s) m. +Proof. +elim: m s a b => [s a b _//|n ih [//|h t] a b]. +rewrite ltnS => nh [/= /andP[ah ht] lb]. +by rewrite (le_trans (ltW ah))// ih. +Qed. + +Lemma itv_partition_nth_le a b s m : (m < (size s).+1)%N -> + itv_partition a b s -> nth b (a :: s) m <= b. +Proof. +elim: m s a => [s a _|n ih]; first exact: itv_partition_le. +by move=> [//|a h t /= nt] H; rewrite ih//; exact: itv_partition_cons H. +Qed. + +Lemma nondecreasing_fun_itv_partition a b f s : + {in `[a, b] &, nondecreasing_fun f} -> itv_partition a b s -> + let F : nat -> R := f \o nth b (a :: s) in + forall k, (k < size s)%N -> F k <= F k.+1. +Proof. +move=> ndf abs F k ks. +have [_] := nondecreasing_seqP F; apply => m n mn; rewrite /F/=. +have [ms|ms] := ltnP m (size s).+1; last first. + rewrite nth_default//. + have [|ns] := ltnP n (size s).+1; last by rewrite nth_default. + by move=> /(leq_ltn_trans mn); rewrite ltnS leqNgt ms. +have [ns|ns] := ltnP n (size s).+1; last first. + rewrite [in leRHS]nth_default//=; apply/ndf/itv_partition_nth_le => //. + by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge. + by rewrite in_itv/= lexx andbT; exact: (itv_partition_le abs). +move: abs; rewrite /itv_partition => -[] sa sab. +move: mn; rewrite leq_eqVlt => /predU1P[->//|mn]. +apply/ndf/ltW/sorted_ltn_nth => //=; last exact: lt_trans. + by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge. +by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge. +Qed. + +Lemma nonincreasing_fun_itv_partition a b f s : + {in `[a, b] &, nonincreasing_fun f} -> itv_partition a b s -> + let F : nat -> R := f \o nth b (a :: s) in + forall k, (k < size s)%N -> F k.+1 <= F k. +Proof. +move/nonincreasing_funN => ndNf abs F k ks; rewrite -(opprK (F k)) ler_oppr. +exact: (nondecreasing_fun_itv_partition ndNf abs). +Qed. + +(** given a partition of [a, b] and c, returns a partition of [a, c] *) +Definition itv_partitionL s c := rcons [seq x <- s | x < c] c. + +Lemma itv_partitionLP a b c s : a < c -> c < b -> itv_partition a b s -> + itv_partition a c (itv_partitionL s c). +Proof. +move=> ac bc [] al /eqP htb; split. + rewrite /itv_partitionL rcons_path/=; apply/andP; split. + by apply: path_filter => //; exact: lt_trans. + exact: (last_filterP [pred x | x < c]). +by rewrite /itv_partitionL last_rcons. +Qed. + +(** given a partition of [a, b] and c, returns a partition of [c, b] *) +Definition itv_partitionR s c := [seq x <- s | c < x]. + +Lemma itv_partitionRP a b c s : a < c -> c < b -> itv_partition a b s -> + itv_partition c b (itv_partitionR s c). +Proof. +move=> ac cb [] sa /eqP alb; rewrite /itv_partition; split. + move: sa; rewrite lt_path_sortedE => /andP[allas ss]. + rewrite lt_path_sortedE filter_all/=. + by apply: sorted_filter => //; exact: lt_trans. +exact/eqP/(path_lt_last_filter ac). +Qed. + +Lemma in_itv_partition c s : sorted <%R s -> c \in s -> + s = itv_partitionL s c ++ itv_partitionR s c. +Proof. +elim: s c => // h t ih c /= ht. +rewrite inE => /predU1P[->{c}/=|ct]. + rewrite ltxx /itv_partitionL /= ltxx /itv_partitionR/= path_lt_filter0//=. + by rewrite path_lt_filterT. +rewrite /itv_partitionL/=; case: ifPn => [hc|]. + by rewrite ltNge (ltW hc)/= /= [in LHS](ih _ _ ct)//; exact: path_sorted ht. +rewrite -leNgt le_eqVlt => /predU1P[ch|ch]. + by rewrite ch ltxx path_lt_filter0//= /itv_partitionR path_lt_filterT. +move: ht; rewrite lt_path_sortedE => /andP[/allP/(_ _ ct)]. +by move=> /lt_trans-/(_ _ ch); rewrite ltxx. +Qed. + +Lemma notin_itv_partition c s : sorted <%R s -> c \notin s -> + s = [seq x <- s | x < c] ++ itv_partitionR s c. +Proof. +elim: s c => // h t ih c /= ht. +rewrite inE negb_or => /andP[]; rewrite neq_lt => /orP[ch|ch] ct. + rewrite ch ltNge (ltW ch)/= path_lt_filter0/= /itv_partitionR; last first. + exact: path_lt_head ht. + by rewrite path_lt_filterT//; exact: path_lt_head ht. +by rewrite ch/= ltNge (ltW ch)/= -ih//; exact: path_sorted ht. +Qed. + +Lemma itv_partition_rev a b s : itv_partition a b s -> + itv_partition (- b) (- a) (rev (belast (- a) (map -%R s))). +Proof. +move=> [sa /eqP alb]; split. + rewrite (_ : - b = last (- a) (map -%R s)); last by rewrite last_map alb. + rewrite rev_path// path_map. + by apply: sub_path sa => x y xy/=; rewrite ltr_oppr opprK. +case: s sa alb => [_ <-//|h t] /= /andP[ah ht] <-{b}. +by rewrite rev_cons last_rcons. +Qed. + +End interval_partition. + +Section variation. +Context {R : realType}. +Implicit Types (a b : R) (f g : R -> R). + +Definition variation a b f s := let F := f \o nth b (a :: s) in + \sum_(0 <= n < size s) `|F n.+1 - F n|%R. + +Lemma variation_zip a b f s : itv_partition a b s -> + variation a b f s = \sum_(x <- zip s (a :: s)) `|f x.1 - f x.2|. +Proof. +elim: s a b => // [a b|h t ih a b]. + by rewrite /itv_partition /= => -[_ /eqP <-]; rewrite /variation/= !big_nil. +rewrite /itv_partition /variation => -[]/= /andP[ah ht] /eqP htb. +rewrite big_nat_recl//= big_cons/=; congr +%R. +have /ih : itv_partition h b t by split => //; exact/eqP. +by rewrite /variation => ->; rewrite !big_seq; apply/eq_bigr => r rt. +Qed. + +(* NB: not used yet but should allow for "term-by-term" comparisons *) +Lemma variation_prev a b f s : itv_partition a b s -> + variation a b f s = \sum_(x <- s) `|f x - f (prev (locked (a :: s)) x)|. +Proof. +move=> [] sa /eqP asb; rewrite /variation [in LHS]/= (big_nth b) !big_nat. +apply: eq_bigr => i /andP[_ si]; congr (`| _ - f _ |). +rewrite -lock. +rewrite prev_nth inE gt_eqF; last first. + rewrite -[a]/(nth b (a :: s) 0) -[ltRHS]/(nth b (a :: s) i.+1). + exact: lt_sorted_ltn_nth. +rewrite orFb mem_nth// index_uniq//. + by apply: set_nth_default => /=; rewrite ltnS ltnW. +by apply: (sorted_uniq lt_trans) => //; apply: path_sorted sa. +Qed. + +Lemma variation_next a b f s : itv_partition a b s -> + variation a b f s = + \sum_(x <- belast a s) `|f (next (locked (a :: s)) x) - f x|. +Proof. +move=> [] sa /eqP asb; rewrite /variation [in LHS]/= (big_nth b) !big_nat. +rewrite size_belast; apply: eq_bigr => i /andP[_ si]. +congr (`| f _ - f _ |); last first. + by rewrite lastI -cats1 nth_cat size_belast// si. +rewrite -lock next_nth. +rewrite {1}lastI mem_rcons inE mem_nth ?size_belast// orbT. +rewrite lastI -cats1 index_cat mem_nth ?size_belast//. +rewrite index_uniq ?size_belast//. + exact: set_nth_default. +have /lt_sorted_uniq : sorted <%R (a :: s) by []. +by rewrite lastI rcons_uniq => /andP[]. +Qed. + +Lemma variation_nil a b f : variation a b f [::] = 0. +Proof. by rewrite /variation/= big_nil. Qed. + +Lemma variation_ge0 a b f s : 0 <= variation a b f s. +Proof. exact/sumr_ge0. Qed. + +Lemma variationN a b f s : variation a b (\- f) s = variation a b f s. +Proof. +by rewrite /variation; apply: eq_bigr => k _ /=; rewrite -opprD normrN. +Qed. + +Lemma variation_le a b f g s : + variation a b (f \+ g)%R s <= variation a b f s + variation a b g s. +Proof. +rewrite [in leRHS]/variation -big_split/=. +apply: ler_sum => k _; apply: le_trans; last exact: ler_norm_add. +by rewrite /= addrACA addrA opprD addrA. +Qed. + +Lemma nondecreasing_variation a b f s : {in `[a, b] &, nondecreasing_fun f} -> + itv_partition a b s -> variation a b f s = f b - f a. +Proof. +move=> ndf abs; rewrite /variation; set F : nat -> R := f \o nth _ (a :: s). +transitivity (\sum_(0 <= n < size s) (F n.+1 - F n)). + rewrite !big_nat; apply: eq_bigr => k; rewrite leq0n/= => ks. + by rewrite ger0_norm// subr_ge0; exact: nondecreasing_fun_itv_partition. +by rewrite telescope_sumr// /F/= (itv_partition_nth_size _ abs). +Qed. + +Lemma nonincreasing_variation a b f s : {in `[a, b] &, nonincreasing_fun f} -> + itv_partition a b s -> variation a b f s = f a - f b. +Proof. +move=> /nonincreasing_funN ndNf abs; have := nondecreasing_variation ndNf abs. +by rewrite opprK addrC => <-; rewrite variationN. +Qed. + +Lemma variationD a b c f s t : a <= c -> c <= b -> + itv_partition a c s -> itv_partition c b t -> + variation a c f s + variation c b f t = variation a b f (s ++ t). +Proof. +rewrite le_eqVlt => /predU1P[<-{c} cb|ac]. + by move=> /itv_partitionxx ->; rewrite variation_nil add0r. +rewrite le_eqVlt => /predU1P[<-{b}|cb]. + by move=> ? /itv_partitionxx ->; rewrite variation_nil addr0 cats0. +move=> acs cbt; rewrite /variation /= [in RHS]/index_iota subn0 size_cat. +rewrite iotaD add0n big_cat/= -[in X in _ = X + _](subn0 (size s)); congr +%R. + rewrite -/(index_iota 0 (size s)) 2!big_nat. + apply: eq_bigr => k /[!leq0n] /= ks. + rewrite nth_cat ks -cat_cons nth_cat /= ltnS (ltnW ks). + by rewrite !(set_nth_default b c)//= ltnS ltnW. +rewrite -[in RHS](addnK (size s) (size t)). +rewrite -/(index_iota (size s) (size t + size s)). +rewrite -{1}[in RHS](add0n (size s)) big_addn addnK 2!big_nat; apply: eq_bigr. +move=> k /[!leq0n]/= kt. +rewrite nth_cat {1}(addnC k) -ltn_subRL subnn ltn0 addnK. +case: k kt => [t0 /=|k kt]. + rewrite add0n -cat_cons nth_cat/= ltnS leqnn -last_nth. + by case: acs => _ /eqP ->. +rewrite addSnnS (addnC k) -cat_cons nth_cat/= -ltn_subRL subnn ltn0. +by rewrite -(addnC k) addnK. +Qed. + +(* NB: this is the only lemma that uses variation_zip *) +Lemma variation_itv_partitionLR a b c f s : a < c -> c < b -> + itv_partition a b s -> + variation a b f s <= variation a b f (itv_partitionL s c ++ itv_partitionR s c). +Proof. +move=> ac bc abs; have [cl|cl] := boolP (c \in s). + by rewrite -in_itv_partition//; case: abs => /path_sorted. +rewrite /itv_partitionL [in leLHS](notin_itv_partition _ cl)//; last first. + by apply: path_sorted; case: abs => + _; exact. +rewrite -notin_itv_partition//; last first. + by apply: path_sorted; case: abs => /= + _; exact. +rewrite !variation_zip//; last first. + by apply: itv_partition_cat; + [exact: (itv_partitionLP _ bc)|exact: (itv_partitionRP ac)]. +rewrite [in leLHS](notin_itv_partition _ cl); last first. + by apply: path_sorted; case: abs => + _; exact. +set L := [seq x <- s | x < c]. +rewrite -cats1 -catA. +move: L => L. +set B := itv_partitionR s c. +move: B => B. +elim/last_ind : L => [|L0 L1 _]. + rewrite !cat0s /=; case: B => [|B0 B1]. + by rewrite big_nil big_cons/= big_nil addr0. + rewrite !big_cons/= addrA lerD// [leRHS]addrC. + by rewrite (le_trans _ (ler_normD _ _))// addrA subrK. +rewrite -cats1. +rewrite (_ : a :: _ ++ B = (a :: L0) ++ [:: L1] ++ B)//; last first. + by rewrite -!catA -cat_cons. +rewrite zip_cat; last by rewrite cats1 size_rcons. +rewrite (_ : a :: _ ++ _ ++ B = (a :: L0) ++ [:: L1] ++ [:: c] ++ B); last first. + by rewrite -!catA -cat_cons. +rewrite zip_cat; last by rewrite cats1 size_rcons. +rewrite !big_cat lerD//. +case: B => [|B0 B1]. + by rewrite /= big_nil big_cons big_nil addr0. +rewrite -cat1s zip_cat// catA. +rewrite (_ : [:: L1] ++ _ ++ B1 = ([:: L1] ++ [:: c]) ++ [:: B0] ++ B1); last first. + by rewrite catA. +rewrite zip_cat// !big_cat lerD//= !big_cons !big_nil !addr0/= [leRHS]addrC. + by rewrite (le_trans _ (ler_normD _ _))// addrA subrK. +Qed. + +Lemma le_variation a b f s x : variation a b f s <= variation a b f (x :: s). +Proof. +case: s => [|h t]. + by rewrite variation_nil /variation/= big_nat_recl//= big_nil addr0. +rewrite /variation/= !big_nat_recl//= addrA lerD2r. +by rewrite (le_trans _ (ler_normD _ _))// (addrC (f x - _)) addrA subrK. +Qed. + +Lemma variation_opp_rev a b f s : itv_partition a b s -> + variation a b f s = + variation (- b) (- a) (f \o -%R) (rev (belast (- a) (map -%R s))). +Proof. +move=> abl; rewrite belast_map /variation /= [LHS]big_nat_rev/= add0n. +rewrite size_rev size_map size_belast 2!big_nat. +apply: eq_bigr => k; rewrite leq0n /= => ks. +rewrite nth_rev ?size_map ?size_belast// [in RHS]distrC. +rewrite (nth_map a); last first. + by rewrite size_belast ltn_subLR// addSn ltnS leq_addl. +rewrite opprK -rev_rcons nth_rev ?size_rcons ?size_map ?size_belast 1?ltnW//. +rewrite subSn// -map_rcons (nth_map b) ?size_rcons ?size_belast; last first. + by rewrite ltnS ltn_subLR// addSn ltnS leq_addl. +rewrite opprK nth_rcons size_belast -subSn// subSS. +rewrite (ltn_subLR _ (ltnW ks)) if_same. +case: k => [|k] in ks *. + rewrite add0n ltnn subn1 (_ : nth b s _ = b); last first. + case: abl ks => _. + elim/last_ind : s => // h t _; rewrite last_rcons => /eqP -> _. + by rewrite nth_rcons size_rcons ltnn eqxx. + rewrite (_ : nth b (a :: s) _ = nth a (belast a s) (size s).-1)//. + case: abl ks => _. + elim/last_ind : s => // h t _; rewrite last_rcons => /eqP -> _. + rewrite belast_rcons size_rcons/= -rcons_cons nth_rcons/= ltnS leqnn. + exact: set_nth_default. +rewrite addSn ltnS leq_addl//; congr (`| f _ - f _ |). + elim/last_ind : s ks {abl} => // h t _; rewrite size_rcons ltnS => kh. + rewrite belast_rcons nth_rcons subSS ltn_subLR//. + by rewrite addSn ltnS leq_addl// subSn. +elim/last_ind : s ks {abl} => // h t _; rewrite size_rcons ltnS => kh. +rewrite belast_rcons subSS -rcons_cons nth_rcons /= ltn_subLR//. +rewrite addnS ltnS leq_addl; apply: set_nth_default => //. +by rewrite /= ltnS leq_subLR leq_addl. +Qed. + +Lemma variation_rev_opp a b f s : itv_partition (- b) (- a) s -> + variation a b f (rev (belast b (map -%R s))) = + variation (- b) (- a) (f \o -%R) s. +Proof. +move=> abs; rewrite [in RHS]variation_opp_rev ?opprK//. +suff: (f \o -%R) \o -%R = f by move=> ->. +by apply/funext=> ? /=; rewrite opprK. +Qed. + +Lemma variation_subseq a b f (s t : list R) : + itv_partition a b s -> itv_partition a b t -> + subseq s t -> + variation a b f s <= variation a b f t. +Proof. +elim: t s a => [? ? ? /= _ /eqP ->//|a s IH [|x t] w]. + by rewrite variation_nil // variation_ge0. +move=> /[dup] /itv_partition_cons itvxb /[dup] /itv_partition_le wb itvxt. +move=> /[dup] /itv_partition_cons itvas itvws /=. +have ab : a <= b by exact: (itv_partition_le itvas). +have wa : w < a by case: itvws => /= /andP[]. +have waW : w <= a := ltW wa. +case: ifPn => [|] nXA. + move/eqP : nXA itvxt itvxb => -> itvat itvt /= ta. + rewrite -[_ :: t]cat1s -[_ :: s]cat1s. + rewrite -?(@variationD _ _ a)//; [|exact: itv_partition1..]. + by rewrite lerD// IH. +move=> xts; rewrite -[_ :: s]cat1s -(@variationD _ _ a) => //; last first. + exact: itv_partition1. +have [y [s' s'E]] : exists y s', s = y :: s'. + by case: {itvas itvws IH} s xts => // y s' ?; exists y, s'. +apply: (@le_trans _ _ (variation w b f s)). + rewrite IH//. + case: itvws => /= /andP[_]; rewrite s'E /= => /andP[ay ys' lyb]. + by split => //; rewrite (path_lt_head wa)//= ys' andbT. +by rewrite variationD //; [exact: le_variation | exact: itv_partition1]. +Qed. + +End variation. + +Section bounded_variation. +Context {R : realType}. +Implicit Type (a b : R) (f : R -> R). + +Definition variations a b f := [set variation a b f l | l in itv_partition a b]. + +Lemma variations_variation a b f s : itv_partition a b s -> + variations a b f (variation a b f s). +Proof. by move=> abs; exists s. Qed. + +Lemma variations_neq0 a b f : a < b -> variations a b f !=set0. +Proof. +move=> ab; exists (variation a b f [:: b]); exists [:: b] => //. +exact: itv_partition1. +Qed. + +Lemma variationsN a b f : variations a b (\- f) = variations a b f. +Proof. +apply/seteqP; split => [_ [s abs] <-|r [s abs]]. + by rewrite variationN; exact: variations_variation. +by rewrite -variationN => <-; exact: variations_variation. +Qed. + +Lemma variationsxx a f : variations a a f = [set 0]. +Proof. +apply/seteqP; split => [x [_ /itv_partitionxx ->]|x ->]. + by rewrite /variation big_nil => <-. +by exists [::] => //=; rewrite /variation /= big_nil. +Qed. + +Definition bounded_variation a b f := has_ubound (variations a b f). + +Notation BV := bounded_variation. + +Lemma bounded_variationxx a f : BV a a f. +Proof. by exists 0 => r; rewrite variationsxx => ->. Qed. + +Lemma bounded_variationD a b f g : a < b -> + BV a b f -> BV a b g -> BV a b (f \+ g). +Proof. +move=> ab [r abfr] [s abgs]; exists (r + s) => _ [l abl] <-. +apply: le_trans; first exact: variation_le. +rewrite lerD//. +- by apply: abfr; exact: variations_variation. +- by apply: abgs; exact: variations_variation. +Qed. + +Lemma bounded_variationN a b f : BV a b f -> BV a b (\- f). +Proof. by rewrite /bounded_variation variationsN. Qed. + +Lemma bounded_variationl a c b f : a <= c -> c <= b -> BV a b f -> BV a c f. +Proof. +rewrite le_eqVlt => /predU1P[<-{c} ? ?|ac]; first exact: bounded_variationxx. +rewrite le_eqVlt => /predU1P[<-{b}//|cb]. +move=> [x Hx]; exists x => _ [s acs] <-. +rewrite (@le_trans _ _ (variation a b f (rcons s b)))//; last first. + apply/Hx/variations_variation; case: acs => sa /eqP asc. + by rewrite /itv_partition rcons_path last_rcons sa/= asc. +rewrite {2}/variation size_rcons -[leLHS]addr0 big_nat_recr//= lerD//. +rewrite /variation !big_nat ler_sum// => k; rewrite leq0n /= => ks. +rewrite nth_rcons// ks -cats1 -cat_cons nth_cat /= ltnS (ltnW ks). +by rewrite ![in leRHS](set_nth_default c)//= ltnS ltnW. +Qed. + +Lemma bounded_variationr a c b f : a <= c -> c <= b -> BV a b f -> BV c b f. +Proof. +rewrite le_eqVlt => /predU1P[<-{c}//|ac]. +rewrite le_eqVlt => /predU1P[<-{b} ?|cb]; first exact: bounded_variationxx. +move=> [x Hx]; exists x => _ [s cbs] <-. +rewrite (@le_trans _ _ (variation a b f (c :: s)))//; last first. + apply/Hx/variations_variation; case: cbs => cs csb. + by rewrite /itv_partition/= ac/= cs. +by rewrite {2}/variation/= -[leLHS]add0r big_nat_recl//= lerD. +Qed. + +Lemma variations_opp a b f : + variations (- b) (- a) (f \o -%R) = variations a b f. +Proof. +rewrite eqEsubset; split=> [_ [s bas <-]| _ [s abs <-]]. + eexists; last exact: variation_rev_opp. + by move/itv_partition_rev : bas; rewrite !opprK. +eexists; last by exact/esym/variation_opp_rev. +exact: itv_partition_rev abs. +Qed. + +Lemma nondecreasing_bounded_variation a b f : + {in `[a, b] &, {homo f : x y / x <= y}} -> BV a b f. +Proof. +move=> incf; exists (f b - f a) => ? [l pabl <-]; rewrite le_eqVlt. +by rewrite nondecreasing_variation// eqxx. +Qed. + +End bounded_variation. + +Section total_variation. +Context {R : realType}. +Implicit Types (a b : R) (f : R -> R). + +Definition total_variation a b f := + ereal_sup [set x%:E | x in variations a b f]. + +Notation BV := bounded_variation. +Notation TV := total_variation. + +Lemma total_variationxx a f : TV a a f = 0%E. +Proof. by rewrite /total_variation variationsxx image_set1 ereal_sup1. Qed. + +Lemma total_variation_ge a b f : a <= b -> (`|f b - f a|%:E <= TV a b f)%E. +Proof. +rewrite le_eqVlt => /predU1P[<-{b}|ab]. + by rewrite total_variationxx subrr normr0. +apply: ereal_sup_ub => /=; exists (variation a b f [:: b]). + exact/variations_variation/itv_partition1. +by rewrite /variation/= big_nat_recr//= big_nil add0r. +Qed. + +Lemma total_variation_ge0 a b f : a <= b -> (0 <= TV a b f)%E. +Proof. by move=> ab; rewrite (le_trans _ (total_variation_ge _ ab)). Qed. + +Lemma bounded_variationP a b f : a <= b -> BV a b f <-> TV a b f \is a fin_num. +Proof. +rewrite le_eqVlt => /predU1P[<-{b}|ab]. + by rewrite total_variationxx; split => // ?; exact: bounded_variationxx. +rewrite ge0_fin_numE; last exact/total_variation_ge0/ltW. +split=> [abf|]. + by rewrite /total_variation ereal_sup_EFin ?ltry//; exact: variations_neq0. +rewrite /total_variation /bounded_variation ltey => /eqP; apply: contra_notP. +by move/hasNub_ereal_sup; apply; exact: variations_neq0. +Qed. + +Lemma nondecreasing_total_variation a b f : a <= b -> + {in `[a, b] &, nondecreasing_fun f} -> TV a b f = (f b - f a)%:E. +Proof. +rewrite le_eqVlt => /predU1P[<-{b} ?|ab ndf]. + by rewrite total_variationxx subrr. +rewrite /total_variation [X in ereal_sup X](_ : _ = [set (f b - f a)%:E]). + by rewrite ereal_sup1. +apply/seteqP; split => [x/= [s [t abt <-{s} <-{x}]]|x/= ->{x}]. + by rewrite nondecreasing_variation. +exists (variation a b f [:: b]) => //. + exact/variations_variation/itv_partition1. +by rewrite nondecreasing_variation//; exact: itv_partition1. +Qed. + +Lemma total_variationN a b f : TV a b (\- f) = TV a b f. +Proof. by rewrite /TV; rewrite variationsN. Qed. + +Lemma total_variation_le a b f g : a <= b -> + (TV a b (f \+ g)%R <= TV a b f + TV a b g)%E. +Proof. +rewrite le_eqVlt => /predU1P[<-{b}|ab]. + by rewrite !total_variationxx adde0. +have [abf|abf] := pselect (BV a b f); last first. + rewrite {2}/total_variation hasNub_ereal_sup//; last first. + exact: variations_neq0. + rewrite addye ?leey// -ltNye (@lt_le_trans _ _ 0%E)//. + exact/total_variation_ge0/ltW. +have [abg|abg] := pselect (BV a b g); last first. + rewrite {3}/total_variation hasNub_ereal_sup//; last first. + exact: variations_neq0. + rewrite addey ?leey// -ltNye (@lt_le_trans _ _ 0%E)//. + exact/total_variation_ge0/ltW. +move: abf abg => [r abfr] [s abgs]. +have BVabfg : BV a b (f \+ g). + by apply: bounded_variationD => //; [exists r|exists s]. +apply: ub_ereal_sup => y /= [r' [s' abs <-{r'} <-{y}]]. +apply: (@le_trans _ _ (variation a b f s' + variation a b g s')%:E). + exact: variation_le. +by rewrite EFinD lee_add// ereal_sup_le//; + (eexists; last exact: lexx); (eexists; last reflexivity); + exact: variations_variation. +Qed. + +Let total_variationD1 a b c f : a <= c -> c <= b -> + (TV a b f >= TV a c f + TV c b f)%E. +Proof. +rewrite le_eqVlt=> /predU1P[<-{c}|ac]; first by rewrite total_variationxx add0e. +rewrite le_eqVlt=> /predU1P[<-{b}|cb]; first by rewrite total_variationxx adde0. +have [abf|abf] := pselect (BV a b f); last first. + rewrite {3}/total_variation hasNub_ereal_sup ?leey//. + by apply: variations_neq0 => //; rewrite (lt_trans ac). +have H s t : itv_partition a c s -> itv_partition c b t -> + (TV a b f >= (variation a c f s)%:E + (variation c b f t)%:E)%E. + move=> acs cbt; rewrite -EFinD; apply: ereal_sup_le. + exists (variation a b f (s ++ t))%:E. + eexists; last reflexivity. + by exists (s ++ t) => //; exact: itv_partition_cat acs cbt. + by rewrite variationD// ltW. +rewrite [leRHS]ereal_sup_EFin//; last first. + by apply: variations_neq0; rewrite (lt_trans ac). +have acf : BV a c f := bounded_variationl (ltW ac) (ltW cb) abf. +have cbf : BV c b f := bounded_variationr (ltW ac) (ltW cb) abf. +rewrite {1 2}/total_variation ereal_sup_EFin//; last exact: variations_neq0. +rewrite ereal_sup_EFin//; last exact: variations_neq0. +rewrite -EFinD -sup_sumE; last 2 first. + by split => //; exact: variations_neq0. + by split => //; exact: variations_neq0. +apply: le_sup. +- move=> r/= [s [l' acl' <-{s}]] [t [l cbl] <-{t} <-{r}]. + exists (variation a b f (l' ++ l)); split; last by rewrite variationD// ltW. + exact/variations_variation/(itv_partition_cat acl' cbl). +- have [r acfr] := variations_neq0 f ac. + have [s cbfs] := variations_neq0 f cb. + by exists (r + s); exists r => //; exists s. +- by split => //; apply: variations_neq0; rewrite (lt_trans ac). +Qed. + +Let total_variationD2 a b c f : a <= c -> c <= b -> + (TV a b f <= TV a c f + TV c b f)%E. +Proof. +rewrite le_eqVlt => /predU1P[<-{c}|ac]; first by rewrite total_variationxx add0e. +rewrite le_eqVlt => /predU1P[<-{b}|cb]; first by rewrite total_variationxx adde0. +case : (pselect (bounded_variation a c f)); first last. + move=> nbdac; have /eqP -> : TV a c f == +oo%E. + have: (-oo < TV a c f)%E by apply: (lt_le_trans _ (total_variation_ge0 f (ltW ac))). + by rewrite ltNye_eq => /orP [] => // /bounded_variationP => /(_ (ltW ac)). + by rewrite addye ?leey // -ltNye (@lt_le_trans _ _ 0)%E // ?total_variation_ge0 // ltW. +case : (pselect (bounded_variation c b f)); first last. + move=> nbdac; have /eqP -> : TV c b f == +oo%E. + have: (-oo < TV c b f)%E. + exact: (lt_le_trans _ (total_variation_ge0 f (ltW cb))). + by rewrite ltNye_eq => /orP [] => // /bounded_variationP => /(_ (ltW cb)). + rewrite addey ?leey // -ltNye (@lt_le_trans _ _ 0%E)//. + exact/total_variation_ge0/ltW. +move=> bdAB bdAC. +rewrite /total_variation [x in (x + _)%E]ereal_sup_EFin //; last first. + exact: variations_neq0. +rewrite [x in (_ + x)%E]ereal_sup_EFin //; last exact: variations_neq0. +rewrite -EFinD -sup_sumE /has_sup; [|(by split => //; exact: variations_neq0)..]. +apply: ub_ereal_sup => ? [? [l pacl <- <-]]; rewrite lee_fin. +apply: (le_trans (variation_itv_partitionLR _ ac _ _)) => //. +apply: sup_ub => /=. + case: bdAB => M ubdM; case: bdAC => N ubdN; exists (N + M). + move=> q [?] [i pabi <-] [? [j pbcj <-]] <-. + by apply: lerD; [apply: ubdN;exists i|apply:ubdM;exists j]. +exists (variation a c f (itv_partitionL l c)). + by apply: variations_variation; exact: itv_partitionLP pacl. +exists (variation c b f (itv_partitionR l c)). + by apply: variations_variation; exact: itv_partitionRP pacl. +by rewrite variationD// ?ltW//; + [exact: itv_partitionLP pacl|exact: itv_partitionRP pacl]. +Qed. + +Lemma total_variationD a b c f : a <= c -> c <= b -> + (TV a b f = TV a c f + TV c b f)%E. +Proof. +by move=> ac cb; apply/eqP; rewrite eq_le; apply/andP; split; + [exact: total_variationD2|exact: total_variationD1]. +Qed. + +End total_variation. + +Section variation_continuity. +Context {R : realType}. +Implicit Type f : R -> R. + +Notation BV := bounded_variation. +Notation TV := total_variation. + +Definition neg_tv a f (x : R) : \bar R := ((TV a x f - (f x)%:E) * 2^-1%:E)%E. + +Definition pos_tv a f (x : R) : \bar R := neg_tv a (\- f) x. + +Lemma neg_tv_nondecreasing a b f : + {in `[a, b] &, nondecreasing_fun (neg_tv a f)}. +Proof. +move=> x y xab yab xy; have ax : a <= x. + by move: xab; rewrite in_itv //= => /andP []. +rewrite /neg_tv lee_pmul2r // lee_subr_addl // addeCA -EFinB. +rewrite [TV a y _](total_variationD _ ax xy) //. +apply: lee_add => //; apply: le_trans; last exact: total_variation_ge. +by rewrite lee_fin ler_norm. +Qed. + +Lemma bounded_variation_pos_neg_tvE a b f : BV a b f -> + {in `[a, b], f =1 (fine \o pos_tv a f) \- (fine \o neg_tv a f)}. +Proof. +move=> bdabf x; rewrite in_itv /= => /andP [ax xb]. +have ffin: TV a x f \is a fin_num. + apply/bounded_variationP => //. + exact: (bounded_variationl _ xb). +have Nffin : TV a x (\- f) \is a fin_num. + apply/bounded_variationP => //; apply/bounded_variationN. + exact: (bounded_variationl ax xb). +rewrite /pos_tv /neg_tv /= total_variationN -fineB -?muleBl // ?fineM //. +- rewrite addeAC oppeD //= ?fin_num_adde_defl //. + by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -Num.Theory.splitr. +- by rewrite fin_numB ?fin_numD ?ffin; apply/andP; split. +- by apply: fin_num_adde_defl; rewrite fin_numN fin_numD; apply/andP; split. +- by rewrite fin_numM // fin_numD; apply/andP; split. +- by rewrite fin_numM // fin_numD; apply/andP; split. +Qed. + +Lemma fine_neg_tv_nondecreasing a b f : BV a b f -> + {in `[a, b] &, nondecreasing_fun (fine \o neg_tv a f)}. +Proof. +move=> bdv p q pab qab pq /=. +move: (pab) (qab); rewrite ?in_itv /= => /andP[ap pb] /andP[aq qb]. +apply: fine_le; rewrite /neg_tv ?fin_numM // ?fin_numB /=. +- apply/andP; split => //; apply/bounded_variationP => //. + exact: (bounded_variationl _ pb). +- apply/andP; split => //; apply/bounded_variationP => //. + exact: (bounded_variationl _ qb). +exact: (neg_tv_nondecreasing _ pab). +Qed. + +Lemma neg_tv_bounded_variation a b f : BV a b f -> BV a b (fine \o neg_tv a f). +Proof. +move=> ?; apply: nondecreasing_bounded_variation. +exact: fine_neg_tv_nondecreasing. +Qed. + +Lemma total_variation_right_continuous a b x f : a <= x -> x < b -> + f @ x^'+ --> f x -> + BV a b f -> + fine \o TV a ^~ f @ x^'+ --> fine (TV a x f). +Proof. +move=> ax xb ctsf bvf; have ? : a <= b by apply:ltW; apply: (le_lt_trans ax). +apply/cvgrPdist_lt=> _/posnumP[eps]. +have ? : Filter (nbhs x^'+) by exact: at_right_proper_filter. +have xbl := ltW xb. +have xbfin : TV x b f \is a fin_num. + by apply/bounded_variationP => //; exact: (bounded_variationr _ _ bvf). +have [//|?] := @ub_ereal_sup_adherent R _ (eps%:num / 2) _ xbfin. +case=> ? [l + <- <-]; rewrite -/(total_variation x b f). +move: l => [|i j]. + by move=> /itv_partition_nil /eqP; rewrite lt_eqF. +move=> [/= /andP[xi ij /eqP ijb]] tv_eps. +apply: filter_app (nbhs_right_ge _). +apply: filter_app (nbhs_right_lt xi). +have e20 : 0 < eps%:num / 2 by []. +move/cvgrPdist_lt/(_ (eps%:num/2) e20) : ctsf; apply: filter_app. +near=> t => fxt ti xt; have ta : a <= t by exact: (le_trans ax). +have tb : t <= b by rewrite (le_trans (ltW ti))// -ijb path_lt_le_last. +rewrite -fineB; last 2 first. + by apply/bounded_variationP => //; exact: bounded_variationl bvf. + by apply/bounded_variationP => //; exact: bounded_variationl bvf. +rewrite (total_variationD _ ax xt). +have tbfin : TV t b f \is a fin_num. + by apply/bounded_variationP => //; exact: (@bounded_variationr _ a). +have xtfin : TV x t f \is a fin_num. + apply/bounded_variationP => //; apply: (@bounded_variationl _ _ _ b) => //. + exact: (@bounded_variationr _ a). +rewrite oppeD ?fin_num_adde_defl// addeA subee //; first last. + by apply/bounded_variationP => //; exact: (@bounded_variationl _ _ _ b). +rewrite sub0e fineN normrN ger0_norm; last first. + by rewrite fine_ge0// total_variation_ge0. +move: (tv_eps); rewrite (total_variationD f _ tb) //. +move: xt; rewrite le_eqVlt => /predU1P[->|xt]. + by rewrite total_variationxx/=. +have : variation x b f (i :: j) <= variation x t f (t :: nil) + + variation t b f (i :: j). + rewrite variationD//; last 2 first. + exact: itv_partition1. + by rewrite /itv_partition/= ti ij ijb. + exact: le_variation. +rewrite -lee_fin => /lt_le_trans /[apply]. +rewrite {1}variation_prev; last exact: itv_partition1. +rewrite /= -addeA -lte_subr_addr; last by rewrite fin_numD; apply/andP. +rewrite EFinD -lte_fin ?fineK // oppeD //= ?fin_num_adde_defl // opprK addeA. +move/lt_trans; apply. +rewrite [x in (_ < x%:E)%E]Num.Theory.splitr EFinD addeC lte_add2lE //. +rewrite -addeA. +apply: (@le_lt_trans _ _ (variation x t f (t :: nil))%:E). + rewrite [in leRHS]variation_prev; last exact: itv_partition1. + rewrite gee_addl // sube_le0; apply: ereal_sup_ub => /=. + exists (variation t b f (i :: j)) => //; apply: variations_variation. + by rewrite /itv_partition/= ijb ij ti. +by rewrite /variation/= big_nat_recr//= big_nil add0r distrC lte_fin. +Unshelve. all: by end_near. Qed. + +Lemma neg_tv_right_continuous a x b f : a <= x -> x < b -> + BV a b f -> + f @ x^'+ --> f x -> + fine \o neg_tv a f @ x^'+ --> fine (neg_tv a f x). +Proof. +move=> ax ? bvf fcts; have xb : x <= b by exact: ltW. +have xbfin : TV a x f \is a fin_num. + by apply/bounded_variationP => //; exact: bounded_variationl bvf. +apply: fine_cvg; rewrite /neg_tv fineM // ?fin_numB ?xbfin //= EFinM. +under eq_fun => i do rewrite EFinN. +apply: (@cvg_trans _ (((TV a n f - (f n)%:E) * 2^-1%:E)%E @[n --> x^'+])). + exact: cvg_id. +apply: cvgeMr; first by []. +rewrite fineD; [|by []..]. +rewrite EFinB; apply: cvgeB; [by []| |]. + apply/ fine_cvgP; split; first exists (b - x). + - by rewrite /= subr_gt0. + - move=> t /= xtbx xt; have ? : a <= t. + by apply: ltW; apply: (le_lt_trans ax). + apply/bounded_variationP => //. + apply: bounded_variationl bvf => //. + move: xtbx; rewrite distrC ger0_norm ?subr_ge0; last by exact: ltW. + by rewrite ltrBrDr -addrA [-_ + _]addrC subrr addr0 => /ltW. + by apply: total_variation_right_continuous => //; last exact: bvf. +apply: cvg_comp; first exact: fcts. +apply/ fine_cvgP; split; first by near=> t => //. +by have -> : fine \o EFin = id by move=> ?; rewrite funeqE => ? /=. +Unshelve. all: by end_near. Qed. + +Lemma total_variation_opp a b f : TV a b f = TV (- b) (- a) (f \o -%R). +Proof. by rewrite /total_variation variations_opp. Qed. + +Lemma total_variation_left_continuous a b x f : a < x -> x <= b -> + f @ x^'- --> f x -> + BV a b f -> + fine \o TV a ^~ f @ x^'- --> fine (TV a x f). +Proof. +move=> ax xb fNcts bvf. +apply/cvg_at_leftNP; rewrite total_variation_opp. +have bvNf : BV (-b) (-a) (f \o -%R). + by case: bvf => M; rewrite -variations_opp => ?; exists M. +have bx : - b <= - x by rewrite lerNl opprK. +have xa : - x < - a by rewrite ltrNl opprK. +have ? : - x <= - a by exact: ltW. +have ? : Filter (nbhs (-x)^'+) by exact: at_right_proper_filter. +have -> : fine (TV (-x) (-a) (f \o -%R)) = + fine (TV (-b) (-a) (f \o -%R)) - fine (TV (-b) (-x) (f \o -%R)). + apply/eqP; rewrite -subr_eq opprK addrC. + rewrite -fineD; last 2 first. + by apply/bounded_variationP => //; exact: bounded_variationl bvNf. + by apply/bounded_variationP => //; exact: bounded_variationr bvNf. + by rewrite -total_variationD. +have /near_eq_cvg/cvg_trans : {near (- x)^'+, + (fun t => fine (TV (- b) (- a) (f \o -%R)) - fine (TV (- b) t (f \o -%R))) =1 + (fine \o (TV a)^~ f) \o -%R}. + apply: filter_app (nbhs_right_lt xa). + apply: filter_app (nbhs_right_ge _). + near=> t => xt ta; have ? : -b <= t by exact: (le_trans bx). + have ? : t <= -a by exact: ltW. + apply/eqP; rewrite eq_sym -subr_eq opprK addrC. + rewrite /= [TV a _ f]total_variation_opp opprK -fineD; last first. + by apply/bounded_variationP => //; apply: bounded_variationr bvNf. + by apply/bounded_variationP => //; apply: bounded_variationl bvNf. + by rewrite -total_variationD. +apply. +apply: cvgB; first exact: cvg_cst. +apply: (total_variation_right_continuous _ _ _ bvNf). +- by rewrite ler_oppl opprK //. +- by rewrite ltr_oppl opprK //. +by apply/cvg_at_leftNP; rewrite /= opprK. +Unshelve. all: by end_near. Qed. + +Lemma total_variation_continuous a b (f : R -> R) : a < b -> + {within `[a,b], continuous f} -> + BV a b f -> + {within `[a,b], continuous (fine \o TV a ^~ f)}. +Proof. +move=> ab /(@continuous_within_itvP _ _ _ _ ab) [int [l r]] bdf. +apply/continuous_within_itvP; (repeat split) => //. +- move=> x /[dup] xab; rewrite in_itv /= => /andP [ax xb]. + apply/left_right_continuousP; split. + apply: (total_variation_left_continuous _ (ltW xb)) => //. + by have /left_right_continuousP [] := int x xab. + apply: (total_variation_right_continuous _ xb) => //; first exact: ltW. + by have /left_right_continuousP [] := int x xab. +- exact: (total_variation_right_continuous _ ab). +- exact: (total_variation_left_continuous ab). +Qed. + +End variation_continuity. diff --git a/theories/topology.v b/theories/topology.v index df5e6d2a63..22dcb838c4 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -304,6 +304,7 @@ Require Import reals signed. (* cover-based definition of compactness *) (* near_covering == a reformulation of covering compact *) (* better suited for use with `near` *) +(* near_covering_within == equivalent definition of near_covering *) (* kolmogorov_space T <-> T is a Kolmogorov space (T0) *) (* accessible_space T <-> T is an accessible space (T1) *) (* close x y <-> x and y are arbitrarily close w.r.t. *) @@ -452,26 +453,29 @@ Require Import reals signed. (* *) (* ### Function space topologies *) (* ``` *) -(* {uniform` A -> V} == the space U -> V, equipped with the topology of *) -(* uniform convergence from a set A to V, where *) -(* V is a uniformType *) -(* {uniform U -> V} := {uniform` [set: U] -> V} *) -(* {uniform A, F --> f} == F converges to f in {uniform A -> V} *) -(* {uniform, F --> f} := {uniform setT, F --> f} *) -(* {ptws U -> V} == the space U -> V, equipped with the topology of *) -(* pointwise convergence from U to V, where V is a *) -(* topologicalType *) -(* This is a notation for @fct_Pointwise U V. *) -(* {ptws, F --> f} == F converges to f in {ptws U -> V} *) -(* {family fam, U -> V} == The space U -> V, equipped with the supremum *) -(* topology of {uniform A -> f} for each A in 'fam' *) -(* In particular {family compact, U -> V} is the *) -(* topology of compact convergence. *) -(* {family fam, F --> f} == F converges to f in {family fam, U -> V} *) +(* {uniform` A -> V} == the space U -> V, equipped with the topology *) +(* of uniform convergence from a set A to V, where *) +(* V is a uniformType *) +(* {uniform U -> V} := {uniform` [set: U] -> V} *) +(* {uniform A, F --> f} == F converges to f in {uniform A -> V} *) +(* {uniform, F --> f} := {uniform setT, F --> f} *) +(* {ptws U -> V} == the space U -> V, equipped with the topology of *) +(* pointwise convergence from U to V, where V is *) +(* a topologicalType *) +(* This is a notation for @fct_Pointwise U V. *) +(* {ptws, F --> f} == F converges to f in {ptws U -> V} *) +(* {family fam, U -> V} == the space U -> V, equipped with the supremum *) +(* topology of {uniform A -> f} for each A in *) +(* 'fam' *) +(* In particular {family compact, U -> V} is the *) +(* topology of compact convergence. *) +(* {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} *) (* *) -(* dense S == the set (S : set T) is dense in T, with T of *) -(* type topologicalType *) -(* weak_pseudoMetricType == the metric space for weak topologies *) +(* dense S == the set (S : set T) is dense in T, with T of *) +(* type topologicalType *) +(* weak_pseudoMetricType == the metric space for weak topologies *) (* ``` *) (* *) (* ### Subspaces of topological spaces *) @@ -558,6 +562,10 @@ Reserved Notation "{ 'family' fam , U -> V }" (at level 0, U at level 69, format "{ 'family' fam , U -> V }"). Reserved Notation "{ 'family' fam , F --> f }" (at level 0, F at level 69, format "{ 'family' fam , F --> f }"). +Reserved Notation "{ 'compact-open' , U -> V }" + (at level 0, U at level 69, format "{ 'compact-open' , U -> V }"). +Reserved Notation "{ 'compact-open' , F --> f }" + (at level 0, F at level 69, format "{ 'compact-open' , F --> f }"). Set Implicit Arguments. Unset Strict Implicit. @@ -1208,7 +1216,7 @@ Qed. Lemma filter_bigI T (I : choiceType) (D : {fset I}) (f : I -> set T) (F : set_system T) : Filter F -> (forall i, i \in D -> F (f i)) -> - F (\bigcap_(i in [set i | i \in D]) f i). + F (\bigcap_(i in [set` D]) f i). Proof. move=> FF FfD. suff: F [set p | forall i, i \in enum_fset D -> f i p] by []. @@ -1621,6 +1629,12 @@ Qed. Canonical within_filter_on T D (F : filter_on T) := FilterType (within D F) (within_filter _ _). +Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T) + (F : set (set T)) (P : set T) : + Filter F -> (forall i, i \in D -> F [set j | P j -> f i j]) -> + F ([set j | P j -> (\bigcap_(i in [set` D]) f i) j]). +Proof. move=> FF FfD; exact: (@filter_bigI T I D f _ (within_filter P FF)). Qed. + Definition subset_filter {T} (F : set_system T) (D : set T) := [set P : set {x | D x} | F [set x | forall Dx : D x, P (exist _ x Dx)]]. Arguments subset_filter {T} F D _. @@ -1645,8 +1659,7 @@ Qed. (* For using near on sets in a filter *) Section NearSet. - -Context {T : choiceType} {Y : filteredType T}. +Context {Y : Type}. Context (F : set_system Y) (PF : ProperFilter F). Definition powerset_filter_from : set_system (set Y) := filter_from @@ -1706,6 +1719,41 @@ Qed. End NearSet. +Lemma near_powerset_map {T U : Type} (f : T -> U) (F : set_system T) + (P : set U -> Prop) : + ProperFilter F -> + (\forall y \near powerset_filter_from (f x @[x --> F]), P y) -> + (\forall y \near powerset_filter_from F, P (f @` y)). +Proof. +move=> FF [] G /= [Gf Gs [D GD GP]]. +have PpF : ProperFilter (powerset_filter_from F). + exact: powerset_filter_from_filter. +have /= := Gf _ GD; rewrite nbhs_simpl => FfD. +near=> M; apply: GP; apply: (Gs D) => //. + apply: filterS; first exact: preimage_image. + exact: (near (near_small_set _) M). +have : M `<=` f @^-1` D by exact: (near (small_set_sub FfD) M). +by move/image_subset/subset_trans; apply; exact: image_preimage_subset. +Unshelve. all: by end_near. Qed. + +Lemma near_powerset_map_monoE {T U : Type} (f : T -> U) (F : set_system T) + (P : set U -> Prop) : + (forall X Y, X `<=` Y -> P Y -> P X) -> + ProperFilter F -> + (\forall y \near powerset_filter_from F, P (f @` y)) = + (\forall y \near powerset_filter_from (f x @[x --> F]), P y). +Proof. +move=> Pmono FF; rewrite propeqE; split; last exact: near_powerset_map. +case=> G /= [Gf Gs [D GD GP]]. +have PpF : ProperFilter (powerset_filter_from (f x @[x-->F])). + exact: powerset_filter_from_filter. +have /= := Gf _ GD; rewrite nbhs_simpl => FfD; have ffiD : fmap f F (f@` D). + by rewrite /fmap /=; apply: filterS; first exact: preimage_image. +near=> M; have FfM : fmap f F M by exact: (near (near_small_set _) M). +apply: (@Pmono _ (f @` D)); first exact: (near (small_set_sub ffiD) M). +exact: GP. +Unshelve. all: by end_near. Qed. + Section PrincipalFilters. Definition principal_filter {X : Type} (x : X) : set_system X := @@ -2468,6 +2516,22 @@ End Prod_Topology. (** Topology on matrices *) +Lemma fst_open {U V : topologicalType} (A : set (U * V)) : + open A -> open (fst @` A). +Proof. +rewrite !openE => oA z [[a b/=] Aab <-]; rewrite /interior. +have [[P Q] [Pa Qb] pqA] := oA _ Aab; apply: (@filterS _ _ _ P) => // p Pp. +by exists (p, b) => //=; apply: pqA; split=> //=; exact: nbhs_singleton. +Qed. + +Lemma snd_open {U V : topologicalType} (A : set (U * V)) : + open A -> open (snd @` A). +Proof. +rewrite !openE => oA z [[a b/=] Aab <-]; rewrite /interior. +have [[P Q] [Pa Qb] pqA] := oA _ Aab; apply: (@filterS _ _ _ Q) => // q Qq. +by exists (a, q) => //=; apply: pqA; split => //; exact: nbhs_singleton. +Qed. + Section matrix_Topology. Variables (m n : nat) (T : topologicalType). @@ -2978,6 +3042,7 @@ by apply: filter_ex; [exact: PF| exact: filterI]. Qed. End Compact. + Arguments hausdorff_space : clear implicits. Section ClopenSets. @@ -3060,8 +3125,38 @@ Proof. by split; [exact: compact_near_covering| exact: near_covering_compact]. Qed. +Definition near_covering_within (K : set X) := + forall (I : Type) (F : set_system I) (P : I -> X -> Prop), + Filter F -> + (forall x, K x -> \forall x' \near x & i \near F, K x' -> P i x') -> + \near F, K `<=` P F. + +Lemma near_covering_withinP (K : set X) : + near_covering_within K <-> near_covering K. +Proof. +split => cvrW I F P FF cvr; near=> i; + (suff: K `<=` fun q : X => K q -> P i q by move=> + k Kk; exact); near: i. + by apply: cvrW => x /cvr; apply: filter_app; near=> j. +have := cvrW _ _ (fun i q => K q -> P i q) FF. +by apply => x /cvr; apply: filter_app; near=> j => + ?; apply. +Unshelve. all: by end_near. Qed. + End near_covering. +Lemma compact_setM {U V : topologicalType} (P : set U) (Q : set V) : + compact P -> compact Q -> compact (P `*` Q). +Proof. +rewrite !compact_near_coveringP => cptP cptQ I F Pr Ff cvfPQ. +have := cptP I F (fun i u => forall q, Q q -> Pr i (u, q)) Ff. +set R := (R in (R -> _) -> _); suff R' : R. + by move/(_ R'); apply:filter_app; near=> i => + [a b] [Pa Qb]; apply. +rewrite /R => x Px; apply: (@cptQ _ (filter_prod _ _)) => v Qv. +case: (cvfPQ (x, v)) => // [[N G]] /= [[[N1 N2 /= [N1x N2v]]]] N1N2N FG ngPr. +exists (N2, N1`*`G); first by split => //; exists (N1, G). +case=> a [b i] /= [N2a [N1b]] Gi. +by apply: (ngPr (b, a, i)); split => //; exact: N1N2N. +Unshelve. all: by end_near. Qed. + Section Tychonoff. Class UltraFilter T (F : set_system T) := { @@ -3250,7 +3345,6 @@ move=> M [MF ME2 [W] MW /(_ _ MW) VUW]. apply: (@filterS _ _ _ (V `&` W)); last by apply: filterI => //; exact: MF. by move=> t [Vt Wt]; apply: contrapT => Ut; exact: (VUW t). Qed. - Section Precompact. Context {X : topologicalType}. @@ -3291,7 +3385,7 @@ Proof. by move=> AsubB [B' B'subB cptB']; exists B' => // ? ?; exact/B'subB/AsubB. Qed. -Lemma compact_precompact (A B : set X) : +Lemma compact_precompact (A : set X) : hausdorff_space X -> compact A -> precompact A. Proof. move=> h c; rewrite precompactE ( _ : closure A = A)//. @@ -3537,8 +3631,43 @@ move=> /DsubC /= [y /= yfs hyz]; exists (h' y) => //. by rewrite set_imfset /=; exists y. Qed. +Section set_nbhs. +Context {T : topologicalType} (A : set T). + +Definition set_nbhs := \bigcap_(x in A) nbhs x. + +Global Instance set_nbhs_filter : Filter set_nbhs. +Proof. +split => P Q; first by exact: filterT. + by move=> Px Qx x Ax; apply: filterI; [exact: Px | exact: Qx]. +by move=> PQ + x Ax => /(_ _ Ax)/filterS; exact. +Qed. + +Global Instance set_nbhs_pfilter : A!=set0 -> ProperFilter set_nbhs. +Proof. +case=> x Ax; split; last exact: set_nbhs_filter. +by move/(_ x Ax)/nbhs_singleton. +Qed. + +Lemma set_nbhsP (B : set T) : + set_nbhs B <-> (exists C, [/\ open C, A `<=` C & C `<=` B]). +Proof. +split; first last. + by case=> V [? AV /filterS +] x /AV ?; apply; apply: open_nbhs_nbhs. +move=> snB; have Ux x : exists U, A x -> [/\ U x, open U & U `<=` B]. + have [/snB|?] := pselect (A x); last by exists point. + by rewrite nbhsE => -[V [? ? ?]]; exists V. +exists (\bigcup_(x in A) (projT1 (cid (Ux x)))); split. +- by apply: bigcup_open => x Ax; have [] := projT2 (cid (Ux x)). +- by move=> x Ax; exists x => //; have [] := projT2 (cid (Ux x)). +- by move=> x [y Ay]; have [//| _ _] := projT2 (cid (Ux y)); exact. +Qed. + +End set_nbhs. + + Section separated_topologicalType. -Variable (T : topologicalType). +Variable T : topologicalType. Implicit Types x y : T. Local Open Scope classical_set_scope. @@ -3652,6 +3781,13 @@ rewrite setIC => /disjoints_subset VUc; exists U; repeat split => //. by rewrite inE; apply: VUc; rewrite -inE. Qed. +Definition normal_space := + forall A : set T, closed A -> + filter_from (set_nbhs A) closure `=>` set_nbhs A. + +Definition regular_space := + forall a : T, filter_from (nbhs a) closure --> a. + Hypothesis sep : hausdorff_space T. Lemma closeE x y : close x y = (x = y). @@ -3696,6 +3832,27 @@ Proof. move=> f_prop fl; apply: get_unique => // l' fl'; exact: cvgi_unique _ fl' fl. Qed. +Lemma compact_regular (x : T) V : compact V -> nbhs x V -> {for x, regular_space}. +Proof. +move=> cptv Vx; apply: (@compact_cluster_set1 T x _ V) => //. +- apply: filter_from_proper => //; first last. + by move=> ? /nbhs_singleton/subset_closure ?; exists x. + apply: filter_from_filter; first by exists setT; exact: filterT. + move=> P Q Px Qx; exists (P `&` Q); [exact: filterI | exact: closureI]. +- by exists V => //; have /closure_id <- : closed V by exact: compact_closed. +rewrite eqEsubset; split; first last. + move=> _ -> A B [C Cx CA /nbhs_singleton Bx]; exists x; split => //. + by apply/CA/subset_closure; exact: nbhs_singleton. +move=> y /=; apply: contraPeq; move: sep; rewrite open_hausdorff => /[apply]. +move=> [[B A]]/=; rewrite ?inE; case=> By Ax [oB oA BA0]. +apply/existsNP; exists (closure A); apply/existsNP; exists B; apply/not_implyP. +split; first by exists A => //; exact: open_nbhs_nbhs. +apply/not_implyP; split; first exact: open_nbhs_nbhs. +apply/set0P/negP; rewrite negbK; apply/eqP/disjoints_subset. +have /closure_id -> : closed (~` B); first by exact: open_closedC. +by apply/closure_subset/disjoints_subset; rewrite setIC. +Qed. + End separated_topologicalType. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvg_lim`")] @@ -4096,40 +4253,6 @@ Qed. End totally_disconnected. -Section set_nbhs. -Context {T : topologicalType} (A : set T). - -Definition set_nbhs := \bigcap_(x in A) nbhs x. - -Global Instance set_nbhs_filter : Filter set_nbhs. -Proof. -split => P Q; first by exact: filterT. - by move=> Px Qx x Ax; apply: filterI; [exact: Px | exact: Qx]. -by move=> PQ + x Ax => /(_ _ Ax)/filterS; exact. -Qed. - -Global Instance set_nbhs_pfilter : A!=set0 -> ProperFilter set_nbhs. -Proof. -case=> x Ax; split; last exact: set_nbhs_filter. -by move/(_ x Ax)/nbhs_singleton. -Qed. - -Lemma set_nbhsP (B : set T) : - set_nbhs B <-> (exists C, [/\ open C, A `<=` C & C `<=` B]). -Proof. -split; first last. - by case=> V [? AV /filterS +] x /AV ?; apply; apply: open_nbhs_nbhs. -move=> snB; have Ux x : exists U, A x -> [/\ U x, open U & U `<=` B]. - have [/snB|?] := pselect (A x); last by exists point. - by rewrite nbhsE => -[V [? ? ?]]; exists V. -exists (\bigcup_(x in A) (projT1 (cid (Ux x)))); split. -- by apply: bigcup_open => x Ax; have [] := projT2 (cid (Ux x)). -- by move=> x Ax; exists x => //; have [] := projT2 (cid (Ux x)). -- by move=> x [y Ay]; have [//| _ _] := projT2 (cid (Ux y)); exact. -Qed. - -End set_nbhs. - (** Uniform spaces *) Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope. @@ -5033,13 +5156,13 @@ Lemma ball_triangle (y x z : M) (e1 e2 : R) : ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z. Proof. exact: ball_triangle_subproof. Qed. -Lemma nbhsx_ballx (x : M) (eps : {posnum R}) : nbhs x (ball x eps%:num). -Proof. by apply/nbhs_ballP; exists eps%:num => /=. Qed. +Lemma nbhsx_ballx (x : M) (eps : R) : 0 < eps -> nbhs x (ball x eps). +Proof. by move=> e0; apply/nbhs_ballP; exists eps. Qed. Lemma open_nbhs_ball (x : M) (eps : {posnum R}) : open_nbhs x ((ball x eps%:num)^°). Proof. split; first exact: open_interior. -by apply: nbhs_singleton; apply: nbhs_interior; apply:nbhsx_ballx. +by apply: nbhs_singleton; apply: nbhs_interior; exact: nbhsx_ballx. Qed. Lemma le_ball (x : M) (e1 e2 : R) : e1 <= e2 -> ball x e1 `<=` ball x e2. @@ -5054,8 +5177,7 @@ apply: Build_ProperFilter; rewrite -entourage_ballE => A [_/posnumP[e] sbeA]. by exists (point, point); apply: sbeA; apply: ballxx. Qed. -Lemma near_ball (y : M) (eps : {posnum R}) : - \forall y' \near y, ball y eps%:num y'. +Lemma near_ball (y : M) (eps : R) : 0 < eps -> \forall y' \near y, ball y eps y'. Proof. exact: nbhsx_ballx. Qed. Lemma dnbhs_ball (a : M) (e : R) : (0 < e)%R -> a^' (ball a e `\ a). @@ -5113,6 +5235,9 @@ End pseudoMetricType_numDomainType. #[global] Hint Resolve close_refl : core. Arguments close_cvg {T} F1 F2 {FF2} _. +Arguments nbhsx_ballx {R M} x eps. +Arguments near_ball {R M} y eps. + #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `cvg_ball`")] Notation app_cvg_locally := cvg_ball (only parsing). @@ -5707,10 +5832,10 @@ Lemma Rhausdorff (R : realFieldType) : hausdorff_space R. Proof. move=> x y clxy; apply/eqP; rewrite eq_le. apply/in_segment_addgt0Pr => _ /posnumP[e]. -rewrite in_itv /= -ler_distl; set he := (e%:num / 2)%:pos. -have [z [zx_he yz_he]] := clxy _ _ (nbhsx_ballx x he) (nbhsx_ballx y he). +rewrite in_itv /= -ler_distl; have he : 0 < (e%:num / 2) by []. +have [z [zx_he yz_he]] := clxy _ _ (nbhsx_ballx x _ he) (nbhsx_ballx y _ he). have := ball_triangle yz_he (ball_sym zx_he). -by rewrite -mulr2n -mulr_natr divfK // => /ltW. +by rewrite -mulr2n -(mulr_natr (_ / _) 2) divfK// => /ltW. Qed. Section RestrictedUniformTopology. @@ -5774,7 +5899,6 @@ Lemma pointwise_cvgE {U : Type} {V : topologicalType} {ptws, F --> f} = (F --> (f : {ptws U -> V})). Proof. by []. Qed. - Definition uniform_fun_family {U} V (fam : set U -> Prop) := U -> V. Notation "{ 'family' fam , U -> V }" := (@uniform_fun_family U V fam). @@ -5973,6 +6097,177 @@ move=> entE famA; have /fam_cvgP /(_ A) : (nbhs f --> f) by []; apply => //. by apply uniform_nbhs; exists E; split. Qed. +Lemma fam_compact_nbhs {U : topologicalType} {V : uniformType} + (A : set U) (O : set V) (f : {family compact, U -> V}) : + open O -> f @` A `<=` O -> compact A -> continuous f -> + nbhs (f : {family compact, U -> V}) [set g | forall y, A y -> O (g y)]. +Proof. +move=> oO fAO /[dup] cA /compact_near_coveringP/near_covering_withinP cfA ctsf. +near=> z => /=; (suff: A `<=` [set y | O (z y)] by exact); near: z. +apply: cfA => x Ax; have : O (f x) by exact: fAO. +move: (oO); rewrite openE /= => /[apply] /[dup] /ctsf Ofx /=. +rewrite /interior -nbhs_entourageE => -[E entE EfO]. +exists (f @^-1` to_set (split_ent E) (f x), + [set g | forall w, A w -> split_ent E (f w, g w)]). + split => //=; last exact: fam_nbhs. + by apply: ctsf; rewrite /= -nbhs_entourageE; exists (split_ent E). +case=> y g [/= Efxy] AEg Ay; apply: EfO; apply: subset_split_ent => //. +by exists (f y) => //=; exact: AEg. +Unshelve. all: by end_near. Qed. + +(**md It turns out `{family compact, U -> V}` can be generalized to only assume + `topologicalType` on `V`. This topology is called the compact-open topology. + This topology is special because it is the _only_ topology that will allow + `curry`/`uncurry` to be continuous. *) + +Section compact_open. +Context {T U : topologicalType}. + +Definition compact_open : Type := T -> U. + +Section compact_open_setwise. +Context {K : set T}. + +Definition compact_openK := let _ := K in compact_open. + +Definition compact_openK_nbhs (f : compact_openK) := + filter_from + [set O | f @` K `<=` O /\ open O] + (fun O => [set g | g @` K `<=` O]). + +Global Instance compact_openK_nbhs_filter (f : compact_openK) : + ProperFilter (compact_openK_nbhs f). +Proof. +split; first by case=> g [gKO oO] /(_ f); apply. +apply: filter_from_filter; first by exists setT; split => //; exact: openT. +move=> P Q [fKP oP] [fKQ oQ]; exists (P `&` Q); first split. +- by move=> ? [z Kz M-]; split; [apply: fKP | apply: fKQ]; exists z. +- exact: openI. +by move=> g /= gPQ; split; exact: (subset_trans gPQ). +Qed. + +HB.instance Definition _ := Pointed.on compact_openK. + +HB.instance Definition _ := hasNbhs.Build compact_openK compact_openK_nbhs. + +Definition compact_open_of_nbhs := [set A : set compact_openK | A `<=` nbhs^~ A]. + +Lemma compact_openK_nbhsE_subproof (p : compact_openK) : + compact_openK_nbhs p = + [set A | exists B : set compact_openK, + [/\ compact_open_of_nbhs B, B p & B `<=` A]]. +Proof. +rewrite eqEsubset; split => A /=. + case=> B /= [fKB oB gKBA]; exists [set g | g @` K `<=` B]; split => //. + by move=> h /= hKB; exists B. +by case=> B [oB Bf /filterS]; apply; exact: oB. +Qed. + +Lemma compact_openK_openE_subproof : + compact_open_of_nbhs = [set A | A `<=` compact_openK_nbhs^~ A]. +Proof. by []. Qed. + +HB.instance Definition _ := + Nbhs_isTopological.Build compact_openK compact_openK_nbhs_filter + compact_openK_nbhsE_subproof compact_openK_openE_subproof. + +End compact_open_setwise. + +HB.instance Definition _ := Pointed.on compact_open. + +Definition compact_open_def := + sup_topology (fun i : sigT (@compact T) => + Topological.class (@compact_openK (projT1 i))). + +HB.instance Definition _ := Nbhs.copy compact_open compact_open_def. + +HB.instance Definition _ : Nbhs_isTopological compact_open := + Topological.copy compact_open compact_open_def. + +Lemma compact_open_cvgP (F : set_system compact_open) + (f : compact_open) : + Filter F -> + F --> f <-> forall K O, @compact T K -> @open U O -> f @` K `<=` O -> + F [set g | g @` K `<=` O]. +Proof. +move=> FF; split. + by move/cvg_sup => + K O cptK ? ? => /(_ (existT _ _ cptK)); apply; exists O. +move=> fko; apply/cvg_sup => -[A cptK] O /= [C /= [fAC oC]]. +by move/filterS; apply; exact: fko. +Qed. + +Lemma compact_open_open (K : set T) (O : set U) : + compact K -> open O -> open ([set g | g @` K `<=` O] : set compact_open). +Proof. +pose C := [set g | g @` K `<=` O]; move=> cptK oO. +exists [set C]; last by rewrite bigcup_set1. +move=> _ ->; exists (fset1 C) => //; last by rewrite set_fset1 bigcap_set1. +by move=> _ /[!inE] ->; exists (existT _ _ cptK) => // z Cz; exists O. +Qed. + +End compact_open. + +Lemma compact_closedI {T : topologicalType} (A B : set T) : + compact A -> closed B -> compact (A `&` B). +Proof. +move=> cptA clB F PF FAB; have FA : F A by move: FAB; exact: filterS. +(have FB : F B by move: FAB; apply: filterS); have [x [Ax]] := cptA F PF FA. +move=> /[dup] clx; rewrite {1}clusterE => /(_ (closure B)); move: clB. +by rewrite closure_id => /[dup] + <- => <- /(_ FB) Bx; exists x. +Qed. + +Notation "{ 'compact-open' , U -> V }" := (@compact_open U V). +Notation "{ 'compact-open' , F --> f }" := + (F --> (f : @compact_open _ _)). + +Section compact_open_uniform. +Context {U : topologicalType} {V : uniformType}. + +Let small_ent_sub := @small_set_sub _ (@entourage V). + +Lemma compact_open_fam_compactP (f : U -> V) (F : set_system (U -> V)) : + continuous f -> Filter F -> + {compact-open, F --> f} <-> {family compact, F --> f}. +Proof. +move=> ctsf FF; split; first last. + move=> cptF; apply/compact_open_cvgP => K O cptK oO fKO. + apply: cptF; have := fam_compact_nbhs oO fKO cptK ctsf; apply: filter_app. + by near=> g => /= gKO ? [z Kx <-]; exact: gKO. +move/compact_open_cvgP=> cptOF; apply/cvg_sup => -[K cptK R]. +case=> D [[E oE <-] Ekf] /filterS; apply. +move: oE; rewrite openE => /(_ _ Ekf); case => A [J entJ] EKR KfE. +near=> z; apply/KfE/EKR => -[u Kp]; rewrite /= /set_val /= /eqincl /incl. +(have Ku : K u by rewrite inE in Kp); move: u Ku {D Kp}; near: z. +move/compact_near_coveringP/near_covering_withinP : (cptK); apply. +move=> u Ku; near (powerset_filter_from (@entourage V)) => E'. +have entE' : entourage E' by exact: (near (near_small_set _)). +pose C := f @^-1` to_set E' (f u). +pose B := \bigcup_(z in K `&` closure C) interior (to_set E' (f z)). +have oB : open B by apply: bigcup_open => ? ?; exact: open_interior. +have fKB : f @` (K `&` closure C) `<=` B. + move=> _ [z KCz <-]; exists z => //; rewrite /interior. + by rewrite -nbhs_entourageE; exists E'. +have cptKC : compact (K `&` closure C). + by apply: compact_closedI => //; exact: closed_closure. +have := cptOF (K `&` closure C) B cptKC oB fKB. +exists (C, [set g | [set g x | x in K `&` closure C] `<=` B]). + split; last exact: cptOF. + by apply: (ctsf) => //; rewrite /filter_of -nbhs_entourageE; exists E'. +case=> z h /= [Cz KB Kz]. +case: (KB (h z)); first by exists z; split => //; exact: subset_closure. +move=> w [Kw Cw /interior_subset Jfwhz]; apply: subset_split_ent => //. +exists (f w); last apply: (near (small_ent_sub _) E') => //. +apply: subset_split_ent => //; exists (f u). + by apply/entourage_sym; apply: (near (small_ent_sub _) E'). +have [] := Cw (f@^-1` (to_set E' (f w))). + by apply: ctsf; rewrite /= -nbhs_entourageE; exists E'. +move=> r [Cr /= Ewr]; apply: subset_split_ent => //; exists (f r). + exact: (near (small_ent_sub _) E'). +by apply/entourage_sym; apply: (near (small_ent_sub _) E'). +Unshelve. all: by end_near. Qed. + +End compact_open_uniform. + Definition compactly_in {U : topologicalType} (A : set U) := [set B | B `<=` A /\ compact B]. @@ -7055,7 +7350,7 @@ move/filterS; apply; have [//|i nclfix] := @sepf _ x (open_closedC oB). apply: (wiFx i); have /= -> := @nbhsE (weak_topology (f_ i)) x. exists (f_ i @^-1` (~` closure [set f_ i x | x in ~` B])); [split=>//|]. apply: open_comp; last by rewrite ?openC; last apply: closed_closure. - by move=> + _; exact: weak_continuous. + by move=> + _; exact: (@weak_continuous _ _ (f_ i)). rewrite closureC preimage_bigcup => z [V [oV]] VnB => /VnB. by move/forall2NP => /(_ z) [] // /contrapT. Qed. @@ -7383,13 +7678,6 @@ move=> entD G /[dup] /asboolP [n _ + _ _] => /filterS; apply. exact: gauge.iter_split_ent. Qed. -Definition normal_space (T : topologicalType) := - forall A : set T, closed A -> - set_nbhs A `<=` filter_from (set_nbhs A) closure. - -Definition regular_space (T : topologicalType) := - forall a : T, nbhs a `<=` filter_from (nbhs a) closure. - Section ArzelaAscoli. Context {X : topologicalType}. Context {Y : uniformType}. @@ -7401,7 +7689,7 @@ Implicit Types (I : Type). Definition equicontinuous {I} (W : set I) (d : I -> (X -> Y)) := forall x (E : set (Y * Y)), entourage E -> - \forall y \near x, forall i, W i -> E(d i x, d i y). + \forall y \near x, forall i, W i -> E (d i x, d i y). Lemma equicontinuous_subset {I J} (W : set I) (V : set J) {fW : I -> X -> Y} {fV : J -> X -> Y} : @@ -7505,7 +7793,7 @@ apply: (@entourage_split _ (g y)) => //; first exact: (near (@ectsW x _ _)). by apply/entourage_sym; exact: (near (pointwise_cvg_entourage _ _ _)). Unshelve. all: by end_near. Qed. -Definition small_ent_sub := @small_set_sub _ _ (@entourage Y). +Definition small_ent_sub := @small_set_sub _ (@entourage Y). Lemma pointwise_compact_cvg (F : set_system {ptws X -> Y}) (f : {ptws X -> Y}) : ProperFilter F -> @@ -7515,13 +7803,15 @@ Proof. move=> PF /near_powerset_filter_fromP; case. exact: equicontinuous_subset_id. move=> W; wlog Wf : f W / W f. - move=> + FW /equicontinuous_closure => /(_ f (closure W)) Q. + move=> + FW /equicontinuous_closure => /(_ f (closure (W : set {ptws X -> Y}))) Q. split => Ff; last by apply: pointwise_cvg_compact_family. - apply Q => //; last by (apply: (filterS _ FW); exact: subset_closure). - by rewrite closureEcvg; exists F; [|split] => // ? /filterS; apply. + apply/Q => //. + by rewrite closureEcvg; exists F; [|split] => // ? /= /filterS; apply. + by apply: (filterS _ FW) => z Wz; apply: subset_closure. move=> FW ectsW; split=> [ptwsF|]; last exact: pointwise_cvg_compact_family. apply/fam_cvgP => K ? U /=; rewrite uniform_nbhs => [[E [eE EsubU]]]. -suff : \forall g \near within W (nbhs f), forall y, K y -> E (f y, g y). +suff : \forall g \near within W (nbhs (f : {ptws X -> Y})), + forall y, K y -> E (f y, g y). rewrite near_withinE; near_simpl => N; apply: (filter_app _ _ FW). by apply: ptwsF; near=> g => ?; apply: EsubU; apply: (near N g). near (powerset_filter_from (@entourage Y)) => E'. @@ -7534,11 +7824,11 @@ apply: (entourage_split (f x) eE). exact: (near (ectsW x E' entE') y). apply: (@entourage_split _ (g x)) => //. apply: (near (small_ent_sub _) E') => //. - near: g; near_simpl; apply: (@cvg_within _ (nbhs f)). + near: g; near_simpl; apply: (@cvg_within _ (nbhs (f : {ptws X -> Y}))). exact: pointwise_cvg_entourage. apply: (near (small_ent_sub _) E') => //. apply: (near (ectsW x E' entE')) => //. -exact: (near (withinT _ (nbhs_filter f))). +exact: (near (withinT _ (nbhs_filter (f : {ptws X -> Y})))). Unshelve. all: end_near. Qed. Lemma pointwise_compact_closure (W : set (X -> Y)) : @@ -7563,16 +7853,17 @@ Lemma pointwise_precompact_equicontinuous (W : set (X -> Y)) : Proof. move=> /pointwise_precompact_precompact + ectsW. rewrite ?precompactE compact_ultra compact_ultra pointwise_compact_closure //. -move=> /= + F UF FcW => /(_ F UF); rewrite image_id; case => // p [cWp Fp]. -exists p; split => //; apply/(pointwise_compact_cvg) => //. +move=> /= + F UF FcW => /(_ F UF); rewrite image_id => /(_ FcW)[p [cWp Fp]]. +exists p; split => //; apply/pointwise_compact_cvg => //. apply/near_powerset_filter_fromP; first exact: equicontinuous_subset_id. -exists (closure (W : set {ptws X -> Y })) => //; exact: equicontinuous_closure. +exists (closure (W : set {ptws X -> Y })) => //. +exact: equicontinuous_closure. Qed. Section precompact_equicontinuous. Hypothesis lcptX : locally_compact [set: X]. -Let compact_equicontinuous (W : set {family compact, X -> Y}) : +Lemma compact_equicontinuous (W : set {family compact, X -> Y}) : (forall f, W f -> continuous f) -> compact (W : set {family compact, X -> Y}) -> equicontinuous W id. @@ -7627,3 +7918,170 @@ exact: precompact_pointwise_precompact. Qed. End ArzelaAscoli. + +Lemma uniform_regular {T : uniformType} : @regular_space T. +Proof. +move=> x R /=; rewrite -{1}nbhs_entourageE => -[E entE ER]. +pose E' := split_ent E; have eE' : entourage E' by exact: entourage_split_ent. +exists (to_set (E' `&` E'^-1%classic) x). + rewrite -nbhs_entourageE; exists (E' `&` E'^-1%classic) => //. + exact: filterI. +move=> z /= clEz; apply: ER; apply: subset_split_ent => //. +have [] := clEz (to_set (E' `&` E'^-1%classic) z). + rewrite -nbhs_entourageE; exists (E' `&` E'^-1%classic) => //. + exact: filterI. +by move=> y /= [[? ?]] [? ?]; exists y. +Qed. + +#[global] Hint Resolve uniform_regular : core. + +Section currying. +Local Notation "U '~>' V" := + ({compact-open, [the topologicalType of U] -> [the topologicalType of V]}) + (at level 99, right associativity). + +Section cartesian_closed. +Context {U V W : topologicalType}. + +(**md In this section, we consider under what conditions \ + `[f in U ~> V ~> W | continuous f /\ forall u, continuous (f u)]` \ + and \ + `[f in U * V ~> W | continuous f]` \ + are homeomorphic. + - Always: \ + `curry` sends continuous functions to continuous functions. + - `V` locally_compact + regular or Hausdorff: \ + `uncurry` sends continuous functions to continuous functions. + - `U` regular or Hausdorff: \ + `curry` itself is a continuous map. + - `U` regular or Hausdorff AND `V` locally_compact + regular or Hausdorff \ + `uncurry` itself is a continuous map. \ + Therefore `curry`/`uncurry` are homeomorphisms. + + So the category of locally compact regular spaces is cartesian closed. +*) + +Lemma continuous_curry (f : (U * V)%type ~> W) : + continuous f -> + continuous (curry f : U ~> V ~> W) /\ forall u, continuous (curry f u). +Proof. +move=> ctsf; split; first last. + move=> u z; apply: continuous_comp; last exact: ctsf. + by apply: cvg_pair => //=; exact: cvg_cst. +move=> x; apply/compact_open_cvgP => K O /= cptK oO fKO. +near=> z => w /= [+ + <-]; near: z. +move/compact_near_coveringP/near_covering_withinP : cptK; apply. +move=> v Kv; have [[P Q] [Px Qv] PQfO] : nbhs (x, v) (f @^-1` O). + by apply: ctsf; move: oO; rewrite openE; apply; apply: fKO; exists v. +by exists (Q, P) => // -[b a] /= [Qb Pa] Kb; exact: PQfO. +Unshelve. all: by end_near. 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 : (U * V)%type ~> W). +Proof. +move=> lcV reg cf cfp /= [u v] D; rewrite /= nbhsE => -[O [oO Ofuv]] /filterS. +apply; have [B] := @lcV v I; rewrite withinET => Bv [cptB clB]. +have [R Rv RO] : exists2 R, nbhs v R & forall z, closure R z -> O (f u z). + have [] := reg v (f u @^-1` O); first by apply: cfp; exact: open_nbhs_nbhs. + by move=> R ? ?; exists R. +exists (f @^-1` [set g | g @` (B `&` closure R) `<=` O], B `&` closure R). + split; [apply/cf/open_nbhs_nbhs; split | apply: filterI] => //. + - apply: compact_open_open => //; apply: compact_closedI => //. + exact: closed_closure. + - by move=> ? [x [? + <-]]; apply: RO. + - by apply: filterS; first exact: subset_closure. +by case=> a r /= [fBMO [Br] cmR]; apply: fBMO; exists r. +Qed. + +Lemma continuous_uncurry (f : U ~> V ~> W) : + locally_compact [set: V] -> hausdorff_space V -> continuous f -> + (forall u, continuous (f u)) -> + continuous ((uncurry : (U ~> V ~> W) -> ((U * V)%type ~> W)) f). +Proof. +move=> lcV hsdf ctsf cf; apply: continuous_uncurry_regular => //. +move=> v; have [B] := @lcV v I; rewrite withinET => Bv [cptB clB]. +by move=> z; exact: (@compact_regular V hsdf v B). +Qed. + +Lemma curry_continuous (f : (U * V)%type ~> W) : continuous f -> @regular_space U -> + {for f, continuous (curry : ((U * V)%type ~> W) -> (U ~> V ~> W))}. +Proof. +move=> ctsf regU; apply/compact_open_cvgP. + by apply: fmap_filter; exact: nbhs_filter. +move=> K ? cptK [D OfinIo <-] fKD /=; near=> z => w [+ + <-]; near: z. +move/compact_near_coveringP/near_covering_withinP : (cptK); apply => u Ku. +have [] := fKD (curry f u); first by exists u. +move=> E /[dup] /[swap] /OfinIo [N Asub <- DIN INf]. +suff : \forall x' \near u & i \near nbhs f, K x' -> + (\bigcap_(i in [set` N]) i) (curry i x'). + apply: filter_app; near=> a b => /[apply] ?. + by exists (\bigcap_(i in [set` N]) i). +apply: filter_bigI_within => R RN; have /set_mem [[M cptM _]] := Asub _ RN. +have Rfu : R (curry f u) by exact: INf. +move/(_ _ Rfu) => [O [fMO oO] MOR]; near=> p => /= Ki; apply: MOR => + [+ + <-]. +move=> _ v Mv; move: v Mv Ki; near: p. +have umb : \forall y \near u, (forall b, M b -> nbhs (y, b) (f @^-1` O)). + move/compact_near_coveringP/near_covering_withinP : (cptM); apply => v Mv. + have [[P Q] [Pu Qv] PQO] : nbhs (u, v) (f @^-1` O). + by apply: ctsf; apply: open_nbhs_nbhs; split => //; apply: fMO; exists v. + exists (Q, P); [by []| move=> [b a [/= Qb Pa Mb]]]. + by apply: ctsf; apply: open_nbhs_nbhs; split => //; exact: PQO. +move/compact_near_coveringP/near_covering_withinP : (cptM); apply => v Mv. +have [P' P'u cPO] := regU u _ umb. +pose L := [set h | h @` ((K `&` closure P') `*` M) `<=` O]. +exists (setT, P' `*` L). + split => //; [exact: filterT|]; exists (P', L) => //; split => //. + apply: open_nbhs_nbhs; split; first apply: compact_open_open => //. + apply: compact_setM => //; apply: compact_closedI => //. + exact: closed_closure. + by move=> ? [[a b] [[Ka /cPO +] Mb <-]] => /(_ _ Mb)/nbhs_singleton. +move=> [b [a h]] [/= _ [Pa] +] Ma Ka; apply. +by exists (a, b); split => //; split => //; exact/subset_closure. +Unshelve. all: by end_near. Qed. + +Lemma uncurry_continuous (f : U ~> V ~> W) : + locally_compact [set: V] -> @regular_space V -> @regular_space U -> + continuous f -> (forall u, continuous (f u)) -> + {for f, continuous (uncurry : (U ~> V ~> W) -> ((U * V)%type ~> W))}. +Proof. +move=> lcV regV regU ctsf ctsfp; apply/compact_open_cvgP. + by apply: fmap_filter; exact:nbhs_filter. +move=> /= K O cptK oO fKO; near=> h => ? [+ + <-]; near: h. +move/compact_near_coveringP/near_covering_withinP: (cptK); apply. +case=> u v Kuv. +have : exists P Q, [/\ closed P, compact Q, nbhs u P, + nbhs v Q & P `*` Q `<=` uncurry f @^-1` O]. + have : continuous (uncurry f) by exact: continuous_uncurry_regular. + move/continuousP/(_ _ oO); rewrite openE => /(_ (u, v))[]. + by apply: fKO; exists (u, v). + case=> /= P' Q' [P'u Q'v] PQO. + have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. + have [P Pu cPP'] := regU u P' P'u; have [Q Qv cQQ'] := regV v Q' Q'v. + exists (closure P), (B `&` closure Q); split. + - exact: closed_closure. + - by apply: compact_closedI => //; exact: closed_closure. + - by apply: filterS; first exact: subset_closure. + - by apply: filterI=> //; apply: filterS; first exact: subset_closure. + - by case => a b [/cPP' ?] [_ /cQQ' ?]; exact: PQO. +case=> P [Q [clP cptQ Pu Qv PQfO]]; pose R := [set g : V ~> W | g @` Q `<=` O]. +(have oR : open R by exact: compact_open_open); pose P' := f @^-1` R. +pose L := [set h : U ~> V ~> W | h @` (fst @` K `&` P) `<=` R]. +exists ((P `&` P') `*` Q, L); first split => /=. +- exists (P `&` P', Q) => //; split => //=; apply: filterI => //. + apply: ctsf; apply: open_nbhs_nbhs; split => // _ [b Qb <-]. + by apply: (PQfO (u, b)); split => //; exact: nbhs_singleton. +- rewrite nbhs_simpl /=; apply: open_nbhs_nbhs; split. + apply: compact_open_open => //; apply: compact_closedI => //. + apply: continuous_compact => //; apply: continuous_subspaceT => x. + exact: cvg_fst. + move=> /= _ [a [Kxa Pa] <-] _ [b Qb <-]. + by apply: (PQfO (a, b)); split => //; exact: nbhs_singleton. +move=> [[a b h]] [/= [[Pa P'a] Qb Lh] Kab]. +apply: (Lh (h a)); first by exists a => //; split => //; exists (a, b). +by exists b. +Unshelve. all: by end_near. Qed. + +End cartesian_closed. + +End currying.