From 6526d2b814dcd1f9ea551b7a4f68ea9535bd94de Mon Sep 17 00:00:00 2001 From: adjevahi Date: Wed, 8 Jul 2026 15:37:24 +0200 Subject: [PATCH 1/8] sigma-algebra for normed modules + sfun codomain sigma ring & module structure --- CHANGELOG_UNRELEASED.md | 430 ++++++++++++++++++ classical/filter.v | 2 +- theories/hoelder.v | 2 +- theories/kernel.v | 4 - theories/lebesgue_integral_theory/giry.v | 3 + .../lebesgue_integral_definition.v | 10 - .../lebesgue_integral_differentiation.v | 1 - .../lebesgue_integral_monotone_convergence.v | 3 - .../lebesgue_integral_nonneg.v | 7 - .../measurable_fun_approximation.v | 6 +- .../simple_functions.v | 180 ++++++-- .../probability_theory/normal_distribution.v | 1 + .../probability_theory/uniform_distribution.v | 1 - .../real_measure/lebesgue_stieltjes_measure.v | 120 +++-- 14 files changed, 650 insertions(+), 120 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d7f0405803..f8d087d901 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -3,6 +3,271 @@ ## [Unreleased] ### Added +- in `borel_hierarchy.v`: + + definition `borel_type` + + lemmas `singleton_bigcap`, `measurable1` + +- in `simple_functions.v`: + + lemmas `sfun_op`, `sfun_submod_closed` + + `{sfun aT >-> borel_type V}` is an `lmodType` when `V` is a `normedModType` + +- in `simple_functions.v`: + + lemmas `mem_sfun_comp_pair`, `sfun_submod_closed` + + `{sfun aT >-> V}` is an `lmodType` when `V` is a `normedModType` + + definitions `indic_lmod` `mindic_lmod` `mindic_lmod_sfun` + + lemmas `indic_lmodE` `preimage_indic_mod` `measurable_indic_lmod` + +- in `set_interval.v`: + + lemmas `setU_itvob1`, `setU_1itvob` + +- in `realfun.v`: + + lemma `derivable_sqrt` +- in `classical_sets.v`: + + definition `rectangle` + + lemmas `rectangle_setX`, `setI_closed_rectangle` + + definitions `cross`, `cross12` + + lemmas `smallest_sub_sub`, `bigcap_closed_smallest`, `smallest_sub_iff` + + lemma `preimage_set_systemS` + + lemma `setD_bigcapr` + +- in `measurable_structure.v`: + + lemmas `g_sigma_algebra_cross`, `g_sigma_algebra_rectangle` + + lemma `sigma_algebra_sub` + +- in `measurable_function.v`: + + lemma `preimage_measurability` + +- in `pseudometric_normed_Zmodule.v`: + + lemma `itv_center_shift` + +- in `normed_module.v`: + + lemmas `closure_itvoo` +- in `unstable.v`: + + structures `SemiNorm`, `Norm` + + lemmas `normMn`, `normN`, `ler_norm_sum` + +- in `normed_module.v`: + + structure `NormedVector` + + notation `normedVectType` + + definition `max_space` + + lemmas `sup_closed_ball_compact`, `equivalence_norms`, + `linear_findim_continuous` + +- in `tvs.v`: + + lemmas `cvg_sum`, `sum_continuous` + +- in `classical_sets.v`: + + lemmas `setI_closed_setT`, `setI_closed_set0` + +- in `measurable_function.v`: + + lemma `g_sigma_algebra_preimage_comp` + +- in `measure_function.v`: + + lemma `g_sigma_algebra_finite_measure_unique` + +- new file `independence.v`: + + definition `independent_events` + + definition `mutual_independence` + + lemma `eq_mutual_independence` + + definition `independence2`, `independence2P` + + lemma `mutual_independence_fset` + + lemma `mutual_independence_finiteS` + + theorem `mutual_independence_finite_g_sigma` + + lemma `mutual_dependence_bigcup` + + definition `independent_RVs` + + lemma `independent_RVsD1` + + theorem `independent_generators` + + definition `independent_RVs2` + + lemmas `independent_RVs2_comp`, `independent_RVs2_funrposneg`, + `independent_RVs2_funrnegpos`, `independent_RVs2_funrnegneg`, + `independent_RVs2_funrpospos` + + definition `pairRV`, lemma `measurable_pairRV` + + lemmas `independent_RVs2_product_measure1` + + lemmas `independent_RVs2_setI_preimage`, + `independent_Lfun1_expectation_product_measure_lty` + + lemma `ge0_independent_expectationM` + + lemmas `independent_Lfun1_expectationM_lty`, `independent_Lfun1M`, + `independent_expectationM` + +- in `ereal.v`: + + lemma `ge0_addBefctE` + +- in `measure_extension.v`: + + definition `caratheodory_measure` +- in `measurable_structure.v`: + + structure `PMeasurable`, notation `pmeasurableType` + +- in `subspace_topology.v`: + + lemma `withinU_continuous_patch` +- in `matrix_normedtype.v`: + + lemma `continuous_mx` + +- in `derive.v`: + + instance `is_derive_mx` + + fact `dmx` + + lemma `diffmx` + + lemma `is_diff_mx` + + instance `is_diff_mx` +- in `realsum.v`: + + lemma `esum_psum` + + lemma `esum_sum` + +- in `constructive_ereal.v`: + + definition `esg` + + lemmas `numEesg`, `gte0_esg`, `lte0_esg`, `esg0` + +- in `esum.v`: + + lemmas `esum_eq0P`, `esumZ`, `exchange_esum` + + lemmas `le_esum`, `esumN` + + lemmas `summable_le_esum`, `summable_esum_funepos`, `summable_esumN`, + `summableZ`, `summable_esumZ` + + lemmas `esum_if_eq_op` + + lemmas `exchange_esum_ereal_sup` + +- in `ereal.v`: + + lemmas `exchange_ereal_sup`, `ge0_ereal_supZl`, `ge0_ereal_supZl_range` + +- in `sequences.v`: + + lemmas `ereal_supD`, `ereal_sup_sum` + +- in `reals.v`: + + lemmas `sup_ge0`, `has_sup_wpZl`, `gt0_has_supZl`, `has_sup_Mn`, `sup_Mn` +- in `mathcomp_extra.v`: + + lemmas `divDl_ge0`, `divDl_le1` + +- in `unstable.v`: + + lemmas `divD_onem` + +- in `filter.v`: + + mixin `isSubNbhs`, structure `SubNbhs`, notation `subNbhsType` + +- in `topology_structure.v`: + + structure `SubTopological`, notation `subTopologicalType` + +- in `tvs.v`: + + structure `SubConvexTvs`, notation `subConvexTvsType` + +- in `normed_module.v`: + + structure `SubNormedModule`, notation `subNormedModType` + + instance `ent_xsection_filter` + + light-weigth factory `subLmodule_isSubNormedmodule` + +- new file `hahn_banach_theorem.v`: + + module `LinearGraph` + * definitions `graph`, `linear_graph` + * lemmas `lingraph_00`, `lingraphZ`, `lingraphD` + + module `HahnBanachZorn` + * definitions `extend_graph`, `le_graph`, `functional_graph`, `le_extend_graph` + * record `zorn_type` + * definition `zphi` + * lemma `zorn_type_eq` + * definition `zornS` + * lemmas `zornS_ex`, `domain_extend`, `hahn_banach_witness` + + theorems `hahn_banach_extension`, `hahn_banach_extension_normed` +- in `normal_distribution.v`: + + lemma `normal_funN` + + lemma `normal_fun_sym` + + lemma `normal_fun0abs` + + lemma `normal_pdf_sym` + + lemma `normal_fun_center_new` + + lemma `normal_fun_shift` + + lemma `normal_pdf_uniq_ae` + + lemma `normal_prob_continuous` + + lemma `integral_normal_prob` + + lemma `measurable_normal_prob` + + lemma `emeasurable_bounded_integrable` + + lemmas `integrable_normal_probD1`, `normal_probD1`, `normal_probD2`, `normal_probD` + +- in `lebesgue_stieltjes_measure.v`: + + definition `lebesgue_display` + +- in `realsum.v`: + + lemma `esum_summableP` + +- in `esum.v`: + + lemma `fsetsTE` +- in `ftc.v`: + + lemma `ge0_integration_by_substitution_shift_itvy`, + `ge0_integration_by_substitution_shift_itvNy` +- in `derive.v`: + + lemmas `derivable_row_mx`, `derive_row_mx` + + instance `is_derive_row_mx` + +- in `matrix_normedtype.v` + + lemmas `norm_row_mx`, `norm_row_mx0r`, `norm_row_mx0l`, `cvg_row_mx` + +- in `unstable.v`: + + lemma `sub_row_mx` + +- in `derive.v`: + + lemmas `eqo_row_mx`, `drow_mx`, `diff_row_mx`, + `differentiable_row_mx` + + instance `is_diff_row_mx` + +- in `functions.v`: + + lemmas `zerofctE`, `onefctE` + +- in `functions.v`: + + lemmas `linfunP`, `linfun_eqP` + + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }` + +- in `tvs.v`: + + structure `LinearContinuous` + + factory `isLinearContinuous` + + instance of `ChoiceType` on `{linear_continuous _ -> _ }` + + instance of `LinearContinuous` with the composition of two functions of type `LinearContinuous` + + instance of `LinearContinuous` with the sum of two functions of type `LinearContinuous` + + instance of `LinearContinuous` with the scalar multiplication of a function of type + `LinearContinuous` + + instance of `Continuous` on \-f when f is of type `LinearContinuous` + + instance of `SubModClosed` on `{linear_continuous _ -> _}` + + instance of `SubLModule` on `{linear_continuous _ -> _ }` + + instance of `LinearContinuous` on the null function + + notations `{linear_continuous _ -> _ | _ }` and `{linear_continuous _ -> _ }` + + definitions `lcfun`, `lcfun_key`, `lcfunP` + + lemmas `lcfun_eqP`, `null_fun_continuous`, `fun_cvgD`, + `fun_cvgN`, `fun_cvgZ`, `fun_cvgZr` + + lemmas `lcfun_continuous` and `lcfun_linear` + +- new files `signed_measure.v` and `radon_nikodym.v` + + with the contents of `charge.v` (deprecated) + +- in `esum.v`: + + lemma `ge0_esum` + + lemma `esum_ge` + +- in `functions.v`: + + lemma `preimageD1` + +- in `measure_function.v`: + + lemmas `cvg_measure_bigcap`, `cvg_measure_bigcup` + +- in `classical_sets.v`: + + lemma `bigcup_bigsetU` + +- in `measurable_structure.v`: + + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable` + +- in `lebesgue_stieltjes_measure.v`: + + module `MeasurableRocitv` + + definition `open_type` + + notations `.-open`, `.-open.-measurable` + + module `MeasurableOpen` + * definition `measurableTypeO` + + definition `borel_display` + * definition `measurableO` + * definition `measurableTypeR` + + definition `lebesgue_display` + * definition `measurableR` + + lemmas `measurable_set1`, `measurable_itv` (also declared as hints) + + lemma `measurable_ball_norm` + + definition `ocitv_measure`, lemma `ocitv_measure_ext` + + module `MeasurableR` + + module `RGenOpenSets` + * lemma `measurableE` + +- in `real_interval.v`: + + lemma `set1_bigcap_oo` - in `exp.v`: + lemmas `cvgy_expR`, `cvgNy_expR`, `lny`, `ge0_lt1_powR_cvg0`, @@ -28,12 +293,177 @@ ### Changed +- in `realsum.v`: + + lemma `__admitted__psumB` proved and renamed to `psumB` + +- moved from `measurable_structure.v` to `classical_sets.v`: + + definition `preimage_set_system` + + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, + `preimage_set_system_id` + +- moved from `measurable_structure.v` to `classical_sets.v`: + + definition `preimage_set_system` + + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, + `preimage_set_system_id` + +- moved from `topology_structure.v` to `filter.v`: + + lemma `continuous_comp` (and generalized) + +- in `numfun.v`: + + `fune_abse` renamed to `funeposDneg` and direction of the equality changed + + `funeposneg` renamed to `funeposBneg` and direction of the equality changed + + `funeD_posD` renamed to `funeDB` and direction of the equality changed + +- in `constructive_ereal.v`: + + lemmas `EFin_semi_additive` and `dEFin_semi_additive` turned into `Let`s + +- moved from `charge.v` to `signed_measure.v`: + + mixin `isAdditiveCharge`, structure `AdditiveCharge` + + mixin `isSemiSigmaAdditive`, structure `Charge` + + factory `isCharge` + + lemmas `charge0`, `charge_semi_additiveW`, `charge_semi_additive2E`, + `charge_semi_additive2`, `chargeU`, `chargeDI`, `charge_partition` + + definitions `measure_of_charge`, `charge_of_finite_measure` + + lemma `chargeD` + + definitions `crestr`, `crestr0`, `czero`, `cscale` + + lemmas `dominates_cscalel`, `dominates_cscaler` + + definition `copp` + + lemma `cscaleN1` + + definition `cadd` + + lemmas `dominates_cadd`, `dominates_pushforward` + + definitions `positive_set`, `negative_set` + + lemmas `negative_set_charge_le0`, `negative_set0`, + `positive_negative0`, `bigcup_negative_set`, `negative_setU`, + `hahn_decomposition_lemma` + + definition `hahn_decomposition` + + theorem `Hahn_decomposition` + + lemmas `Hahn_decomposition_uniq`, `cjordan_posE`, `cjordan_negE` + + definitions `jordan_pos`, `jordan_neg` + + lemmas `jordan_posE`, `jordan_negE`, `jordan_decomp`, `jordan_pos_dominates`, + `jordan_neg_dominates` + + definition `charge_variation`, `charge_dominates` + + lemmas `abse_charge_variation`, `null_charge_dominatesP`, + `content_charge_dominatesP`, `charge_variation_continuous` + +- moved from `charge.v` to `radon_nikodym.v`: + + definition `induced_charge` + + lemmas `semi_sigma_additive_nng_induced`, `dominates_induced`, + `integral_normr_continuous` + + definitions `approxRN`, `int_approxRN`, `sup_int_approxRN` + + lemmas `sup_int_approxRN_ge0`, `radon_nikodym_finite`, + `radon_nikodym_sigma_finite`, `change_of_variables`, `integrableM`, + `chain_rule` + + definition `Radon_Nikodym` + + lemmas `Radon_NikodymE`, `Radon_Nikodym_fin_num`, `Radon_Nikodym_integrable`, + `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`, + `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule` +- in `realsum.v`: + + the following now use `funrpos` and `funrneg`: + * definition `sum` + * lemmas `summable_funrpos`, `summable_funrneg` + + lemma `sum0` (now uses `cst`) + +- moved from `realsum` to `numfun.v`: + + now use `funrpos` and `funrneg`: + * lemmas `eq_funrpos`, `eq_funrneg` + * lemma `fpos0` (renamed to `funrpos_cst0`) + * lemma `fneg0` (renamed to `funrneg_cst0`) + * lemmas `funrposZ`, `funrnegZ` + * lemmas `funrpos_natrM`, `funrneg_natrM` + * lemmas `le_funrpos_norm` + +- moved from `numfun.v` to `unstable.v`: + + notations `nondecreasing_fun`, `nonincreasing_fun`, + `decreasing_fun`, `increasing_fun` + +- in `esum.v`: + + definition `esum` + + lemma `esum_fset` + + lemma `esum_ge` -> `PosEsum.pos_esum_ge` + + lemma `le_esum` -> `PosEsum.le_pos_esum` + +- moved from `normed_module.v` to `metric_structure.v` + + lemma `squeeze_cvgr` + +- moved from `pseudometric_normed_Zmodule.v` to `metric_structure.v` + + lemmas `real_cvgr_lt`, `real_cvgr_le`, `real_cvgr_le`, `real_cvgr_gt` + + lemmas `cvgr_lt`, `cvgr_gt`, `cvgr_ge`, `cvgr_le` +- in `normal_distribution.v: + + `normal_fun_center` -> `normal_fun_center0` + +- moved from `measurable_structure.v` to `measure_function.v`: + + definition `subset_sigma_subadditive` + +- moved from `measurable_structure.v` to `unstable.v`: + + notations `nondecreasing_seq`, `nonincreasing_seq` + +- moved from `measurable_structure.v` to `classical_sets.v`: + + notation `^nat` + + defintion `sequence` + + defintion `seqDU` + + lemmas `seqDU_bigcup_eq`, `trivIset_seqDU` + + definition `seqD` + + lemmas `eq_bigcup_seqD`, `trivIset_seqD`, `seqDU_seqD`, `bigcup_bigsetU_bigcup` + +- in `functions.v` + + lemma `fctE` (include `zerofctE` and `onefctE`) + +- in `classical_sets.v` + + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`) + +- moved from `measurable_realfun.v` to `lebesgue_stieltjes_measure.v` + + module `RGenOInfty` + + module `RGenInftyO` + + module `RGenCInfty` + + module `RGenOpens` + +- moved inside module `MeasurableRocitv` (`lebesgue_stieltjes_measure.v`): + + lemmas `measurable_set1`, `measurable_itv` + +- in `lebesgue_stieltjes_measure.v`: + + lemma `lebesgue_stieltjes_measure_unique` is now about the sigma-algebra generated by open sets + ### Renamed ### Generalized - in `lebesgue_integral_nonneg.v`: + lemmas `ge0_integralZl`, `ge0_integralZr` +- in `measurable_structure.v`: + + lemma `sigma_algebra_measurable` (not specialized to `setT` anymore) + +- in `measurable_function.v`: + + lemma `preimage_set_system_measurable_fun` + +- in `measurable_structure.v` + + structure `SemiRingOfSets`, mixin `isSigmaRing`, factories `isRingOfSets`, + `isRingOfSets_setY`, `isAlgebraOfSets`, `isAlgebraOfSets_setD`, `isMeasurable` + are not required to be pointed anymore + + lemmas `measurable_g_measurableTypeE`, `g_sigma_algebra_preimageType`, + `g_sigma_algebra_preimage`, `g_sigma_preimageE`, `g_sigma_preimageE`, + `g_sigma_algebra_rectangle` are generalized from `pointedType` to `choiceType` + (the list might not be exhaustive) + +- in `ereal.v`: + + lemma `funID` generalized from `pointedType` to `Type` + +- in `numfun.v`: + + lemma `indic_restrict` generalized from `pointedType` to `Type` + + factory `FiniteDecomp` generalized from `pointedType`/`nzRingType` to + `Type/pzRingType` + +- in `simple_functions.v`: + + lemmas `fctD`, `fctN`, `fctM`, `fctZ` + + lemmas `sfun0`, `sfunN`, `sfunD`, `sfunB`, `sfunZ`, `sfun_sum`, `sfunprod` + + lemma `simple_bounded` + + structure `SimpleFun` (and notation `{sfun aT >-> _}`): codomain + generalized from `realType` to `sigmaRingType d'`, adding a display parameter `d'`; + +- in `ereal.v`: + + lemmas `ge0_mule_fsumr`, `ge0_mule_fsuml` + +- in `esum.v`: + + lemma `esum_set1` ### Deprecated diff --git a/classical/filter.v b/classical/filter.v index 591459b297..461e0135df 100644 --- a/classical/filter.v +++ b/classical/filter.v @@ -1239,7 +1239,7 @@ move=> near_hom fFG; apply/cvg_to_withinP; split. Qed. Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T) - (F : set_system T) (P : set T) : + (F : set_system T) (P : set T) : Filter F -> (forall i, i \in D -> F [set j | P j -> f i j]) -> F ([set j | P j -> (\bigcap_(i in [set` D]) f i) j]). Proof. move=> FF FfD; exact: (@filter_bigI T I D f _ (within_filter P FF)). Qed. diff --git a/theories/hoelder.v b/theories/hoelder.v index 44fce50f98..11c333ec1b 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -860,7 +860,7 @@ Reserved Notation "{ 'mfun_' mu , U >-> V }" Notation "{ 'mfun_' mu , aT >-> T }" := (@aeEqMfun _ _ aT T _ mu) : form_scope. -Import numFieldNormedType.Exports HBNNSimple. +Import numFieldNormedType.Exports. HB.mixin Record isFinLebesgue d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E) diff --git a/theories/kernel.v b/theories/kernel.v index 1f418be452..c669004aa6 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -1062,7 +1062,6 @@ HB.export KCOMP_SFINITE_KERNEL. Section measurable_fun_preimage_integral. Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). -Import HBNNSimple. Variables (k : Y -> \bar R) (k_ : ({nnsfun Y >-> R}) ^nat) (ndk_ : nondecreasing_seq (k_ : (Y -> R)^nat)) @@ -1109,7 +1108,6 @@ End measurable_fun_preimage_integral. Section measurable_fun_integral_kernel. -Import HBNNSimple. Lemma measurable_fun_integral_kernel d d' (X : measurableType d) (Y : measurableType d') (R : realType) @@ -1140,7 +1138,6 @@ rewrite integral_indic//= /kcomp. by apply: eq_integral => y _; rewrite integral_indic. Qed. -Import HBNNSimple. Let integral_kcomp_nnsfun x (f : {nnsfun Z >-> R}) : \int[kcomp l k x]_z (f z)%:E = \int[l x]_y (\int[k (x, y)]_z (f z)%:E). @@ -1322,7 +1319,6 @@ split => //. + by split => //; rewrite kfcompkindic. Qed. -Import HBNNSimple. (* [Lemma 14.20, Klenke 2014] *) Lemma measurable_kfcomp : measurable_fun [set: T1 * T2] f -> diff --git a/theories/lebesgue_integral_theory/giry.v b/theories/lebesgue_integral_theory/giry.v index 3c98adfd58..f756f62a4d 100644 --- a/theories/lebesgue_integral_theory/giry.v +++ b/theories/lebesgue_integral_theory/giry.v @@ -290,7 +290,10 @@ apply: measurable_giry_codensity => //= B mB. by apply: measurable_giry_int => //; exact: measurable_giry_ev. Qed. +<<<<<<< HEAD Import HBNNSimple. +======= +>>>>>>> 1d806e2cf (sigma-algebra for normed modules + sfun codomain sigma ring & module structure) Import MeasurableR. Lemma sintegral_giry_join (M : giry (giry T R) R) (h : {nnsfun T >-> R}) : diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v index ad2b814d30..39122860ca 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v @@ -84,7 +84,6 @@ rewrite sintegralE fsbig1// => r _; rewrite preimage_cst. by case: ifPn => [/[!inE] <-|]; rewrite ?mul0e// measure0 mule0. Qed. -Import HBNNSimple. Lemma sintegral_ge0 (f : {nnsfun T >-> R}) : 0 <= sintegral mu f. Proof. by rewrite sintegralE fsume_ge0// => r _; exact: nnsfun_mulemu_ge0. Qed. @@ -140,7 +139,6 @@ Local Open Scope ereal_scope. Context d (T : sigmaRingType d) (R : realType). Variables (m : {measure set T -> \bar R}) (r : R) (f : {nnsfun T >-> R}). -Import HBNNSimple. Lemma sintegralrM : sintegral m (cst r \* f)%R = r%:E * sintegral m f. Proof. @@ -197,7 +195,6 @@ Section le_sintegral. Context d (T : measurableType d) (R : realType) (m : {measure set T -> \bar R}). Variables f g : {nnsfun T >-> R}. -Import HBNNSimple. Hypothesis fg : forall x, f x <= g x. @@ -214,7 +211,6 @@ Qed. End le_sintegral. Section is_cvg_sintegral. -Import HBNNSimple. Lemma is_cvg_sintegral d (T : measurableType d) (R : realType) (m : {measure set T -> \bar R}) (f : {nnsfun T >-> R}^nat) : @@ -231,7 +227,6 @@ Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. Variables (g : {nnsfun T >-> R}^nat) (f : {nnsfun T >-> R}). -Import HBNNSimple. Hypothesis nd_g : forall x, nondecreasing_seq (g^~ x). Hypothesis gf : forall x, cvgn (g^~ x) -> f x <= limn (g^~ x). @@ -351,7 +346,6 @@ Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. Variables (g : {nnsfun T >-> R}^nat) (f : {nnsfun T >-> R}). -Import HBNNSimple. Hypothesis nd_g : forall x, nondecreasing_seq (g^~ x). Hypothesis gf : forall x, g ^~ x @ \oo --> f x. @@ -378,7 +372,6 @@ Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). Implicit Types (f g : T -> \bar R) (D : set T). -Import HBNNSimple. Let nnintegral mu f := ereal_sup [set sintegral mu h | h in [set h : {nnsfun T >-> R} | forall x, (h x)%:E <= f x]]. @@ -477,7 +470,6 @@ Context {d} {T : measurableType d} {R : realType}. Variables m1 m2 : {measure set T -> \bar R}. Hypothesis m12 : forall S, measurable S -> m1 S <= m2 S. -Import HBNNSimple. Lemma ge0_le_measure_integral (f : T -> \bar R) S : measurable S -> (forall x, 0 <= f x) -> measurable_fun [set: T] f -> @@ -496,7 +488,6 @@ Context d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D). Implicit Type A : set T. -Import HBNNSimple. Lemma integral_indic A : measurable A -> \int[mu]_(x in D) (\1_A x)%:E = mu (A `&` D). @@ -515,7 +506,6 @@ Context {d} {T : measurableType d} {R : realType} Lemma integral_mkcond D f : \int[mu]_(x in D) f x = \int[mu]_x (f \_ D) x. Proof. by rewrite /integral patch_setT. Qed. -Import HBNNSimple. Lemma integralT_nnsfun (h : {nnsfun T >-> R}) : \int[mu]_x (h x)%:E = sintegral mu h. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v index 41a86b07f3..c650da9ce9 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v @@ -81,7 +81,6 @@ Import MeasurableR. Let R : measurableType _ := measurableTypeR rT. Local Open Scope ereal_scope. -Import HBSimple. Lemma approximation_continuous_integrable (E : set _) (f : rT -> rT): measurable E -> mu E < +oo -> mu.-integrable E (EFin \o f) -> diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v index 2ede24962a..1eb4406df9 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v @@ -35,7 +35,6 @@ Variables (mu : {measure set T -> \bar R}) (f : T -> \bar R) Hypothesis f0 : forall x, 0 <= f x. Hypothesis mf : measurable_fun setT f. -Import HBNNSimple. Hypothesis nd_g : forall x, nondecreasing_seq (g^~x). Hypothesis gf : forall x, EFin \o g^~ x @ \oo --> f x. @@ -90,7 +89,6 @@ Hypothesis f10 : forall x, D x -> 0 <= f1 x. Hypothesis mf1 : measurable_fun D f1. Hypothesis mf2 : measurable_fun D f2. -Import HBNNSimple. Lemma ge0_le_integral : (forall x, D x -> f1 x <= f2 x) -> \int[mu]_(x in D) f1 x <= \int[mu]_(x in D) f2 x. @@ -163,7 +161,6 @@ Local Definition max_g2' : (T -> R)^nat := Local Definition max_g2 : {nnsfun T >-> R}^nat := fun k => bigmax_nnsfun (g2^~ k) k. -Import HBNNSimple. Let is_cvg_g2 n t : cvgn (EFin \o (g2 n ^~ t)). Proof. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index a4af3f425b..5189d5c04f 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -85,7 +85,6 @@ Context d (T : measurableType d) (R : realType). Let sintegral_measure_zero (f : T -> R) : sintegral mzero f = 0. Proof. by rewrite sintegralE big1// => r _ /=; rewrite /mzero mule0. Qed. -Import HBNNSimple. Lemma integral_measure_zero (D : set T) (f : T -> \bar R) : \int[mzero]_(x in D) f x = 0. @@ -118,7 +117,6 @@ Context {d} {T : measurableType d} {R : realType} Hypothesis f0 : forall x, D x -> 0 <= f x. Hypothesis mf : measurable_fun D f. -Import HBNNSimple. Let ge0_integralZl_EFin_subproof k : (0 <= k)%R -> \int[mu]_(x in D) (k%:E * f x) = k%:E * \int[mu]_(x in D) f x. @@ -203,7 +201,6 @@ Hypothesis mf1 : measurable_fun D f1. Hypothesis f20 : forall x, D x -> 0 <= f2 x. Hypothesis mf2 : measurable_fun D f2. -Import HBNNSimple. Lemma ge0_integralD : \int[mu]_(x in D) (f1 x + f2 x) = \int[mu]_(x in D) f1 x + \int[mu]_(x in D) f2 x. @@ -449,7 +446,6 @@ rewrite !fsbig_set1 mul0e add0e preimage_restrict//. by rewrite ifN ?set0U ?setIidl//= notin_setE => /esym; exact/eqP. Qed. -Import HBNNSimple. Local Lemma integral_cstr r : \int[mu]_(x in D) r%:E = r%:E * mu D. Proof. @@ -691,7 +687,6 @@ Qed. End integral_measure_sum_nnsfun. Section integral_measure_add_nnsfun. -Import HBNNSimple. Lemma integral_measure_add_nnsfun d (T : measurableType d) (R : realType) (m1 m2 : {measure set T -> \bar R}) (D : set T) (mD : measurable D) @@ -710,7 +705,6 @@ Local Open Scope ereal_scope. Context {d} {T : measurableType d} {R : realType} (m_ : {measure set T -> \bar R}^nat). -Import HBNNSimple. Lemma ge0_integral_measure_sum (D : set T) (mD : measurable D) (f : T -> \bar R) : @@ -808,7 +802,6 @@ Context {d} {T : measurableType d} {R : realType} (m_ : {measure set T -> \bar R}^nat). Let m := mseries m_ O. -Import HBNNSimple. Lemma ge0_integral_measure_series (D : set T) (mD : measurable D) (f : T -> \bar R) : (forall t, D t -> 0 <= f t) -> diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v index cc5f2ab413..6b238370f5 100644 --- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v +++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v @@ -351,7 +351,6 @@ Definition nnsfun_approx : {nnsfun T >-> R}^nat := fun n => locked (add_nnsfun else nnsfun0) (n * 2 ^ n)%N) (scale_nnsfun (indic_nnsfun _ (mB n)) (ler0n _ n))). -Import HBNNSimple. Lemma nnsfun_approxE n : nnsfun_approx n = approx n :> (T -> R). Proof. @@ -377,13 +376,11 @@ End approximation. Section approximation_sfun. Context d (T : measurableType d) (R : realType) (f : T -> \bar R). Variables (D : set T) (mD : measurable D) (mf : measurable_fun D f). - -Import HBSimple. +Import MeasurableR. (* NB: already instantiated in cardinality.v *) (*HB.instance Definition _ x : @FImFun T R (cst x) := FImFun.on (cst x).*) (* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *) -Import HBNNSimple. (* NB: already instantiated in lebesgue_integral.v *) (*HB.instance Definition _ x : @NonNegFun T R (cst x%:num) := NonNegFun.on (cst x%:num).*) @@ -707,7 +704,6 @@ Let R : measurableType _ := measurableTypeR rT. Hypothesis mA : measurable A. Hypothesis finA : mu A < +oo. -Import HBSimple. Let lusin_simple (f : {sfun R >-> rT}) (eps : rT) : (0 < eps)%R -> exists K, [/\ compact K, K `<=` A, mu (A `\` K) < eps%:E & diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 71977785e5..90d6986baa 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -28,8 +28,9 @@ From mathcomp Require Import real_measure numfun realfun. (* *) (* Detailed contents: *) (* ```` *) -(* {sfun T >-> R} == type of simple functions *) -(* They form a (potentially zero) ring. *) +(* {sfun aT >-> bT} == type of simple functions *) +(* They can form a ring or a module depending on *) +(* the structure of bT *) (* {nnsfun T >-> R} == type of non-negative simple functions *) (* indic_sfun mD := mindic _ mD *) (* cst_sfun r == constant simple function *) @@ -73,24 +74,19 @@ Local Open Scope ring_scope. Module HBSimple. Import MeasurableR. -HB.structure Definition SimpleFun d (aT : sigmaRingType d) (rT : realType) := - {f of @isMeasurableFun d _ aT rT f & @FiniteImage aT rT f}. +HB.structure Definition SimpleFun d d' + (aT : sigmaRingType d) (rT : sigmaRingType d') := + {f of @isMeasurableFun d d' aT rT f & @FiniteImage aT rT f}. -End HBSimple. - -Notation "{ 'sfun' aT >-> T }" := (@HBSimple.SimpleFun.type _ aT T) : form_scope. +Notation "{ 'sfun' aT >-> T }" := (@SimpleFun.type _ _ aT T) : form_scope. Notation "[ 'sfun' 'of' f ]" := [the {sfun _ >-> _} of f] : form_scope. -Module HBNNSimple. -Import HBSimple. HB.structure Definition NonNegSimpleFun d (aT : sigmaRingType d) (rT : realType) := - {f of @SimpleFun d _ _ f & @NonNegFun aT rT f}. - -End HBNNSimple. + {f of @SimpleFun d _ aT rT f & @NonNegFun aT rT f}. -Notation "{ 'nnsfun' aT >-> T }" := (@HBNNSimple.NonNegSimpleFun.type _ aT%type T) : form_scope. +Notation "{ 'nnsfun' aT >-> T }" := (@NonNegSimpleFun.type _ aT%type T) : form_scope. Notation "[ 'nnsfun' 'of' f ]" := [the {nnsfun _ >-> _} of f] : form_scope. Section sfun_pred. @@ -104,19 +100,18 @@ Lemma sub_sfun_fimfun : {subset sfun <= fimfun}. Proof. by move=> x /andP[]. Qed End sfun_pred. Section sfun. -Context {d} {aT : measurableType d} {rT : realType}. +Context {d d'} {aT : measurableType d} {rT : measurableType d'}. Notation T := {sfun aT >-> rT}. -Notation sfun := (@sfun _ aT rT). +Notation sfun := (@sfun _ _ aT rT). Section Sub. Context (f : aT -> rT) (fP : f \in sfun). Import MeasurableR. Definition sfun_Sub1_subproof := - @isMeasurableFun.Build d _ aT rT f (set_mem (sub_sfun_mfun fP)). + @isMeasurableFun.Build d d' aT rT f (set_mem (sub_sfun_mfun fP)). #[local] HB.instance Definition _ := sfun_Sub1_subproof. Definition sfun_Sub2_subproof := @FiniteImage.Build aT rT f (set_mem (sub_sfun_fimfun fP)). -Import HBSimple. #[local] HB.instance Definition _ := sfun_Sub2_subproof. Definition sfun_Sub := [sfun of f]. @@ -131,7 +126,6 @@ have -> : Pf2 = set_mem (sub_sfun_fimfun Pf) by []. exact: Ksub. Qed. -Import HBSimple. Lemma sfun_valP f (Pf : f \in sfun) : sfun_Sub Pf = f :> (_ -> _). Proof. by []. Qed. @@ -155,9 +149,9 @@ Lemma cst_sfunE x : @cst_sfun x =1 cst x. Proof. by []. Qed. End sfun. (* a better way to refactor function stuffs *) -Lemma fctD (T : Type) (K : pzRingType) (f g : T -> K) : f + g = f \+ g. +Lemma fctD (T : Type) (N : nmodType) (f g : T -> N) : f + g = f \+ g. Proof. by []. Qed. -Lemma fctN (T : Type) (K : pzRingType) (f : T -> K) : - f = \- f. +Lemma fctN (T : Type) (N : zmodType) (f : T -> N) : - f = \- f. Proof. by []. Qed. Lemma fctM (T : Type) (K : pzRingType) (f g : T -> K) : f * g = f \* g. Proof. by []. Qed. @@ -170,32 +164,20 @@ Definition fctWE := (fctD, fctN, fctM, fctZ). Section ring. Context d (aT : measurableType d) (rT : realType). -Lemma sfun_subring_closed : subring_closed (@sfun d aT rT). +Lemma sfun_subring_closed : subring_closed (@sfun d _ aT rT). Proof. by split=> [|f g|f g]; rewrite ?inE/= ?rpred1//; move=> /andP[/= mf ff] /andP[/= mg fg]; rewrite !(rpredB, rpredM). Qed. -HB.instance Definition _ := GRing.isSubringClosed.Build _ sfun +HB.instance Definition _ := GRing.isSubringClosed.Build _ (@sfun d _ aT rT) sfun_subring_closed. HB.instance Definition _ := [SubChoice_isSubComPzRing of {sfun aT >-> rT} by <:]. Implicit Types (f g : {sfun aT >-> rT}). -Import HBSimple. - -Lemma sfun0 : (0 : {sfun aT >-> rT}) =1 cst 0. Proof. by []. Qed. Lemma sfun1 : (1 : {sfun aT >-> rT}) =1 cst 1. Proof. by []. Qed. -Lemma sfunN f : - f =1 \- f. Proof. by []. Qed. -Lemma sfunD f g : f + g =1 f \+ g. Proof. by []. Qed. -Lemma sfunB f g : f - g =1 f \- g. Proof. by []. Qed. Lemma sfunM f g : f * g =1 f \* g. Proof. by []. Qed. -Lemma sfun_sum I r (P : {pred I}) (f : I -> {sfun aT >-> rT}) (x : aT) : - (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. -Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. -Lemma sfun_prod I r (P : {pred I}) (f : I -> {sfun aT >-> rT}) (x : aT) : - (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. -Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. Lemma sfunX f n : f ^+ n =1 (fun x => f x ^+ n). Proof. by move=> x; elim: n => [|n IHn]//; rewrite !exprS sfunM/= IHn. Qed. @@ -206,7 +188,6 @@ HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f). HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g). -Import HBSimple. (* TODO: mv to `measurable_realfun.v`? *) HB.instance Definition _ (D : set aT) (mD : measurable D) : @@ -214,12 +195,123 @@ HB.instance Definition _ (D : set aT) (mD : measurable D) : Definition indic_sfun (D : set aT) (mD : measurable D) : {sfun aT >-> rT} := mindic rT mD. -HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst_sfun k). -Definition scale_sfun k f : {sfun aT >-> rT} := k \o* f. - End ring. + Arguments indic_sfun {d aT rT} _. +Section sfun_lmodType. +Context d (aT : measurableType d) (R : realType) (N : normedModType R). + +Lemma mem_sfun_comp_pair (U V W : normedModType R) (f : {sfun aT >-> U}) + (g : {sfun aT >-> V}) (h : U * V -> W) : + (fun x => h (f x, g x)) \in @sfun _ _ aT W. +Proof. +rewrite inE; apply/andP; split; rewrite inE/=. + move=> _ Y mY; rewrite setTI. + rewrite (_ : _ @^-1` Y = + \bigcup_(a in range f) (\bigcup_(b in range g) + ((f @^-1` [set a] `&` g @^-1` [set b]) `&` [set _ | Y (h (a, b))]))). + apply/seteqP; split=> [x/= Yfg|x [a _] [b _] [[/= <- <-]]//]. + by exists (f x); [exists x|exists (g x); [exists x|]]. + apply: fin_bigcup_measurable; first exact: fimfunP. + move=> a _; apply: fin_bigcup_measurable; first exact: fimfunP. + move=> b _; apply: measurableI. + exact: measurableI. + have [Yhab|Yhab] := pselect (Y (h (a, b))). + by rewrite (_ : [set _ | _] = setT); + [apply/seteqP; split|exact: measurableT]. + rewrite (_ : [set _ | _] = set0); last exact: measurable0. + by apply/seteqP; split. +apply: (@sub_finite_set _ _ (h @` (range f `*` range g))). + by move=> _ [x _ <-]/=; exists (f x, g x) => //; split; exists x. +exact/finite_image/finite_setX/fimfunP. +Qed. + +Lemma sfun_submod_closed : + submod_closed (@sfun _ _ aT N). +Proof. +split=> [|k f g sf sg]; first exact: (valP (cst_sfun (0 : N))). +exact: (mem_sfun_comp_pair (sfun_Sub sf) (sfun_Sub sg) (fun t => k *: t.1 + t.2)). +Qed. + +HB.instance Definition _ := + GRing.isSubmodClosed.Build _ _ (@sfun _ _ aT N) + sfun_submod_closed. +HB.instance Definition _ := + [SubChoice_isSubLmodule of {sfun aT >-> N} by <:]. + +Implicit Types (f g : {sfun aT >-> N} : lmodType _). + +Lemma sfun0 : (0 : {sfun aT >-> N} : lmodType _) =1 cst 0. Proof. by []. Qed. +Lemma sfunN f : - f =1 \- f. Proof. by []. Qed. +Lemma sfunD f g : f + g =1 f \+ g. Proof. by []. Qed. +Lemma sfunB f g : f - g =1 f \- g. Proof. by []. Qed. +Lemma sfunZ k f : k *: f =1 k \*: f. Proof. by []. Qed. +Lemma sfun_sum I r (P : {pred I}) (f : I -> {sfun aT >-> N} : lmodType _) (x : aT) : + (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. +Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. +Lemma sfun_prod I r (P : {pred I}) (f : I -> {sfun aT >-> N} : lmodType _) (x : aT) : + (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. +Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. + +HB.instance Definition _ f g := MeasurableFun.copy (f \+ g) (f + g). +HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f). +HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). +HB.instance Definition _ k f := MeasurableFun.copy (k \*: f) (k *: f). + +End sfun_lmodType. + +(* This could be moved elsewhere *) +Section indic_lmod. +Context {T : Type} {K : pzRingType} {L : lmodType K}. + +Definition indic_lmod (A : set T) (z : L) := ( *:%R^~ z) \o \1_A. + +Lemma indic_lmodE A z : indic_lmod A z = (fun x => if x \in A then z else 0). +Proof. +by apply/funext=> x; rewrite/indic_lmod/= indicE; +case: ifPn=> _ /=; rewrite ?scale0r ?scale1r. +Qed. + +Lemma preimage_indic_mod A (B : set L) (z : L) : + (indic_lmod A z) @^-1` B = if z \in B then if 0 \in B then [set: T] else A + else if 0 \in B then ~` A else set0. +Proof. +rewrite comp_preimage preimage_indic. by do 4 (case: ifPn => [|]); + rewrite ?in_setE ?notin_setE //= ?scale0r ?scale1r. +Qed. + +Lemma indic_lmod_fimfun_subproof (A : set T) (z : L) : +@FiniteImage T L (indic_lmod A z). Proof. by []. Qed. + +HB.instance Definition _ A z := @indic_lmod_fimfun_subproof A z. + +End indic_lmod. + +Section mindic_lmod. +Context d {aT : measurableType d} {rT : realType} {nT : normedModType rT}. + +Definition mindic_lmod (A : set aT) (mA : measurable A) := + @indic_lmod aT rT nT A. + +Lemma measurable_indic_lmod {D} (A : set aT) (mA : d.-measurable A) (z:nT) : +measurable_fun D (mindic_lmod mA z). +Proof. +move=> mD Y mY; rewrite preimage_indic_mod //. +do 2 (case: ifP => _); apply: measurableI=>//; exact: measurableC. +Qed. + +HB.instance Definition _ A mA z := @isMeasurableFun.Build _ _ aT nT + (mindic_lmod mA z) (@measurable_indic_lmod [set: aT] A mA z). + +HB.instance Definition _ (D : set aT) (mD : measurable D) (z : nT) : + @FImFun aT nT (mindic_lmod mD z) := FImFun.on (mindic_lmod mD z). + +Definition mindic_lmod_sfun (D : set aT) (mD : measurable D) (z : nT) : + {sfun aT >-> nT} := mindic_lmod mD z. + +End mindic_lmod. + Lemma preimage_nnfun0 T (R : realDomainType) (f : {nnfun T >-> R}) t : t < 0 -> f @^-1` [set t] = set0. Proof. @@ -235,11 +327,13 @@ by split=> [z/= <-|z/= ->]; rewrite [x * _]mulrC (mulfK, divfK). Qed. Section simple_bounded. +<<<<<<< HEAD Context {d} {T : sigmaRingType d} {R : realType}. +======= +Context d (T : sigmaRingType d) (R : realType) (N : normedModType R). +>>>>>>> b5e0fd857 (sigma-algebra for normed modules + sfun codomain sigma ring & module structure) -Import HBSimple. - -Lemma simple_bounded (f : {sfun T >-> R}) : bounded_fun f. +Lemma simple_bounded (f : {sfun T >-> N}) : bounded_fun f. Proof. have /finite_seqP[r fr] := fimfunP f. exists (fine (\big[maxe/-oo%E]_(i <- r) `|i|%:E)). @@ -331,7 +425,6 @@ Definition proj_nnsfun d (T : measurableType d) (R : realType) mul_nnsfun f (indic_nnsfun R mA). Section mrestrict. -Import HBNNSimple. Lemma mrestrict d (T : measurableType d) (R : realType) (f : {nnsfun T >-> R}) A (mA : measurable A) : f \_ A = proj_nnsfun f mA. @@ -348,7 +441,6 @@ Variable f : {nnsfun T >-> R}^nat. Definition sum_nnsfun n := \big[add_nnsfun/nnsfun0]_(i < n) f i. -Import HBNNSimple. Lemma sum_nnsfunE n t : sum_nnsfun n t = \sum_(i < n) (f i t). Proof. by rewrite /sum_nnsfun; elim/big_ind2 : _ => [|x g y h <- <-|]. Qed. @@ -365,7 +457,6 @@ Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). Variable f : {nnsfun T >-> R}. -Import HBNNSimple. Lemma nnsfun_cover : \big[setU/set0]_(i \in range f) (f @^-1` [set i]) = setT. Proof. by rewrite fsbig_setU//= -subTset => x _; exists (f x). Qed. @@ -437,7 +528,6 @@ by move=> xA; rewrite (@mulef_ge0 _ _ (mu \o _))//= => /xA ->; rewrite measure0. Qed. Global Arguments mulemu_ge0 {d T R mu x} A. -Import HBNNSimple. Lemma nnsfun_mulemu_ge0 d (T : sigmaRingType d) (R : realType) (mu : {measure set T -> \bar R}) (f : {nnsfun T >-> R}) x : diff --git a/theories/probability_theory/normal_distribution.v b/theories/probability_theory/normal_distribution.v index a2df3f5dc2..ed296f469f 100644 --- a/theories/probability_theory/normal_distribution.v +++ b/theories/probability_theory/normal_distribution.v @@ -588,6 +588,7 @@ Section normal_prob_lemmas. Context {R : realType}. Local Notation mu := lebesgue_measure. Local Open Scope ereal_scope. +Import MeasurableR. Import MeasurableR. diff --git a/theories/probability_theory/uniform_distribution.v b/theories/probability_theory/uniform_distribution.v index db21ea3dde..4ea91d5f4d 100644 --- a/theories/probability_theory/uniform_distribution.v +++ b/theories/probability_theory/uniform_distribution.v @@ -149,7 +149,6 @@ case: ifPn => //. by rewrite inE/= in_itv/= => axb; rewrite indicE (negbTE xE) mule0. Qed. -Import HBNNSimple. Let integral_uniform_nnsfun (f : {nnsfun _ >-> R}) : (\int[uniform_prob ab]_x (f x)%:E = diff --git a/theories/real_measure/lebesgue_stieltjes_measure.v b/theories/real_measure/lebesgue_stieltjes_measure.v index 0ddbb8bffd..946ab0ea68 100644 --- a/theories/real_measure/lebesgue_stieltjes_measure.v +++ b/theories/real_measure/lebesgue_stieltjes_measure.v @@ -463,85 +463,127 @@ Qed. End rgenopensets. End RGenOpenSets. +(* Could be moved elsewhere and generalized to metric spaces *) +Section normed_lemmas. +Context {R : realType} {N : normedModType R}. + +Lemma set1_bigcap_ball (x : N) : [set x] = \bigcap_n ball x n.+1%:R^-1. +Proof. +rewrite eqEsubset/bigcap; split=> [y -> n _ | y /= bn]/=. + by apply: ballxx; rewrite invr_gt0. +apply: close_eq _=>//; rewrite ball_close=> e0; rewrite ball_symE. +apply: (le_ball _ (bn (truncn e0%:num^-1) I)). rewrite invf_ple ?posrE//. +exact: (ltW (truncnS_gt _)). +Qed. + +End normed_lemmas. + +(* Should be moved to a more general file *) Section open. -Context {R : realType}. +Context {R : realType} {N : normedModType R}. -Definition open_type : Type := R. +Definition open_type : Type := N. HB.instance Definition _ := Pointed.on open_type. -Let measurable : set_system R := @measurable _ (g_sigma_algebraType (@open R)). +Let measurable : set_system N := @measurable _ (g_sigma_algebraType (@open N)). Let measurable0 : measurable set0. Proof. exact: measurable0. Qed. Let measurableC A : measurable A -> measurable (~` A). Proof. by move=> /measurableC. Qed. -Let measurable_bigcup (F : (set R)^nat) : (forall i, measurable (F i)) -> +Let measurable_bigcup (F : (set N)^nat) : (forall i, measurable (F i)) -> measurable (\bigcup_i (F i)). Proof. move=> mF; exact: bigcupT_measurable. Qed. HB.instance Definition _ := - @isMeasurable.Build (sigma_display (@open R)) + @isMeasurable.Build (sigma_display (@open N)) open_type measurable measurable0 measurableC measurable_bigcup. End open. -Notation "R .-open" := (sigma_display (@open R)) : measure_display_scope. -Notation "R .-open.-measurable" := (measurable : set_system (@open_type R)) : +Notation "N .-open" := (sigma_display (@open N)) : measure_display_scope. +Notation "N .-open.-measurable" := (measurable : set_system (@open_type _ N)) : classical_set_scope. -Module MeasurableRopen. -Section measurableRopen. -Context {R : realType}. +Module MeasurableOpen. +Section measurableOpen. +Context {R : realType} {N : normedModType R}. -Definition measurableTypeR := g_sigma_algebraType (@open R). +Definition measurableTypeO := g_sigma_algebraType (@open N). -Definition lebesgue_display : measure_display := R.-open. +Definition borel_display : measure_display := N.-open. -Definition measurableR : set_system R := R.-open.-measurable. +Definition measurableO : set_system N := N.-open.-measurable. -HB.instance Definition _ : Measurable lebesgue_display measurableTypeR := - Measurable.on measurableTypeR. +HB.instance Definition _ : Measurable borel_display measurableTypeO := + Measurable.on measurableTypeO. (* Presumably it is safe to use NFI here because morally R is unique and nothing else can be used here *) #[non_forgetful_inheritance] -HB.instance Definition _ := Measurable.copy R measurableTypeR. +HB.instance Definition _ := Measurable.copy N measurableTypeO. -Lemma measurable_set1 (r : R) : measurable [set r]. +Lemma measurable_set1 (x : N) : measurable [set x]. Proof. -rewrite set1_bigcap_oo; apply: bigcap_measurable => // k _. -exact: sub_sigma_algebra. +rewrite set1_bigcap_ball; apply: bigcap_measurable => // k _. +apply: sub_sigma_algebra; exact: ball_open. Qed. #[local] Hint Resolve measurable_set1 : core. -Lemma measurable_itv (i : interval R) : measurable [set` i]. -Proof. -have := MeasurableRocitv.measurable_itv i. -rewrite /MeasurableRocitv.lebesgue_display. -by rewrite RGenOpenSets.measurableE. -Qed. +Lemma measurable_ball_norm (x : N) e : measurable (ball x e). +Proof. by apply: (sub_sigma_algebra (ball_open _ _)). Qed. -End measurableRopen. -Arguments measurableTypeR : clear implicits. +End measurableOpen. +Arguments measurableTypeO : clear implicits. #[global] Hint Extern 0 (measurable (_ @^-1` [set _])) => solve [apply: measurable_funPTI; exact: measurable_set1] : core. #[global] Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. -#[global] -Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. -Lemma measurable_funP1 {d} {aT : measurableType d} {rT : realType} - (f : {mfun aT >-> rT}) D (y : rT) : - measurable D -> measurable (D `&` f @^-1` [set y]). +Lemma measurable_funP1 {d} {aT : measurableType d} {rT : realType} + {nT : normedModType rT} (f : {mfun aT >-> nT}) D (z : nT) : + measurable D -> measurable (D `&` f @^-1` [set z]). Proof. by move=> /(measurable_funP f); exact. Qed. #[deprecated(since="mathcomp-analysis 1.13.0", use=measurable_funP1)] Notation measurable_sfun_inP := measurable_funP1 (only parsing). #[global] Hint Extern 0 (measurable (_ `&` _ @^-1` [set _])) => solve [apply: measurable_funP1; assumption] : core. +Section measurableReal. +Context {R : realType}. +Import numFieldNormedType.Exports. + +Definition measurableTypeR := @measurableTypeO R R. + +Definition lebesgue_display : measure_display := @borel_display R R. + +Definition measurableR := @measurableO R R. +(* Shouldn't be needing ideally... *) +HB.instance Definition _ := Measurable.copy R measurableTypeR. + +Lemma measurable_itv (i : interval R) : measurable [set` i]. +Proof. +have := MeasurableRocitv.measurable_itv i. +rewrite /MeasurableRocitv.lebesgue_display. +by rewrite RGenOpenSets.measurableE. +Qed. + +End measurableReal. +Arguments measurableTypeR : clear implicits. +#[global] +Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. + +End MeasurableOpen. + +Module MeasurableR. +Export numFieldNormedType.Exports. +Export MeasurableOpen. +End MeasurableR. + Section ocitv_measure. +Import MeasurableR. Context {R : realType} (mu : measure (measurableTypeR R) R). Definition ocitv_measure : set (MeasurableRocitv.measurableTypeR R) -> \bar R := @@ -568,12 +610,6 @@ Lemma ocitv_measure_ext A : ocitv_measure A = mu A. Proof. by []. Qed. End ocitv_measure. -End MeasurableRopen. - -Module MeasurableR. -Export MeasurableRopen. -End MeasurableR. - (** The construction of the Lebesgue-Stieltjes measure actually starts here. *) Section wlength. @@ -950,13 +986,13 @@ Let ocitv_lebesgue_stieltjes_measure_unique Proof. move=> muE A mA. apply: measure_extension_unique => //=. -- exact: wlength_sigma_finite. -- by move=> X mX; rewrite -muE// -measurable_mu_extE. -- by rewrite RGenOpenSets.measurableE. + exact: wlength_sigma_finite. +by move=> X mX; rewrite -muE// -measurable_mu_extE. +by rewrite RGenOpenSets.measurableE. Qed. Lemma lebesgue_stieltjes_measure_unique - (mu : {measure set (MeasurableRopen.measurableTypeR R) -> \bar R}) : + (mu : {measure set (measurableTypeR R) -> \bar R}) : (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) -> forall A : set R, measurable A -> lebesgue_stieltjes_measure f A = mu A. Proof. From 5e79d432801e67b0544049ff737216e8ae11bed1 Mon Sep 17 00:00:00 2001 From: adjevahi Date: Thu, 9 Jul 2026 15:30:15 +0200 Subject: [PATCH 2/8] added image_indic_lmod_sub --- theories/lebesgue_integral_theory/simple_functions.v | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 90d6986baa..63ec57e9ae 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -273,7 +273,14 @@ by apply/funext=> x; rewrite/indic_lmod/= indicE; case: ifPn=> _ /=; rewrite ?scale0r ?scale1r. Qed. -Lemma preimage_indic_mod A (B : set L) (z : L) : +Lemma image_indic_lmod_sub A z D : (indic_lmod A z) @` D `<=` [set 0;z]. +Proof. +rewrite -image_comp; apply: (subset_trans (image_subset ( *:%R ^~ z) _)); + first exact: image_indic_sub. +move=> y /= [x [->|->]]; rewrite ?scale0r ?scale1r=> ->; first by left. by right. +Qed. + +Lemma preimage_indic_lmod A (B : set L) (z : L) : (indic_lmod A z) @^-1` B = if z \in B then if 0 \in B then [set: T] else A else if 0 \in B then ~` A else set0. Proof. @@ -297,7 +304,7 @@ Definition mindic_lmod (A : set aT) (mA : measurable A) := Lemma measurable_indic_lmod {D} (A : set aT) (mA : d.-measurable A) (z:nT) : measurable_fun D (mindic_lmod mA z). Proof. -move=> mD Y mY; rewrite preimage_indic_mod //. +move=> mD Y mY; rewrite preimage_indic_lmod //. do 2 (case: ifP => _); apply: measurableI=>//; exact: measurableC. Qed. From de4f13ac1d5a151d3e7586f9b476da333e0d9eca Mon Sep 17 00:00:00 2001 From: arthurd Date: Tue, 10 Nov 2026 11:05:31 +0100 Subject: [PATCH 3/8] rebase --- CHANGELOG_UNRELEASED.md | 430 ------------------ classical/filter.v | 2 +- theories/hoelder.v | 2 +- theories/kernel.v | 4 + theories/lebesgue_integral_theory/giry.v | 3 - .../lebesgue_integral_definition.v | 10 + .../lebesgue_integral_differentiation.v | 1 + .../lebesgue_integral_monotone_convergence.v | 3 + .../lebesgue_integral_nonneg.v | 7 + .../measurable_fun_approximation.v | 6 +- .../probability_theory/normal_distribution.v | 1 - .../probability_theory/uniform_distribution.v | 1 + .../real_measure/lebesgue_stieltjes_measure.v | 2 +- 13 files changed, 34 insertions(+), 438 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f8d087d901..d7f0405803 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -3,271 +3,6 @@ ## [Unreleased] ### Added -- in `borel_hierarchy.v`: - + definition `borel_type` - + lemmas `singleton_bigcap`, `measurable1` - -- in `simple_functions.v`: - + lemmas `sfun_op`, `sfun_submod_closed` - + `{sfun aT >-> borel_type V}` is an `lmodType` when `V` is a `normedModType` - -- in `simple_functions.v`: - + lemmas `mem_sfun_comp_pair`, `sfun_submod_closed` - + `{sfun aT >-> V}` is an `lmodType` when `V` is a `normedModType` - + definitions `indic_lmod` `mindic_lmod` `mindic_lmod_sfun` - + lemmas `indic_lmodE` `preimage_indic_mod` `measurable_indic_lmod` - -- in `set_interval.v`: - + lemmas `setU_itvob1`, `setU_1itvob` - -- in `realfun.v`: - + lemma `derivable_sqrt` -- in `classical_sets.v`: - + definition `rectangle` - + lemmas `rectangle_setX`, `setI_closed_rectangle` - + definitions `cross`, `cross12` - + lemmas `smallest_sub_sub`, `bigcap_closed_smallest`, `smallest_sub_iff` - + lemma `preimage_set_systemS` - + lemma `setD_bigcapr` - -- in `measurable_structure.v`: - + lemmas `g_sigma_algebra_cross`, `g_sigma_algebra_rectangle` - + lemma `sigma_algebra_sub` - -- in `measurable_function.v`: - + lemma `preimage_measurability` - -- in `pseudometric_normed_Zmodule.v`: - + lemma `itv_center_shift` - -- in `normed_module.v`: - + lemmas `closure_itvoo` -- in `unstable.v`: - + structures `SemiNorm`, `Norm` - + lemmas `normMn`, `normN`, `ler_norm_sum` - -- in `normed_module.v`: - + structure `NormedVector` - + notation `normedVectType` - + definition `max_space` - + lemmas `sup_closed_ball_compact`, `equivalence_norms`, - `linear_findim_continuous` - -- in `tvs.v`: - + lemmas `cvg_sum`, `sum_continuous` - -- in `classical_sets.v`: - + lemmas `setI_closed_setT`, `setI_closed_set0` - -- in `measurable_function.v`: - + lemma `g_sigma_algebra_preimage_comp` - -- in `measure_function.v`: - + lemma `g_sigma_algebra_finite_measure_unique` - -- new file `independence.v`: - + definition `independent_events` - + definition `mutual_independence` - + lemma `eq_mutual_independence` - + definition `independence2`, `independence2P` - + lemma `mutual_independence_fset` - + lemma `mutual_independence_finiteS` - + theorem `mutual_independence_finite_g_sigma` - + lemma `mutual_dependence_bigcup` - + definition `independent_RVs` - + lemma `independent_RVsD1` - + theorem `independent_generators` - + definition `independent_RVs2` - + lemmas `independent_RVs2_comp`, `independent_RVs2_funrposneg`, - `independent_RVs2_funrnegpos`, `independent_RVs2_funrnegneg`, - `independent_RVs2_funrpospos` - + definition `pairRV`, lemma `measurable_pairRV` - + lemmas `independent_RVs2_product_measure1` - + lemmas `independent_RVs2_setI_preimage`, - `independent_Lfun1_expectation_product_measure_lty` - + lemma `ge0_independent_expectationM` - + lemmas `independent_Lfun1_expectationM_lty`, `independent_Lfun1M`, - `independent_expectationM` - -- in `ereal.v`: - + lemma `ge0_addBefctE` - -- in `measure_extension.v`: - + definition `caratheodory_measure` -- in `measurable_structure.v`: - + structure `PMeasurable`, notation `pmeasurableType` - -- in `subspace_topology.v`: - + lemma `withinU_continuous_patch` -- in `matrix_normedtype.v`: - + lemma `continuous_mx` - -- in `derive.v`: - + instance `is_derive_mx` - + fact `dmx` - + lemma `diffmx` - + lemma `is_diff_mx` - + instance `is_diff_mx` -- in `realsum.v`: - + lemma `esum_psum` - + lemma `esum_sum` - -- in `constructive_ereal.v`: - + definition `esg` - + lemmas `numEesg`, `gte0_esg`, `lte0_esg`, `esg0` - -- in `esum.v`: - + lemmas `esum_eq0P`, `esumZ`, `exchange_esum` - + lemmas `le_esum`, `esumN` - + lemmas `summable_le_esum`, `summable_esum_funepos`, `summable_esumN`, - `summableZ`, `summable_esumZ` - + lemmas `esum_if_eq_op` - + lemmas `exchange_esum_ereal_sup` - -- in `ereal.v`: - + lemmas `exchange_ereal_sup`, `ge0_ereal_supZl`, `ge0_ereal_supZl_range` - -- in `sequences.v`: - + lemmas `ereal_supD`, `ereal_sup_sum` - -- in `reals.v`: - + lemmas `sup_ge0`, `has_sup_wpZl`, `gt0_has_supZl`, `has_sup_Mn`, `sup_Mn` -- in `mathcomp_extra.v`: - + lemmas `divDl_ge0`, `divDl_le1` - -- in `unstable.v`: - + lemmas `divD_onem` - -- in `filter.v`: - + mixin `isSubNbhs`, structure `SubNbhs`, notation `subNbhsType` - -- in `topology_structure.v`: - + structure `SubTopological`, notation `subTopologicalType` - -- in `tvs.v`: - + structure `SubConvexTvs`, notation `subConvexTvsType` - -- in `normed_module.v`: - + structure `SubNormedModule`, notation `subNormedModType` - + instance `ent_xsection_filter` - + light-weigth factory `subLmodule_isSubNormedmodule` - -- new file `hahn_banach_theorem.v`: - + module `LinearGraph` - * definitions `graph`, `linear_graph` - * lemmas `lingraph_00`, `lingraphZ`, `lingraphD` - + module `HahnBanachZorn` - * definitions `extend_graph`, `le_graph`, `functional_graph`, `le_extend_graph` - * record `zorn_type` - * definition `zphi` - * lemma `zorn_type_eq` - * definition `zornS` - * lemmas `zornS_ex`, `domain_extend`, `hahn_banach_witness` - + theorems `hahn_banach_extension`, `hahn_banach_extension_normed` -- in `normal_distribution.v`: - + lemma `normal_funN` - + lemma `normal_fun_sym` - + lemma `normal_fun0abs` - + lemma `normal_pdf_sym` - + lemma `normal_fun_center_new` - + lemma `normal_fun_shift` - + lemma `normal_pdf_uniq_ae` - + lemma `normal_prob_continuous` - + lemma `integral_normal_prob` - + lemma `measurable_normal_prob` - + lemma `emeasurable_bounded_integrable` - + lemmas `integrable_normal_probD1`, `normal_probD1`, `normal_probD2`, `normal_probD` - -- in `lebesgue_stieltjes_measure.v`: - + definition `lebesgue_display` - -- in `realsum.v`: - + lemma `esum_summableP` - -- in `esum.v`: - + lemma `fsetsTE` -- in `ftc.v`: - + lemma `ge0_integration_by_substitution_shift_itvy`, - `ge0_integration_by_substitution_shift_itvNy` -- in `derive.v`: - + lemmas `derivable_row_mx`, `derive_row_mx` - + instance `is_derive_row_mx` - -- in `matrix_normedtype.v` - + lemmas `norm_row_mx`, `norm_row_mx0r`, `norm_row_mx0l`, `cvg_row_mx` - -- in `unstable.v`: - + lemma `sub_row_mx` - -- in `derive.v`: - + lemmas `eqo_row_mx`, `drow_mx`, `diff_row_mx`, - `differentiable_row_mx` - + instance `is_diff_row_mx` - -- in `functions.v`: - + lemmas `zerofctE`, `onefctE` - -- in `functions.v`: - + lemmas `linfunP`, `linfun_eqP` - + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }` - -- in `tvs.v`: - + structure `LinearContinuous` - + factory `isLinearContinuous` - + instance of `ChoiceType` on `{linear_continuous _ -> _ }` - + instance of `LinearContinuous` with the composition of two functions of type `LinearContinuous` - + instance of `LinearContinuous` with the sum of two functions of type `LinearContinuous` - + instance of `LinearContinuous` with the scalar multiplication of a function of type - `LinearContinuous` - + instance of `Continuous` on \-f when f is of type `LinearContinuous` - + instance of `SubModClosed` on `{linear_continuous _ -> _}` - + instance of `SubLModule` on `{linear_continuous _ -> _ }` - + instance of `LinearContinuous` on the null function - + notations `{linear_continuous _ -> _ | _ }` and `{linear_continuous _ -> _ }` - + definitions `lcfun`, `lcfun_key`, `lcfunP` - + lemmas `lcfun_eqP`, `null_fun_continuous`, `fun_cvgD`, - `fun_cvgN`, `fun_cvgZ`, `fun_cvgZr` - + lemmas `lcfun_continuous` and `lcfun_linear` - -- new files `signed_measure.v` and `radon_nikodym.v` - + with the contents of `charge.v` (deprecated) - -- in `esum.v`: - + lemma `ge0_esum` - + lemma `esum_ge` - -- in `functions.v`: - + lemma `preimageD1` - -- in `measure_function.v`: - + lemmas `cvg_measure_bigcap`, `cvg_measure_bigcup` - -- in `classical_sets.v`: - + lemma `bigcup_bigsetU` - -- in `measurable_structure.v`: - + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable` - -- in `lebesgue_stieltjes_measure.v`: - + module `MeasurableRocitv` - + definition `open_type` - + notations `.-open`, `.-open.-measurable` - + module `MeasurableOpen` - * definition `measurableTypeO` - + definition `borel_display` - * definition `measurableO` - * definition `measurableTypeR` - + definition `lebesgue_display` - * definition `measurableR` - + lemmas `measurable_set1`, `measurable_itv` (also declared as hints) - + lemma `measurable_ball_norm` - + definition `ocitv_measure`, lemma `ocitv_measure_ext` - + module `MeasurableR` - + module `RGenOpenSets` - * lemma `measurableE` - -- in `real_interval.v`: - + lemma `set1_bigcap_oo` - in `exp.v`: + lemmas `cvgy_expR`, `cvgNy_expR`, `lny`, `ge0_lt1_powR_cvg0`, @@ -293,177 +28,12 @@ ### Changed -- in `realsum.v`: - + lemma `__admitted__psumB` proved and renamed to `psumB` - -- moved from `measurable_structure.v` to `classical_sets.v`: - + definition `preimage_set_system` - + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, - `preimage_set_system_id` - -- moved from `measurable_structure.v` to `classical_sets.v`: - + definition `preimage_set_system` - + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, - `preimage_set_system_id` - -- moved from `topology_structure.v` to `filter.v`: - + lemma `continuous_comp` (and generalized) - -- in `numfun.v`: - + `fune_abse` renamed to `funeposDneg` and direction of the equality changed - + `funeposneg` renamed to `funeposBneg` and direction of the equality changed - + `funeD_posD` renamed to `funeDB` and direction of the equality changed - -- in `constructive_ereal.v`: - + lemmas `EFin_semi_additive` and `dEFin_semi_additive` turned into `Let`s - -- moved from `charge.v` to `signed_measure.v`: - + mixin `isAdditiveCharge`, structure `AdditiveCharge` - + mixin `isSemiSigmaAdditive`, structure `Charge` - + factory `isCharge` - + lemmas `charge0`, `charge_semi_additiveW`, `charge_semi_additive2E`, - `charge_semi_additive2`, `chargeU`, `chargeDI`, `charge_partition` - + definitions `measure_of_charge`, `charge_of_finite_measure` - + lemma `chargeD` - + definitions `crestr`, `crestr0`, `czero`, `cscale` - + lemmas `dominates_cscalel`, `dominates_cscaler` - + definition `copp` - + lemma `cscaleN1` - + definition `cadd` - + lemmas `dominates_cadd`, `dominates_pushforward` - + definitions `positive_set`, `negative_set` - + lemmas `negative_set_charge_le0`, `negative_set0`, - `positive_negative0`, `bigcup_negative_set`, `negative_setU`, - `hahn_decomposition_lemma` - + definition `hahn_decomposition` - + theorem `Hahn_decomposition` - + lemmas `Hahn_decomposition_uniq`, `cjordan_posE`, `cjordan_negE` - + definitions `jordan_pos`, `jordan_neg` - + lemmas `jordan_posE`, `jordan_negE`, `jordan_decomp`, `jordan_pos_dominates`, - `jordan_neg_dominates` - + definition `charge_variation`, `charge_dominates` - + lemmas `abse_charge_variation`, `null_charge_dominatesP`, - `content_charge_dominatesP`, `charge_variation_continuous` - -- moved from `charge.v` to `radon_nikodym.v`: - + definition `induced_charge` - + lemmas `semi_sigma_additive_nng_induced`, `dominates_induced`, - `integral_normr_continuous` - + definitions `approxRN`, `int_approxRN`, `sup_int_approxRN` - + lemmas `sup_int_approxRN_ge0`, `radon_nikodym_finite`, - `radon_nikodym_sigma_finite`, `change_of_variables`, `integrableM`, - `chain_rule` - + definition `Radon_Nikodym` - + lemmas `Radon_NikodymE`, `Radon_Nikodym_fin_num`, `Radon_Nikodym_integrable`, - `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`, - `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule` -- in `realsum.v`: - + the following now use `funrpos` and `funrneg`: - * definition `sum` - * lemmas `summable_funrpos`, `summable_funrneg` - + lemma `sum0` (now uses `cst`) - -- moved from `realsum` to `numfun.v`: - + now use `funrpos` and `funrneg`: - * lemmas `eq_funrpos`, `eq_funrneg` - * lemma `fpos0` (renamed to `funrpos_cst0`) - * lemma `fneg0` (renamed to `funrneg_cst0`) - * lemmas `funrposZ`, `funrnegZ` - * lemmas `funrpos_natrM`, `funrneg_natrM` - * lemmas `le_funrpos_norm` - -- moved from `numfun.v` to `unstable.v`: - + notations `nondecreasing_fun`, `nonincreasing_fun`, - `decreasing_fun`, `increasing_fun` - -- in `esum.v`: - + definition `esum` - + lemma `esum_fset` - + lemma `esum_ge` -> `PosEsum.pos_esum_ge` - + lemma `le_esum` -> `PosEsum.le_pos_esum` - -- moved from `normed_module.v` to `metric_structure.v` - + lemma `squeeze_cvgr` - -- moved from `pseudometric_normed_Zmodule.v` to `metric_structure.v` - + lemmas `real_cvgr_lt`, `real_cvgr_le`, `real_cvgr_le`, `real_cvgr_gt` - + lemmas `cvgr_lt`, `cvgr_gt`, `cvgr_ge`, `cvgr_le` -- in `normal_distribution.v: - + `normal_fun_center` -> `normal_fun_center0` - -- moved from `measurable_structure.v` to `measure_function.v`: - + definition `subset_sigma_subadditive` - -- moved from `measurable_structure.v` to `unstable.v`: - + notations `nondecreasing_seq`, `nonincreasing_seq` - -- moved from `measurable_structure.v` to `classical_sets.v`: - + notation `^nat` - + defintion `sequence` - + defintion `seqDU` - + lemmas `seqDU_bigcup_eq`, `trivIset_seqDU` - + definition `seqD` - + lemmas `eq_bigcup_seqD`, `trivIset_seqD`, `seqDU_seqD`, `bigcup_bigsetU_bigcup` - -- in `functions.v` - + lemma `fctE` (include `zerofctE` and `onefctE`) - -- in `classical_sets.v` - + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`) - -- moved from `measurable_realfun.v` to `lebesgue_stieltjes_measure.v` - + module `RGenOInfty` - + module `RGenInftyO` - + module `RGenCInfty` - + module `RGenOpens` - -- moved inside module `MeasurableRocitv` (`lebesgue_stieltjes_measure.v`): - + lemmas `measurable_set1`, `measurable_itv` - -- in `lebesgue_stieltjes_measure.v`: - + lemma `lebesgue_stieltjes_measure_unique` is now about the sigma-algebra generated by open sets - ### Renamed ### Generalized - in `lebesgue_integral_nonneg.v`: + lemmas `ge0_integralZl`, `ge0_integralZr` -- in `measurable_structure.v`: - + lemma `sigma_algebra_measurable` (not specialized to `setT` anymore) - -- in `measurable_function.v`: - + lemma `preimage_set_system_measurable_fun` - -- in `measurable_structure.v` - + structure `SemiRingOfSets`, mixin `isSigmaRing`, factories `isRingOfSets`, - `isRingOfSets_setY`, `isAlgebraOfSets`, `isAlgebraOfSets_setD`, `isMeasurable` - are not required to be pointed anymore - + lemmas `measurable_g_measurableTypeE`, `g_sigma_algebra_preimageType`, - `g_sigma_algebra_preimage`, `g_sigma_preimageE`, `g_sigma_preimageE`, - `g_sigma_algebra_rectangle` are generalized from `pointedType` to `choiceType` - (the list might not be exhaustive) - -- in `ereal.v`: - + lemma `funID` generalized from `pointedType` to `Type` - -- in `numfun.v`: - + lemma `indic_restrict` generalized from `pointedType` to `Type` - + factory `FiniteDecomp` generalized from `pointedType`/`nzRingType` to - `Type/pzRingType` - -- in `simple_functions.v`: - + lemmas `fctD`, `fctN`, `fctM`, `fctZ` - + lemmas `sfun0`, `sfunN`, `sfunD`, `sfunB`, `sfunZ`, `sfun_sum`, `sfunprod` - + lemma `simple_bounded` - + structure `SimpleFun` (and notation `{sfun aT >-> _}`): codomain - generalized from `realType` to `sigmaRingType d'`, adding a display parameter `d'`; - -- in `ereal.v`: - + lemmas `ge0_mule_fsumr`, `ge0_mule_fsuml` - -- in `esum.v`: - + lemma `esum_set1` ### Deprecated diff --git a/classical/filter.v b/classical/filter.v index 461e0135df..591459b297 100644 --- a/classical/filter.v +++ b/classical/filter.v @@ -1239,7 +1239,7 @@ move=> near_hom fFG; apply/cvg_to_withinP; split. Qed. Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T) - (F : set_system T) (P : set T) : + (F : set_system T) (P : set T) : Filter F -> (forall i, i \in D -> F [set j | P j -> f i j]) -> F ([set j | P j -> (\bigcap_(i in [set` D]) f i) j]). Proof. move=> FF FfD; exact: (@filter_bigI T I D f _ (within_filter P FF)). Qed. diff --git a/theories/hoelder.v b/theories/hoelder.v index 11c333ec1b..44fce50f98 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -860,7 +860,7 @@ Reserved Notation "{ 'mfun_' mu , U >-> V }" Notation "{ 'mfun_' mu , aT >-> T }" := (@aeEqMfun _ _ aT T _ mu) : form_scope. -Import numFieldNormedType.Exports. +Import numFieldNormedType.Exports HBNNSimple. HB.mixin Record isFinLebesgue d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E) diff --git a/theories/kernel.v b/theories/kernel.v index c669004aa6..1f418be452 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -1062,6 +1062,7 @@ HB.export KCOMP_SFINITE_KERNEL. Section measurable_fun_preimage_integral. Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Import HBNNSimple. Variables (k : Y -> \bar R) (k_ : ({nnsfun Y >-> R}) ^nat) (ndk_ : nondecreasing_seq (k_ : (Y -> R)^nat)) @@ -1108,6 +1109,7 @@ End measurable_fun_preimage_integral. Section measurable_fun_integral_kernel. +Import HBNNSimple. Lemma measurable_fun_integral_kernel d d' (X : measurableType d) (Y : measurableType d') (R : realType) @@ -1138,6 +1140,7 @@ rewrite integral_indic//= /kcomp. by apply: eq_integral => y _; rewrite integral_indic. Qed. +Import HBNNSimple. Let integral_kcomp_nnsfun x (f : {nnsfun Z >-> R}) : \int[kcomp l k x]_z (f z)%:E = \int[l x]_y (\int[k (x, y)]_z (f z)%:E). @@ -1319,6 +1322,7 @@ split => //. + by split => //; rewrite kfcompkindic. Qed. +Import HBNNSimple. (* [Lemma 14.20, Klenke 2014] *) Lemma measurable_kfcomp : measurable_fun [set: T1 * T2] f -> diff --git a/theories/lebesgue_integral_theory/giry.v b/theories/lebesgue_integral_theory/giry.v index f756f62a4d..3c98adfd58 100644 --- a/theories/lebesgue_integral_theory/giry.v +++ b/theories/lebesgue_integral_theory/giry.v @@ -290,10 +290,7 @@ apply: measurable_giry_codensity => //= B mB. by apply: measurable_giry_int => //; exact: measurable_giry_ev. Qed. -<<<<<<< HEAD Import HBNNSimple. -======= ->>>>>>> 1d806e2cf (sigma-algebra for normed modules + sfun codomain sigma ring & module structure) Import MeasurableR. Lemma sintegral_giry_join (M : giry (giry T R) R) (h : {nnsfun T >-> R}) : diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v index 39122860ca..ad2b814d30 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v @@ -84,6 +84,7 @@ rewrite sintegralE fsbig1// => r _; rewrite preimage_cst. by case: ifPn => [/[!inE] <-|]; rewrite ?mul0e// measure0 mule0. Qed. +Import HBNNSimple. Lemma sintegral_ge0 (f : {nnsfun T >-> R}) : 0 <= sintegral mu f. Proof. by rewrite sintegralE fsume_ge0// => r _; exact: nnsfun_mulemu_ge0. Qed. @@ -139,6 +140,7 @@ Local Open Scope ereal_scope. Context d (T : sigmaRingType d) (R : realType). Variables (m : {measure set T -> \bar R}) (r : R) (f : {nnsfun T >-> R}). +Import HBNNSimple. Lemma sintegralrM : sintegral m (cst r \* f)%R = r%:E * sintegral m f. Proof. @@ -195,6 +197,7 @@ Section le_sintegral. Context d (T : measurableType d) (R : realType) (m : {measure set T -> \bar R}). Variables f g : {nnsfun T >-> R}. +Import HBNNSimple. Hypothesis fg : forall x, f x <= g x. @@ -211,6 +214,7 @@ Qed. End le_sintegral. Section is_cvg_sintegral. +Import HBNNSimple. Lemma is_cvg_sintegral d (T : measurableType d) (R : realType) (m : {measure set T -> \bar R}) (f : {nnsfun T >-> R}^nat) : @@ -227,6 +231,7 @@ Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. Variables (g : {nnsfun T >-> R}^nat) (f : {nnsfun T >-> R}). +Import HBNNSimple. Hypothesis nd_g : forall x, nondecreasing_seq (g^~ x). Hypothesis gf : forall x, cvgn (g^~ x) -> f x <= limn (g^~ x). @@ -346,6 +351,7 @@ Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. Variables (g : {nnsfun T >-> R}^nat) (f : {nnsfun T >-> R}). +Import HBNNSimple. Hypothesis nd_g : forall x, nondecreasing_seq (g^~ x). Hypothesis gf : forall x, g ^~ x @ \oo --> f x. @@ -372,6 +378,7 @@ Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). Implicit Types (f g : T -> \bar R) (D : set T). +Import HBNNSimple. Let nnintegral mu f := ereal_sup [set sintegral mu h | h in [set h : {nnsfun T >-> R} | forall x, (h x)%:E <= f x]]. @@ -470,6 +477,7 @@ Context {d} {T : measurableType d} {R : realType}. Variables m1 m2 : {measure set T -> \bar R}. Hypothesis m12 : forall S, measurable S -> m1 S <= m2 S. +Import HBNNSimple. Lemma ge0_le_measure_integral (f : T -> \bar R) S : measurable S -> (forall x, 0 <= f x) -> measurable_fun [set: T] f -> @@ -488,6 +496,7 @@ Context d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D). Implicit Type A : set T. +Import HBNNSimple. Lemma integral_indic A : measurable A -> \int[mu]_(x in D) (\1_A x)%:E = mu (A `&` D). @@ -506,6 +515,7 @@ Context {d} {T : measurableType d} {R : realType} Lemma integral_mkcond D f : \int[mu]_(x in D) f x = \int[mu]_x (f \_ D) x. Proof. by rewrite /integral patch_setT. Qed. +Import HBNNSimple. Lemma integralT_nnsfun (h : {nnsfun T >-> R}) : \int[mu]_x (h x)%:E = sintegral mu h. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v index c650da9ce9..41a86b07f3 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v @@ -81,6 +81,7 @@ Import MeasurableR. Let R : measurableType _ := measurableTypeR rT. Local Open Scope ereal_scope. +Import HBSimple. Lemma approximation_continuous_integrable (E : set _) (f : rT -> rT): measurable E -> mu E < +oo -> mu.-integrable E (EFin \o f) -> diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v index 1eb4406df9..2ede24962a 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v @@ -35,6 +35,7 @@ Variables (mu : {measure set T -> \bar R}) (f : T -> \bar R) Hypothesis f0 : forall x, 0 <= f x. Hypothesis mf : measurable_fun setT f. +Import HBNNSimple. Hypothesis nd_g : forall x, nondecreasing_seq (g^~x). Hypothesis gf : forall x, EFin \o g^~ x @ \oo --> f x. @@ -89,6 +90,7 @@ Hypothesis f10 : forall x, D x -> 0 <= f1 x. Hypothesis mf1 : measurable_fun D f1. Hypothesis mf2 : measurable_fun D f2. +Import HBNNSimple. Lemma ge0_le_integral : (forall x, D x -> f1 x <= f2 x) -> \int[mu]_(x in D) f1 x <= \int[mu]_(x in D) f2 x. @@ -161,6 +163,7 @@ Local Definition max_g2' : (T -> R)^nat := Local Definition max_g2 : {nnsfun T >-> R}^nat := fun k => bigmax_nnsfun (g2^~ k) k. +Import HBNNSimple. Let is_cvg_g2 n t : cvgn (EFin \o (g2 n ^~ t)). Proof. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index 5189d5c04f..a4af3f425b 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -85,6 +85,7 @@ Context d (T : measurableType d) (R : realType). Let sintegral_measure_zero (f : T -> R) : sintegral mzero f = 0. Proof. by rewrite sintegralE big1// => r _ /=; rewrite /mzero mule0. Qed. +Import HBNNSimple. Lemma integral_measure_zero (D : set T) (f : T -> \bar R) : \int[mzero]_(x in D) f x = 0. @@ -117,6 +118,7 @@ Context {d} {T : measurableType d} {R : realType} Hypothesis f0 : forall x, D x -> 0 <= f x. Hypothesis mf : measurable_fun D f. +Import HBNNSimple. Let ge0_integralZl_EFin_subproof k : (0 <= k)%R -> \int[mu]_(x in D) (k%:E * f x) = k%:E * \int[mu]_(x in D) f x. @@ -201,6 +203,7 @@ Hypothesis mf1 : measurable_fun D f1. Hypothesis f20 : forall x, D x -> 0 <= f2 x. Hypothesis mf2 : measurable_fun D f2. +Import HBNNSimple. Lemma ge0_integralD : \int[mu]_(x in D) (f1 x + f2 x) = \int[mu]_(x in D) f1 x + \int[mu]_(x in D) f2 x. @@ -446,6 +449,7 @@ rewrite !fsbig_set1 mul0e add0e preimage_restrict//. by rewrite ifN ?set0U ?setIidl//= notin_setE => /esym; exact/eqP. Qed. +Import HBNNSimple. Local Lemma integral_cstr r : \int[mu]_(x in D) r%:E = r%:E * mu D. Proof. @@ -687,6 +691,7 @@ Qed. End integral_measure_sum_nnsfun. Section integral_measure_add_nnsfun. +Import HBNNSimple. Lemma integral_measure_add_nnsfun d (T : measurableType d) (R : realType) (m1 m2 : {measure set T -> \bar R}) (D : set T) (mD : measurable D) @@ -705,6 +710,7 @@ Local Open Scope ereal_scope. Context {d} {T : measurableType d} {R : realType} (m_ : {measure set T -> \bar R}^nat). +Import HBNNSimple. Lemma ge0_integral_measure_sum (D : set T) (mD : measurable D) (f : T -> \bar R) : @@ -802,6 +808,7 @@ Context {d} {T : measurableType d} {R : realType} (m_ : {measure set T -> \bar R}^nat). Let m := mseries m_ O. +Import HBNNSimple. Lemma ge0_integral_measure_series (D : set T) (mD : measurable D) (f : T -> \bar R) : (forall t, D t -> 0 <= f t) -> diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v index 6b238370f5..cc5f2ab413 100644 --- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v +++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v @@ -351,6 +351,7 @@ Definition nnsfun_approx : {nnsfun T >-> R}^nat := fun n => locked (add_nnsfun else nnsfun0) (n * 2 ^ n)%N) (scale_nnsfun (indic_nnsfun _ (mB n)) (ler0n _ n))). +Import HBNNSimple. Lemma nnsfun_approxE n : nnsfun_approx n = approx n :> (T -> R). Proof. @@ -376,11 +377,13 @@ End approximation. Section approximation_sfun. Context d (T : measurableType d) (R : realType) (f : T -> \bar R). Variables (D : set T) (mD : measurable D) (mf : measurable_fun D f). -Import MeasurableR. + +Import HBSimple. (* NB: already instantiated in cardinality.v *) (*HB.instance Definition _ x : @FImFun T R (cst x) := FImFun.on (cst x).*) (* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *) +Import HBNNSimple. (* NB: already instantiated in lebesgue_integral.v *) (*HB.instance Definition _ x : @NonNegFun T R (cst x%:num) := NonNegFun.on (cst x%:num).*) @@ -704,6 +707,7 @@ Let R : measurableType _ := measurableTypeR rT. Hypothesis mA : measurable A. Hypothesis finA : mu A < +oo. +Import HBSimple. Let lusin_simple (f : {sfun R >-> rT}) (eps : rT) : (0 < eps)%R -> exists K, [/\ compact K, K `<=` A, mu (A `\` K) < eps%:E & diff --git a/theories/probability_theory/normal_distribution.v b/theories/probability_theory/normal_distribution.v index ed296f469f..a2df3f5dc2 100644 --- a/theories/probability_theory/normal_distribution.v +++ b/theories/probability_theory/normal_distribution.v @@ -588,7 +588,6 @@ Section normal_prob_lemmas. Context {R : realType}. Local Notation mu := lebesgue_measure. Local Open Scope ereal_scope. -Import MeasurableR. Import MeasurableR. diff --git a/theories/probability_theory/uniform_distribution.v b/theories/probability_theory/uniform_distribution.v index 4ea91d5f4d..db21ea3dde 100644 --- a/theories/probability_theory/uniform_distribution.v +++ b/theories/probability_theory/uniform_distribution.v @@ -149,6 +149,7 @@ case: ifPn => //. by rewrite inE/= in_itv/= => axb; rewrite indicE (negbTE xE) mule0. Qed. +Import HBNNSimple. Let integral_uniform_nnsfun (f : {nnsfun _ >-> R}) : (\int[uniform_prob ab]_x (f x)%:E = diff --git a/theories/real_measure/lebesgue_stieltjes_measure.v b/theories/real_measure/lebesgue_stieltjes_measure.v index 946ab0ea68..0f9d55a829 100644 --- a/theories/real_measure/lebesgue_stieltjes_measure.v +++ b/theories/real_measure/lebesgue_stieltjes_measure.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import boot order finmap ssralg ssrnum ssrint interval. +From mathcomp Require Import boot order finmap ssralg ssrnum ssrint algebra interval. From mathcomp Require Import interval_inference archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From bf3fdfd52302ce85db7058d1ad1c87d2594cda26 Mon Sep 17 00:00:00 2001 From: arthurd Date: Tue, 10 Nov 2026 12:24:19 +0100 Subject: [PATCH 4/8] small fixes --- .../simple_functions.v | 187 +++++------------- .../real_measure/lebesgue_stieltjes_measure.v | 41 ++-- theories/topology_theory/metric_structure.v | 14 ++ 3 files changed, 73 insertions(+), 169 deletions(-) diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 63ec57e9ae..71977785e5 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -28,9 +28,8 @@ From mathcomp Require Import real_measure numfun realfun. (* *) (* Detailed contents: *) (* ```` *) -(* {sfun aT >-> bT} == type of simple functions *) -(* They can form a ring or a module depending on *) -(* the structure of bT *) +(* {sfun T >-> R} == type of simple functions *) +(* They form a (potentially zero) ring. *) (* {nnsfun T >-> R} == type of non-negative simple functions *) (* indic_sfun mD := mindic _ mD *) (* cst_sfun r == constant simple function *) @@ -74,19 +73,24 @@ Local Open Scope ring_scope. Module HBSimple. Import MeasurableR. -HB.structure Definition SimpleFun d d' - (aT : sigmaRingType d) (rT : sigmaRingType d') := - {f of @isMeasurableFun d d' aT rT f & @FiniteImage aT rT f}. +HB.structure Definition SimpleFun d (aT : sigmaRingType d) (rT : realType) := + {f of @isMeasurableFun d _ aT rT f & @FiniteImage aT rT f}. -Notation "{ 'sfun' aT >-> T }" := (@SimpleFun.type _ _ aT T) : form_scope. +End HBSimple. + +Notation "{ 'sfun' aT >-> T }" := (@HBSimple.SimpleFun.type _ aT T) : form_scope. Notation "[ 'sfun' 'of' f ]" := [the {sfun _ >-> _} of f] : form_scope. +Module HBNNSimple. +Import HBSimple. HB.structure Definition NonNegSimpleFun d (aT : sigmaRingType d) (rT : realType) := - {f of @SimpleFun d _ aT rT f & @NonNegFun aT rT f}. + {f of @SimpleFun d _ _ f & @NonNegFun aT rT f}. + +End HBNNSimple. -Notation "{ 'nnsfun' aT >-> T }" := (@NonNegSimpleFun.type _ aT%type T) : form_scope. +Notation "{ 'nnsfun' aT >-> T }" := (@HBNNSimple.NonNegSimpleFun.type _ aT%type T) : form_scope. Notation "[ 'nnsfun' 'of' f ]" := [the {nnsfun _ >-> _} of f] : form_scope. Section sfun_pred. @@ -100,18 +104,19 @@ Lemma sub_sfun_fimfun : {subset sfun <= fimfun}. Proof. by move=> x /andP[]. Qed End sfun_pred. Section sfun. -Context {d d'} {aT : measurableType d} {rT : measurableType d'}. +Context {d} {aT : measurableType d} {rT : realType}. Notation T := {sfun aT >-> rT}. -Notation sfun := (@sfun _ _ aT rT). +Notation sfun := (@sfun _ aT rT). Section Sub. Context (f : aT -> rT) (fP : f \in sfun). Import MeasurableR. Definition sfun_Sub1_subproof := - @isMeasurableFun.Build d d' aT rT f (set_mem (sub_sfun_mfun fP)). + @isMeasurableFun.Build d _ aT rT f (set_mem (sub_sfun_mfun fP)). #[local] HB.instance Definition _ := sfun_Sub1_subproof. Definition sfun_Sub2_subproof := @FiniteImage.Build aT rT f (set_mem (sub_sfun_fimfun fP)). +Import HBSimple. #[local] HB.instance Definition _ := sfun_Sub2_subproof. Definition sfun_Sub := [sfun of f]. @@ -126,6 +131,7 @@ have -> : Pf2 = set_mem (sub_sfun_fimfun Pf) by []. exact: Ksub. Qed. +Import HBSimple. Lemma sfun_valP f (Pf : f \in sfun) : sfun_Sub Pf = f :> (_ -> _). Proof. by []. Qed. @@ -149,9 +155,9 @@ Lemma cst_sfunE x : @cst_sfun x =1 cst x. Proof. by []. Qed. End sfun. (* a better way to refactor function stuffs *) -Lemma fctD (T : Type) (N : nmodType) (f g : T -> N) : f + g = f \+ g. +Lemma fctD (T : Type) (K : pzRingType) (f g : T -> K) : f + g = f \+ g. Proof. by []. Qed. -Lemma fctN (T : Type) (N : zmodType) (f : T -> N) : - f = \- f. +Lemma fctN (T : Type) (K : pzRingType) (f : T -> K) : - f = \- f. Proof. by []. Qed. Lemma fctM (T : Type) (K : pzRingType) (f g : T -> K) : f * g = f \* g. Proof. by []. Qed. @@ -164,20 +170,32 @@ Definition fctWE := (fctD, fctN, fctM, fctZ). Section ring. Context d (aT : measurableType d) (rT : realType). -Lemma sfun_subring_closed : subring_closed (@sfun d _ aT rT). +Lemma sfun_subring_closed : subring_closed (@sfun d aT rT). Proof. by split=> [|f g|f g]; rewrite ?inE/= ?rpred1//; move=> /andP[/= mf ff] /andP[/= mg fg]; rewrite !(rpredB, rpredM). Qed. -HB.instance Definition _ := GRing.isSubringClosed.Build _ (@sfun d _ aT rT) +HB.instance Definition _ := GRing.isSubringClosed.Build _ sfun sfun_subring_closed. HB.instance Definition _ := [SubChoice_isSubComPzRing of {sfun aT >-> rT} by <:]. Implicit Types (f g : {sfun aT >-> rT}). +Import HBSimple. + +Lemma sfun0 : (0 : {sfun aT >-> rT}) =1 cst 0. Proof. by []. Qed. Lemma sfun1 : (1 : {sfun aT >-> rT}) =1 cst 1. Proof. by []. Qed. +Lemma sfunN f : - f =1 \- f. Proof. by []. Qed. +Lemma sfunD f g : f + g =1 f \+ g. Proof. by []. Qed. +Lemma sfunB f g : f - g =1 f \- g. Proof. by []. Qed. Lemma sfunM f g : f * g =1 f \* g. Proof. by []. Qed. +Lemma sfun_sum I r (P : {pred I}) (f : I -> {sfun aT >-> rT}) (x : aT) : + (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. +Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. +Lemma sfun_prod I r (P : {pred I}) (f : I -> {sfun aT >-> rT}) (x : aT) : + (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. +Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. Lemma sfunX f n : f ^+ n =1 (fun x => f x ^+ n). Proof. by move=> x; elim: n => [|n IHn]//; rewrite !exprS sfunM/= IHn. Qed. @@ -188,6 +206,7 @@ HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f). HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g). +Import HBSimple. (* TODO: mv to `measurable_realfun.v`? *) HB.instance Definition _ (D : set aT) (mD : measurable D) : @@ -195,130 +214,12 @@ HB.instance Definition _ (D : set aT) (mD : measurable D) : Definition indic_sfun (D : set aT) (mD : measurable D) : {sfun aT >-> rT} := mindic rT mD. -End ring. +HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst_sfun k). +Definition scale_sfun k f : {sfun aT >-> rT} := k \o* f. +End ring. Arguments indic_sfun {d aT rT} _. -Section sfun_lmodType. -Context d (aT : measurableType d) (R : realType) (N : normedModType R). - -Lemma mem_sfun_comp_pair (U V W : normedModType R) (f : {sfun aT >-> U}) - (g : {sfun aT >-> V}) (h : U * V -> W) : - (fun x => h (f x, g x)) \in @sfun _ _ aT W. -Proof. -rewrite inE; apply/andP; split; rewrite inE/=. - move=> _ Y mY; rewrite setTI. - rewrite (_ : _ @^-1` Y = - \bigcup_(a in range f) (\bigcup_(b in range g) - ((f @^-1` [set a] `&` g @^-1` [set b]) `&` [set _ | Y (h (a, b))]))). - apply/seteqP; split=> [x/= Yfg|x [a _] [b _] [[/= <- <-]]//]. - by exists (f x); [exists x|exists (g x); [exists x|]]. - apply: fin_bigcup_measurable; first exact: fimfunP. - move=> a _; apply: fin_bigcup_measurable; first exact: fimfunP. - move=> b _; apply: measurableI. - exact: measurableI. - have [Yhab|Yhab] := pselect (Y (h (a, b))). - by rewrite (_ : [set _ | _] = setT); - [apply/seteqP; split|exact: measurableT]. - rewrite (_ : [set _ | _] = set0); last exact: measurable0. - by apply/seteqP; split. -apply: (@sub_finite_set _ _ (h @` (range f `*` range g))). - by move=> _ [x _ <-]/=; exists (f x, g x) => //; split; exists x. -exact/finite_image/finite_setX/fimfunP. -Qed. - -Lemma sfun_submod_closed : - submod_closed (@sfun _ _ aT N). -Proof. -split=> [|k f g sf sg]; first exact: (valP (cst_sfun (0 : N))). -exact: (mem_sfun_comp_pair (sfun_Sub sf) (sfun_Sub sg) (fun t => k *: t.1 + t.2)). -Qed. - -HB.instance Definition _ := - GRing.isSubmodClosed.Build _ _ (@sfun _ _ aT N) - sfun_submod_closed. -HB.instance Definition _ := - [SubChoice_isSubLmodule of {sfun aT >-> N} by <:]. - -Implicit Types (f g : {sfun aT >-> N} : lmodType _). - -Lemma sfun0 : (0 : {sfun aT >-> N} : lmodType _) =1 cst 0. Proof. by []. Qed. -Lemma sfunN f : - f =1 \- f. Proof. by []. Qed. -Lemma sfunD f g : f + g =1 f \+ g. Proof. by []. Qed. -Lemma sfunB f g : f - g =1 f \- g. Proof. by []. Qed. -Lemma sfunZ k f : k *: f =1 k \*: f. Proof. by []. Qed. -Lemma sfun_sum I r (P : {pred I}) (f : I -> {sfun aT >-> N} : lmodType _) (x : aT) : - (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. -Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. -Lemma sfun_prod I r (P : {pred I}) (f : I -> {sfun aT >-> N} : lmodType _) (x : aT) : - (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. -Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. - -HB.instance Definition _ f g := MeasurableFun.copy (f \+ g) (f + g). -HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f). -HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). -HB.instance Definition _ k f := MeasurableFun.copy (k \*: f) (k *: f). - -End sfun_lmodType. - -(* This could be moved elsewhere *) -Section indic_lmod. -Context {T : Type} {K : pzRingType} {L : lmodType K}. - -Definition indic_lmod (A : set T) (z : L) := ( *:%R^~ z) \o \1_A. - -Lemma indic_lmodE A z : indic_lmod A z = (fun x => if x \in A then z else 0). -Proof. -by apply/funext=> x; rewrite/indic_lmod/= indicE; -case: ifPn=> _ /=; rewrite ?scale0r ?scale1r. -Qed. - -Lemma image_indic_lmod_sub A z D : (indic_lmod A z) @` D `<=` [set 0;z]. -Proof. -rewrite -image_comp; apply: (subset_trans (image_subset ( *:%R ^~ z) _)); - first exact: image_indic_sub. -move=> y /= [x [->|->]]; rewrite ?scale0r ?scale1r=> ->; first by left. by right. -Qed. - -Lemma preimage_indic_lmod A (B : set L) (z : L) : - (indic_lmod A z) @^-1` B = if z \in B then if 0 \in B then [set: T] else A - else if 0 \in B then ~` A else set0. -Proof. -rewrite comp_preimage preimage_indic. by do 4 (case: ifPn => [|]); - rewrite ?in_setE ?notin_setE //= ?scale0r ?scale1r. -Qed. - -Lemma indic_lmod_fimfun_subproof (A : set T) (z : L) : -@FiniteImage T L (indic_lmod A z). Proof. by []. Qed. - -HB.instance Definition _ A z := @indic_lmod_fimfun_subproof A z. - -End indic_lmod. - -Section mindic_lmod. -Context d {aT : measurableType d} {rT : realType} {nT : normedModType rT}. - -Definition mindic_lmod (A : set aT) (mA : measurable A) := - @indic_lmod aT rT nT A. - -Lemma measurable_indic_lmod {D} (A : set aT) (mA : d.-measurable A) (z:nT) : -measurable_fun D (mindic_lmod mA z). -Proof. -move=> mD Y mY; rewrite preimage_indic_lmod //. -do 2 (case: ifP => _); apply: measurableI=>//; exact: measurableC. -Qed. - -HB.instance Definition _ A mA z := @isMeasurableFun.Build _ _ aT nT - (mindic_lmod mA z) (@measurable_indic_lmod [set: aT] A mA z). - -HB.instance Definition _ (D : set aT) (mD : measurable D) (z : nT) : - @FImFun aT nT (mindic_lmod mD z) := FImFun.on (mindic_lmod mD z). - -Definition mindic_lmod_sfun (D : set aT) (mD : measurable D) (z : nT) : - {sfun aT >-> nT} := mindic_lmod mD z. - -End mindic_lmod. - Lemma preimage_nnfun0 T (R : realDomainType) (f : {nnfun T >-> R}) t : t < 0 -> f @^-1` [set t] = set0. Proof. @@ -334,13 +235,11 @@ by split=> [z/= <-|z/= ->]; rewrite [x * _]mulrC (mulfK, divfK). Qed. Section simple_bounded. -<<<<<<< HEAD Context {d} {T : sigmaRingType d} {R : realType}. -======= -Context d (T : sigmaRingType d) (R : realType) (N : normedModType R). ->>>>>>> b5e0fd857 (sigma-algebra for normed modules + sfun codomain sigma ring & module structure) -Lemma simple_bounded (f : {sfun T >-> N}) : bounded_fun f. +Import HBSimple. + +Lemma simple_bounded (f : {sfun T >-> R}) : bounded_fun f. Proof. have /finite_seqP[r fr] := fimfunP f. exists (fine (\big[maxe/-oo%E]_(i <- r) `|i|%:E)). @@ -432,6 +331,7 @@ Definition proj_nnsfun d (T : measurableType d) (R : realType) mul_nnsfun f (indic_nnsfun R mA). Section mrestrict. +Import HBNNSimple. Lemma mrestrict d (T : measurableType d) (R : realType) (f : {nnsfun T >-> R}) A (mA : measurable A) : f \_ A = proj_nnsfun f mA. @@ -448,6 +348,7 @@ Variable f : {nnsfun T >-> R}^nat. Definition sum_nnsfun n := \big[add_nnsfun/nnsfun0]_(i < n) f i. +Import HBNNSimple. Lemma sum_nnsfunE n t : sum_nnsfun n t = \sum_(i < n) (f i t). Proof. by rewrite /sum_nnsfun; elim/big_ind2 : _ => [|x g y h <- <-|]. Qed. @@ -464,6 +365,7 @@ Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). Variable f : {nnsfun T >-> R}. +Import HBNNSimple. Lemma nnsfun_cover : \big[setU/set0]_(i \in range f) (f @^-1` [set i]) = setT. Proof. by rewrite fsbig_setU//= -subTset => x _; exists (f x). Qed. @@ -535,6 +437,7 @@ by move=> xA; rewrite (@mulef_ge0 _ _ (mu \o _))//= => /xA ->; rewrite measure0. Qed. Global Arguments mulemu_ge0 {d T R mu x} A. +Import HBNNSimple. Lemma nnsfun_mulemu_ge0 d (T : sigmaRingType d) (R : realType) (mu : {measure set T -> \bar R}) (f : {nnsfun T >-> R}) x : diff --git a/theories/real_measure/lebesgue_stieltjes_measure.v b/theories/real_measure/lebesgue_stieltjes_measure.v index 0f9d55a829..77bc93a252 100644 --- a/theories/real_measure/lebesgue_stieltjes_measure.v +++ b/theories/real_measure/lebesgue_stieltjes_measure.v @@ -463,21 +463,6 @@ Qed. End rgenopensets. End RGenOpenSets. -(* Could be moved elsewhere and generalized to metric spaces *) -Section normed_lemmas. -Context {R : realType} {N : normedModType R}. - -Lemma set1_bigcap_ball (x : N) : [set x] = \bigcap_n ball x n.+1%:R^-1. -Proof. -rewrite eqEsubset/bigcap; split=> [y -> n _ | y /= bn]/=. - by apply: ballxx; rewrite invr_gt0. -apply: close_eq _=>//; rewrite ball_close=> e0; rewrite ball_symE. -apply: (le_ball _ (bn (truncn e0%:num^-1) I)). rewrite invf_ple ?posrE//. -exact: (ltW (truncnS_gt _)). -Qed. - -End normed_lemmas. - (* Should be moved to a more general file *) Section open. Context {R : realType} {N : normedModType R}. @@ -507,22 +492,23 @@ Notation "N .-open" := (sigma_display (@open N)) : measure_display_scope. Notation "N .-open.-measurable" := (measurable : set_system (@open_type _ N)) : classical_set_scope. -Module MeasurableOpen. +Module MeasurableNormedModuleOpen. Section measurableOpen. Context {R : realType} {N : normedModType R}. +Import numFieldNormedType.Exports. -Definition measurableTypeO := g_sigma_algebraType (@open N). +Definition measurableTypeNormedModule := g_sigma_algebraType (@open N). Definition borel_display : measure_display := N.-open. -Definition measurableO : set_system N := N.-open.-measurable. +Definition measurableNormedModule : set_system N := N.-open.-measurable. -HB.instance Definition _ : Measurable borel_display measurableTypeO := - Measurable.on measurableTypeO. +HB.instance Definition _ : Measurable borel_display measurableTypeNormedModule := + Measurable.on measurableTypeNormedModule. (* Presumably it is safe to use NFI here because morally R is unique and nothing else can be used here *) #[non_forgetful_inheritance] -HB.instance Definition _ := Measurable.copy N measurableTypeO. +HB.instance Definition _ := Measurable.copy N measurableTypeNormedModule. Lemma measurable_set1 (x : N) : measurable [set x]. Proof. @@ -535,14 +521,14 @@ Lemma measurable_ball_norm (x : N) e : measurable (ball x e). Proof. by apply: (sub_sigma_algebra (ball_open _ _)). Qed. End measurableOpen. -Arguments measurableTypeO : clear implicits. +Arguments measurableTypeNormedModule : clear implicits. #[global] Hint Extern 0 (measurable (_ @^-1` [set _])) => solve [apply: measurable_funPTI; exact: measurable_set1] : core. #[global] Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. -Lemma measurable_funP1 {d} {aT : measurableType d} {rT : realType} +Lemma measurable_funP1 {d} {aT : measurableType d} {rT : realType} {nT : normedModType rT} (f : {mfun aT >-> nT}) D (z : nT) : measurable D -> measurable (D `&` f @^-1` [set z]). Proof. by move=> /(measurable_funP f); exact. Qed. @@ -555,11 +541,12 @@ Section measurableReal. Context {R : realType}. Import numFieldNormedType.Exports. -Definition measurableTypeR := @measurableTypeO R R. +Definition measurableTypeR := @measurableTypeNormedModule R R. Definition lebesgue_display : measure_display := @borel_display R R. -Definition measurableR := @measurableO R R. +Definition measurableR := @measurableNormedModule R R. + (* Shouldn't be needing ideally... *) HB.instance Definition _ := Measurable.copy R measurableTypeR. @@ -575,11 +562,11 @@ Arguments measurableTypeR : clear implicits. #[global] Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. -End MeasurableOpen. +End MeasurableNormedModuleOpen. Module MeasurableR. Export numFieldNormedType.Exports. -Export MeasurableOpen. +Export MeasurableNormedModuleOpen. End MeasurableR. Section ocitv_measure. diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v index 06f4b1a94e..7eba93cbab 100644 --- a/theories/topology_theory/metric_structure.v +++ b/theories/topology_theory/metric_structure.v @@ -109,6 +109,20 @@ Qed. End metric_numFieldType. +Section metric_archiRealFieldType. +Context {R : archiRealFieldType} {N : metricType R}. + +Lemma set1_bigcap_ball (x : N) : [set x] = \bigcap_n ball x n.+1%:R^-1. +Proof. +rewrite eqEsubset; split=> [y -> n _ | y /= bn]/=; first by apply: ballxx; + rewrite invr_gt0. +apply: close_eq _=>//; first exact: metric_hausdorff; rewrite ball_close=> e0; +rewrite ball_symE. apply: (le_ball _ (bn (truncn e0%:num^-1) I)). +by rewrite invf_ple ?posrE//; exact: (ltW (truncnS_gt _)). +Qed. + +End metric_archiRealFieldType. + Section prod_metric. Context {K : numDomainType} (T U : metricType K). From d5cfc5588f65b322b4adbe24d99e560711956d2e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 12 Nov 2026 21:27:40 +0900 Subject: [PATCH 5/8] add normedtype_measure.v --- _CoqProject | 1 + theories/Make | 1 + .../lebesgue_integral_differentiation.v | 6 +- .../lebesgue_integral_nonneg.v | 6 +- .../measurable_fun_approximation.v | 2 +- theories/probability_theory/random_variable.v | 8 +- theories/real_measure/lebesgue_measure.v | 17 +- .../real_measure/lebesgue_stieltjes_measure.v | 175 +++++------------- theories/real_measure/measurable_realfun.v | 48 +++-- theories/real_measure/normedtype_measure.v | 116 ++++++++++++ 10 files changed, 203 insertions(+), 177 deletions(-) create mode 100644 theories/real_measure/normedtype_measure.v diff --git a/_CoqProject b/_CoqProject index 0dcbd12ffa..e3cf7974b9 100644 --- a/_CoqProject +++ b/_CoqProject @@ -116,6 +116,7 @@ theories/measure_theory/measurable_function.v theories/measure_theory/signed_measure.v theories/measure_theory/measure.v +theories/real_measure/normedtype_measure.v theories/real_measure/lebesgue_stieltjes_measure.v theories/real_measure/lebesgue_measure.v theories/real_measure/measurable_realfun.v diff --git a/theories/Make b/theories/Make index 15781fc7db..3120733ea3 100644 --- a/theories/Make +++ b/theories/Make @@ -83,6 +83,7 @@ measure_theory/measurable_function.v measure_theory/signed_measure.v measure_theory/measure.v +real_measure/normedtype_measure.v real_measure/lebesgue_stieltjes_measure.v real_measure/lebesgue_measure.v real_measure/measurable_realfun.v diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v index 41a86b07f3..ab9855cd3d 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v @@ -58,7 +58,7 @@ Section continuous_compact_integrable. Context {rT : realType}. Let mu : measure _ _ := @lebesgue_measure rT. Import MeasurableR. -Let R : measurableType _ := measurableTypeR rT. +Let R : measurableType _ := (*measurableTypeR*) rT. Local Open Scope ereal_scope. Lemma continuous_compact_integrable (f : R -> R^o) (A : set R^o) : @@ -78,7 +78,7 @@ Section continuous_density_L1. Context (rT : realType). Let mu : measure _ _ := @lebesgue_measure rT. Import MeasurableR. -Let R : measurableType _ := measurableTypeR rT. +Let R : measurableType _ := (*measurableTypeR*) rT. Local Open Scope ereal_scope. Import HBSimple. @@ -180,7 +180,7 @@ Section lebesgue_differentiation_continuous. Context {rT : realType}. Let mu : measure _ _ := @lebesgue_measure rT. Import MeasurableR. -Let R : measurableType _ := measurableTypeR rT. +Let R : measurableType _ := (*measurableTypeR*) rT. Let ballE (x : R) (r : {posnum rT}) : ball x r%:num = `](x - r%:num), (x + r%:num)[%classic :> set rT. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index a4af3f425b..c142c7979c 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -557,7 +557,7 @@ Local Notation mu := lebesgue_measure. Import MeasurableR. Lemma lebesgue_measureN (A : set R) : measurable A -> - pushforward mu (-%R : _ -> measurableTypeR R) A = mu A. + pushforward mu (-%R : _ -> (*measurableTypeR*) R) A = mu A. Proof. move=> mA; apply/esym/lebesgue_measure_unique => //= _ [[a b]] _ <-. rewrite /pushforward opp_preimage_itvbndbnd/= !lebesgue_measure_itv/=. @@ -569,7 +569,7 @@ Lemma ge0_integration_by_substitution0 (f : R -> \bar R) : \int[mu]_(r in `[0%R, +oo[) f r = \int[mu]_(r in `]-oo, 0%R]) f (- r)%R. Proof. move=> mf f0; rewrite (_ : `]-oo, 0%R]%classic = - (-%R : _ -> measurableTypeR R) @^-1` `[0%R, +oo[). + (-%R : _ -> (*measurableTypeR*) R) @^-1` `[0%R, +oo[). by rewrite opp_preimage_itvbndy oppr0. rewrite -ge0_integral_pushforward//=; first exact: measurable_funS mf. by apply: eq_measure_integral => //= A mA AS; exact/esym/lebesgue_measureN. @@ -1068,7 +1068,7 @@ End integral_patch. Section ge0_cvgn_integral. Local Open Scope ereal_scope. Import MeasurableR. -Context {R : realType} (mu : {measure set (@measurableTypeR R) -> \bar R}) +Context {R : realType} (mu : {measure set ((*@measurableTypeR*) R) -> \bar R}) (f : R -> R). Hypothesis f0 : (forall x, 0 <= f x)%R. diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v index cc5f2ab413..8794f07ef1 100644 --- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v +++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v @@ -703,7 +703,7 @@ Hint Extern 0 (hausdorff_space _) => (exact: Rhausdorff) : core. Local Open Scope ereal_scope. Context (rT : realType) (A : set rT). Let mu : measure _ _ := @lebesgue_measure rT. -Let R : measurableType _ := measurableTypeR rT. +Let R : measurableType _ := rT(*measurableTypeR rT*). Hypothesis mA : measurable A. Hypothesis finA : mu A < +oo. diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index efebbbfa82..bcd8f48fef 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -381,7 +381,7 @@ Context {R : realType} (f : cumulativeBounded (0:R) (1:R)). Local Open Scope measure_display_scope. Import MeasurableR. -Let idTR : measurableTypeR R -> R := idfun. +Let idTR : (*measurableTypeR*) R -> R := idfun. #[local] HB.instance Definition _ := @isMeasurableFun.Build _ _ _ _ idTR (@measurable_id _ _ setT). @@ -410,10 +410,10 @@ End cdf_of_lebesgue_stieltjes_measure. Section lebesgue_stieltjes_measure_of_cdf. Import MeasurableR. -Context {R : realType} (P : probability (measurableTypeR R) R). +Context {R : realType} (P : probability ((*measurableTypeR*) R) R). Local Open Scope measure_display_scope. -Let idTR : measurableTypeR R -> R := idfun. +Let idTR : (*measurableTypeR*) R -> R := idfun. #[local] HB.instance Definition _ := @isMeasurableFun.Build _ _ _ _ idTR (@measurable_id _ _ setT). @@ -626,7 +626,7 @@ Let mu : {measure set _ -> \bar R} := @lebesgue_measure R. Lemma ge0_expectation_ccdf (X : {RV P >-> R}) : (forall x, 0 <= X x)%R -> 'E_P[X] = \int[mu]_(r in `[0%R, +oo[) ccdf X r. Proof. -pose GR := measurableTypeR R. +pose GR := (*measurableTypeR*) R. pose distrX := distribution P X. pose D : set R := `[0%R, +oo[%classic. move=> X_ge0. diff --git a/theories/real_measure/lebesgue_measure.v b/theories/real_measure/lebesgue_measure.v index 246eff542f..9102eec35a 100644 --- a/theories/real_measure/lebesgue_measure.v +++ b/theories/real_measure/lebesgue_measure.v @@ -8,7 +8,7 @@ From mathcomp Require Import boolp classical_sets functions cardinality fsbigop reals. From mathcomp Require Import topology ereal numfun normedtype sequences esum measure. -From mathcomp Require Export lebesgue_stieltjes_measure measurable_realfun. +From mathcomp Require Export normedtype_measure lebesgue_stieltjes_measure measurable_realfun. (**md**************************************************************************) (* # Lebesgue Measure *) @@ -572,9 +572,7 @@ apply: (@measure_semi_sigma_additive _ _ _ (@lebesgue_measure R) move=> [X mX [X' mX']] XX'Fn. apply: measurable_image_fine. rewrite -XX'Fn. - apply: measurableU. - apply: measurable_image_EFin. - by rewrite RGenOpenSets.measurableE/= in mX. + apply: measurableU; first exact: measurable_image_EFin. by case: mX' => //; exact: measurableU. - move=> i j _ _ [x [[a [Fia aoo ax] [b [Fjb boo] bx]]]]. move: tF => /(_ i j Logic.I Logic.I); apply. @@ -591,17 +589,16 @@ apply: (@measure_semi_sigma_additive _ _ _ (@lebesgue_measure R) + by rewrite not_orP => -[]/(_ erefl). + by rewrite not_orP => -[]/(_ erefl). - move: mUF. - rewrite {1}/measurable /emeasurable /= => -[X mX [Y []]] {Y}; - have moX : measurable X by rewrite -RGenOpenSets.measurableE. + rewrite {1}/measurable /emeasurable /= => -[X mX [Y []]] {Y}. + rewrite setU0 => h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. + rewrite [X in measurable X](_ : _ = X)// predeqE => r; split => [|Xr]. move=> -[n _ [x [Fnx xoo <-{r}]]]. have : (\bigcup_n F n) x by exists n. by rewrite -h => -[x' Xx' <-]. have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; exists r. by exists n => //; exists r%:E => //; split => // -[]. + move=> h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. + rewrite [X in measurable X](_ : _ = X)// predeqE => r; split => [|Xr]. move=> -[n _ [x [Fnx xoo <-]]]. have : (\bigcup_n F n) x by exists n. by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[]. @@ -609,14 +606,14 @@ apply: (@measure_semi_sigma_additive _ _ _ (@lebesgue_measure R) by exists n => //; exists r%:E => //; split => // -[]. + (* NB: almost the same as the previous one, factorize?*) move=> h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. + rewrite [X in measurable X](_ : _ = X)// predeqE => r; split => [|Xr]. move=> -[n _ [x [Fnx xoo <-]]]. have : (\bigcup_n F n) x by exists n. by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[]. have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r. by exists n => //; exists r%:E => //; split => // -[]. + move=> h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. + rewrite [X in measurable X](_ : _ = X)// predeqE => r; split => [|Xr]. move=> -[n _ [x [Fnx xoo <-]]]. have : (\bigcup_n F n) x by exists n. by rewrite -h => -[[x' Xx' <-//]|]. diff --git a/theories/real_measure/lebesgue_stieltjes_measure.v b/theories/real_measure/lebesgue_stieltjes_measure.v index 77bc93a252..dea64c85ea 100644 --- a/theories/real_measure/lebesgue_stieltjes_measure.v +++ b/theories/real_measure/lebesgue_stieltjes_measure.v @@ -6,7 +6,7 @@ From mathcomp Require Import interval_inference archimedean. From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets fsbigop cardinality. From mathcomp Require Import reals ereal topology normedtype sequences esum - measure realfun. + measure realfun normedtype_measure. (**md**************************************************************************) (* # Lebesgue Stieltjes Measure *) @@ -30,7 +30,7 @@ From mathcomp Require Import reals ereal topology normedtype sequences esum (* The HB class is CumulativeBounded. *) (* ``` *) (* *) -(* The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens, ROpenSets *) +(* The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenItvoo, ROpenSets *) (* provide proofs of equivalence between the sigma-algebra generated by *) (* open-closed intervals and the sigma-algebras generated by open rays, *) (* closed rays, open intervals, and open sets. *) @@ -43,7 +43,6 @@ From mathcomp Require Import reals ereal topology normedtype sequences esum (* x and y are real numbers *) (* R.-ocitv == display for ocitv_type R *) (* R.-ocitv.-measurable == semiring of sets of open-closed intervals *) -(* open_type R == alias for R : realType *) (* R.-open := sigma_display (@open R) *) (* R.-open.-measurable == sigma-algebra generated by open sets *) (* ``` *) @@ -54,9 +53,7 @@ From mathcomp Require Import reals ereal topology normedtype sequences esum (* measurableTypeR R == measurableType generated by *) (* R.-ocitv or R.-open *) (* @lebesgue_display R == (measure_)display for the sigma-algebra *) -(* generated by R.-ocitv or R.-open *) -(* @measurableR R == measurable sets generated by *) -(* R.-ocitv or R.-open *) +(* generated by R.-open *) (* ``` *) (* The module `MeasurableR` contains the default sigma-algebra, which is *) (* `MeasurableRopen`. The latter contains in addition: *) @@ -97,9 +94,6 @@ Local Open Scope ring_scope. Reserved Notation "R .-ocitv" (at level 1, format "R .-ocitv"). Reserved Notation "R .-ocitv.-measurable" (at level 2, format "R .-ocitv.-measurable"). -Reserved Notation "R .-open" (at level 1, format "R .-open"). -Reserved Notation "R .-open.-measurable" - (at level 2, format "R .-open.-measurable"). Notation right_continuous f := (forall x, f%function @ at_right x --> f%function x). @@ -167,11 +161,11 @@ Definition ocitv := [set `]x.1, x.2]%classic | x in [set: R * R]]. Lemma is_ocitv a b : ocitv `]a, b]%classic. Proof. by exists (a, b); split => //=; rewrite in_itv/= andbT. Qed. -Hint Extern 0 (ocitv _) => solve [apply: is_ocitv] : core. +#[local] Hint Extern 0 (ocitv _) => solve [apply: is_ocitv] : core. Lemma ocitv0 : ocitv set0. Proof. by exists (1, 0); rewrite //= set_itv_ge ?bnd_simp//= ltr10. Qed. -Hint Resolve ocitv0 : core. +#[local] Hint Resolve ocitv0 : core. Lemma ocitvP X : ocitv X <-> X = set0 \/ exists2 x, x.1 < x.2 & X = `]x.1, x.2]%classic. Proof. @@ -234,41 +228,40 @@ Context {R : realType}. Definition measurableTypeR := g_sigma_algebraType (@ocitv R). -Definition lebesgue_display : measure_display := (@ocitv R).-sigma. +Let ocitv_lebesgue_display : measure_display := (@ocitv R).-sigma. -Definition measurableR : set_system R := (@ocitv R).-sigma.-measurable. +Let measurableR : set_system R := (@ocitv R).-sigma.-measurable. -HB.instance Definition _ : Measurable lebesgue_display measurableTypeR := +HB.instance Definition _ : Measurable ocitv_lebesgue_display measurableTypeR := Measurable.on measurableTypeR. (* Presumably it is safe to use NFI here because morally R is unique and nothing else can be used here *) #[non_forgetful_inheritance] HB.instance Definition _ := Measurable.copy R measurableTypeR. -Lemma measurable_set1 (r : R) : measurable [set r]. +Lemma ocitv_measurable_set1 (r : R) : measurable [set r]. Proof. rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _. by apply: sub_sigma_algebra; exact/is_ocitv. Qed. -#[local] Hint Resolve measurable_set1 : core. +#[local] Hint Resolve ocitv_measurable_set1 : core. -Lemma measurable_itv (i : interval R) : measurable [set` i]. +Lemma ocitv_measurable_itv (i : interval R) : measurable [set` i]. Proof. have moc (a b : R) : measurable `]a, b]. - by apply: sub_sigma_algebra; apply: is_ocitv. + by apply: sub_sigma_algebra; exact: is_ocitv. have mopoo (x : R) : measurable `]x, +oo[. by rewrite itv_bndy_bigcup_BRight; exact: bigcup_measurable. have mnooc (x : R) : measurable `]-oo, x]. by rewrite -setCitvr; exact/measurableC. -have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b. - by rewrite setDitv1r. +have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b by rewrite setDitv1r. have moo (a b : R) : measurable `]a, b[ by rewrite ooE; exact: measurableD. have mcc (a b : R) : measurable `[a, b]. case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge. - by rewrite -setU_1itvob//; apply/measurableU. + by rewrite -setU_1itvob//; exact/measurableU. have mco (a b : R) : measurable `[a, b[. case: (boolP (a < b)) => ab; last by rewrite set_itv_ge. - by rewrite -setU_1itvob//; apply/measurableU. + by rewrite -setU_1itvob//; exact/measurableU. have oooE (b : R) : `]-oo, b[%classic = `]-oo, b] `\ b. by rewrite setDitv1r. case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge. @@ -279,13 +272,6 @@ Qed. End measurableRocitv. Arguments measurableTypeR : clear implicits. -#[global] -Hint Extern 0 (measurable (_ @^-1` [set _])) => - solve [apply: measurable_funPTI; exact: measurable_set1] : core. -#[global] -Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. -#[global] -Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. End MeasurableRocitv. Module RGenOInfty. @@ -317,7 +303,8 @@ Proof. rewrite eqEsubset; split => A. apply: smallest_sub; first exact: smallest_sigma_algebra. by move=> I [x _ <-]; exact: measurable_itv_bounded. -by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. +apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. +exact: MeasurableRocitv.ocitv_measurable_itv. Qed. End rgenoinfty. @@ -353,7 +340,8 @@ Proof. rewrite eqEsubset; split => A. apply: smallest_sub; first exact: smallest_sigma_algebra. by move=> I [x _ <-]; exact: measurable_itv_bounded. -by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. +apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. +exact: MeasurableRocitv.ocitv_measurable_itv. Qed. End rgeninftyo. @@ -388,13 +376,14 @@ Proof. rewrite eqEsubset; split => A. apply: smallest_sub; first exact: smallest_sigma_algebra. by move=> I [x _ <-]; exact: measurable_itv_bounded. -by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. +apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]]. +exact: MeasurableRocitv.ocitv_measurable_itv. Qed. End rgencinfty. End RGenCInfty. -Module RGenOpens. +Module RGenItvoo. Section rgenopens. Context (R : realType). Implicit Types x y z : R. @@ -437,11 +426,12 @@ Proof. rewrite eqEsubset; split => A. apply: smallest_sub; first exact: smallest_sigma_algebra. by move=> I [x _ <-]; exact: measurable_itv_bounded. -by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x [y ->]]]. +apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x [y ->]]]. +exact: MeasurableRocitv.ocitv_measurable_itv. Qed. End rgenopens. -End RGenOpens. +End RGenItvoo. Module RGenOpenSets. Section rgenopensets. @@ -451,127 +441,49 @@ Import MeasurableRocitv. Lemma measurableE : (@ocitv R).-sigma.-measurable = open.-sigma.-measurable. Proof. -rewrite eqEsubset; split; [rewrite RGenOpens.measurableE|]; +rewrite eqEsubset; split; [rewrite RGenItvoo.measurableE|]; apply: sigma_algebra_subl=> U. -- by rewrite /RGenOpens.G/= => -[a [b ->]]; exact: sub_sigma_algebra. +- by rewrite /RGenItvoo.G/= => -[a [b ->]]; exact: sub_sigma_algebra. - move=> oU; rewrite (open_disjoint_itv_bigcup oU). apply: sigma_algebra_bigcup => k. have /is_intervalP -> := @open_disjoint_itv_is_interval _ U oU k. - exact: measurable_itv. + exact: ocitv_measurable_itv. Qed. End rgenopensets. End RGenOpenSets. -(* Should be moved to a more general file *) -Section open. -Context {R : realType} {N : normedModType R}. - -Definition open_type : Type := N. - -HB.instance Definition _ := Pointed.on open_type. - -Let measurable : set_system N := @measurable _ (g_sigma_algebraType (@open N)). - -Let measurable0 : measurable set0. Proof. exact: measurable0. Qed. - -Let measurableC A : measurable A -> measurable (~` A). -Proof. by move=> /measurableC. Qed. - -Let measurable_bigcup (F : (set N)^nat) : (forall i, measurable (F i)) -> - measurable (\bigcup_i (F i)). -Proof. move=> mF; exact: bigcupT_measurable. Qed. - -HB.instance Definition _ := - @isMeasurable.Build (sigma_display (@open N)) - open_type measurable measurable0 measurableC measurable_bigcup. - -End open. - -Notation "N .-open" := (sigma_display (@open N)) : measure_display_scope. -Notation "N .-open.-measurable" := (measurable : set_system (@open_type _ N)) : - classical_set_scope. - -Module MeasurableNormedModuleOpen. -Section measurableOpen. -Context {R : realType} {N : normedModType R}. -Import numFieldNormedType.Exports. - -Definition measurableTypeNormedModule := g_sigma_algebraType (@open N). - -Definition borel_display : measure_display := N.-open. - -Definition measurableNormedModule : set_system N := N.-open.-measurable. - -HB.instance Definition _ : Measurable borel_display measurableTypeNormedModule := - Measurable.on measurableTypeNormedModule. -(* Presumably it is safe to use NFI here because morally R is unique - and nothing else can be used here *) -#[non_forgetful_inheritance] -HB.instance Definition _ := Measurable.copy N measurableTypeNormedModule. - -Lemma measurable_set1 (x : N) : measurable [set x]. -Proof. -rewrite set1_bigcap_ball; apply: bigcap_measurable => // k _. -apply: sub_sigma_algebra; exact: ball_open. -Qed. -#[local] Hint Resolve measurable_set1 : core. - -Lemma measurable_ball_norm (x : N) e : measurable (ball x e). -Proof. by apply: (sub_sigma_algebra (ball_open _ _)). Qed. - -End measurableOpen. -Arguments measurableTypeNormedModule : clear implicits. -#[global] -Hint Extern 0 (measurable (_ @^-1` [set _])) => - solve [apply: measurable_funPTI; exact: measurable_set1] : core. -#[global] -Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. - -Lemma measurable_funP1 {d} {aT : measurableType d} {rT : realType} - {nT : normedModType rT} (f : {mfun aT >-> nT}) D (z : nT) : - measurable D -> measurable (D `&` f @^-1` [set z]). -Proof. by move=> /(measurable_funP f); exact. Qed. -#[deprecated(since="mathcomp-analysis 1.13.0", use=measurable_funP1)] -Notation measurable_sfun_inP := measurable_funP1 (only parsing). -#[global] Hint Extern 0 (measurable (_ `&` _ @^-1` [set _])) => - solve [apply: measurable_funP1; assumption] : core. - +Module MeasurableROpen. Section measurableReal. Context {R : realType}. Import numFieldNormedType.Exports. -Definition measurableTypeR := @measurableTypeNormedModule R R. +Import MeasurableNormedModule. Definition lebesgue_display : measure_display := @borel_display R R. -Definition measurableR := @measurableNormedModule R R. - -(* Shouldn't be needing ideally... *) -HB.instance Definition _ := Measurable.copy R measurableTypeR. +#[non_forgetful_inheritance] +HB.instance Definition _ := Measurable.copy R (g_sigma_algebraType (@open R)). Lemma measurable_itv (i : interval R) : measurable [set` i]. Proof. -have := MeasurableRocitv.measurable_itv i. -rewrite /MeasurableRocitv.lebesgue_display. -by rewrite RGenOpenSets.measurableE. +by rewrite -RGenOpenSets.measurableE; exact: MeasurableRocitv.ocitv_measurable_itv. Qed. End measurableReal. -Arguments measurableTypeR : clear implicits. -#[global] -Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. +#[global] Hint Extern 0 (measurable [set` _]) => exact: measurable_itv : core. -End MeasurableNormedModuleOpen. +End MeasurableROpen. Module MeasurableR. Export numFieldNormedType.Exports. -Export MeasurableNormedModuleOpen. +Export MeasurableNormedModule. +Export MeasurableROpen. End MeasurableR. Section ocitv_measure. Import MeasurableR. -Context {R : realType} (mu : measure (measurableTypeR R) R). +Context {R : realType} (mu : {measure set R -> \bar R}). Definition ocitv_measure : set (MeasurableRocitv.measurableTypeR R) -> \bar R := mu. @@ -807,7 +719,7 @@ HB.instance Definition _ (f : cumulative R R) := (wlength_ge0 f) (wlength_semi_additive f). -Hint Extern 0 (measurable _) => solve [apply: is_ocitv] : core. +(*Hint Extern 0 (measurable _) => solve [apply: is_ocitv] : core.*) Lemma cumulative_content_sub_fsum (f : cumulative R R) (D : {fset nat}) a0 b0 (a b : nat -> R) : (forall i, i \in D -> a i <= b i) -> @@ -819,7 +731,8 @@ move=> Dab h; have [ab|ab] := leP a0 b0; last first. by rewrite subr_le0 cumulative_is_nondecreasing// ltW. rewrite big_seq sumr_ge0// => i iD. by rewrite subr_ge0 cumulative_is_nondecreasing// Dab. -have mab k : [set` D] k -> R.-ocitv.-measurable `]a k, b k]%classic by []. +have mab k : [set` D] k -> R.-ocitv.-measurable `]a k, b k]%classic. + by move=> ?; exact: is_ocitv. move: h; rewrite -bigcup_fset. move/(content_sub_fsum (wlength f) (finite_fset D) mab (is_ocitv a0 b0)) => /=. rewrite wlength_itv_bnd// -lee_fin => /le_trans; apply. @@ -907,8 +820,8 @@ Proof. exists (fun k => `](- k%:R), k%:R]%classic). apply/esym; rewrite -subTset => /= x _ /=. by exists (Num.bound x); rewrite //= in_itv/= ltrNl ltrNbound ltW// ltr_bound. -move=> k; split => //; rewrite wlength_itv /= -EFinB. -by case: ifP; rewrite ltey. +move=> k; split; first exact: is_ocitv. +by rewrite wlength_itv /= -EFinB; case: ifP; rewrite ltey. Qed. Definition ocitv_lebesgue_stieltjes_measure (f : cumulative R R) := @@ -979,7 +892,7 @@ by rewrite RGenOpenSets.measurableE. Qed. Lemma lebesgue_stieltjes_measure_unique - (mu : {measure set (measurableTypeR R) -> \bar R}) : + (mu : {measure set ((*measurableTypeR*) R) -> \bar R}) : (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) -> forall A : set R, measurable A -> lebesgue_stieltjes_measure f A = mu A. Proof. diff --git a/theories/real_measure/measurable_realfun.v b/theories/real_measure/measurable_realfun.v index 90857b09cf..e8cf442a54 100644 --- a/theories/real_measure/measurable_realfun.v +++ b/theories/real_measure/measurable_realfun.v @@ -7,7 +7,7 @@ From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import reals ereal topology numfun normedtype sequences measure realfun exp. -From mathcomp Require Import lebesgue_stieltjes_measure. +From mathcomp Require Import lebesgue_stieltjes_measure normedtype_measure. (**md**************************************************************************) (* # Measurable Functions over $\mathbb{R}$ and $\overline{\mathbb{R}}$ *) @@ -186,7 +186,7 @@ End puncture_ereal_itv. Section salgebra_R_ssets. Context {R : realType}. -HB.instance Definition _ := (ereal_isMeasurable (R.-ocitv.-measurable)). +HB.instance Definition _ := ereal_isMeasurable (@open R). (* NB: Until we dropped support for Coq 8.12, we were using HB.instance (\bar (Real.sort R)) (ereal_isMeasurable (@measurable (@itvs_semiRingOfSets R))). @@ -205,7 +205,7 @@ Import MeasurableR. Lemma measurable_image_EFin (A : set R) : measurable A -> measurable (EFin @` A). Proof. -move=> mA; exists A; first by rewrite RGenOpenSets.measurableE. +move=> mA; exists A => //. by exists set0; [constructor|rewrite setU0]. Qed. @@ -224,7 +224,7 @@ Let emeasurable_itv_bndy b (y : \bar R) : measurable [set` Interval (BSide b y) +oo%O]. Proof. move: y => [y| |]. -- exists [set` Interval (BSide b y) +oo%O]; first by []. +- exists [set` Interval (BSide b y) +oo%O] => //. by exists [set +oo%E]; [constructor|rewrite -punct_eitv_bndy]. - by case: b; rewrite ?itv_oyy ?itv_cyy. - case: b; first by rewrite itv_cNyy. @@ -249,24 +249,24 @@ Lemma measurable_image_fine (X : set \bar R) : measurable X -> Proof. case => Y mY [X' [ | <-{X} | <-{X} | <-{X} ]]. - rewrite setU0 => <-{X}. - rewrite [X in measurable X](_ : _ = Y) -?RGenOpenSets.measurableE// predeqE => r; split. + rewrite [X in measurable X](_ : _ = Y)// predeqE => r; split. by move=> [x [[x' Yx' <-{x}/= _ <-//]]]. by move=> Yr; exists r%:E; split => [|[]//]; exists r. -- rewrite [X in measurable X](_ : _ = Y) -?RGenOpenSets.measurableE// predeqE => r; split. +- rewrite [X in measurable X](_ : _ = Y)// predeqE => r; split. move=> [x [[[x' Yx' <- _ <-//]|]]]. by move=> <-; rewrite not_orP => -[]/(_ erefl). by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. -- rewrite [X in measurable X](_ : _ = Y) -?RGenOpenSets.measurableE// predeqE => r; split. +- rewrite [X in measurable X](_ : _ = Y)// predeqE => r; split. move=> [x [[[x' Yx' <-{x} _ <-//]|]]]. by move=> ->; rewrite not_orP => -[_]/(_ erefl). by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. -- rewrite [X in measurable X](_ : _ = Y) -?RGenOpenSets.measurableE// predeqE => r; split. +- rewrite [X in measurable X](_ : _ = Y)// predeqE => r; split. by rewrite setDUl setDv setU0 => -[_ [[x' Yx' <-]] _ <-]. by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. Qed. Lemma measurable_ball (x : R) e : measurable (ball x e). -Proof. by rewrite ball_itv -?RGenOpenSets.measurableE//. Qed. +Proof. by rewrite ball_itv. Qed. Lemma measurable_closed_ball (x : R) r : measurable (closed_ball x r). Proof. @@ -444,9 +444,9 @@ rewrite eset1y; apply: bigcapT_measurable => i. by apply: sub_sigma_algebra; exists i%:R. Qed. -Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable. +Lemma measurableE : emeasurable (@open R) = G.-sigma.-measurable. Proof. -apply/seteqP; split; last first. +rewrite /emeasurable -RGenOpenSets.measurableE; apply/seteqP; split; last first. apply: smallest_sub. split; first exact: emeasurable0. by move=> *; rewrite setTD; exact: emeasurableC. @@ -497,9 +497,9 @@ apply: bigcap_measurable => // j _; rewrite -setCitvr; apply: measurableC. by apply: sub_sigma_algebra; exists (i%:R + j.+1%:R^-1)%R. Qed. -Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable. +Lemma measurableE : emeasurable (@open R) = G.-sigma.-measurable. Proof. -apply/seteqP; split; last first. +rewrite /emeasurable -RGenOpenSets.measurableE; apply/seteqP; split; last first. apply: smallest_sub. split; first exact: emeasurable0. by move=> *; rewrite setTD; exact: emeasurableC. @@ -533,7 +533,7 @@ Context (R : realType). Definition G := [set A : set \bar R | exists r, A = `]-oo, r%:E[%classic]. -Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable. +Lemma measurableE : emeasurable (@open R) = G.-sigma.-measurable. Proof. rewrite ErealGenCInfty.measurableE eqEsubset; split => A. apply: smallest_sub; first exact: smallest_sigma_algebra. @@ -551,7 +551,7 @@ End ErealGenInftyO. Lemma is_interval_measurable (R : realType) (I : set R) : is_interval I -> measurable I. -Proof. by move/is_intervalP => ->; rewrite -?RGenOpenSets.measurableE//. Qed. +Proof. by move/is_intervalP => ->. Qed. Section coutinuous_measurable. Context {R : realType}. @@ -582,8 +582,8 @@ Lemma subspace_continuous_measurable_fun (D : set R) (f : subspace D -> R) : measurable D -> continuous f -> measurable_fun D f. Proof. move=> mD /continuousP cf. -rewrite /measurable_fun -?RGenOpenSets.measurableE. -apply: (measurability _ (RGenOpens.measurableE R)). +rewrite /measurable_fun -!RGenOpenSets.measurableE. +apply: (measurability _ (RGenItvoo.measurableE R)). move=> _ [_ [a [b ->] <-]]. rewrite RGenOpenSets.measurableE. apply: open_measurable_subspace => //. @@ -608,7 +608,8 @@ End coutinuous_measurable. Lemma lower_semicontinuous_measurable {R : realType} (f : R -> \bar R) : lower_semicontinuous f -> measurable_fun setT f. Proof. -move=> scif; apply: (measurability _ (ErealGenOInfty.measurableE R)). +move=> scif. +apply: (measurability _ (ErealGenOInfty.measurableE R)). move=> /= _ [_ [a ->]] <-; apply: measurableI => //; apply: open_measurable. by rewrite preimage_itvoy; move/lower_semicontinuousP : scif; exact. Qed. @@ -635,7 +636,7 @@ have [x0|x0] := leP 0 x; last first. rewrite [X in measurable X](_ : _ = setT)// predeqE => r. by split => // _; rewrite /= in_itv /= andbT (lt_le_trans x0). rewrite [X in measurable X](_ : _ = `]-oo, (- x)[ `|` `]x, +oo[); last first. - exact: measurableU. + by apply: measurableU => //; exact: MeasurableRocitv.ocitv_measurable_itv. rewrite predeqE => r; split => [|[|]]; rewrite preimage_itv ?in_itv ?andbT/=. - (have [r0|r0] := leP 0 r; [rewrite ger0_norm|rewrite ltr0_norm]) => // xr; rewrite 2!in_itv/=. @@ -1238,7 +1239,7 @@ Lemma EFin_measurable (D : set R) : measurable_fun D EFin. Proof. move=> mD; apply: (measurability _ (ErealGenOInfty.measurableE R)) => //. move=> /= _ [_ [x ->]] <-; apply: measurableI => //. -by rewrite -RGenOpenSets.measurableE preimage_itvoy EFin_itv. +by rewrite preimage_itvoy EFin_itv. Qed. Lemma abse_measurable (D : set (\bar R)) : measurable_fun D abse. @@ -1249,14 +1250,12 @@ rewrite [X in _ @^-1` X](punct_eitv_bndy _ x) preimage_setU setIUr. apply: measurableU; last first. by rewrite preimage_abse_pinfty; apply: measurableI => //; exact: measurableU. apply: measurableI => //; exists (normr @^-1` `]x, +oo[%classic). - rewrite -[X in measurable X]setTI. - rewrite RGenOpenSets.measurableE. - exact: normr_measurable. + by rewrite -[X in measurable X]setTI; exact: normr_measurable. exists set0; first by constructor. rewrite setU0 predeqE => -[y| |]; split => /= => -[r]; rewrite ?/= /= ?in_itv /= ?andbT => xr//. + by move=> [ry]; exists `|y| => //=; rewrite in_itv/= andbT -ry. - + by move=> [ry]; exists y => //=; rewrite /= in_itv/= andbT -ry. + + by move=> [ry]; exists y => //=; rewrite in_itv/= andbT -ry. Qed. Lemma oppe_measurable (D : set (\bar R)) : @@ -1284,7 +1283,6 @@ Proof. split=> [mf mD A mA|]; last by move=> mg; exact: measurableT_comp. rewrite [X in measurable X](_ : _ = D `&` (EFin \o g) @^-1` (EFin @` A)); last first. apply: mf => //; exists A => //. - by rewrite RGenOpenSets.measurableE//. by exists set0; [constructor|rewrite setU0]. congr (_ `&` _);rewrite eqEsubset; split=> [|? []/= _ /[swap] -[->//]]. by move=> ? ?; exact: preimage_image. diff --git a/theories/real_measure/normedtype_measure.v b/theories/real_measure/normedtype_measure.v new file mode 100644 index 0000000000..d5245fb9e8 --- /dev/null +++ b/theories/real_measure/normedtype_measure.v @@ -0,0 +1,116 @@ +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import boot order algebra. +From mathcomp Require Import boolp classical_sets. +From mathcomp Require Import topology normedtype measure. + +(**md**************************************************************************) +(* # Sigma-algebra for normed modules *) +(* *) +(* `open_type N` *) +(* : alias for `N : normedModType R` *) +(* *) +(* `N .-open.-measurable` *) +(* : the set of measurable sets *) +(* *) +(* `MeasurableNormedModule` *) +(* : module that contains the definition of the sigma-algebra for normed *) +(* : modules *) +(* *) +(******************************************************************************) + +Reserved Notation "R .-open" (at level 1, format "R .-open"). +Reserved Notation "R .-open.-measurable" + (at level 2, format "R .-open.-measurable"). + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Section open. +Context {R : numFieldType} {N : normedModType R}. + +(* TODO: borel_type? *) +Definition open_type : Type := N. + +HB.instance Definition _ := Pointed.on open_type. + +Let measurable : set_system N := @measurable _ (g_sigma_algebraType (@open N)). + +Let measurable0 : measurable set0. Proof. exact: measurable0. Qed. + +Let measurableC A : measurable A -> measurable (~` A). +Proof. by move=> /measurableC. Qed. + +Let measurable_bigcup (F : (set N)^nat) : (forall i, measurable (F i)) -> + measurable (\bigcup_i (F i)). +Proof. move=> mF; exact: bigcupT_measurable. Qed. + +HB.instance Definition _ := + @isMeasurable.Build (sigma_display (@open N)) + open_type measurable measurable0 measurableC measurable_bigcup. + +End open. + +Notation "N .-open" := (sigma_display (@open N)) : measure_display_scope. +Notation "N .-open.-measurable" := (measurable : set_system (@open_type _ N)) : + classical_set_scope. + +Module MeasurableNormedModuleOpen. +Section measurableOpen. +Context {R : archiRealFieldType} {N : normedModType R}. +Import numFieldNormedType.Exports. + +Let measurableTypeNormedModule := g_sigma_algebraType (@open N). + +Definition borel_display : measure_display := N.-open. + +Let measurableNormedModule : set_system N := N.-open.-measurable. + +HB.instance Definition _ : Measurable borel_display measurableTypeNormedModule := + Measurable.on measurableTypeNormedModule. +(* Presumably it is safe to use NFI here because morally R is unique + and nothing else can be used here *) +#[non_forgetful_inheritance] +HB.instance Definition _ := Measurable.copy N measurableTypeNormedModule. + +Lemma measurable_set1 (x : N) : measurable [set x]. +Proof. +rewrite set1_bigcap_ball; apply: bigcap_measurable => // k _. +by apply: sub_sigma_algebra; exact: ball_open. +Qed. +#[local] Hint Resolve measurable_set1 : core. + +Lemma measurable_ball_norm (x : N) e : measurable (ball x e). +Proof. exact: (sub_sigma_algebra (ball_open _ _)). Qed. + +End measurableOpen. + +Lemma measurable_funP1 {d} {aT : measurableType d} {rT : archiRealFieldType} + {nT : normedModType rT} (f : {mfun aT >-> nT}) D (z : nT) : + measurable D -> measurable (D `&` f @^-1` [set z]). +Proof. +by move=> /(measurable_funP f); apply => //; exact: measurable_set1. +Qed. + +(* NB: really used, e.g., in simple_functions.v *) +#[global] Hint Extern 0 (measurable (_ @^-1` [set _])) => + solve [apply: measurable_funPTI; exact: measurable_set1] : core. + +(* NB: really used, e.g., in radon_nikodym.v *) +#[global] Hint Extern 0 (measurable (_ `&` _ @^-1` [set _])) => + solve [apply: measurable_funP1; assumption] : core. + +(* NB: really used, e.g., in realfun.v *) +#[global] Hint Extern 0 (measurable [set _]) => + solve [apply: measurable_set1] : core. + +End MeasurableNormedModuleOpen. + +Module MeasurableNormedModule. +Export numFieldNormedType.Exports. +Export MeasurableNormedModuleOpen. +End MeasurableNormedModule. From 5e2fb8d560d8442825c05844dcc839f4c44bccbf Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 12 Nov 2026 21:58:23 +0900 Subject: [PATCH 6/8] changelog --- CHANGELOG_UNRELEASED.md | 28 ++++++++++++++++++- _CoqProject | 2 +- theories/Make | 2 +- theories/real_measure/lebesgue_measure.v | 3 +- .../real_measure/lebesgue_stieltjes_measure.v | 6 ++-- theories/real_measure/measurable_realfun.v | 6 ++-- ...type_measure.v => normedtype_measurable.v} | 2 +- theories/real_measure/real_measure.v | 1 + 8 files changed, 37 insertions(+), 13 deletions(-) rename theories/real_measure/{normedtype_measure.v => normedtype_measurable.v} (98%) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d7f0405803..b0daa261f1 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -10,6 +10,16 @@ `pownMexpr_cvgn0` + instance `is_derive1_powRl` +- in `metric_structure.v`: + + lemma `set1_bigcap_ball` + +- file `normedtype_measurable.v` + + module `MeasurableNormedModuleOpen` + * definition `borel_display` + * lemma `measurable_set1` + * lemma `measurable_ball_norm` + * lemma ` measurable_funP1` + ### Changed - in `lebesgue_integral_nonneg.v`, generalized and deprecated: @@ -26,10 +36,22 @@ `derivable_oo_LRcontinuousN`, `derivable_oo_LRcontinuous_shift`, `derivable_oo_LRcontinuousS` -### Changed +- from `lebesgue_stieltjes_measure.v` to (new) `normedtyped_measurable.v`: + + move definition `open_type` + + move notations `.-open`, `.-open.-measurable` + +- in `lebesgue_stieltjes_measure.v`: + + sigma-algebra for `\bar R` now uses open sets instead of octiv ### Renamed +- in `lebesgue_stieltjes_measure.v`: + + `RGenOpens` -> `RGenItvoo` + + `MeasurableRocitv.measurable_set1` -> `MeasurableRocitv.ocitv_measurable_set1` + + `MeasurableRocitv.measurable_itv` -> `MeasurableRocitv.ocitv_measurable_itv` + +- in `lebesgue_stieltjes_measure.v`: + ### Generalized - in `lebesgue_integral_nonneg.v`: @@ -39,6 +61,10 @@ ### Removed +- in `lebesgue_stieltjes_measure.v`: + + definition `MeasurableRocitv.lebesgue_display` + + definition `MeasurableRocitv.measurableR` + ### Infrastructure ### Misc diff --git a/_CoqProject b/_CoqProject index e3cf7974b9..20e376835e 100644 --- a/_CoqProject +++ b/_CoqProject @@ -116,7 +116,7 @@ theories/measure_theory/measurable_function.v theories/measure_theory/signed_measure.v theories/measure_theory/measure.v -theories/real_measure/normedtype_measure.v +theories/real_measure/normedtype_measurable.v theories/real_measure/lebesgue_stieltjes_measure.v theories/real_measure/lebesgue_measure.v theories/real_measure/measurable_realfun.v diff --git a/theories/Make b/theories/Make index 3120733ea3..b228cf3b83 100644 --- a/theories/Make +++ b/theories/Make @@ -83,7 +83,7 @@ measure_theory/measurable_function.v measure_theory/signed_measure.v measure_theory/measure.v -real_measure/normedtype_measure.v +real_measure/normedtype_measurable.v real_measure/lebesgue_stieltjes_measure.v real_measure/lebesgue_measure.v real_measure/measurable_realfun.v diff --git a/theories/real_measure/lebesgue_measure.v b/theories/real_measure/lebesgue_measure.v index 9102eec35a..110626a7af 100644 --- a/theories/real_measure/lebesgue_measure.v +++ b/theories/real_measure/lebesgue_measure.v @@ -8,7 +8,8 @@ From mathcomp Require Import boolp classical_sets functions cardinality fsbigop reals. From mathcomp Require Import topology ereal numfun normedtype sequences esum measure. -From mathcomp Require Export normedtype_measure lebesgue_stieltjes_measure measurable_realfun. +From mathcomp Require Export normedtype_measurable lebesgue_stieltjes_measure + measurable_realfun. (**md**************************************************************************) (* # Lebesgue Measure *) diff --git a/theories/real_measure/lebesgue_stieltjes_measure.v b/theories/real_measure/lebesgue_stieltjes_measure.v index dea64c85ea..2baa90cfc8 100644 --- a/theories/real_measure/lebesgue_stieltjes_measure.v +++ b/theories/real_measure/lebesgue_stieltjes_measure.v @@ -6,7 +6,7 @@ From mathcomp Require Import interval_inference archimedean. From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets fsbigop cardinality. From mathcomp Require Import reals ereal topology normedtype sequences esum - measure realfun normedtype_measure. + measure realfun normedtype_measurable. (**md**************************************************************************) (* # Lebesgue Stieltjes Measure *) @@ -719,8 +719,6 @@ HB.instance Definition _ (f : cumulative R R) := (wlength_ge0 f) (wlength_semi_additive f). -(*Hint Extern 0 (measurable _) => solve [apply: is_ocitv] : core.*) - Lemma cumulative_content_sub_fsum (f : cumulative R R) (D : {fset nat}) a0 b0 (a b : nat -> R) : (forall i, i \in D -> a i <= b i) -> `]a0, b0] `<=` \big[setU/set0]_(i <- D) `]a i, b i]%classic -> @@ -892,7 +890,7 @@ by rewrite RGenOpenSets.measurableE. Qed. Lemma lebesgue_stieltjes_measure_unique - (mu : {measure set ((*measurableTypeR*) R) -> \bar R}) : + (mu : {measure set R -> \bar R}) : (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) -> forall A : set R, measurable A -> lebesgue_stieltjes_measure f A = mu A. Proof. diff --git a/theories/real_measure/measurable_realfun.v b/theories/real_measure/measurable_realfun.v index e8cf442a54..6534efc8f7 100644 --- a/theories/real_measure/measurable_realfun.v +++ b/theories/real_measure/measurable_realfun.v @@ -7,7 +7,7 @@ From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import reals ereal topology numfun normedtype sequences measure realfun exp. -From mathcomp Require Import lebesgue_stieltjes_measure normedtype_measure. +From mathcomp Require Import lebesgue_stieltjes_measure normedtype_measurable. (**md**************************************************************************) (* # Measurable Functions over $\mathbb{R}$ and $\overline{\mathbb{R}}$ *) @@ -45,7 +45,6 @@ From mathcomp Require Import lebesgue_stieltjes_measure normedtype_measure. (* ``` *) (******************************************************************************) -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -608,8 +607,7 @@ End coutinuous_measurable. Lemma lower_semicontinuous_measurable {R : realType} (f : R -> \bar R) : lower_semicontinuous f -> measurable_fun setT f. Proof. -move=> scif. -apply: (measurability _ (ErealGenOInfty.measurableE R)). +move=> scif; apply: (measurability _ (ErealGenOInfty.measurableE R)). move=> /= _ [_ [a ->]] <-; apply: measurableI => //; apply: open_measurable. by rewrite preimage_itvoy; move/lower_semicontinuousP : scif; exact. Qed. diff --git a/theories/real_measure/normedtype_measure.v b/theories/real_measure/normedtype_measurable.v similarity index 98% rename from theories/real_measure/normedtype_measure.v rename to theories/real_measure/normedtype_measurable.v index d5245fb9e8..a30c1fd2fb 100644 --- a/theories/real_measure/normedtype_measure.v +++ b/theories/real_measure/normedtype_measurable.v @@ -14,7 +14,7 @@ From mathcomp Require Import topology normedtype measure. (* : the set of measurable sets *) (* *) (* `MeasurableNormedModule` *) -(* : module that contains the definition of the sigma-algebra for normed *) +(* : module that contains the definition of a sigma-algebra for normed *) (* : modules *) (* *) (******************************************************************************) diff --git a/theories/real_measure/real_measure.v b/theories/real_measure/real_measure.v index 44582f4c6a..480fac9700 100644 --- a/theories/real_measure/real_measure.v +++ b/theories/real_measure/real_measure.v @@ -1,4 +1,5 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Export normedtype_measurable. From mathcomp Require Export lebesgue_stieltjes_measure. From mathcomp Require Export lebesgue_measure. From mathcomp Require Export measurable_realfun. From 893c16237efbc001c28b103bfafae8c992f34a81 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 12 Nov 2026 22:00:18 +0900 Subject: [PATCH 7/8] fix changelog --- CHANGELOG_UNRELEASED.md | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b0daa261f1..efa7371a0d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -10,6 +10,21 @@ `pownMexpr_cvgn0` + instance `is_derive1_powRl` +- in `function_spaces.v`: + + lemma `within_continuous_big` + +- in `nat_topology.v`: + + lemma `near_infty_after` + +- in `num_topology.v`: + + lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, + `at_left_shift`, `at_right_shift` + +- in `realfun.v`: + + lemmas `derivable_oo_LRcontinuousZ`, `derivable_oo_LRcontinuousD`, + `derivable_oo_LRcontinuousN`, `derivable_oo_LRcontinuous_shift`, + `derivable_oo_LRcontinuousS` + - in `metric_structure.v`: + lemma `set1_bigcap_ball` @@ -24,17 +39,6 @@ - in `lebesgue_integral_nonneg.v`, generalized and deprecated: + lemma `ge0_integralZl_EFin` (no condition on `k`) -- in file `function_spaces.v`, - + new lemma `within_continuous_big`. -- in file `nat_topology.v`, - + new lemma `near_infty_after`. -- in file `num_topology.v`, - + new lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`, - `at_left_shift`, and `at_right_shift`. -- in `realfun.v`: - + lemmas `derivable_oo_LRcontinuousZ`, `derivable_oo_LRcontinuousD`, - `derivable_oo_LRcontinuousN`, `derivable_oo_LRcontinuous_shift`, - `derivable_oo_LRcontinuousS` - from `lebesgue_stieltjes_measure.v` to (new) `normedtyped_measurable.v`: + move definition `open_type` From 9661ebebfab844f461ef72b50ad926ee38e74a59 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 12 Nov 2026 23:00:35 +0900 Subject: [PATCH 8/8] improvement? --- CHANGELOG_UNRELEASED.md | 3 +- theories/real_measure/normedtype_measurable.v | 42 +++++++------------ theories/topology_theory/metric_structure.v | 8 ++-- 3 files changed, 22 insertions(+), 31 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index efa7371a0d..ab374cb110 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -29,8 +29,9 @@ + lemma `set1_bigcap_ball` - file `normedtype_measurable.v` + + definition `borel_type` + + definition `borel_display` + module `MeasurableNormedModuleOpen` - * definition `borel_display` * lemma `measurable_set1` * lemma `measurable_ball_norm` * lemma ` measurable_funP1` diff --git a/theories/real_measure/normedtype_measurable.v b/theories/real_measure/normedtype_measurable.v index a30c1fd2fb..ed642432b8 100644 --- a/theories/real_measure/normedtype_measurable.v +++ b/theories/real_measure/normedtype_measurable.v @@ -7,9 +7,12 @@ From mathcomp Require Import topology normedtype measure. (**md**************************************************************************) (* # Sigma-algebra for normed modules *) (* *) -(* `open_type N` *) +(* `borel_type N` *) (* : alias for `N : normedModType R` *) (* *) +(* `borel_display N` *) +(* : display for `borel_type N` *) +(* *) (* `N .-open.-measurable` *) (* : the set of measurable sets *) (* *) @@ -33,47 +36,34 @@ Local Open Scope ring_scope. Section open. Context {R : numFieldType} {N : normedModType R}. -(* TODO: borel_type? *) -Definition open_type : Type := N. - -HB.instance Definition _ := Pointed.on open_type. - -Let measurable : set_system N := @measurable _ (g_sigma_algebraType (@open N)). - -Let measurable0 : measurable set0. Proof. exact: measurable0. Qed. +Definition borel_type : Type := N. -Let measurableC A : measurable A -> measurable (~` A). -Proof. by move=> /measurableC. Qed. +Definition borel_display : measure_display := sigma_display (@open N). -Let measurable_bigcup (F : (set N)^nat) : (forall i, measurable (F i)) -> - measurable (\bigcup_i (F i)). -Proof. move=> mF; exact: bigcupT_measurable. Qed. +(*HB.instance Definition _ := Pointed.on borel_type.*) HB.instance Definition _ := - @isMeasurable.Build (sigma_display (@open N)) - open_type measurable measurable0 measurableC measurable_bigcup. + Measurable.copy borel_type (g_sigma_algebraType (@open N)). End open. +Arguments borel_type {R} N. +Arguments borel_display {R} N. -Notation "N .-open" := (sigma_display (@open N)) : measure_display_scope. -Notation "N .-open.-measurable" := (measurable : set_system (@open_type _ N)) : +Notation "N .-open" := (borel_display N) : measure_display_scope. +Notation "N .-open.-measurable" := (measurable : set_system (@borel_type _ N)) : classical_set_scope. Module MeasurableNormedModuleOpen. Section measurableOpen. Context {R : archiRealFieldType} {N : normedModType R}. -Import numFieldNormedType.Exports. Let measurableTypeNormedModule := g_sigma_algebraType (@open N). -Definition borel_display : measure_display := N.-open. - -Let measurableNormedModule : set_system N := N.-open.-measurable. - -HB.instance Definition _ : Measurable borel_display measurableTypeNormedModule := +HB.instance Definition _ : Measurable (borel_display N) measurableTypeNormedModule := Measurable.on measurableTypeNormedModule. -(* Presumably it is safe to use NFI here because morally R is unique - and nothing else can be used here *) + +(* Presumably it is safe to use NFI here because the sigma-algebra of opens + for N is unique and nothing else can be used here *) #[non_forgetful_inheritance] HB.instance Definition _ := Measurable.copy N measurableTypeNormedModule. diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v index 7eba93cbab..4abf633194 100644 --- a/theories/topology_theory/metric_structure.v +++ b/theories/topology_theory/metric_structure.v @@ -114,10 +114,10 @@ Context {R : archiRealFieldType} {N : metricType R}. Lemma set1_bigcap_ball (x : N) : [set x] = \bigcap_n ball x n.+1%:R^-1. Proof. -rewrite eqEsubset; split=> [y -> n _ | y /= bn]/=; first by apply: ballxx; - rewrite invr_gt0. -apply: close_eq _=>//; first exact: metric_hausdorff; rewrite ball_close=> e0; -rewrite ball_symE. apply: (le_ball _ (bn (truncn e0%:num^-1) I)). +rewrite eqEsubset; split=> [y -> n _ | y /= bn]/=; first exact: ballxx. +apply: close_eq _ => //; first exact: metric_hausdorff. +rewrite ball_close => e0. +apply/ball_sym/(le_ball _ (bn (truncn e0%:num^-1) Logic.I)). by rewrite invf_ple ?posrE//; exact: (ltW (truncnS_gt _)). Qed.