From dc87225fed3387bcc1ff306b4e27e97bd6f47cfb Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 14:10:18 +0200 Subject: [PATCH 1/2] Update changelog --- CHANGELOG_UNRELEASED.md | 129 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 129 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 67bb43c3b6..cb0445c1c1 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,8 +4,137 @@ ### Added +- in file `function_spaces.v`, + + new lemma `within_continuous_big`. +- in file `nat_topology.v`, + + new lemma `near_infty_after`. +- in file `num_topology.v`, + + new lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, + `at_left_shift`, and `at_right_shift`. + ### Changed +- in `realsum.v`: + + lemma `__admitted__psumB` proved and renamed to `psumB` + +- moved from `measurable_structure.v` to `classical_sets.v`: + + definition `preimage_set_system` + + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, + `preimage_set_system_id` + +- moved from `measurable_structure.v` to `classical_sets.v`: + + definition `preimage_set_system` + + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, + `preimage_set_system_id` + +- moved from `topology_structure.v` to `filter.v`: + + lemma `continuous_comp` (and generalized) + +- in `numfun.v`: + + `fune_abse` renamed to `funeposDneg` and direction of the equality changed + + `funeposneg` renamed to `funeposBneg` and direction of the equality changed + + `funeD_posD` renamed to `funeDB` and direction of the equality changed + +- in `constructive_ereal.v`: + + lemmas `EFin_semi_additive` and `dEFin_semi_additive` turned into `Let`s + +- moved from `charge.v` to `signed_measure.v`: + + mixin `isAdditiveCharge`, structure `AdditiveCharge` + + mixin `isSemiSigmaAdditive`, structure `Charge` + + factory `isCharge` + + lemmas `charge0`, `charge_semi_additiveW`, `charge_semi_additive2E`, + `charge_semi_additive2`, `chargeU`, `chargeDI`, `charge_partition` + + definitions `measure_of_charge`, `charge_of_finite_measure` + + lemma `chargeD` + + definitions `crestr`, `crestr0`, `czero`, `cscale` + + lemmas `dominates_cscalel`, `dominates_cscaler` + + definition `copp` + + lemma `cscaleN1` + + definition `cadd` + + lemmas `dominates_cadd`, `dominates_pushforward` + + definitions `positive_set`, `negative_set` + + lemmas `negative_set_charge_le0`, `negative_set0`, + `positive_negative0`, `bigcup_negative_set`, `negative_setU`, + `hahn_decomposition_lemma` + + definition `hahn_decomposition` + + theorem `Hahn_decomposition` + + lemmas `Hahn_decomposition_uniq`, `cjordan_posE`, `cjordan_negE` + + definitions `jordan_pos`, `jordan_neg` + + lemmas `jordan_posE`, `jordan_negE`, `jordan_decomp`, `jordan_pos_dominates`, + `jordan_neg_dominates` + + definition `charge_variation`, `charge_dominates` + + lemmas `abse_charge_variation`, `null_charge_dominatesP`, + `content_charge_dominatesP`, `charge_variation_continuous` + +- moved from `charge.v` to `radon_nikodym.v`: + + definition `induced_charge` + + lemmas `semi_sigma_additive_nng_induced`, `dominates_induced`, + `integral_normr_continuous` + + definitions `approxRN`, `int_approxRN`, `sup_int_approxRN` + + lemmas `sup_int_approxRN_ge0`, `radon_nikodym_finite`, + `radon_nikodym_sigma_finite`, `change_of_variables`, `integrableM`, + `chain_rule` + + definition `Radon_Nikodym` + + lemmas `Radon_NikodymE`, `Radon_Nikodym_fin_num`, `Radon_Nikodym_integrable`, + `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`, + `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule` +- in `realsum.v`: + + the following now use `funrpos` and `funrneg`: + * definition `sum` + * lemmas `summable_funrpos`, `summable_funrneg` + + lemma `sum0` (now uses `cst`) + +- moved from `realsum` to `numfun.v`: + + now use `funrpos` and `funrneg`: + * lemmas `eq_funrpos`, `eq_funrneg` + * lemma `fpos0` (renamed to `funrpos_cst0`) + * lemma `fneg0` (renamed to `funrneg_cst0`) + * lemmas `funrposZ`, `funrnegZ` + * lemmas `funrpos_natrM`, `funrneg_natrM` + * lemmas `le_funrpos_norm` + +- moved from `numfun.v` to `unstable.v`: + + notations `nondecreasing_fun`, `nonincreasing_fun`, + `decreasing_fun`, `increasing_fun` + +- in `esum.v`: + + definition `esum` + + lemma `esum_fset` + + lemma `esum_ge` -> `PosEsum.pos_esum_ge` + + lemma `le_esum` -> `PosEsum.le_pos_esum` + +- moved from `normed_module.v` to `metric_structure.v` + + lemma `squeeze_cvgr` + +- moved from `pseudometric_normed_Zmodule.v` to `metric_structure.v` + + lemmas `real_cvgr_lt`, `real_cvgr_le`, `real_cvgr_le`, `real_cvgr_gt` + + lemmas `cvgr_lt`, `cvgr_gt`, `cvgr_ge`, `cvgr_le` +- in `normal_distribution.v: + + `normal_fun_center` -> `normal_fun_center0` + +- moved from `measurable_structure.v` to `measure_function.v`: + + definition `subset_sigma_subadditive` + +- moved from `measurable_structure.v` to `unstable.v`: + + notations `nondecreasing_seq`, `nonincreasing_seq` + +- moved from `measurable_structure.v` to `classical_sets.v`: + + notation `^nat` + + defintion `sequence` + + defintion `seqDU` + + lemmas `seqDU_bigcup_eq`, `trivIset_seqDU` + + definition `seqD` + + lemmas `eq_bigcup_seqD`, `trivIset_seqD`, `seqDU_seqD`, `bigcup_bigsetU_bigcup` + +- in `functions.v` + + lemma `fctE` (include `zerofctE` and `onefctE`) + +- in `classical_sets.v` + + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`) + +- moved from `metric_structure.v` to `num_topology.v`: + + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`. + ### Renamed ### Generalized From 055752b7089c007d896f36b6a097993e7382b941 Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 17:54:36 +0200 Subject: [PATCH 2/2] new series convergence criteria --- CHANGELOG_UNRELEASED.md | 130 +--------------------------------------- theories/sequences.v | 43 +++++++++++-- 2 files changed, 40 insertions(+), 133 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index cb0445c1c1..75707194be 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,137 +4,11 @@ ### Added -- in file `function_spaces.v`, - + new lemma `within_continuous_big`. -- in file `nat_topology.v`, - + new lemma `near_infty_after`. -- in file `num_topology.v`, - + new lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, - `at_left_shift`, and `at_right_shift`. +- in `sequences.v`, + + lemmas `is_cvg_series_shiftn`, `series_near_le_cvg` ### Changed -- in `realsum.v`: - + lemma `__admitted__psumB` proved and renamed to `psumB` - -- moved from `measurable_structure.v` to `classical_sets.v`: - + definition `preimage_set_system` - + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, - `preimage_set_system_id` - -- moved from `measurable_structure.v` to `classical_sets.v`: - + definition `preimage_set_system` - + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, - `preimage_set_system_id` - -- moved from `topology_structure.v` to `filter.v`: - + lemma `continuous_comp` (and generalized) - -- in `numfun.v`: - + `fune_abse` renamed to `funeposDneg` and direction of the equality changed - + `funeposneg` renamed to `funeposBneg` and direction of the equality changed - + `funeD_posD` renamed to `funeDB` and direction of the equality changed - -- in `constructive_ereal.v`: - + lemmas `EFin_semi_additive` and `dEFin_semi_additive` turned into `Let`s - -- moved from `charge.v` to `signed_measure.v`: - + mixin `isAdditiveCharge`, structure `AdditiveCharge` - + mixin `isSemiSigmaAdditive`, structure `Charge` - + factory `isCharge` - + lemmas `charge0`, `charge_semi_additiveW`, `charge_semi_additive2E`, - `charge_semi_additive2`, `chargeU`, `chargeDI`, `charge_partition` - + definitions `measure_of_charge`, `charge_of_finite_measure` - + lemma `chargeD` - + definitions `crestr`, `crestr0`, `czero`, `cscale` - + lemmas `dominates_cscalel`, `dominates_cscaler` - + definition `copp` - + lemma `cscaleN1` - + definition `cadd` - + lemmas `dominates_cadd`, `dominates_pushforward` - + definitions `positive_set`, `negative_set` - + lemmas `negative_set_charge_le0`, `negative_set0`, - `positive_negative0`, `bigcup_negative_set`, `negative_setU`, - `hahn_decomposition_lemma` - + definition `hahn_decomposition` - + theorem `Hahn_decomposition` - + lemmas `Hahn_decomposition_uniq`, `cjordan_posE`, `cjordan_negE` - + definitions `jordan_pos`, `jordan_neg` - + lemmas `jordan_posE`, `jordan_negE`, `jordan_decomp`, `jordan_pos_dominates`, - `jordan_neg_dominates` - + definition `charge_variation`, `charge_dominates` - + lemmas `abse_charge_variation`, `null_charge_dominatesP`, - `content_charge_dominatesP`, `charge_variation_continuous` - -- moved from `charge.v` to `radon_nikodym.v`: - + definition `induced_charge` - + lemmas `semi_sigma_additive_nng_induced`, `dominates_induced`, - `integral_normr_continuous` - + definitions `approxRN`, `int_approxRN`, `sup_int_approxRN` - + lemmas `sup_int_approxRN_ge0`, `radon_nikodym_finite`, - `radon_nikodym_sigma_finite`, `change_of_variables`, `integrableM`, - `chain_rule` - + definition `Radon_Nikodym` - + lemmas `Radon_NikodymE`, `Radon_Nikodym_fin_num`, `Radon_Nikodym_integrable`, - `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`, - `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule` -- in `realsum.v`: - + the following now use `funrpos` and `funrneg`: - * definition `sum` - * lemmas `summable_funrpos`, `summable_funrneg` - + lemma `sum0` (now uses `cst`) - -- moved from `realsum` to `numfun.v`: - + now use `funrpos` and `funrneg`: - * lemmas `eq_funrpos`, `eq_funrneg` - * lemma `fpos0` (renamed to `funrpos_cst0`) - * lemma `fneg0` (renamed to `funrneg_cst0`) - * lemmas `funrposZ`, `funrnegZ` - * lemmas `funrpos_natrM`, `funrneg_natrM` - * lemmas `le_funrpos_norm` - -- moved from `numfun.v` to `unstable.v`: - + notations `nondecreasing_fun`, `nonincreasing_fun`, - `decreasing_fun`, `increasing_fun` - -- in `esum.v`: - + definition `esum` - + lemma `esum_fset` - + lemma `esum_ge` -> `PosEsum.pos_esum_ge` - + lemma `le_esum` -> `PosEsum.le_pos_esum` - -- moved from `normed_module.v` to `metric_structure.v` - + lemma `squeeze_cvgr` - -- moved from `pseudometric_normed_Zmodule.v` to `metric_structure.v` - + lemmas `real_cvgr_lt`, `real_cvgr_le`, `real_cvgr_le`, `real_cvgr_gt` - + lemmas `cvgr_lt`, `cvgr_gt`, `cvgr_ge`, `cvgr_le` -- in `normal_distribution.v: - + `normal_fun_center` -> `normal_fun_center0` - -- moved from `measurable_structure.v` to `measure_function.v`: - + definition `subset_sigma_subadditive` - -- moved from `measurable_structure.v` to `unstable.v`: - + notations `nondecreasing_seq`, `nonincreasing_seq` - -- moved from `measurable_structure.v` to `classical_sets.v`: - + notation `^nat` - + defintion `sequence` - + defintion `seqDU` - + lemmas `seqDU_bigcup_eq`, `trivIset_seqDU` - + definition `seqD` - + lemmas `eq_bigcup_seqD`, `trivIset_seqD`, `seqDU_seqD`, `bigcup_bigsetU_bigcup` - -- in `functions.v` - + lemma `fctE` (include `zerofctE` and `onefctE`) - -- in `classical_sets.v` - + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`) - -- moved from `metric_structure.v` to `num_topology.v`: - + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`. - ### Renamed ### Generalized diff --git a/theories/sequences.v b/theories/sequences.v index fc1aeb39fe..8f572e59c9 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -558,7 +558,7 @@ Proof. by rewrite telescopeK/= addrC addrNK. Qed. Section series_patched. Context (N : nat) {K : numFieldType} {V : normedModType K}. -Implicit Types (f : nat -> V) (u : V ^nat) (l : set_system V). +Implicit Types (f : nat -> V) (u : V ^nat) (l : set_system V). Lemma is_cvg_series_restrict u_ : cvgn [sequence \sum_(N <= k < n) u_ k]_n = cvgn (series u_). @@ -571,6 +571,20 @@ rewrite funeqE => n; case: leqP => // ltNn; apply: (canRL (addrK _)). by rewrite seriesEnat addrC -big_cat_nat// ltnW. Qed. +Lemma is_cvg_series_shiftn u_ : cvgn (series u_) <-> cvgn [series u_ (n + N)]_n. +Proof. +split. +- rewrite -is_cvg_series_restrict => /cvg_ex[/= l +]. + rewrite -(cvg_shiftn N)/= => Nnul; apply: cvgP; apply: cvg_trans Nnul. + apply: near_eq_cvg; near=> n. + rewrite /series/=. + by rewrite -{1}(add0n N) big_addn addnK. +- move=> cvgu; rewrite -is_cvg_series_restrict. + apply: cvgP; rewrite -(cvg_shiftn N)/=; apply: cvg_trans cvgu. + apply: near_eq_cvg; near=> n => /=. + by rewrite -{2}(add0n N) big_addn addnK. +Unshelve. all: by end_near. Qed. + End series_patched. Section sequences_R_lemmas. @@ -972,17 +986,36 @@ have := su_cv; rewrite near_swap => su_cvC; near=> m => /=; rewrite sub_series. by have [|/ltnW]:= leqP m.2 m.1 => m12; rewrite ?normrN; near: m. Unshelve. all: by end_near. Qed. -Lemma series_le_cvg (R : realType) (u_ v_ : R ^nat) : - (forall n, 0 <= u_ n) -> (forall n, 0 <= v_ n) -> - (forall n, u_ n <= v_ n) -> +Lemma series_le_cvg {R : realType} (u_ v_ : R ^nat) : + (forall n, 0 <= u_ n) -> (forall n, 0 <= v_ n) -> + (forall n, u_ n <= v_ n) -> cvgn (series v_) -> cvgn (series u_). Proof. move=> u_ge0 v_ge0 le_uv /cvg_seq_bounded/bounded_fun_has_ubound[M v_M]. apply: nondecreasing_is_cvgn; first exact: nondecreasing_series. exists M => _ [n _ <-]. -by apply: le_trans (v_M (series v_ n) _); [apply: ler_sum | exists n]. +by apply: le_trans (v_M (series v_ n) _); [exact: ler_sum | exists n]. Qed. +Lemma series_near_le_cvg {R : realType} (u_ v_ : R^nat) : + (\forall n \near \oo, 0 <= u_ n) -> (\forall n \near \oo, 0 <= v_ n) -> + (\forall n \near \oo, u_ n <= v_ n) -> + cvgn (series v_) -> cvgn (series u_). +Proof. +move=> u0 v0 uv cvg_v. +near \oo => N; apply/(is_cvg_series_shiftn N). +move: cvg_v => /(is_cvg_series_shiftn N); apply: series_le_cvg => /= n. +- have : forall n, (n >= N)%N -> 0 <= u_ n. + by near: N; exact: (iffLR (near_infty_leq _)). + by apply; exact: leq_addl. +- have : forall n, (n >= N)%N -> 0 <= v_ n. + by near: N; exact: (iffLR (near_infty_leq _)). + by apply; exact: leq_addl. +- have : forall n, (n >= N)%N -> u_ n <= v_ n. + by near: N; exact: (iffLR (near_infty_leq _)). + by apply; exact: leq_addl. +Unshelve. all: by end_near. Qed. + Lemma normed_cvg {R : realType} (V : completeNormedModType R) (u_ : V ^nat) : cvgn [normed series u_] -> cvgn (series u_). Proof.