diff --git a/CHANGELOG.md b/CHANGELOG.md index 432ab90df8..cf118f6c58 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,373 @@ # Changelog -Latest releases: [[1.14.0] - 2025-11-07](#1140---2025-11-07), [[1.13.0] - 2025-08-16](#1130---2025-08-16), and [[1.12.0] - 2025-07-03](#1120---2025-07-03) +Latest releases: [[1.15.0] - 2026-01-15](#1150---2026-01-15), [[1.14.0] - 2025-11-07](#1140---2025-11-07), and [[1.13.0] - 2025-08-16](#1130---2025-08-16) + +## [1.15.0] - 2026-01-15 + +### Added + +- in `unstable.v`: + + definitions `monotonic`, `strict_monotonic` + + lemma `strict_monotonicW` + + notation `.~` for `onem` + +- in `classical_sets.v`: + + lemma `nonemptyPn` + + lemmas `setUDl`, `setUDr` + +- in `cardinality.v`: + + lemma `infinite_setD` + + lemmas `finite_setX_or`, `infinite_setX` + + lemmas `infinite_prod_rat`, ``card_rat2` + + notation `cofinite_set` + + lemmas `cofinite_setT`, `infinite_setN0`, `sub_cofinite_set`, + `sub_infinite_set`, `cofinite_setUl`, `cofinite_setUr`, `cofinite_setU`, + `cofinite_setI`, `cofinite_set_infinite`, `infinite_setIl`, + `infinite_setIr` + + lemma `injective_gtn` + +- in `topology_structure.v`: + + definition `isolated` + + lemma `isolatedS` + + lemma `disjoint_isolated_limit_point` + + lemma `closure_isolated_limit_point` + +- in `subspace_topology.v`: + + definition `from_subspace` + +- in `order_topology.v`: + + structures `POrderedNbhs`, `POrderedTopological`, `POrderedUniform`, `POrderedPseudoMetric`, + `POrderedPointedTopological` + +- in `num_topology.v`: + + lemmas `continuous_rsubmx`, `continuous_lsubmx` + +- new file `metric_structure.v`: + + mixin `PseudoMetric_isMetric`, structure `Metric`, type `metricType` + * with fields `mdist`, `mdist_ge0`, `mdist_positivity`, `ballEmdist` + + lemmas `metric_sym`, `mdistxx`, `mdist_gt0`, `metric_triangle`, + `metric_hausdorff` + + `R^o` declared to be an instance of `metricType` + + module `metricType_numDomainType` + * lemmas `ball_mdistE`, `nbhs_nbhs_mdist`, `nbhs_mdistP`, + `filter_from_mdist_nbhs`, `fcvgrPdist_lt`, `cvgrPdist_lt`, + `cvgr_dist_lt`, `cvgr_dist_le`, `nbhsr0P`, `cvgrPdist_le` + + factory `isMetric` + +- in `separation_axioms.v`: + + lemma `perfectP` + +- in `reals.v`: + + lemma `nat_has_minimum` + +- in `normed_module.v`: + + lemma `limit_point_infinite_setP` + + lemma `open_subball_rat` + + fact `isolated_rat_ball` + + lemma `countable_isolated` + + lemma `limit_point_setD` + +- in `convex.v`: + + lemmas `convN`, `conv_le` + +- in `sequences.v`: + + lemma `increasing_seq_injective` + + definition `adjacent_set` + + lemmas `adjacent_sup_inf`, `adjacent_sup_inf_unique` + + definition `cut` + + lemmas `cut_adjacent`, `infinite_bounded_limit_point_nonempty` + + lemma `cluster_eventuallyP` + + lemmas `cluster_eventually_cvg`, `limit_point_cluster_eventually` + + lemma `finite_range_cst_subsequence` + + lemmas `infinite_increasing_seq`, `infinite_increasing_seq_wf` + + lemma `finite_range_cvg_subsequence` + + theorem `bolzano_weierstrass` + +- in `derive.v`: + + lemmas `differentiable_rsubmx`, `differentiable_lsubmx` + +- in `measurable_structure.v`: + + lemma `dynkin_induction` + +- in `measure_negligible.v`: + + definition `null_set` with notation `_.-null_set` + + lemma `subset_null_set` + + lemma `negligible_null_set` + + lemma `measure0_null_setP` + + lemma `null_setU` + + definition `null_dominates` + + lemma `null_dominates_trans` + + lemma `null_content_dominatesP` + +- in `measurable_realfun.v`: + + lemma `measurable_funN` + + lemmas `nondecreasing_measurable`, `nonincreasing_measurable` + +- in `lebesgue_integrable.v` + + lemma `null_set_integrable` + + lemma `integrable_set0` + + lemma `integrable_norm` + +- in `lebesgue_integral_fubini.v`: + + definition `product_subprobability` + + lemma `product_subprobability_setC` + +- new file `lebesgue_integral_theory/giry.v` + + definition `measure_eq` + + definition `giry` + + definition `giry_ev` + + definition `giry_measurable` + + definition `preimg_giry_ev` + + definition `giry_display` + + lemma `measurable_giry_ev` + + definition `giry_int` + + lemmas `measurable_giry_int`, `measurable_giry_codensity` + + definition `giry_map` + + lemmas `measurable_giry_map`, `giry_int_map`, `giry_map_dirac` + + definition `giry_ret` + + lemmas `measurable_giry_ret`, `giry_int_ret` + + definition `giry_join` + + lemmas `measurable_giry_join`, `sintegral_giry_join`, `giry_int_join` + + definition `giry_bind` + + lemmas `measurable_giry_bind`, `giry_int_bind` + + lemmas `giry_joinA`, `giry_join_id1`, `giry_join_id2`, `giry_map_zero` + + definition `giry_prod` + + lemmas `measurable_giry_prod`, `giry_int_prod1`, `giry_int_prod2` + +- in `charge.v`: + + definition `charge_dominates` + + lemma `charge_null_dominatesP` + + lemma `content_charge_dominatesP` + +### Changed + +- in `Rstruct.v`: + + lemmas `RleP`, `RltP` (change implicits) + +- in `subspace_topology.v`: + + notation `{within _, continuous _}` (now uses `from_subspace`) + +- in `pseudometric_normed_Zmodule.v`: + + factory `NormedZmoduleMetric` with field `mdist_norm` + +- moved from `pseudometric_normed_Zmodule.v` to `num_topology.v`: + + notations `^'+`, `^'-` + + definitions `at_left`, `at_right` + + instances `at_right_proper_filter`, `at_left_proper_filter` + + lemmas `nbhs_right_gt`, `nbhs_left_lt`, `nbhs_right_neq`, `nbhs_left_neq`, + `nbhs_left_neq`, `nbhs_left_le`, `nbhs_right_lt`, `nbhs_right_ltW`, + `nbhs_right_ltDr`, `nbhs_right_le`, `not_near_at_rightP` + +- in `measurable_structure.v`: + + the notation ``` `<< ``` is now for `null_set_dominates`, + the previous definition can be recovered with the lemma + `null_dominatesP` + +- moved from `realfun.v` to `numfun.v`: + + notations `nondecreasing_fun`, `nonincreasing_fun`, `increasing_fun`, + `decreasing_fun` + + generalized from `realType` to `numDomainType`: + * lemmas `nondecreasing_funN`, `nonincreasing_funN` + + generalized from `realType` to `porderType` + * definitions `itv_partition`, `itv_partitionL`, `itv_partitionR` + * 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` + + generalized from `realType` to `orderType` + * lemmas `itv_partitionLP`, `itv_partitionRP`, `in_itv_partition`, + `notin_itv_partition` + + generalize from `realType` to `numDomainType`: + * lemmas `nonincreasing_fun_itv_partition`, `itv_partition_rev` + +- moved from `realfun.v` to `numfun.v`: + + generalize from `realType` to `numDomainType` + * definition `variation` + * lemmas `variation_zip`, `variation_prev`, `variation_next`, + `variation_nil`, `variation_ge0`, `variationN`, `variation_le`, + `nondecreasing_variation`, `nonincreasing_variation`, + `variation_cat` (order of parameters also changed), `le_variation`, + `variation_opp_rev`, `variation_rev_opp` + + generalize from `realType` to `realDomainType` + * lemmas `variation_itv_partitionLR`, `variation_subseq` + +- moved from `realfun.v` to `numfun.v`: + + generalize from `realType` to `numDomainType` + * definition `variations`, `bounded_variation` + * lemmas `variations_variation`, `variations_neq0`, `variationsN`, + `variationsxx` + * lemmas `bounded_variationxx`, `bounded_variationD`, + `bounded_variationN`, `bounded_variationl`, `bounded_variationr`, + `variations_opp`, `nondecreasing_bounded_variation` + +- moved from `realfun.v` to `metric_structure.v` and generalized: + + lemma `cvg_nbhsP` + +- in `lebesgue_integral_monotone_convergence.v`: + + lemma `ge0_le_integral` (remove superfluous hypothesis) + +- in `charge.v`: + + `dominates_cscalel` specialized from + `set _ -> \bar _` to `{measure set _ -> \bar _}` + +### Renamed + +- in `boolp.v`: + + `notP` -> `not_notP` + + `notE` -> `not_notE` + +- in `measure_negligible.v`: + + `measure_dominates_ae_eq` -> `null_dominates_ae_eq` + +- in `probability.v`: + + `derivable_oo_continuous_bnd_onemXnMr` -> `derivable_oo_LRcontinuous_onemXnMr` + +- in `charge.v`: + + `induced` -> `induced_charge` + +### Generalized + +- in `num_topology.v`: + + lemma `in_continuous_mksetP` + +- in `pseudometric_normed_Zmodule.v`: + + lemmas `continuous_within_itvP`, `continuous_within_itvcyP`, + `continuous_within_itvNycP` + + lemma `within_continuous_continuous` + + lemmas `open_itvoo_subset`, `open_itvcc_subset`, `realFieldType` + +- in `num_normedtype.v`: + + weaken hypothesis in lemmas `mono_mem_image_segment`, `mono_surj_image_segment`, + `inc_surj_image_segment`, `dec_surj_image_segment`, `inc_surj_image_segmentP`, + `dec_surj_image_segmentP`, `mono_surj_image_segmentP` + +- in `derive.v`: + + definition `jacobian` + + lemmas `deriveEjacobian`, `differentiable_coord` + +- in `lebesgue_integral_under.v`: + + weaken an hypothesis of lemma `continuity_under_integral` + +- in `lebesgue_integrable.v`: + + weaken an hypothesis of lemma `finite_measure_integrable_cst` + + lemma `null_set_integral` + +- in `realfun.v`: + + generalized from `realType` to `realFieldType`: + * definition `total_variation` + * lemmas `total_variationxx`, `nondecreasing_total_variation`, + `total_variationN` + +- in `ftc.v`: + + lemmas `parameterized_integral_continuous`, + `integration_by_substitution_decreasing`, + `integration_by_substitution_oppr`, + `integration_by_substitution_increasing`, + `integration_by_substitution_onem`, + `Rintegration_by_substitution_onem` + +### Deprecated + +- in `unstable.v`: + + notation ``` `1- ``` + +- in `topology_structure.v`: + + lemma `closure_limit_point` (use `closure_limit_point_isolated` instead) + +### Removed + +- in `unstable.v`: + + definition `monotonous` (use `strict_monotonic` instead) + + lemma `abs_ceil_ge` + +- in `set_interval.v`: + + lemma `interval_set1` (use `set_itv1` instead) + + notation `subset_itvS` (deprecated since 1.4.0) + +- in `classical_sets.v`: + + notation `notin_set` (deprecated since 1.2.0) + + notations `in_setM`, `setM0`, `set0M`, `setMTT`, `setMT`, `setTM`, + `setMI`, `setM_bigcupr`, `setM_bigcupl`, `setSM`, `bigcupM1l`, + `bigcupM1r`, `setM`, `setMR`, `setML`, `bigcup_setM_dep`, + `bigcup_setM`, `fst_setM`, `snd_setM`, `fst_setMR`, + `in_xsectionM`, `in_ysectionM`, `notin_xsectionM`, `notin_ysectionM` + (deprecared since 1.3.0) + +- in `cardinality.v`: + + notations `finite_setM`, `fset_setM`, `finite_setMR`, `finite_setML`, + `countableMR`, `countableM`, `countableML`, `infiniteMRl`, + `cardMR_eq_nat` + (deprecared since 1.3.0) + +- in `signed.v`: + + notations `num_le_maxr`, `num_le_maxl`, `num_le_minr`, `num_le_minl`, + `num_lt_maxr`, `num_lt_maxl`, `num_lt_minr`, `num_lt_minl` + (deprecated since 1.2.0) + +- in `separation_axioms.v`: + + definition `cvg_toi_locally_close` (deprecated since 1.5.0) + +- in `pseudometric_structure.v`: + + definition `cvg_toi_locally` (deprecated since 1.6.0) + +- in `constructive_ereal.v`: + + notations `gee_pmull`, `gee_addl`, `gee_addr`, `gte_addr`, `gte_addl`, + `lte_subl_addr`, `lte_subl_addl`, `lte_subr_addr`, `lte_subr_addl`, + `lee_subl_addr`, `lee_subl_addl`, `lee_subr_addr`, `lee_subr_addl` + (deprecated since 1.2.0) + + notations `gte_dopp`, `lte_le_add`, `lee_lt_add`, `lte_le_sub`, + `lee_opp2`, `lte_opp2`, `lte_dadd`, `lee_daddl`, `lee_daddr` + `gee_daddl`, `gee_daddr`, `lte_daddl`, `lte_daddr`, `gte_dsubl`, + `gte_dsubr`, `gte_daddl`, `gte_daddr`, `lte_dadd2lE`, `lee_dadd2rE`, + `lee_dadd2l`, `lee_dadd2r`, `lee_dadd`, `lee_dsub`, `lte_dsubl_addr`, + `lte_dsubl_addl`, `lte_dsubr_addr`, `lte_dsubr_addl`, `lte_le_dadd`, + `lee_lt_dadd`, `lte_le_dsub`, `lte_pdivr_mull`, `lte_pdivr_mulr`, + `lte_pdivl_mull`, `lte_pdivl_mulr`, `lee_pdivr_mull`, `lee_pdivr_mulr`, + `lee_pdivl_mull`, `lee_pdivl_mulr`, `lte_ndivr_mull`, `lte_ndivr_mulr`, + `lte_ndivl_mull`, `lte_ndivl_mulr`, `lee_ndivr_mull`, `lee_ndivr_mulr`, + `lee_ndivl_mull`, `lee_ndivl_mulr`, `eqe_pdivr_mull` + (deprecared since 1.3.0) + +- in `reals.v`: + + lemma `le_ceil` (deprecated since 1.3.0) + +- in `sequences.v`: + + notation `eq_bigsetU_seqD`(deprecated since 1.2.0) + +- in `realfun.v`: + + notation `lime_sup_ge0` (deprecated since 1.3.0) + +- in `measurable_structure.v`: + + notations `monotone_class`, `monotone_class_g_salgebra`, + `smallest_monotone_classE`, `monotone_class_subset`, + `setI_closed_gdynkin_salgebra`, `dynkin_g_dynkin`, `dynkin_monotone`, + `salgebraType` + (deprecated since 1.2.0) + + definition `measure_dominates` (use `null_set_dominates` instead) + + lemma `measure_dominates_trans` + + notation `measurableM` (deprecated since 1.3.0) + +- in `measure_function.v`: + + notations `g_salgebra_measure_unique_trace`, + `g_salgebra_measure_unique_cover`, `g_salgebra_measure_unique` + (deprecated since 1.2.0) + +- in `measurable_realfun.v`: + + notations `measurable_fine`, `measurable_exprn`, `measurable_mulrl`, + `measurable_mulrr`, `measurable_oppr`, `measurable_normr`, + `measurable_fun_pow`, `measurable_oppe`, `measurable_abse`, + `measurable_EFin`, `measurable_natmul` + (deprecated since 1.4.0) + + notation `EFin_measurable_fun` (deprecated since 1.6.0) + +- in `lebesgue_stieltjes_measure.v`: + + notation `wlength_sigma_sub_additive` (deprecated since 1.1.0) + +- in `lebesgue_integral_nonneg.v`: + + notations `integral_setI_indic`, `integralEindic` (deprecated since 1.3.0) + +- in `charge.v`: + + lemma `dominates_charge_variation` (use `charge_null_dominatesP` instead) ## [1.14.0] - 2025-11-07 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 8eb7df5b4f..67bb43c3b6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,325 +4,16 @@ ### Added -- in `classical_sets.v`: - + lemma `nonemptyPn` - -- in `cardinality.v`: - + lemma `infinite_setD` - -- in `convex.v`: - + lemmas `convN`, `conv_le` - -- in `normed_module.v`: - + lemma `limit_point_infinite_setP` -- in `measure_negligible.v`: - + definition `null_set` with notation `_.-null_set` - + lemma `subset_null_set` - + lemma `negligible_null_set` - + lemma `measure0_null_setP` - + lemma `null_setU` - + definition `null_dominates` - + lemma `null_dominates_trans` - + lemma `null_content_dominatesP` - -- in `charge.v`: - + definition `charge_dominates` - + lemma `charge_null_dominatesP` - + lemma `content_charge_dominatesP` - -- in `sequences.v`: - + lemma `increasing_seq_injective` - + definition `adjacent_set` - + lemmas `adjacent_sup_inf`, `adjacent_sup_inf_unique` - + definition `cut` - + lemmas `cut_adjacent`, `infinite_bounded_limit_point_nonempty` - -- in `measurable_structure.v`: - + lemma `dynkin_induction`` - -- in `lebesgue_integral_fubini.v`: - + definition `product_subprobability` - + lemma `product_subprobability_setC` - -- in `lebesgue_integral_theory/lebesgue_integrable.v` - + lemma `null_set_integrable` - -- new file `lebesgue_integral_theory/giry.v` - + definition `measure_eq` - + definition `giry` - + definition `giry_ev` - + definition `giry_measurable` - + definition `preimg_giry_ev` - + definition `giry_display` - + lemma `measurable_giry_ev` - + definition `giry_int` - + lemmas `measurable_giry_int`, `measurable_giry_codensity` - + definition `giry_map` - + lemmas `measurable_giry_map`, `giry_int_map`, `giry_map_dirac` - + definition `giry_ret` - + lemmas `measurable_giry_ret`, `giry_int_ret` - + definition `giry_join` - + lemmas `measurable_giry_join`, `sintegral_giry_join`, `giry_int_join` - + definition `giry_bind` - + lemmas `measurable_giry_bind`, `giry_int_bind` - + lemmas `giry_joinA`, `giry_join_id1`, `giry_join_id2`, `giry_map_zero` - + definition `giry_prod` - + lemmas `measurable_giry_prod`, `giry_int_prod1`, `giry_int_prod2` - -- in `measurable_realfun.v`: - + lemma `measurable_funN` - + lemmas `nondecreasing_measurable`, `nonincreasing_measurable` -- in `subspace_topology.v`: - + definition `from_subspace` -- in `topology_structure.v`: - + definition `isolated` - + lemma `isolatedS` - + lemma `disjoint_isolated_limit_point` - + lemma `closure_isolated_limit_point` - -- in `separation_axioms.v`: - + lemma `perfectP` - -- in `cardinality.v`: - + lemmas `finite_setX_or`, `infinite_setX` - + lemmas `infinite_prod_rat`, ``card_rat2` - -- in `normed_module.v`: - + lemma `open_subball_rat` - + fact `isolated_rat_ball` - + lemma `countable_isolated` -- in `normed_module.v`: - + lemma `limit_point_setD` - -- in `reals.v`: - + lemma `nat_has_minimum` - -- in `sequences.v`: - + lemma `cluster_eventuallyP` - + lemmas `cluster_eventually_cvg`, `limit_point_cluster_eventually` - -- in `lebesgue_integrable.v`: - + lemma `integrable_set0` - -- in `classical_sets.v`: - + lemmas `setUDl`, `setUDr` - -- in `cardinality.v`: - + notation `cofinite_set` - + lemmas `cofinite_setT`, `infinite_setN0`, `sub_cofinite_set`, - `sub_infinite_set`, `cofinite_setUl`, `cofinite_setUr`, `cofinite_setU`, - `cofinite_setI`, `cofinite_set_infinite`, `infinite_setIl`, - `infinite_setIr` - + lemma `injective_gtn` - -- in `sequences.v`: - + lemma `finite_range_cst_subsequence` - + lemmas `infinite_increasing_seq`, `infinite_increasing_seq_wf` - + lemma `finite_range_cvg_subsequence` - + theorem `bolzano_weierstrass` - -- in `lebesgue_integrable.v`: - + lemma `integrable_norm` -- in `order_topology.v`: - + structures `POrderedNbhs`, `POrderedTopological`, `POrderedUniform`, `POrderedPseudoMetric`, - `POrderedPointedTopological` -- in `num_topology.v`: - + lemmas `continuous_rsubmx`, `continuous_lsubmx` - -- in `derive.v`: - + lemmas `differentiable_rsubmx`, `differentiable_lsubmx` - -- in `unstable.v`: - + definitions `monotonic`, `strict_monotonic` - + lemma `strict_monotonicW` - ### Changed -- in `charge.v`: - + `dominates_cscalel` specialized from - `set _ -> \bar _` to `{measure set _ -> \bar _}` - -- in `measurable_structure.v`: - + the notation ``` `<< ``` is now for `null_set_dominates`, - the previous definition can be recovered with the lemma - `null_dominatesP` - -- in `lebesgue_integral_monotone_convergence.v`: - + lemma `ge0_le_integral` (remove superfluous hypothesis) -- in `subspace_topology.v`: - + notation `{within _, continuous _}` (now uses `from_subspace`) - -- moved from `realfun.v` to `numfun.v`: - + notations `nondecreasing_fun`, `nonincreasing_fun`, `increasing_fun`, - `decreasing_fun` - + generalized from `realType` to `numDomainType`: - * lemmas `nondecreasing_funN`, `nonincreasing_funN` - + generalized from `realType` to `porderType` - * definitions `itv_partition`, `itv_partitionL`, `itv_partitionR` - * 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` - + generalized from `realType` to `orderType` - * lemmas `itv_partitionLP`, `itv_partitionRP`, `in_itv_partition`, - `notin_itv_partition` - + generalize from `realType` to `numDomainType`: - * lemmas `nonincreasing_fun_itv_partition`, `itv_partition_rev` - -- moved from `realfun.v` to `numfun.v`: - + generalize from `realType` to `numDomainType` - * definition `variation` - * lemmas `variation_zip`, `variation_prev`, `variation_next`, - `variation_nil`, `variation_ge0`, `variationN`, `variation_le`, - `nondecreasing_variation`, `nonincreasing_variation`, - `variation_cat` (order of parameters also changed), `le_variation`, - `variation_opp_rev`, `variation_rev_opp` - + generalize from `realType` to `realDomainType` - * lemmas `variation_itv_partitionLR`, `variation_subseq` - -- moved from `realfun.v` to `numfun.v`: - + generalize from `realType` to `numDomainType` - * definition `variations`, `bounded_variation` - * lemmas `variations_variation`, `variations_neq0`, `variationsN`, - `variationsxx` - * lemmas `bounded_variationxx`, `bounded_variationD`, - `bounded_variationN`, `bounded_variationl`, `bounded_variationr`, - `variations_opp`, `nondecreasing_bounded_variation` -- in `Rstruct.v`: - + lemmas `RleP`, `RltP` (change implicits) -- new file `metric_structure.v`: - + mixin `PseudoMetric_isMetric`, structure `Metric`, type `metricType` - * with fields `mdist`, `mdist_ge0`, `mdist_positivity`, `ballEmdist` - + lemmas `metric_sym`, `mdistxx`, `mdist_gt0`, `metric_triangle`, - `metric_hausdorff` - + `R^o` declared to be an instance of `metricType` - + module `metricType_numDomainType` - * lemmas `ball_mdistE`, `nbhs_nbhs_mdist`, `nbhs_mdistP`, - `filter_from_mdist_nbhs`, `fcvgrPdist_lt`, `cvgrPdist_lt`, - `cvgr_dist_lt`, `cvgr_dist_le`, `nbhsr0P`, `cvgrPdist_le` - + factory `isMetric` - -- in `pseudometric_normed_Zmodule.v`: - + factory `NormedZmoduleMetric` with field `mdist_norm` - -### Changed - -- moved from `pseudometric_normed_Zmodule.v` to `num_topology.v`: - + notations `^'+`, `^'-` - + definitions `at_left`, `at_right` - + instances `at_right_proper_filter`, `at_left_proper_filter` - + lemmas `nbhs_right_gt`, `nbhs_left_lt`, `nbhs_right_neq`, `nbhs_left_neq`, - `nbhs_left_neq`, `nbhs_left_le`, `nbhs_right_lt`, `nbhs_right_ltW`, - `nbhs_right_ltDr`, `nbhs_right_le`, `not_near_at_rightP` - -- moved from `realfun.v` to `metric_structure.v` and generalized: - + lemma `cvg_nbhsP` - ### Renamed -- in `probability.v`: - + `derivable_oo_continuous_bnd_onemXnMr` -> `derivable_oo_LRcontinuous_onemXnMr` -- in `measure_negligible.v`: - + `measure_dominates_ae_eq` -> `null_dominates_ae_eq` - -- in `charge.v`: - + `induced` -> `induced_charge` - -- in `boolp.v`: - + `notP` -> `not_notP` - + `notE` -> `not_notE` - ### Generalized -- in `lebesgue_integral_under.v`: - + weaken an hypothesis of lemma `continuity_under_integral` - -- in `lebesgue_integrable.v`: - + weaken an hypothesis of lemma `finite_measure_integrable_cst` - -- in `derive.v`: - + definition `jacobian` - + lemmas `deriveEjacobian`, `differentiable_coord` - -- in `ftc.v`: - + lemmas `parameterized_integral_continuous`, - `integration_by_substitution_decreasing`, - `integration_by_substitution_oppr`, - `integration_by_substitution_increasing`, - `integration_by_substitution_onem`, - `Rintegration_by_substitution_onem` - -- in `lebesgue_integral_theory/lebesgue_integrable.v` - + lemma `null_set_integral` - -- in `realfun.v`: - + generalized from `realType` to `realFieldType`: - * definition `total_variation` - * lemmas `total_variationxx`, `nondecreasing_total_variation`, - `total_variationN` - -- in `num_topology.v`: - + lemma `in_continuous_mksetP` - -- in `pseudometric_normed_Zmodule.v`: - + lemmas `continuous_within_itvP`, `continuous_within_itvcyP`, - `continuous_within_itvNycP` - + lemma `within_continuous_continuous` - + lemmas `open_itvoo_subset`, `open_itvcc_subset`, `realFieldType` -- in `num_normedtype.v`: - + weaken hypothesis in lemmas `mono_mem_image_segment`, `mono_surj_image_segment`, - `inc_surj_image_segment`, `dec_surj_image_segment`, `inc_surj_image_segmentP`, - `dec_surj_image_segmentP`, `mono_surj_image_segmentP` - ### Deprecated -- in `topology_structure.v`: - + lemma `closure_limit_point` (use `closure_limit_point_isolated` instead) - ### Removed -- in `lebesgue_stieltjes_measure.v`: - + notation `wlength_sigma_sub_additive` (deprecated since 1.1.0) - -- in `constructive_ereal.v`: - + notations `gee_pmull`, `gee_addl`, `gee_addr`, `gte_addr`, `gte_addl`, - `lte_subl_addr`, `lte_subl_addl`, `lte_subr_addr`, `lte_subr_addl`, - `lee_subl_addr`, `lee_subl_addl`, `lee_subr_addr`, `lee_subr_addl` - (deprecated since 1.2.0) - -- in `signed.v`: - + notations `num_le_maxr`, `num_le_maxl`, `num_le_minr`, `num_le_minl`, - `num_lt_maxr`, `num_lt_maxl`, `num_lt_minr`, `num_lt_minl` - (deprecated since 1.2.0) - -- in `measure_function.v`: - + notations `g_salgebra_measure_unique_trace`, - `g_salgebra_measure_unique_cover`, `g_salgebra_measure_unique` - (deprecated since 1.2.0) - -- in `measurable_structure.v`: - + notations `monotone_class`, `monotone_class_g_salgebra`, - `smallest_monotone_classE`, `monotone_class_subset`, - `setI_closed_gdynkin_salgebra`, `dynkin_g_dynkin`, `dynkin_monotone`, - `salgebraType` - (deprecated since 1.2.0) - -- in `sequences.v`: - + notation `eq_bigsetU_seqD` - (deprecated since 1.2.0) -- in `measurable_structure.v`: - + definition `measure_dominates` (use `null_set_dominates` instead) - + lemma `measure_dominates_trans` - -- in `charge.v`: - + lemma `dominates_charge_variation` (use `charge_null_dominatesP` instead) - -- in `set_interval.v`: - + lemma `interval_set1` (use `set_itv1` instead) - -- in `unstable.v`: - + definition `monotonous` (use `strict_monotonic` instead) - ### Infrastructure ### Misc diff --git a/INSTALL.md b/INSTALL.md index 67fc748191..4c69982950 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -50,7 +50,7 @@ $ opam install coq-mathcomp-analysis ``` To install a precise version, type, say ``` -$ opam install coq-mathcomp-analysis.1.14.0 +$ opam install coq-mathcomp-analysis.1.15.0 ``` 4. Everytime you want to work in this same context, you need to type ``` diff --git a/README.md b/README.md index 265195dd40..fe9a7c3787 100644 --- a/README.md +++ b/README.md @@ -62,7 +62,7 @@ make install Each file is documented in its header in ASCII. -[HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc_1_14_0/index.html) (using [`rocqnavi`](https://github.com/affeldt-aist/rocqnavi)). +[HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc/1_15_0/index.html) (using [`rocqnavi`](https://github.com/affeldt-aist/rocqnavi)). It includes inheritance diagrams for the mathematical structures that MathComp-Analysis adds on top of MathComp's ones. Overview presentations: @@ -97,6 +97,8 @@ Other work using MathComp-Analysis: - [Semantics of Probabilistic Programs using s-Finite Kernels in Dependent Type Theory](https://dl.acm.org/doi/pdf/10.1145/3732291) (2025) - [A Formal Foundation for Equational Reasoning on Probabilistic Programs](https://staff.aist.go.jp/reynald.affeldt/documents/eddy_aplas2025.pdf) (2025) doi:[10.1007/978-981-95-3585-9_3](https://doi.org/10.1007/978-981-95-3585-9_3) +- [Cylindrical Algebraic Decomposition in Coq/Rocq](https://dl.acm.org/doi/epdf/10.1145/3779031.3779100) (2026) + doi:[3779031.3779100](https://doi.org/10.1145/3779031.3779100) ## About the stability of this library diff --git a/classical/cardinality.v b/classical/cardinality.v index 078276a223..a4f2dae11c 100644 --- a/classical/cardinality.v +++ b/classical/cardinality.v @@ -742,8 +742,6 @@ move=> /finite_fsetP[{}A ->] /finite_fsetP[{}B ->]. apply/finite_fsetP; exists (A `*` B)%fset; apply/predeqP => x. by split; rewrite /= inE => /andP. Qed. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to finite_setX.")] -Notation finite_setM := finite_setX (only parsing). Lemma finite_image2 [aT bT rT : Type] [A : set aT] [B : set bT] (f : aT -> bT -> rT) : @@ -843,8 +841,6 @@ apply/fsetP => i; apply/idP/idP; rewrite !(inE, in_fset_set)//=. by move=> [/mem_set-> /mem_set->]. by move=> /andP[]; rewrite !inE. Qed. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to fset_setX.")] -Notation fset_setM := fset_setX (only parsing). Definition fst_fset (T1 T2 : choiceType) (A : {fset (T1 * T2)}) : {fset T1} := [fset x.1 | x in A]%fset. @@ -912,8 +908,6 @@ Proof. move=> Afin Bfin; rewrite -bigcupX1l. by apply: bigcup_finite => // i Ai; exact/finite_setX/Bfin. Qed. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to finite_setXR.")] -Notation finite_setMR := finite_setXR (only parsing). Lemma finite_setXL (T T' : choiceType) (A : T' -> set T) (B : set T') : (forall x, B x -> finite_set (A x)) -> finite_set B -> finite_set (A ``*` B). @@ -921,8 +915,6 @@ Proof. move=> Afin Bfin; rewrite -bigcupX1r. by apply: bigcup_finite => // i Ai; apply/finite_setX => //; exact: Afin. Qed. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to finite_setXL.")] -Notation finite_setML := finite_setXL (only parsing). Lemma fset_set_II n : fset_set `I_n = [fset val i | i in 'I_n]%fset. Proof. @@ -1232,14 +1224,10 @@ have /ppcard_leP[f] := Bc i Ai; apply/pcard_geP/surjPex. exists (fun k => (i, f^-1%FUN k)) => -[_ j]/= [-> dj]. by exists (f j) => //=; rewrite funK ?inE. Qed. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to countableXR.")] -Notation countableMR := countableXR (only parsing). Lemma countableX T1 T2 (D1 : set T1) (D2 : set T2) : countable D1 -> countable D2 -> countable (D1 `*` D2). Proof. by move=> D1c D2c; exact: countableXR (fun _ _ => D2c). Qed. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to countableX.")] -Notation countableM := countableX (only parsing). Lemma countableXL T T' (A : T' -> set T) (B : set T') : countable B -> (forall i, B i -> countable (A i)) -> countable (A ``*` B). @@ -1247,8 +1235,6 @@ Proof. move=> Bc Ac; rewrite -bigcupX1r; apply: bigcup_countable => // i Bi. by apply: countableX => //; exact: Ac. Qed. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to countableXL.")] -Notation countableML := countableXL (only parsing). Lemma infiniteXRl T T' (A : set T) (B : T -> set T') : infinite_set A -> (forall i, B i !=set0) -> infinite_set (A `*`` B). @@ -1257,8 +1243,6 @@ move=> /infiniteP/pcard_geP[f] /(_ _)/cid-/all_sig[b Bb]. apply/infiniteP/pcard_geP/surjPex; exists (fun x => f x.1). by move=> i iT; have [a Aa fa] := 'oinvP_f iT; exists (a, b a). Qed. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to infiniteXRl.")] -Notation infiniteMRl := infiniteXRl (only parsing). Lemma cardXR_eq_nat T T' (A : set T) (B : T -> set T') : (A #= [set: nat] -> (forall i, countable (B i) /\ B i !=set0) -> @@ -1267,8 +1251,6 @@ Proof. rewrite !card_eq_le => /andP[Acnt /infiniteP Ainfty] /all_and2[Bcnt Bn0]. by rewrite [(_ #<= _)%card]countableXR//=; exact/infiniteP/infiniteXRl. Qed. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to cardXR_eq_nat.")] -Notation cardMR_eq_nat := cardXR_eq_nat (only parsing). Lemma eq_cardSP {T : Type} (A : set T) n : reflect (exists2 x, A x & A `\ x #= `I_n) (A #= `I_n.+1). diff --git a/classical/classical_sets.v b/classical/classical_sets.v index bb1f91d6dc..bc88f41214 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -337,14 +337,8 @@ Arguments setU _ _ _ _ /. Arguments setC _ _ _ /. Arguments setD _ _ _ _ /. Arguments setX _ _ _ _ _ /. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setX.")] -Notation setM := setX (only parsing). Arguments setXR _ _ _ _ _ /. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setXR.")] -Notation setMR := setXR (only parsing). Arguments setXL _ _ _ _ _ /. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setXL.")] -Notation setML := setXL (only parsing). Arguments fst_set _ _ _ _ /. Arguments snd_set _ _ _ _ /. Arguments subsetP {T A B}. @@ -1189,33 +1183,7 @@ Arguments subsetT {T} A. #[global] Hint Resolve subsetUl subsetUr subIsetl subIsetr subDsetl subDsetr : core. -#[deprecated(since="mathcomp-analysis 1.2.0", note="Use notin_setE instead.")] -Notation notin_set := notin_setE (only parsing). Arguments setU_id2r {T} C {A B}. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to in_setX.")] -Notation in_setM := in_setX (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setX0.")] -Notation setM0 := setX0 (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to set0X.")] -Notation set0M := set0X (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setXTT.")] -Notation setMTT := setXTT (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setXT.")] -Notation setMT := setXT (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setTX.")] -Notation setTM := setTX (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setXI.")] -Notation setMI := setXI (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setX_bigcupr.")] -Notation setM_bigcupr := setX_bigcupr (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setX_bigcupl.")] -Notation setM_bigcupl := setX_bigcupl (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to setSX.")] -Notation setSM := setSX (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to bigcupX1l.")] -Notation bigcupM1l := bigcupX1l (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to bigcupX1r.")] -Notation bigcupM1r := bigcupX1r (only parsing). Lemma set_cst {T I} (x : T) (A : set I) : [set x | _ in A] = if A == set0 then set0 else [set x]. @@ -2090,11 +2058,6 @@ End bigop_lemmas. Arguments bigcup_setD1 {T I} x. Arguments bigcap_setD1 {T I} x. -#[deprecated(since="mathcomp-analysis 1.3.0",note="renamed to bigcup_setX_dep")] -Notation bigcup_setM_dep := bigcup_setX_dep (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0",note="renamed to bigcup_setX")] -Notation bigcup_setM := bigcup_setX (only parsing). - Lemma setD_bigcup {T} (I : eqType) (F : I -> set T) (P : set I) (j : I) : P j -> F j `\` \bigcup_(i in [set k | P k /\ k != j]) (F j `\` F i) = \bigcap_(i in P) F i. @@ -3250,12 +3213,6 @@ Lemma fst_setXR (X : set T1) (Y : T1 -> set T2) : (X `*`` Y).`1 `<=` X. Proof. by move=> x [y [//]]. Qed. End product. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to fst_setX.")] -Notation fst_setM := fst_setX (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to snd_setX.")] -Notation snd_setM := snd_setX (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to fst_setXR instead.")] -Notation fst_setMR := fst_setXR (only parsing). Section section. Variables (T1 T2 : Type). @@ -3376,14 +3333,6 @@ Lemma ysection_preimage_fst (A : set T1) y : ysection (fst @^-1` A) y = A. Proof. by apply/seteqP; split; move=> x/=; rewrite /ysection/= inE. Qed. End section. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to in_xsectionX.")] -Notation in_xsectionM := in_xsectionX (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to in_ysectionX.")] -Notation in_ysectionM := in_ysectionX (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to notin_xsectionX.")] -Notation notin_xsectionM := notin_xsectionX (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to notin_ysectionX.")] -Notation notin_ysectionM := notin_ysectionX (only parsing). Declare Scope relation_scope. Delimit Scope relation_scope with relation. diff --git a/classical/fsbigop.v b/classical/fsbigop.v index e58ee8f5df..e0fc85da63 100644 --- a/classical/fsbigop.v +++ b/classical/fsbigop.v @@ -1,6 +1,8 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets. From mathcomp Require Import functions cardinality. (**md**************************************************************************) diff --git a/classical/functions.v b/classical/functions.v index e76c099074..38cf34e941 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -1,7 +1,9 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat. From HB Require Import structures. -From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets. Add Search Blacklist "__canonical__". Add Search Blacklist "__functions_". Add Search Blacklist "_factory_". diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 8e097c5c08..f9dd338c0e 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1,5 +1,5 @@ -(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum. +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint. (**md**************************************************************************) (* # MathComp extra *) @@ -83,3 +83,15 @@ Proof. by move=> F0; elim/big_rec : _ => // i x Pi; apply/ler_wnDl/F0. Qed. Lemma card_fset_sum1 (T : choiceType) (A : {fset T}) : #|` A| = (\sum_(i <- A) 1)%N. Proof. by rewrite big_seq_fsetE/= sum1_card cardfE. Qed. + +(**************************) +(* MathComp 2.6 additions *) +(**************************) + +(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *) +Lemma intrD1 {R : pzRingType} (i : int) : (i + 1)%:~R = i%:~R + 1 :> R. +Proof. by rewrite intrD. Qed. + +(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *) +Lemma intr1D {R : pzRingType} (i : int) : (1 + i)%:~R = 1 + i%:~R :> R. +Proof. by rewrite intrD. Qed. diff --git a/classical/set_interval.v b/classical/set_interval.v index beb62092d8..ae5d6163cc 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -1,7 +1,9 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum interval. -From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets. From mathcomp Require Import functions. (**md**************************************************************************) @@ -208,8 +210,6 @@ Qed. End set_itv_porderType. Arguments neitv {disp T} _. -#[deprecated(since="mathcomp-analysis 1.4.0", note="renamed to `subset_itvScc`")] -Notation subset_itvS := subset_itvScc (only parsing). #[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `set_itvNyy`")] Notation set_itv_infty_infty := set_itvNyy (only parsing). #[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `set_itvoy`")] @@ -707,7 +707,7 @@ Lemma range_factor ba bb a b : a < b -> [set` Interval (BSide ba 0) (BSide bb 1)]. Proof. by move=> /(factor_itv_bij ba bb)/Pbij[f ->]; rewrite image_eq. Qed. -Lemma onem_factor a b x : a != b -> `1-(factor a b x) = factor b a x. +Lemma onem_factor a b x : a != b -> (factor a b x).~ = factor b a x. Proof. rewrite eq_sym -subr_eq0 => ab; rewrite /onem /factor -(divff ab) -mulrBl. by rewrite opprB addrA subrK -mulrNN opprB -invrN opprB. diff --git a/classical/unstable.v b/classical/unstable.v index 10df3539f6..da4e0b8087 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint. -From mathcomp Require Import archimedean interval mathcomp_extra. +From mathcomp Require Import archimedean interval. (**md**************************************************************************) (* # MathComp extra *) @@ -275,27 +275,31 @@ by rewrite (leq_trans (leq_card_setU _ _))// leq_add. Qed. Definition onem {R : pzRingType} (r : R) : R := 1 - r. +#[deprecated(since="mathcomp-analysis 1.15.0")] Notation "`1- r" := (onem r) : ring_scope. +Reserved Notation "p '.~'" (format "p .~", at level 1). +Notation "p '.~'" := (onem p) : ring_scope. + Section onem_ring. Context {R : pzRingType}. Implicit Type r : R. -Lemma onem0 : `1-0 = 1 :> R. Proof. by rewrite /onem subr0. Qed. +Lemma onem0 : 0.~ = 1 :> R. Proof. by rewrite /onem subr0. Qed. -Lemma onem1 : `1-1 = 0 :> R. Proof. by rewrite /onem subrr. Qed. +Lemma onem1 : 1.~ = 0 :> R. Proof. by rewrite /onem subrr. Qed. -Lemma onemK r : `1-(`1-r) = r. Proof. exact: subKr. Qed. +Lemma onemK r : (r.~).~ = r. Proof. exact: subKr. Qed. -Lemma add_onemK r : r + `1- r = 1. Proof. by rewrite /onem addrC subrK. Qed. +Lemma add_onemK r : r + r.~ = 1. Proof. by rewrite /onem addrC subrK. Qed. -Lemma onemD r s : `1-(r + s) = `1-r - s. +Lemma onemD r s : (r + s).~ = r.~ - s. Proof. by rewrite /onem opprD addrA. Qed. -Lemma onemMr r s : s * `1-r = s - s * r. +Lemma onemMr r s : s * r.~ = s - s * r. Proof. by rewrite /onem mulrBr mulr1. Qed. -Lemma onemM r s : `1-(r * s) = `1-r + `1-s - `1-r * `1-s. +Lemma onemM r s : (r * s).~ = r.~ + s.~ - r.~ * s.~. Proof. by rewrite /onem mulrBl 2!mulrBr !mul1r mulr1 addrKA opprK subrKA. Qed. End onem_ring. @@ -304,34 +308,34 @@ Section onem_order. Variable R : numDomainType. Implicit Types r : R. -Lemma onem_gt0 r : r < 1 -> 0 < `1-r. Proof. by rewrite subr_gt0. Qed. +Lemma onem_gt0 r : r < 1 -> 0 < r.~. Proof. by rewrite subr_gt0. Qed. -Lemma onem_ge0 r : r <= 1 -> 0 <= `1-r. +Lemma onem_ge0 r : r <= 1 -> 0 <= r.~. Proof. by rewrite le_eqVlt => /predU1P[->|/onem_gt0/ltW]; rewrite ?onem1. Qed. -Lemma onem_le1 r : 0 <= r -> `1-r <= 1. +Lemma onem_le1 r : 0 <= r -> r.~ <= 1. Proof. by rewrite lerBlDr lerDl. Qed. -Lemma onem_lt1 r : 0 < r -> `1-r < 1. +Lemma onem_lt1 r : 0 < r -> r.~ < 1. Proof. by rewrite ltrBlDr ltrDl. Qed. -Lemma onemX_ge0 r n : 0 <= r -> r <= 1 -> 0 <= `1-(r ^+ n). +Lemma onemX_ge0 r n : 0 <= r -> r <= 1 -> 0 <= (r ^+ n).~. Proof. by move=> ? ?; rewrite subr_ge0 exprn_ile1. Qed. -Lemma onemX_lt1 r n : 0 < r -> `1-(r ^+ n) < 1. +Lemma onemX_lt1 r n : 0 < r -> (r ^+ n).~ < 1. Proof. by move=> ?; rewrite onem_lt1// exprn_gt0. Qed. End onem_order. Lemma normr_onem {R : realDomainType} (x : R) : - (0 <= x <= 1 -> `| `1-x | <= 1)%R. + (0 <= x <= 1 -> `| x.~ | <= 1)%R. Proof. move=> /andP[x0 x1]; rewrite ler_norml; apply/andP; split. by rewrite lerBrDl lerBlDr (le_trans x1)// lerDl. by rewrite lerBlDr lerDl. Qed. -Lemma onemV (F : numFieldType) (x : F) : x != 0 -> `1-(x^-1) = (x - 1) / x. +Lemma onemV (F : numFieldType) (x : F) : x != 0 -> x^-1.~ = (x - 1) / x. Proof. by move=> ?; rewrite mulrDl divff// mulN1r. Qed. Lemma lez_abs2 (a b : int) : 0 <= a -> a <= b -> (`|a| <= `|b|)%N. @@ -401,14 +405,6 @@ Qed. End order_min. -(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *) -Lemma intrD1 {R : pzRingType} (i : int) : i%:~R + 1 = (i + 1)%:~R :> R. -Proof. by rewrite intrD. Qed. - -(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *) -Lemma intr1D {R : pzRingType} (i : int) : 1 + i%:~R = (1 + i)%:~R :> R. -Proof. by rewrite intrD. Qed. - Section bijection_forall. Lemma bij_forall A B (f : A -> B) (P : B -> Prop) : diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index d9cd247e12..93cf4d82b5 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) (* -------------------------------------------------------------------- *) (* Copyright (c) - 2015--2016 - IMDEA Software Institute *) (* Copyright (c) - 2015--2018 - Inria *) @@ -1721,9 +1721,6 @@ Qed. End DualERealArithTh_numDomainType. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dN`")] -Notation gte_dopp := gte_dN (only parsing). - End DualAddTheoryNumDomain. Section ERealArithTh_realDomainType. @@ -2957,16 +2954,6 @@ Arguments lee_sum_nneg_natl {R}. Arguments lee_sum_npos_natl {R}. #[global] Hint Extern 0 (is_true (0 <= `| _ |)%E) => solve [apply: abse_ge0] : core. -#[deprecated(since="mathcomp-analysis 1.3.0", note="Use `lte_leD` instead.")] -Notation lte_le_add := lte_leD (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="Use `lee_ltD` instead.")] -Notation lee_lt_add := lee_ltD (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="Use `lte_leB` instead.")] -Notation lte_le_sub := lte_leB (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="Use leeN2 instead.")] -Notation lee_opp2 := leeN2 (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="Use lteN2 instead.")] -Notation lte_opp2 := lteN2 (only parsing). #[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to maxe_pMr")] Notation maxeMr := maxe_pMr (only parsing). #[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to maxe_pMl")] @@ -3380,55 +3367,6 @@ Arguments lee_dsum_npos_natr {R}. Arguments lee_dsum_nneg_natl {R}. Arguments lee_dsum_npos_natl {R}. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dD`")] -Notation lte_dadd := lte_dD (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dDl`")] -Notation lee_daddl := lee_dDl (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dDr`")] -Notation lee_daddr := lee_dDr (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gee_dDl`")] -Notation gee_daddl := gee_dDl (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gee_dDr`")] -Notation gee_daddr := gee_dDr (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dDl`")] -Notation lte_daddl := lte_dDl (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dDr`")] -Notation lte_daddr := lte_dDr (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dBl`")] -Notation gte_dsubl := gte_dBl (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dBr`")] -Notation gte_dsubr := gte_dBr (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dDl`")] -Notation gte_daddl := gte_dDl (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dDr`")] -Notation gte_daddr := gte_dDr (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dD2lE`")] -Notation lte_dadd2lE := lte_dD2lE (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dD2rE`")] -Notation lee_dadd2rE := lee_dD2rE (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dD2l`")] -Notation lee_dadd2l := lee_dD2l (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dD2r`")] -Notation lee_dadd2r := lee_dD2r (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dD`")] -Notation lee_dadd := lee_dD (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dB`")] -Notation lee_dsub := lee_dB (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dBlDr`")] -Notation lte_dsubl_addr := lte_dBlDr (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dBlDl`")] -Notation lte_dsubl_addl := lte_dBlDl (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dBrDr`")] -Notation lte_dsubr_addr := lte_dBrDr (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dBrDl`")] -Notation lte_dsubr_addl := lte_dBrDl (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_le_dD`")] -Notation lte_le_dadd := lte_le_dD (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_lt_dD`")] -Notation lee_lt_dadd := lee_lt_dD (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_le_dB`")] -Notation lte_le_dsub := lte_le_dD (only parsing). - End DualAddTheoryRealDomain. Section realFieldType_lemmas. @@ -3728,40 +3666,6 @@ rewrite neq_lt => /orP[|] r0. Qed. End realFieldType_lemmas. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_pdivrMl`")] -Notation lte_pdivr_mull := lte_pdivrMl (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_pdivrMr`")] -Notation lte_pdivr_mulr := lte_pdivrMr (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_pdivlMl`")] -Notation lte_pdivl_mull := lte_pdivlMl (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_pdivlMr`")] -Notation lte_pdivl_mulr := lte_pdivlMr (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_pdivrMl`")] -Notation lee_pdivr_mull := lee_pdivrMl (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_pdivrMr`")] -Notation lee_pdivr_mulr := lee_pdivrMr (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_pdivlMl`")] -Notation lee_pdivl_mull := lee_pdivlMl (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_pdivlMr`")] -Notation lee_pdivl_mulr := lee_pdivlMr (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_ndivrMl`")] -Notation lte_ndivr_mull := lte_ndivrMl (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_ndivrMr`")] -Notation lte_ndivr_mulr := lte_ndivrMr (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_ndivlMl`")] -Notation lte_ndivl_mull := lte_ndivlMl (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_ndivlMr`")] -Notation lte_ndivl_mulr := lte_ndivlMr (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_ndivrMl`")] -Notation lee_ndivr_mull := lee_ndivrMl (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_ndivrMr`")] -Notation lee_ndivr_mulr := lee_ndivrMr (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_ndivlMl`")] -Notation lee_ndivl_mull := lee_ndivlMl (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_ndivlMr`")] -Notation lee_ndivl_mulr := lee_ndivlMr (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `eqe_pdivrMl`")] -Notation eqe_pdivr_mull := eqe_pdivrMl (only parsing). Module DualAddTheoryRealField. diff --git a/reals/reals.v b/reals/reals.v index fee962db81..0ec78136a6 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) (* -------------------------------------------------------------------- *) (* Copyright (c) - 2015--2016 - IMDEA Software Institute *) (* Copyright (c) - 2015--2018 - Inria *) @@ -45,7 +45,9 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra. -From mathcomp Require Import boolp classical_sets set_interval. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval. Declare Scope real_scope. @@ -55,7 +57,6 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Theory. -From mathcomp Require Import unstable. (* -------------------------------------------------------------------- *) Delimit Scope real_scope with real. @@ -430,8 +431,7 @@ Notation inf_lbound := ge_inf (only parsing). (* -------------------------------------------------------------------- *) Section FloorTheory. Variable R : realType. - -Implicit Types x y : R. +Implicit Types (x y : R) (i : int). Lemma has_sup_floor_set x : has_sup (floor_set x). Proof. @@ -469,7 +469,7 @@ Lemma RfloorE x : Rfloor x = (Num.floor x)%:~R. Proof. by []. Qed. Lemma mem_rg1_floor x : (range1 (Num.floor x)%:~R) x. -Proof. by rewrite /range1 /mkset intrD1 floor_le_tmp floorD1_gt. Qed. +Proof. by rewrite /range1 /mkset -intrD1 floor_le_tmp floorD1_gt. Qed. Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x. Proof. exact: mem_rg1_floor. Qed. @@ -480,27 +480,26 @@ Proof. by case/andP: (mem_rg1_Rfloor x). Qed. Lemma lt_succ_Rfloor x : x < Rfloor x + 1. Proof. by case/andP: (mem_rg1_Rfloor x). Qed. -Lemma range1z_inj x (m1 m2 : int) : - (range1 m1%:~R) x -> (range1 m2%:~R) x -> m1 = m2. +Lemma range1z_inj x i1 i2 : (range1 i1%:~R) x -> (range1 i2%:~R) x -> i1 = i2. Proof. -move=> /andP[m1x x_m1] /andP[m2x x_m2]. -wlog suffices: m1 m2 m1x {x_m1 m2x} x_m2 / (m1 <= m2). +move=> /andP[i1x x_i1] /andP[i2x x_i2]. +wlog suffices: i1 i2 i1x {x_i1 i2x} x_i2 / (i1 <= i2). by move=> ih; apply/eqP; rewrite eq_le !ih. rewrite -(lerD2r 1) lezD1 -(@ltr_int R) intrD. -exact/(le_lt_trans m1x). +exact/(le_lt_trans i1x). Qed. Lemma range1rr x : (range1 x) x. Proof. by rewrite /range1/mkset lexx /= ltrDl ltr01. Qed. -Lemma range1zP (m : int) x : Rfloor x = m%:~R <-> (range1 m%:~R) x. +Lemma range1zP i x : Rfloor x = i%:~R <-> (range1 i%:~R) x. Proof. split=> [<-|h]; first exact/mem_rg1_Rfloor. -by congr intmul; apply/floor_def; rewrite -intrD1. +by congr intmul; apply/floor_def; rewrite intrD1. Qed. -Lemma Rfloor_natz (z : int) : Rfloor z%:~R = z%:~R :> R. -Proof. by apply/range1zP/range1rr. Qed. +Lemma Rfloor_natz i : Rfloor i%:~R = i%:~R :> R. +Proof. exact/range1zP/range1rr. Qed. Lemma Rfloor0 : Rfloor 0 = 0 :> R. Proof. by rewrite /Rfloor floor0. Qed. @@ -509,10 +508,10 @@ Lemma Rfloor1 : Rfloor 1 = 1 :> R. Proof. by rewrite /Rfloor floor1. Qed. Lemma le_Rfloor : {homo (@Rfloor R) : x y / x <= y}. Proof. by move=> x y /Num.Theory.le_floor; rewrite ler_int. Qed. -Lemma Rfloor_ge_int x (n : int) : (n%:~R <= x)= (n%:~R <= Rfloor x). +Lemma Rfloor_ge_int x (i : int) : (i%:~R <= x)= (i%:~R <= Rfloor x). Proof. by rewrite ler_int floor_ge_int_tmp. Qed. -Lemma Rfloor_lt_int x (z : int) : (x < z%:~R) = (Rfloor x < z%:~R). +Lemma Rfloor_lt_int x (i : int) : (x < i%:~R) = (Rfloor x < i%:~R). Proof. by rewrite ltr_int -floor_lt_int. Qed. Lemma Rfloor_le0 x : x <= 0 -> Rfloor x <= 0. @@ -521,7 +520,7 @@ Proof. by move=> ?; rewrite -Rfloor0 le_Rfloor. Qed. Lemma Rfloor_lt0 x : x < 0 -> Rfloor x < 0. Proof. by move=> x0; rewrite (le_lt_trans _ x0) // Rfloor_le. Qed. -Lemma ltr_add_invr (y x : R) : y < x -> exists k, y + k.+1%:R^-1 < x. +Lemma ltr_add_invr y x : y < x -> exists k, y + k.+1%:R^-1 < x. Proof. move=> yx; exists (Num.truncn (x - y)^-1). by rewrite -ltrBrDl invf_plt 1?posrE 1?subr_gt0// truncnS_gt. @@ -552,10 +551,6 @@ Proof. by move=> x0; rewrite /Rceil ler0z -(ceil0 R) le_ceil_tmp. Qed. Lemma RceilE x : Rceil x = (Num.ceil x)%:~R. Proof. by []. Qed. -#[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.ceil_le` instead")] -Lemma le_ceil : {homo @Num.ceil R : x y / x <= y}. -Proof. exact: le_ceil_tmp. Qed. - End CeilTheory. (* -------------------------------------------------------------------- *) diff --git a/reals/signed.v b/reals/signed.v index d73bea1d2c..4dc5e44a65 100644 --- a/reals/signed.v +++ b/reals/signed.v @@ -1,8 +1,10 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import ssreflect ssrfun ssrbool. From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint. -From mathcomp Require Import mathcomp_extra unstable. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra. Attributes deprecated(since="mathcomp-analysis 1.9.0", note="Use ""From mathcomp Require Import interval_inference."" instead."). @@ -1203,14 +1205,14 @@ Section onem_signed. Variable R : numDomainType. Implicit Types r : R. -Lemma onem_PosNum r (r1 : r < 1) : `1-r = (PosNum (onem_gt0 r1))%:num. +Lemma onem_PosNum r (r1 : r < 1) : r.~ = (PosNum (onem_gt0 r1))%:num. Proof. by []. Qed. Lemma onemX_NngNum r (r1 : r <= 1) (r0 : 0 <= r) n : - `1-(r ^+ n) = (NngNum (onemX_ge0 n r0 r1))%:num. + (r ^+ n).~ = (NngNum (onemX_ge0 n r0 r1))%:num. Proof. by []. Qed. -Lemma onem_nonneg_proof (p : {nonneg R}) : p%:num <= 1 -> 0 <= `1-(p%:num). +Lemma onem_nonneg_proof (p : {nonneg R}) : p%:num <= 1 -> 0 <= (p%:num).~. Proof. by rewrite /onem/= subr_ge0. Qed. Definition onem_nonneg (p : {nonneg R}) (p1 : p%:num <= 1) := diff --git a/theories/charge.v b/theories/charge.v index 2b4c9a09cc..8c89636c7e 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1,10 +1,12 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. From mathcomp Require Import finmap fingroup perm rat. -From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. -From mathcomp Require Import cardinality functions fsbigop set_interval. -From mathcomp Require Import reals interval_inference ereal topology numfun. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets cardinality. +From mathcomp Require Import functions fsbigop set_interval reals. +From mathcomp Require Import interval_inference ereal topology numfun. From mathcomp Require Import normedtype sequences esum measure realfun. From mathcomp Require Import lebesgue_measure lebesgue_integral. diff --git a/theories/convex.v b/theories/convex.v index e56d6d5c8f..baf57b7a23 100644 --- a/theories/convex.v +++ b/theories/convex.v @@ -2,6 +2,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect finmap ssralg ssrint ssrnum interval. From mathcomp Require Import interval_inference. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval. From mathcomp Require Import functions cardinality ereal reals topology. From mathcomp Require Import prodnormedzmodule normedtype derive realfun. @@ -54,7 +56,7 @@ Local Notation "x <| p |> y" := (conv p x y). Definition law := forall (p q r s : {i01 R}) (a b c : T), p%:num = r%:num * s%:num -> - `1- (s%:num) = `1- (p%:num) * `1- (q%:num) -> + s%:num.~ = p%:num.~ * q%:num.~ -> a <| p |> (b <| q |> c) = (a <| r |> b) <| s |> c. End def. @@ -130,7 +132,7 @@ Implicit Type p q r : {i01 R}. Let E := convex_lmodType E'. -Let avg p (a b : E) := p%:inum *: a + `1-(p%:inum) *: b. +Let avg p (a b : E) := p%:inum *: a + p%:inum.~ *: b. Let avg1 a b : avg 1%:i01 a b = a. Proof. by rewrite /avg/= onem1 scale0r scale1r addr0. Qed. @@ -195,11 +197,11 @@ by rewrite subr_gt0 lt_neqAle t1 le1. Qed. Lemma convRE (a b : R^o) (t : {i01 R}) : - a <| t |> b = t%:inum * a + `1-(t%:inum) * b. + a <| t |> b = t%:inum * a + t%:inum.~ * b. Proof. by []. Qed. Let convRCE (a b : R^o) (t : {i01 R}) : - a <| t |> b = `1-(t%:inum) * b + t%:inum * a. + a <| t |> b = t%:inum.~ * b + t%:inum * a. Proof. by rewrite addrC convRE. Qed. Lemma convR_line_path (a b : R^o) (t : {i01 R}) : diff --git a/theories/derive.v b/theories/derive.v index 36e66ada9a..440a1497e2 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -2,8 +2,10 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval poly. From mathcomp Require Import sesquilinear. -From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. -From mathcomp Require Import functions reals interval_inference topology. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import reals interval_inference topology. From mathcomp Require Import prodnormedzmodule tvs normedtype landau. (**md**************************************************************************) @@ -1261,7 +1263,7 @@ Proof. by have /derivableP := @derivable_id x v; rewrite derive_val. Qed. End derive_id. Lemma derive1_onem {R : numFieldType} : - (fun x => `1-x : R^o)^`()%classic = cst (-1). + (fun x => x.~ : R^o)^`()%classic = cst (-1). Proof. by apply/funext => x; rewrite derive1E deriveB// derive_id derive_cst sub0r. Qed. diff --git a/theories/ereal.v b/theories/ereal.v index 8c0eb51a68..1b206b7cee 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) (* -------------------------------------------------------------------- *) (* Copyright (c) - 2015--2016 - IMDEA Software Institute *) (* Copyright (c) - 2015--2018 - Inria *) @@ -6,10 +6,11 @@ (* -------------------------------------------------------------------- *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap. -From mathcomp Require Import boolp classical_sets functions. -From mathcomp Require Import fsbigop cardinality set_interval. -From mathcomp Require Import reals interval_inference topology. -From mathcomp Require Export constructive_ereal unstable. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import fsbigop cardinality set_interval reals. +From mathcomp Require Export interval_inference topology constructive_ereal. (**md**************************************************************************) (* # Extended real numbers, classical part ($\overline{\mathbb{R}}$) *) @@ -55,12 +56,9 @@ Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Theory. Import numFieldTopology.Exports. -From mathcomp Require Import mathcomp_extra unstable. Local Open Scope ring_scope. - Local Open Scope ereal_scope. - Local Open Scope classical_set_scope. Lemma EFin_bigcup T (F : nat -> set T) : diff --git a/theories/exp.v b/theories/exp.v index d4993d29e6..e3a5271069 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -1,9 +1,11 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat interval_inference. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions mathcomp_extra. -From mathcomp Require Import unstable reals topology ereal tvs normedtype. -From mathcomp Require Import landau sequences derive realfun convex. +From mathcomp Require Import reals topology ereal tvs normedtype landau. +From mathcomp Require Import sequences derive realfun convex. (**md**************************************************************************) (* # Theory of exponential/logarithm functions *) diff --git a/theories/ftc.v b/theories/ftc.v index 98077abc63..b83b6a397f 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -2,6 +2,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop reals interval_inference ereal. From mathcomp Require Import topology tvs normedtype sequences real_interval. @@ -1805,11 +1807,11 @@ Lemma integration_by_substitution_onem (G : R -> R) (r : R) : (0 <= r <= 1)%R -> {within `[0%R, r], continuous G} -> \int[mu]_(x in `[0%R, r]) (G x)%:E = - \int[mu]_(x in `[`1-r, 1%R]) (G `1-x)%:E. + \int[mu]_(x in `[r.~, 1%R]) (G x.~)%:E. Proof. move=> /andP[]; rewrite le_eqVlt => /predU1P[<- *|r0 r1 cG]. by rewrite onem0 2!set_itv1 2!integral_set1. -have := @integration_by_substitution_decreasing R onem G `1-r 1. +have := @integration_by_substitution_decreasing R onem G r.~ 1. rewrite onemK onem1 => -> //. - by apply: eq_integral => x xr; rewrite !fctE derive1_onem opprK mulr1. - by rewrite lerBlDl lerDr ltW. @@ -1830,7 +1832,7 @@ Lemma Rintegration_by_substitution_onem (G : R -> R) (r : R) : (0 <= r <= 1)%R -> {within `[0%R, r], continuous G} -> (\int[mu]_(x in `[0, r]) (G x) = - \int[mu]_(x in `[`1-r, 1]) (G `1-x))%R. + \int[mu]_(x in `[r.~, 1]) (G x.~))%R. Proof. by move=> r01 cG; rewrite [in LHS]/Rintegral integration_by_substitution_onem. Qed. diff --git a/theories/function_spaces.v b/theories/function_spaces.v index 5c8b871fa0..a20bb345d3 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -1,9 +1,11 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. -From mathcomp Require Import boolp classical_sets functions. -From mathcomp Require Import cardinality mathcomp_extra unstable fsbigop reals. -From mathcomp Require Import interval_inference topology. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop reals interval_inference. +From mathcomp Require Import topology. (**md**************************************************************************) (* # The topology of functions spaces *) diff --git a/theories/hoelder.v b/theories/hoelder.v index 1b24000c39..8f7bab2e18 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -1,7 +1,9 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import mathcomp_extra unstable boolp interval_inference. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp interval_inference. From mathcomp Require Import classical_sets functions cardinality fsbigop reals. From mathcomp Require Import ereal topology normedtype sequences real_interval. From mathcomp Require Import esum measure ess_sup_inf lebesgue_measure. @@ -534,7 +536,7 @@ Lemma convex_powR p : 1 <= p -> Proof. move=> p1 t x y /[!inE] /= /[!in_itv] /= /[!andbT] x_ge0 y_ge0. have p0 : 0 < p by rewrite (lt_le_trans _ p1). -rewrite !convRE; set w1 := t%:num; set w2 := `1-(t%:inum). +rewrite !convRE; set w1 := t%:num; set w2 := t%:inum.~. have [->|w20] := eqVneq w2 0. rewrite !mul0r !addr0; have [->|w10] := eqVneq w1 0. by rewrite !mul0r powR0// gt_eqF. @@ -693,7 +695,7 @@ rewrite ge0_integralD//; last 2 first. exact: measurableT_comp. exact/measurableT_comp_powR/measurableT_comp/measurable_funD. rewrite [leRHS](_ : _ = ('N_p%:E[f] + 'N_p%:E[g]) * - (\int[mu]_x (`|f x + g x| `^ p)%:E) `^ `1-(p^-1)). + (\int[mu]_x (`|f x + g x| `^ p)%:E) `^ p^-1.~). rewrite muleDl; last 2 first. - rewrite fin_num_poweR//. under eq_integral do rewrite -poweR_EFin -abse_EFin. diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index d436b7cc77..d9f999083e 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -1,9 +1,10 @@ -(* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. -From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. -From mathcomp Require Import functions cardinality fsbigop reals topology. -From mathcomp Require Import function_spaces. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop reals topology function_spaces. (**md**************************************************************************) (* # wedge sum for sigT *) diff --git a/theories/lebesgue_integral_theory/giry.v b/theories/lebesgue_integral_theory/giry.v index 7594918993..3d369c65cc 100644 --- a/theories/lebesgue_integral_theory/giry.v +++ b/theories/lebesgue_integral_theory/giry.v @@ -203,8 +203,7 @@ Lemma giry_map_dirac (mu1 : giry T1 R) (B : set T2) : measurable B -> Proof. move=> mB. rewrite -[in LHS](setIT B) -[LHS]integral_indic// [LHS]giry_int_map//. - exact/measurable_EFinP/measurable_indic. -by move=> ?; rewrite lee_fin. +exact/measurable_EFinP/measurable_indic. Qed. End giry_map_lemmas. diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v index fec5bd46e5..5f8c7703f6 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integrable.v +++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v @@ -1,13 +1,15 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. -From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. -From mathcomp Require Import functions cardinality reals fsbigop. -From mathcomp Require Import interval_inference topology ereal tvs normedtype. -From mathcomp Require Import sequences real_interval function_spaces esum. -From mathcomp Require Import measure lebesgue_measure numfun realfun. -From mathcomp Require Import simple_functions measurable_fun_approximation. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality reals fsbigop interval_inference. +From mathcomp Require Import topology ereal tvs normedtype sequences. +From mathcomp Require Import real_interval function_spaces esum measure. +From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. +From mathcomp Require Import measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. From mathcomp Require Import lebesgue_integral_monotone_convergence. From mathcomp Require Import lebesgue_integral_nonneg. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v index 5e2bcad05a..385c2ae69c 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v @@ -1,12 +1,13 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. -From mathcomp Require Import functions cardinality reals fsbigop. -From mathcomp Require Import interval_inference ereal topology tvs normedtype. -From mathcomp Require Import sequences real_interval esum measure. -From mathcomp Require Import lebesgue_measure numfun realfun function_spaces. -From mathcomp Require Import simple_functions. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality reals fsbigop interval_inference. +From mathcomp Require Import ereal topology tvs normedtype sequences. +From mathcomp Require Import real_interval esum measure lebesgue_measure numfun. +From mathcomp Require Import realfun function_spaces simple_functions. (**md**************************************************************************) (* # Definition of the Lebesgue integral *) diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v index eeb4e48f6a..94707803b4 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v @@ -1,13 +1,15 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. -From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. -From mathcomp Require Import functions cardinality reals fsbigop. -From mathcomp Require Import interval_inference topology ereal tvs normedtype. -From mathcomp Require Import sequences real_interval function_spaces esum. -From mathcomp Require Import measure lebesgue_measure numfun realfun. -From mathcomp Require Import simple_functions measurable_fun_approximation. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality reals fsbigop interval_inference. +From mathcomp Require Import topology ereal tvs normedtype sequences. +From mathcomp Require Import real_interval function_spaces esum measure. +From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. +From mathcomp Require Import measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. (**md**************************************************************************) diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index 087a36bd8c..a6ad41e9fb 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -1,13 +1,15 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. -From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. -From mathcomp Require Import functions cardinality reals fsbigop. -From mathcomp Require Import interval_inference topology ereal tvs normedtype. -From mathcomp Require Import sequences real_interval function_spaces esum. -From mathcomp Require Import measure lebesgue_measure numfun realfun. -From mathcomp Require Import simple_functions measurable_fun_approximation. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality reals fsbigop interval_inference. +From mathcomp Require Import topology ereal tvs normedtype sequences. +From mathcomp Require Import real_interval function_spaces esum measure. +From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. +From mathcomp Require Import measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. From mathcomp Require Import lebesgue_integral_monotone_convergence. @@ -1034,10 +1036,6 @@ Lemma integralEpatch (D : set T) (mD : measurable D) (f : T -> \bar R) : Proof. by rewrite -[in LHS](setIid D) integral_mkcondr. Qed. End integral_patch. -#[deprecated(since="mathcomp-analysis 1.3.0", note="use `integral_mkcondr` instead")] -Notation integral_setI_indic := __deprecated__integral_setI_indic (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="use `integralEpatch` instead")] -Notation integralEindic := __deprecated__integralEindic (only parsing). Section ge0_cvgn_integral. Local Open Scope ereal_scope. diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v index 88af112a6a..14da12b366 100644 --- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v +++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v @@ -1,12 +1,14 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. -From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. -From mathcomp Require Import functions cardinality reals fsbigop. -From mathcomp Require Import interval_inference topology ereal tvs normedtype. -From mathcomp Require Import sequences real_interval function_spaces esum. -From mathcomp Require Import measure lebesgue_measure numfun realfun exp. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality reals fsbigop interval_inference. +From mathcomp Require Import topology ereal tvs normedtype sequences. +From mathcomp Require Import real_interval function_spaces esum measure. +From mathcomp Require Import lebesgue_measure numfun realfun exp. From mathcomp Require Import simple_functions. (**md**************************************************************************) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index c05a9532e6..1bdafa94af 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1,7 +1,9 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean rat. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets. From mathcomp Require Import functions cardinality fsbigop reals. From mathcomp Require Import interval_inference ereal topology numfun tvs. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 0e7947c120..7f0d773d3b 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean rat. @@ -360,8 +360,6 @@ by apply: measurableU; [exact: measurable_image_EFin|exact: measurableU]. Qed. #[global] Hint Extern 0 (measurable_fun _ fine) => solve [exact: fine_measurable] : core. -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `fine_measurable` instead")] -Notation measurable_fine := fine_measurable (only parsing). Section measurable_fun_measurable. Local Open Scope ereal_scope. @@ -895,16 +893,6 @@ End standard_measurable_fun. solve [exact: mulrl_measurable] : core. #[global] Hint Extern 0 (measurable_fun _ (fun x => x ^+ _)) => solve [exact: exprn_measurable] : core. -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `exprn_measurable` instead")] -Notation measurable_exprn := exprn_measurable (only parsing). -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `mulrl_measurable` instead")] -Notation measurable_mulrl := mulrl_measurable (only parsing). -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `mulrr_measurable` instead")] -Notation measurable_mulrr := mulrr_measurable (only parsing). -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `oppr_measurable` instead")] -Notation measurable_oppr := oppr_measurable (only parsing). -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `normr_measurable` instead")] -Notation measurable_normr := normr_measurable (only parsing). Lemma measurable_funX d (T : measurableType d) {R : realType} D (f : T -> R) n : measurable_fun D f -> measurable_fun D (fun x => f x ^+ n). @@ -912,8 +900,6 @@ Proof. move=> mf. exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f). Qed. -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `measurable_funX` instead")] -Notation measurable_fun_pow := measurable_funX (only parsing). Section measurable_fun_realType. Context d (T : measurableType d) (R : realType). @@ -1455,14 +1441,6 @@ End standard_emeasurable_fun. solve [exact: EFin_measurable] : core. #[global] Hint Extern 0 (measurable_fun _ -%E) => solve [exact: oppe_measurable] : core. -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `oppe_measurable` instead")] -Notation measurable_oppe := oppe_measurable (only parsing). -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `abse_measurable` instead")] -Notation measurable_abse := abse_measurable (only parsing). -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `EFin_measurable` instead")] -Notation measurable_EFin := EFin_measurable (only parsing). -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `natmul_measurable` instead")] -Notation measurable_natmul := natmul_measurable (only parsing). (* NB: real-valued function *) Lemma measurable_EFinP d (T : measurableType d) (R : realType) (D : set T) @@ -1475,8 +1453,6 @@ rewrite [X in measurable X](_ : _ = D `&` (EFin \o g) @^-1` (EFin @` A)). congr (_ `&` _);rewrite eqEsubset; split=> [|? []/= _ /[swap] -[->//]]. by move=> ? ?; exact: preimage_image. Qed. -#[deprecated(since="mathcomp-analysis 1.6.0", note="use `measurable_EFinP` instead")] -Notation EFin_measurable_fun := measurable_EFinP (only parsing). Lemma measurable_fun_dirac d {T : measurableType d} {R : realType} D (U : set T) : diff --git a/theories/measure_theory/counting_measure.v b/theories/measure_theory/counting_measure.v index 630555f9e6..164a39e3c1 100644 --- a/theories/measure_theory/counting_measure.v +++ b/theories/measure_theory/counting_measure.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap. From mathcomp Require Import boolp classical_sets functions cardinality reals. @@ -16,7 +16,6 @@ From mathcomp Require Import sequences measurable_structure measure_function. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import ProperNotations. Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope classical_set_scope. diff --git a/theories/measure_theory/dirac_measure.v b/theories/measure_theory/dirac_measure.v index 21124ee7c9..f9267eef01 100644 --- a/theories/measure_theory/dirac_measure.v +++ b/theories/measure_theory/dirac_measure.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets. @@ -21,7 +21,6 @@ Reserved Notation "'\d_' a" (at level 8, a at level 2, format "'\d_' a"). Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import ProperNotations. Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope classical_set_scope. diff --git a/theories/measure_theory/measurable_function.v b/theories/measure_theory/measurable_function.v index ce3f705fd3..56c294b87d 100644 --- a/theories/measure_theory/measurable_function.v +++ b/theories/measure_theory/measurable_function.v @@ -1,6 +1,8 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality reals. From mathcomp Require Import ereal topology normedtype. From mathcomp Require Import sequences measurable_structure. diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index d9196e229f..2866461f8a 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -1,6 +1,8 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality reals. From mathcomp Require Import ereal topology normedtype sequences. @@ -214,8 +216,6 @@ Definition lambda_system := Definition monotone := ndseq_closed /\ niseq_closed. End set_systems. -(*#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `setSD_closed`")] -Notation setD_closed := setSD_closed (only parsing).*) #[deprecated(since="mathcomp-analysis 1.9.0", note="renamed `setD_closed`")] Notation setDI_closed := setD_closed (only parsing). #[deprecated(since="mathcomp-analysis 1.9.0", note="renamed `setD_semi_setD_closed`")] @@ -1571,8 +1571,6 @@ rewrite setXT setTX; apply: measurableI. - by apply: sub_sigma_algebra; left; exists A => //; rewrite setTI. - by apply: sub_sigma_algebra; right; exists B => //; rewrite setTI. Qed. -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `measurableX`")] -Notation measurableM := measurableX (only parsing). Section product_salgebra_algebraOfSetsType. Context d1 d2 (T1 : algebraOfSetsType d1) (T2 : algebraOfSetsType d2). diff --git a/theories/measure_theory/measure_extension.v b/theories/measure_theory/measure_extension.v index 368e6dab3d..1db0086dd2 100644 --- a/theories/measure_theory/measure_extension.v +++ b/theories/measure_theory/measure_extension.v @@ -81,7 +81,6 @@ Reserved Notation "mu .-cara.-measurable" (format "mu .-cara.-measurable"). Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import ProperNotations. Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope classical_set_scope. diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v index bc8b51584d..8324cef378 100644 --- a/theories/measure_theory/measure_function.v +++ b/theories/measure_theory/measure_function.v @@ -1,6 +1,8 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. From mathcomp Require Import reals interval_inference ereal topology normedtype. From mathcomp Require Import sequences esum. diff --git a/theories/measure_theory/measure_negligible.v b/theories/measure_theory/measure_negligible.v index 05c563edc8..f3d1511d94 100644 --- a/theories/measure_theory/measure_negligible.v +++ b/theories/measure_theory/measure_negligible.v @@ -1,6 +1,8 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality reals. From mathcomp Require Import interval_inference ereal topology normedtype. From mathcomp Require Import sequences numfun. diff --git a/theories/measure_theory/probability_measure.v b/theories/measure_theory/probability_measure.v index adcdb9f54d..46a04c39ee 100644 --- a/theories/measure_theory/probability_measure.v +++ b/theories/measure_theory/probability_measure.v @@ -41,7 +41,6 @@ From mathcomp Require Import measurable_structure measure_function dirac_measure Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import ProperNotations. Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope classical_set_scope. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 779eeb8d5b..e6fe7b6c9b 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -3,6 +3,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint. From mathcomp Require Import archimedean rat interval zmodp vector. From mathcomp Require Import fieldext falgebra. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets filter functions cardinality. From mathcomp Require Import set_interval interval_inference ereal reals. From mathcomp Require Import topology function_spaces real_interval. diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v index 9465b43a0f..ef634f6da2 100644 --- a/theories/normedtype_theory/num_normedtype.v +++ b/theories/normedtype_theory/num_normedtype.v @@ -1,10 +1,11 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean rat. -From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. -From mathcomp Require Import functions cardinality set_interval. -From mathcomp Require Import interval_inference reals topology. -From mathcomp Require Import function_spaces real_interval. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality set_interval interval_inference reals. +From mathcomp Require Import topology function_spaces real_interval. From mathcomp Require Import prodnormedzmodule tvs. (**md**************************************************************************) diff --git a/theories/normedtype_theory/urysohn.v b/theories/normedtype_theory/urysohn.v index 28d4131220..116662c57b 100644 --- a/theories/normedtype_theory/urysohn.v +++ b/theories/normedtype_theory/urysohn.v @@ -2,6 +2,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import set_interval interval_inference ereal reals. From mathcomp Require Import topology function_spaces tvs num_normedtype. diff --git a/theories/normedtype_theory/vitali_lemma.v b/theories/normedtype_theory/vitali_lemma.v index 09fcecb53e..57ff3f6031 100644 --- a/theories/normedtype_theory/vitali_lemma.v +++ b/theories/normedtype_theory/vitali_lemma.v @@ -1,7 +1,9 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean rat. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import set_interval interval_inference ereal reals. From mathcomp Require Import topology function_spaces tvs num_normedtype. diff --git a/theories/numfun.v b/theories/numfun.v index 0ce6da7b8e..1079b0eeb2 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -1,6 +1,8 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets fsbigop. From mathcomp Require Import functions cardinality set_interval. From mathcomp Require Import interval_inference reals ereal topology normedtype. diff --git a/theories/probability.v b/theories/probability.v index 0c87621819..add6f3e5f8 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -1,7 +1,9 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg. From mathcomp Require Import poly ssrnum ssrint interval archimedean finmap. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets. From mathcomp Require Import functions cardinality fsbigop. From mathcomp Require Import exp numfun lebesgue_measure lebesgue_integral. @@ -70,7 +72,7 @@ From mathcomp Require Import charge ftc gauss_integral hoelder. (* exponential_prob r == exponential probability measure *) (* poisson_pmf r k == pmf of the Poisson distribution with parameter r *) (* poisson_prob r == Poisson probability measure *) -(* XMonemX a b := x ^+ a * `1-x ^+ b *) +(* XMonemX a b := x ^+ a * x.~ ^+ b *) (* beta_fun a b := \int[mu]_x (XMonemX a.-1 b.-1 \_`[0,1] x) *) (* beta_pdf == probability density function for beta *) (* beta_prob == beta probability measure *) @@ -1276,11 +1278,11 @@ Variables (p : R) (p01 : (0 <= p <= 1)%R). Local Open Scope ereal_scope. Lemma bernoulli_probE A : - bernoulli_prob p A = p%:E * \d_true A + (`1-p)%:E * \d_false A. + bernoulli_prob p A = p%:E * \d_true A + p.~%:E * \d_false A. Proof. by case/andP : p01 => p0 p1; rewrite bernoulli_dirac// measure_addE. Qed. Lemma integral_bernoulli_prob (f : bool -> \bar R) : (forall x, 0 <= f x) -> - \int[bernoulli_prob p]_y (f y) = p%:E * f true + (`1-p)%:E * f false. + \int[bernoulli_prob p]_y (f y) = p%:E * f true + p.~%:E * f false. Proof. move=> f0; case/andP : p01 => p0 p1; rewrite bernoulli_dirac/=. rewrite ge0_integral_measure_sum// 2!big_ord_recl/= big_ord0 adde0/=. @@ -1323,7 +1325,7 @@ Section binomial_pmf. Local Open Scope ring_scope. Context {R : realType} (n : nat) (p : R). -Definition binomial_pmf k := p ^+ k * (`1-p) ^+ (n - k) *+ 'C(n, k). +Definition binomial_pmf k := p ^+ k * p.~ ^+ (n - k) *+ 'C(n, k). Lemma binomial_pmf_ge0 k (p01 : (0 <= p <= 1)%R) : 0 <= binomial_pmf k. Proof. @@ -1378,7 +1380,7 @@ Let binomial_setT : binomial [set: _] = 1. Proof. rewrite /binomial; case: ifPn; last by move=> _; rewrite probability_setT. move=> p01; rewrite /binomial_pmf. -have pkn k : 0%R <= (p ^+ k * `1-p ^+ (n - k) *+ 'C(n, k))%:E. +have pkn k : 0%R <= (p ^+ k * p.~ ^+ (n - k) *+ 'C(n, k))%:E. case/andP : p01 => p0 p1. by rewrite lee_fin mulrn_wge0// mulr_ge0 ?exprn_ge0 ?subr_ge0. rewrite (esumID `I_n.+1)// [X in _ + X]esum1 ?adde0; last first. @@ -1420,7 +1422,7 @@ Proof. apply/funext => U. rewrite /binomial_prob; case: ifPn => [_|]; last by rewrite p1 p0. rewrite /msum/= /mscale/= /binomial_pmf. -have pkn k : (0%R <= (p ^+ k * `1-p ^+ (n - k) *+ 'C(n, k))%:E)%E. +have pkn k : (0%R <= (p ^+ k * p.~ ^+ (n - k) *+ 'C(n, k))%:E)%E. by rewrite lee_fin mulrn_wge0// mulr_ge0 ?exprn_ge0 ?subr_ge0. rewrite (esumID `I_n.+1)//= [X in _ + X]esum1 ?adde0; last first. by move=> /= k [_ /negP]; rewrite -leqNgt => nk; rewrite bin_small. @@ -1446,7 +1448,7 @@ End binomial_probability. Lemma integral_binomial_prob (R : realType) n p U : (0 <= p <= 1)%R -> (\int[binomial_prob n p]_y \d_(0 < y)%N U = - bernoulli_prob (1 - `1-p ^+ n) U :> \bar R)%E. + bernoulli_prob (1 - p.~ ^+ n) U :> \bar R)%E. Proof. move=> /andP[p0 p1]; rewrite bernoulli_probE//=; last first. rewrite subr_ge0 exprn_ile1//=; [|exact/onem_ge0|exact/onem_le1]. @@ -1460,12 +1462,12 @@ rewrite -ge0_sume_distrl; last first. move=> i _. by apply/mulrn_wge0/mulr_ge0; apply/exprn_ge0 => //; exact/onem_ge0. congr *%E. -transitivity (\sum_(i < n.+1) (`1-p ^+ (n - i) * p ^+ i *+ 'C(n, i))%:E - - (`1-p ^+ n)%:E)%E. +transitivity (\sum_(i < n.+1) (p.~ ^+ (n - i) * p ^+ i *+ 'C(n, i))%:E - + (p.~ ^+ n)%:E)%E. rewrite big_ord_recl/=. rewrite expr0 mulr1 subn0 bin0 mulr1n addrAC -EFinD subrr add0e. by rewrite /bump; under [RHS]eq_bigr do rewrite leq0n add1n mulrC. -rewrite sumEFin -(@exprDn_comm _ `1-p p n)//. +rewrite sumEFin -(@exprDn_comm _ p.~ p n)//. by rewrite subrK expr1n. by rewrite /GRing.comm/onem mulrC. Qed. @@ -2176,21 +2178,21 @@ Section about_onemXn. Context {R : realType}. Implicit Types x y : R. -Lemma continuous_onemXn n x : {for x, continuous (fun y => `1-y ^+ n)}. +Lemma continuous_onemXn n x : {for x, continuous (fun y => y.~ ^+ n)}. Proof. apply: (@continuous_comp _ _ _ (@onem R) (fun x => x ^+ n)). by apply: (@cvgB _ R^o); [exact: cvg_cst|exact: cvg_id]. exact: exprn_continuous. Qed. -Lemma onemXn_derivable n x : derivable (fun y => `1-y ^+ n) x 1. +Lemma onemXn_derivable n x : derivable (fun y => y.~ ^+ n) x 1. Proof. have := @derivableX _ _ (@onem R) n x 1. by rewrite fctE; apply; exact: derivableB. Qed. Lemma derivable_oo_LRcontinuous_onemXnMr n x : - derivable_oo_LRcontinuous (fun y => `1-y ^+ n * x) 0 1. + derivable_oo_LRcontinuous (fun y => y.~ ^+ n * x) 0 1. Proof. split. - by move=> y y01; apply: derivableM => //=; exact: onemXn_derivable. @@ -2207,7 +2209,7 @@ split. Qed. Lemma derive_onemXn n x : - (fun y => `1-y ^+ n)^`()%classic x = - n%:R * `1-x ^+ n.-1. + (fun y => y.~ ^+ n)^`()%classic x = - n%:R * x.~ ^+ n.-1. Proof. rewrite (@derive1_comp _ (@onem _) (fun x => x ^+ n))//; last first. exact: exprn_derivable. @@ -2216,10 +2218,10 @@ by rewrite derive1_cst derive_id sub0r mulrN1 [in RHS]mulNr scaler1. Qed. Lemma Rintegral_onemXn n : - \int[lebesgue_measure]_(x in `[0, 1]) (`1-x ^+ n) = n.+1%:R^-1 :> R. + \int[lebesgue_measure]_(x in `[0, 1]) (x.~ ^+ n) = n.+1%:R^-1 :> R. Proof. rewrite /Rintegral. -rewrite (@continuous_FTC2 _ _ (fun x => `1-x ^+ n.+1 / - n.+1%:R))//=. +rewrite (@continuous_FTC2 _ _ (fun x => x.~ ^+ n.+1 / - n.+1%:R))//=. - rewrite onem1 expr0n/= mul0r onem0 expr1n mul1r sub0r. by rewrite -invrN -2!mulNrn opprK. - by apply: continuous_in_subspaceT => x x01; exact: continuous_onemXn. @@ -2237,7 +2239,7 @@ Section XMonemX. Context {R : numDomainType}. Implicit Types (x : R) (a b : nat). -Definition XMonemX a b := fun x => x ^+ a * `1-x ^+ b. +Definition XMonemX a b := fun x => x ^+ a * x.~ ^+ b. Lemma XMonemX_ge0 a b x : x \in `[0, 1] -> 0 <= XMonemX a b x. Proof. @@ -2250,7 +2252,7 @@ rewrite in_itv/= => /andP[t0 t1]. by rewrite mulr_ile1// ?(exprn_ge0,onem_ge0,exprn_ile1,onem_le1). Qed. -Lemma XMonemX0n n x : XMonemX 0 n x = `1-x ^+ n. +Lemma XMonemX0n n x : XMonemX 0 n x = x.~ ^+ n. Proof. by rewrite /XMonemX/= expr0 mul1r. Qed. Lemma XMonemXn0 n x : XMonemX n 0 x = x ^+ n. @@ -2385,7 +2387,7 @@ Lemma beta_funSSnSm a b : beta_fun a.+2 b.+1 = a.+1%:R / b.+1%:R * beta_fun a.+1 b.+2. Proof. rewrite -[LHS]Rintegral_mkcond. -rewrite (@Rintegration_by_parts _ _ (fun x => `1-x ^+ b.+1 / - b.+1%:R) +rewrite (@Rintegration_by_parts _ _ (fun x => x.~ ^+ b.+1 / - b.+1%:R) (fun x => a.+1%:R * x ^+ a)); last 7 first. exact: ltr01. apply/continuous_subspaceT => x. @@ -2396,7 +2398,7 @@ rewrite (@Rintegration_by_parts _ _ (fun x => `1-x ^+ b.+1 / - b.+1%:R) by apply: cvg_at_left_filter; exact: exprn_continuous. by move=> x x01; rewrite derive1E exp_derive scaler1. by apply/continuous_subspaceT => x x01; exact: continuous_onemXn. - exact: derivable_oo_continuous_bnd_onemXnMr. + exact: derivable_oo_LRcontinuous_onemXnMr. move=> x x01; rewrite derive1Mr; last exact: onemXn_derivable. by rewrite derive_onemXn mulrAC divff// mul1r. rewrite {1}/onem !(expr1n,mul1r,expr0n,subr0,subrr,mul0r,oppr0,sub0r)/=. @@ -2699,7 +2701,7 @@ Qed. Local Close Scope ereal_scope. Lemma integral_beta_prob_bernoulli_prob_onemX_lty {R : realType} n a b U : - (\int[beta_prob a b]_x `|bernoulli_prob (`1-x ^+ n) U| < +oo :> \bar R)%E. + (\int[beta_prob a b]_x `|bernoulli_prob (x.~ ^+ n) U| < +oo :> \bar R)%E. Proof. apply: integral_beta_prob_bernoulli_prob_lty => //=. by apply: measurable_funX => //; exact: measurable_funB. @@ -2709,7 +2711,7 @@ by rewrite lerBlDl -lerBlDr subrr. Qed. Lemma integral_beta_prob_bernoulli_prob_onem_lty {R : realType} n a b U : - (\int[beta_prob a b]_x `|bernoulli_prob (1 - `1-x ^+ n) U| < +oo :> \bar R)%E. + (\int[beta_prob a b]_x `|bernoulli_prob (1 - x.~ ^+ n) U| < +oo :> \bar R)%E. Proof. apply: integral_beta_prob_bernoulli_prob_lty => //=. apply: measurable_funB => //. @@ -2740,7 +2742,7 @@ Qed. Lemma beta_prob_integrable_onem {R : realType} a b a' b' : (beta_prob a b).-integrable `[0, 1] - (fun x : measurableTypeR R => (`1-(XMonemX a' b' x))%:E). + (fun x : measurableTypeR R => (XMonemX a' b' x).~%:E). Proof. apply: (eq_integrable _ (cst 1 \- (fun x : measurableTypeR R => (XMonemX a' b' x)%:E))%E) => //. @@ -2777,7 +2779,7 @@ Qed. Lemma beta_prob_integrable_onem_dirac {R : realType} a b a' b' (c : bool) U : (beta_prob a b).-integrable `[0, 1] - (fun x : measurableTypeR R => (`1-(XMonemX a' b' x))%:E * \d_c U)%E. + (fun x : measurableTypeR R => (XMonemX a' b' x).~%:E * \d_c U)%E. Proof. apply: integrableMl => //=; last first. exists 1; split => // x x1/= _ _; rewrite (le_trans _ (ltW x1))//. @@ -2885,7 +2887,7 @@ congr (_ + _). by apply/measurableT_comp => //; exact: measurable_XMonemX. by have /integrableP[_] := @beta_prob_integrable R a b c d. transitivity ((\int[mu]_(x in `[0%R, 1%R]) - ((`1-x ^+ d)%:E * ((beta_pdf a b x)%:E * (x ^+ c)%:E)))%E : \bar R). + ((x.~ ^+ d)%:E * ((beta_pdf a b x)%:E * (x ^+ c)%:E)))%E : \bar R). apply: eq_integral => /= x _. by rewrite [in LHS]EFinM -[LHS]muleA [LHS]muleC -[LHS]muleA. transitivity ((beta_fun a b)^-1%:E * \int[mu]_(x in `[0%R, 1%R]) diff --git a/theories/realfun.v b/theories/realfun.v index 59b17fe0de..1acb9d7af9 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -2,6 +2,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint. From mathcomp Require Import archimedean interval. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality contra ereal reals interval_inference. From mathcomp Require Import topology prodnormedzmodule tvs normedtype derive. @@ -1092,8 +1094,6 @@ move=> supfal inffal; apply/cvg_at_leftNP/lime_sup_inf_at_right. Qed. End lime_sup_inf. -#[deprecated(since="mathcomp-analysis 1.3.0", note="use `limf_esup_ge0` instead")] -Notation lime_sup_ge0 := __deprecated__lime_sup_ge0 (only parsing). Section derivable_oo_LRcontinuous. Context {R : numFieldType} {V : normedModType R}. diff --git a/theories/sequences.v b/theories/sequences.v index 703056d04b..52f168ea92 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -2,6 +2,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint. From mathcomp Require Import interval interval_inference archimedean. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp contra classical_sets. From mathcomp Require Import functions cardinality set_interval reals. From mathcomp Require Import ereal topology tvs normedtype landau. @@ -3063,8 +3065,8 @@ have /le_trans -> // : `| y n - y (n + m)| <= rewrite [_ * `|_|]mulrC exprD mulrA geometric_seriesE ?lt_eqF//=. pose q' := Itv01 [elaborate ge0 q] (ltW q1). rewrite -[q%:num]/(q'%:num) -!mulrA -mulrDr ler_pM// {}/q'/=. - rewrite -!/(`1-_) -mulrDr exprSr onemM -addrA. - rewrite -[in leRHS](mulrC _ `1-(_ ^+ m)) -onemMr onemK. + rewrite -!/(_.~) -mulrDr exprSr onemM -addrA. + rewrite -[in leRHS](mulrC _ (_ ^+ m).~) -onemMr onemK. by rewrite [in leRHS]mulrDl mulrAC mulfV ?mul1r// gt_eqF// onem_gt0. rewrite geometric_seriesE ?lt_eqF//= -[leRHS]mulr1 (ACl (1*4*2*3))/= -/C. by rewrite ler_wpM2l// 1?mulr_ge0// lerBlDr lerDl. diff --git a/theories/showcase/pnt.v b/theories/showcase/pnt.v index 44515bb727..b57bd3ec1f 100644 --- a/theories/showcase/pnt.v +++ b/theories/showcase/pnt.v @@ -1,4 +1,6 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import classical_sets boolp topology. From mathcomp Require Import ereal sequences reals. Import Order.POrderTheory GRing.Theory Num.Theory. diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v index 9c60d0d450..4b5ffb1bb1 100644 --- a/theories/topology_theory/metric_structure.v +++ b/theories/topology_theory/metric_structure.v @@ -1,9 +1,11 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. From mathcomp Require Import interval_inference rat interval zmodp vector. From mathcomp Require Import fieldext falgebra archimedean finmap. -From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets. From mathcomp Require Import contra reals topology_structure. From mathcomp Require Import uniform_structure pseudometric_structure. From mathcomp Require Import num_topology product_topology separation_axioms. diff --git a/theories/topology_theory/order_topology.v b/theories/topology_theory/order_topology.v index 575beac12a..8ebe9b9229 100644 --- a/theories/topology_theory/order_topology.v +++ b/theories/topology_theory/order_topology.v @@ -1,7 +1,9 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap all_classical. -From mathcomp Require Import unstable topology_structure uniform_structure. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import topology_structure uniform_structure. From mathcomp Require Import product_topology pseudometric_structure. (**md**************************************************************************) diff --git a/theories/topology_theory/product_topology.v b/theories/topology_theory/product_topology.v index 8f5ee2b032..56dd633458 100644 --- a/theories/topology_theory/product_topology.v +++ b/theories/topology_theory/product_topology.v @@ -1,6 +1,8 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical unstable. +From mathcomp Require Import all_ssreflect all_algebra all_classical. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import interval_inference topology_structure. From mathcomp Require Import uniform_structure pseudometric_structure compact. diff --git a/theories/topology_theory/pseudometric_structure.v b/theories/topology_theory/pseudometric_structure.v index 74575ef120..2d76d10172 100644 --- a/theories/topology_theory/pseudometric_structure.v +++ b/theories/topology_theory/pseudometric_structure.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra all_classical. From mathcomp Require Import interval_inference reals topology_structure. @@ -260,9 +260,6 @@ have [//|z [fxz yz]] := near (Fy _ (gt0 eps)) x. by exists z => //; split => //; apply: subP. Unshelve. all: end_near. Qed. -#[deprecated(since="mathcomp-analysis 1.6.0", note="use `cvgi_ballP` instead")] -Definition cvg_toi_locally := @cvgi_ballP. - Lemma cvgi_ball T {F} {FF : Filter F} (f : T -> M -> Prop) y : f `@ F --> y -> forall eps : R, 0 < eps -> F [set x | exists z, f x z /\ ball y eps z]. diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v index 808f3b5c7c..bfd887b681 100644 --- a/theories/topology_theory/separation_axioms.v +++ b/theories/topology_theory/separation_axioms.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap. From mathcomp Require Import boolp classical_sets functions wochoice. @@ -328,9 +328,6 @@ have: (f `@ F) setT by apply: fFl; apply: filterT. by rewrite fmapiE; apply: filterS => x [y []]; exists y. Unshelve. all: by end_near. Qed. -#[deprecated(since="mathcomp-analysis 1.5.0", note="use `cvgi_close` instead")] -Definition cvg_toi_locally_close := @cvgi_close. - Hypothesis sep : hausdorff_space T. Lemma closeE x y : close x y = (x = y). diff --git a/theories/topology_theory/sigT_topology.v b/theories/topology_theory/sigT_topology.v index adcc862390..4de744f871 100644 --- a/theories/topology_theory/sigT_topology.v +++ b/theories/topology_theory/sigT_topology.v @@ -1,6 +1,8 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical unstable. +From mathcomp Require Import all_ssreflect all_algebra all_classical. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import topology_structure compact subspace_topology. (**md**************************************************************************) diff --git a/theories/topology_theory/weak_topology.v b/theories/topology_theory/weak_topology.v index 9cdf931535..963fefbf74 100644 --- a/theories/topology_theory/weak_topology.v +++ b/theories/topology_theory/weak_topology.v @@ -1,6 +1,8 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical unstable. +From mathcomp Require Import all_ssreflect all_algebra all_classical. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import interval_inference reals topology_structure. From mathcomp Require Import uniform_structure order_topology. From mathcomp Require Import pseudometric_structure. diff --git a/theories/trigo.v b/theories/trigo.v index f70d8256ee..3b3eaf2822 100644 --- a/theories/trigo.v +++ b/theories/trigo.v @@ -1,12 +1,13 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat. -From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. -From mathcomp Require Import functions reals ereal interval_inference topology. -From mathcomp Require Import normedtype landau sequences derive realfun exp. -From mathcomp Require Import realfun measure lebesgue_measure lebesgue_integral. -From mathcomp Require Import ftc. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import reals ereal interval_inference topology normedtype. +From mathcomp Require Import landau sequences derive realfun exp realfun. +From mathcomp Require Import measure lebesgue_measure lebesgue_integral ftc. (**md**************************************************************************) (* # Theory of trigonometric functions *)