From 6526d2b814dcd1f9ea551b7a4f68ea9535bd94de Mon Sep 17 00:00:00 2001 From: adjevahi Date: Wed, 8 Jul 2026 15:37:24 +0200 Subject: [PATCH 1/4] 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/4] 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/4] 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/4] 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).