From 8113ed9573571054276b9a58d92e67ca4290b18f Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Sat, 6 Jun 2026 12:25:28 +0200 Subject: [PATCH 01/10] generalize SimpleFun codomain from realType to sigmaRingType Co-authored-by: Arthur Djevahirdjian --- CHANGELOG_UNRELEASED.md | 2 + .../simple_functions.v | 37 ++++++++++--------- 2 files changed, 21 insertions(+), 18 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index de4c407ce2..32e23def1c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -393,6 +393,8 @@ - in `simple_functions.v`: + lemmas `fctD`, `fctN`, `fctM`, `fctZ` + + 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` diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 0029be1576..c72f97dbd4 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -72,12 +72,13 @@ Local Open Scope ring_scope. Module HBSimple. -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) + (bT : sigmaRingType d') := + {f of @isMeasurableFun d d' aT bT f & @FiniteImage aT bT f}. End HBSimple. -Notation "{ 'sfun' aT >-> T }" := (@HBSimple.SimpleFun.type _ aT T) : form_scope. +Notation "{ 'sfun' aT >-> T }" := (@HBSimple.SimpleFun.type _ _ aT T) : form_scope. Notation "[ 'sfun' 'of' f ]" := [the {sfun _ >-> _} of f] : form_scope. Module HBNNSimple. @@ -85,7 +86,7 @@ Import HBSimple. HB.structure Definition NonNegSimpleFun d (aT : sigmaRingType d) (rT : realType) := - {f of @SimpleFun d _ _ f & @NonNegFun aT rT f}. + {f of @SimpleFun d _ _ _ f & @NonNegFun aT rT f}. End HBNNSimple. @@ -93,8 +94,8 @@ Notation "{ 'nnsfun' aT >-> T }" := (@HBNNSimple.NonNegSimpleFun.type _ aT%type Notation "[ 'nnsfun' 'of' f ]" := [the {nnsfun _ >-> _} of f] : form_scope. Section sfun_pred. -Context {d} {aT : sigmaRingType d} {rT : realType}. -Definition sfun : {pred _ -> _} := [predI @mfun _ _ aT rT & fimfun]. +Context {d d'} {aT : sigmaRingType d} {bT : sigmaRingType d'}. +Definition sfun : {pred _ -> _} := [predI @mfun _ _ aT bT & fimfun]. Definition sfun_key : pred_key sfun. Proof. exact. Qed. Canonical sfun_keyed := KeyedPred sfun_key. Lemma sub_sfun_mfun : {subset sfun <= mfun}. Proof. by move=> x /andP[]. Qed. @@ -102,16 +103,16 @@ 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}. -Notation T := {sfun aT >-> rT}. -Notation sfun := (@sfun _ aT rT). +Context {d d'} {aT : measurableType d} {bT : sigmaRingType d'}. +Notation T := {sfun aT >-> bT}. +Notation sfun := (@sfun _ _ aT bT). Section Sub. -Context (f : aT -> rT) (fP : f \in sfun). +Context (f : aT -> bT) (fP : f \in sfun). Definition sfun_Sub1_subproof := - @isMeasurableFun.Build d _ aT rT f (set_mem (sub_sfun_mfun fP)). + @isMeasurableFun.Build d d' aT bT 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)). + @FiniteImage.Build aT bT f (set_mem (sub_sfun_fimfun fP)). Import HBSimple. @@ -135,15 +136,15 @@ Proof. by []. Qed. HB.instance Definition _ := isSub.Build _ _ T sfun_rect sfun_valP. -Lemma sfuneqP (f g : {sfun aT >-> rT}) : f = g <-> f =1 g. +Lemma sfuneqP (f g : {sfun aT >-> bT}) : f = g <-> f =1 g. Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. -HB.instance Definition _ := [Choice of {sfun aT >-> rT} by <:]. +HB.instance Definition _ := [Choice of {sfun aT >-> bT} by <:]. (* NB: already in cardinality.v *) -HB.instance Definition _ x : @FImFun aT rT (cst x) := FImFun.on (cst x). +HB.instance Definition _ x : @FImFun aT bT (cst x) := FImFun.on (cst x). -Definition cst_sfun x : {sfun aT >-> rT} := cst x. +Definition cst_sfun x : {sfun aT >-> bT} := cst x. Lemma cst_sfunE x : @cst_sfun x =1 cst x. Proof. by []. Qed. @@ -165,13 +166,13 @@ 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 <:]. From 764515b3eaa0a74181069c5a52276bf15503c003 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Sat, 6 Jun 2026 11:47:58 +0000 Subject: [PATCH 02/10] generalize fctD and fctN codomain from pzRingType to nmodType and zmodType Co-authored-by: Arthur Djevahirdjian --- theories/lebesgue_integral_theory/simple_functions.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index c72f97dbd4..dd1f207f52 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -151,9 +151,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. From ac467f8df639de56b904ef1abba804e8c2c3ae99 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Sat, 6 Jun 2026 18:57:20 +0000 Subject: [PATCH 03/10] 80 char limit --- theories/lebesgue_integral_theory/simple_functions.v | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index dd1f207f52..c4c9020a5c 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -72,13 +72,14 @@ Local Open Scope ring_scope. Module HBSimple. -HB.structure Definition SimpleFun d d' (aT : sigmaRingType d) - (bT : sigmaRingType d') := +HB.structure Definition SimpleFun d d' + (aT : sigmaRingType d) (bT : sigmaRingType d') := {f of @isMeasurableFun d d' aT bT f & @FiniteImage aT bT f}. End HBSimple. -Notation "{ 'sfun' aT >-> T }" := (@HBSimple.SimpleFun.type _ _ aT T) : form_scope. +Notation "{ 'sfun' aT >-> T }" := + (@HBSimple.SimpleFun.type _ _ aT T) : form_scope. Notation "[ 'sfun' 'of' f ]" := [the {sfun _ >-> _} of f] : form_scope. Module HBNNSimple. @@ -90,7 +91,8 @@ HB.structure Definition NonNegSimpleFun End HBNNSimple. -Notation "{ 'nnsfun' aT >-> T }" := (@HBNNSimple.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. From 30ab285ad923b8b8536b38d88997b3f356406bcf Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Sat, 6 Jun 2026 19:58:48 +0000 Subject: [PATCH 04/10] add Borel sigma-algebra wrapper borel_type and measurable singletons Co-authored-by: Arthur Djevahirdjian --- CHANGELOG_UNRELEASED.md | 4 ++++ theories/borel_hierarchy.v | 27 ++++++++++++++++++++++++++- 2 files changed, 30 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 32e23def1c..21a4226692 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -15,6 +15,10 @@ + lemmas `zerofctE`, `onefctE` ### Added +- in `borel_hierarchy.v`: + + definition `borel_type` + + lemmas `singleton_bigcap`, `measurable1` + - in `set_interval.v`: + lemmas `setU_itvob1`, `setU_1itvob` diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index 9fc7243db5..0e78f7a41e 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -20,7 +20,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import Order.TTheory GRing.Theory Num.Theory. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. Import numFieldNormedType.Exports. Local Open Scope classical_set_scope. @@ -80,6 +80,31 @@ Qed. End irrational_Gdelta. +Definition borel_type (T : topologicalType) := g_sigma_algebraType (@open T). + +Section borel_normedModType. +Local Open Scope ring_scope. +Context {R : realType} {V : normedModType R}. + +Lemma singleton_bigcap (x : V) : + [set x] = \bigcap_(k : nat) ball x (k.+1%:R)^-1. +Proof. +apply/seteqP; split => [_ -> k _|y xy]. + by rewrite -ball_normE/= subrr normr0 invr_gt0 ltr0n. +apply/eqP; rewrite eq_sym -subr_eq0 -normr_eq0 eq_le normr_ge0 andbT. +apply/ler_addgt0Pl => e e0; rewrite addr0. +have := xy (truncn e^-1) I; rewrite -ball_normE/= => /ltW/le_trans; apply. +by rewrite invf_ple ?posrE ?ltr0n ?invr_gt0//; apply/ltW/truncnS_gt. +Qed. + +Lemma measurable1 (x : borel_type V) : measurable [set x]. +Proof. +rewrite singleton_bigcap; apply: bigcap_measurable => // k _. +by apply: sub_sigma_algebra; exact: ball_open. +Qed. + +End borel_normedModType. + Lemma not_rational_Gdelta (R : realType) : ~ Gdelta (@rational R). Proof. apply/forall2NP => A; apply/not_andP => -[oA ratrA]. From afc4884ece54cb2aa4944e3d88355624bd86c809 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Sat, 6 Jun 2026 20:27:20 +0000 Subject: [PATCH 05/10] lmodType structure on simple functions valued in a normed module Co-authored-by: Arthur Djevahirdjian --- CHANGELOG_UNRELEASED.md | 4 ++ .../simple_functions.v | 50 +++++++++++++++++++ 2 files changed, 54 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 21a4226692..664736f33d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -19,6 +19,10 @@ + 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 `set_interval.v`: + lemmas `setU_itvob1`, `setU_1itvob` diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index c4c9020a5c..7bd1b179e3 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -6,6 +6,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality reals fsbigop ereal topology tvs. From mathcomp Require Import normedtype sequences real_interval esum measure. From mathcomp Require Import lebesgue_measure numfun realfun measurable_realfun. +From mathcomp Require Import borel_hierarchy. (**md**************************************************************************) (* # Simple functions *) @@ -216,6 +217,55 @@ 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). +Import HBSimple. + +HB.instance Definition _ (V : normedModType R) := GRing.Lmodule.on (borel_type V). + +Lemma sfun_op (U V W : normedModType R) + (f : {sfun aT >-> borel_type U}) (g : {sfun aT >-> borel_type V}) + (h : U * V -> W) : + (fun x => h (f x, g x)) \in @sfun _ _ aT (borel_type 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|split]]. + apply: fin_bigcup_measurable; first exact: fimfunP. + move=> a _; apply: fin_bigcup_measurable; first exact: fimfunP. + move=> b _; apply: measurableI; last first. + 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: measurableI. + exact: (measurable_funPTI f (measurable1 a)). + exact: (measurable_funPTI g (measurable1 b)). +apply: (sub_finite_set (B := h @` (range f `*` range g))). + by move=> _ [x _ <-]/=; exists (f x, g x) => //; split; exists x. +by apply: finite_image; apply: finite_setX; exact: fimfunP. +Qed. + +Lemma sfun_submod_closed (V : normedModType R) : + submod_closed (@sfun _ _ aT (borel_type V)). +Proof. +split=> [|k f g sf sg]; first exact: (valP (cst_sfun (0 : borel_type V))). +exact: (sfun_op (sfun_Sub sf) (sfun_Sub sg) (fun t => k *: t.1 + t.2)). +Qed. + +HB.instance Definition _ (V : normedModType R) := + GRing.isSubmodClosed.Build _ _ (@sfun _ _ aT (borel_type V)) + (sfun_submod_closed V). +HB.instance Definition _ (V : normedModType R) := + [SubChoice_isSubLmodule of {sfun aT >-> borel_type V} by <:]. + +End sfun_lmodType. + Lemma preimage_nnfun0 T (R : realDomainType) (f : {nnfun T >-> R}) t : t < 0 -> f @^-1` [set t] = set0. Proof. From 8383d3a2633a1284bc5a97ace6276033db8b834f Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Tue, 16 Jun 2026 13:54:34 +0000 Subject: [PATCH 06/10] copy on borel_type --- theories/borel_hierarchy.v | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index 0e78f7a41e..d642eecd9c 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -1,4 +1,5 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat algebra. From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import reals topology normedtype sequences. @@ -105,6 +106,10 @@ Qed. End borel_normedModType. +#[non_forgetful_inheritance] +HB.instance Definition _ (R : realType) (V : normedModType R) := + Measurable.copy V (borel_type V). + Lemma not_rational_Gdelta (R : realType) : ~ Gdelta (@rational R). Proof. apply/forall2NP => A; apply/not_andP => -[oA ratrA]. From 144ba8813f1167eee46aefa1f3ef7dd30668c11e Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Fri, 19 Jun 2026 16:05:01 +0200 Subject: [PATCH 07/10] drop borel_type wrap on sfun_op and submodule structure --- .../lebesgue_integral_theory/simple_functions.v | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 7bd1b179e3..cb84c703e7 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -221,12 +221,10 @@ Section sfun_lmodType. Context d (aT : measurableType d) (R : realType). Import HBSimple. -HB.instance Definition _ (V : normedModType R) := GRing.Lmodule.on (borel_type V). - Lemma sfun_op (U V W : normedModType R) - (f : {sfun aT >-> borel_type U}) (g : {sfun aT >-> borel_type V}) + (f : {sfun aT >-> U}) (g : {sfun aT >-> V}) (h : U * V -> W) : - (fun x => h (f x, g x)) \in @sfun _ _ aT (borel_type 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. @@ -252,17 +250,17 @@ by apply: finite_image; apply: finite_setX; exact: fimfunP. Qed. Lemma sfun_submod_closed (V : normedModType R) : - submod_closed (@sfun _ _ aT (borel_type V)). + submod_closed (@sfun _ _ aT V). Proof. -split=> [|k f g sf sg]; first exact: (valP (cst_sfun (0 : borel_type V))). +split=> [|k f g sf sg]; first exact: (valP (cst_sfun (0 : V))). exact: (sfun_op (sfun_Sub sf) (sfun_Sub sg) (fun t => k *: t.1 + t.2)). Qed. HB.instance Definition _ (V : normedModType R) := - GRing.isSubmodClosed.Build _ _ (@sfun _ _ aT (borel_type V)) + GRing.isSubmodClosed.Build _ _ (@sfun _ _ aT V) (sfun_submod_closed V). HB.instance Definition _ (V : normedModType R) := - [SubChoice_isSubLmodule of {sfun aT >-> borel_type V} by <:]. + [SubChoice_isSubLmodule of {sfun aT >-> V} by <:]. End sfun_lmodType. From 052c1d653964e69f390df336127fd31cd35de9c7 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Mon, 29 Jun 2026 11:21:41 +0200 Subject: [PATCH 08/10] refactor sfun_op into mem_sfun_comp_pair --- CHANGELOG_UNRELEASED.md | 2 +- .../simple_functions.v | 29 +++++++++---------- 2 files changed, 14 insertions(+), 17 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 664736f33d..a19f959434 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -20,7 +20,7 @@ + lemmas `singleton_bigcap`, `measurable1` - in `simple_functions.v`: - + lemmas `sfun_op`, `sfun_submod_closed` + + lemmas `mem_sfun_comp_pair`, `sfun_submod_closed` + `{sfun aT >-> borel_type V}` is an `lmodType` when `V` is a `normedModType` - in `set_interval.v`: diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index cb84c703e7..4ae209cfbd 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -221,9 +221,8 @@ Section sfun_lmodType. Context d (aT : measurableType d) (R : realType). Import HBSimple. -Lemma sfun_op (U V W : normedModType R) - (f : {sfun aT >-> U}) (g : {sfun aT >-> V}) - (h : U * V -> W) : +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/=. @@ -232,28 +231,26 @@ rewrite inE; apply/andP; split; rewrite inE/=. \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|split]]. + 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; last first. - 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: measurableI. - exact: (measurable_funPTI f (measurable1 a)). - exact: (measurable_funPTI g (measurable1 b)). -apply: (sub_finite_set (B := h @` (range f `*` range g))). + move=> b _; apply: measurableI. + by apply: measurableI; exact/(measurable_funPTI _ (measurable1 _)). + 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. -by apply: finite_image; apply: finite_setX; exact: fimfunP. +exact/finite_image/finite_setX/fimfunP. Qed. Lemma sfun_submod_closed (V : normedModType R) : submod_closed (@sfun _ _ aT V). Proof. split=> [|k f g sf sg]; first exact: (valP (cst_sfun (0 : V))). -exact: (sfun_op (sfun_Sub sf) (sfun_Sub sg) (fun t => k *: t.1 + t.2)). +exact: (mem_sfun_comp_pair (sfun_Sub sf) (sfun_Sub sg) (fun t => k *: t.1 + t.2)). Qed. HB.instance Definition _ (V : normedModType R) := From f1b2953c4637235c5943ff3ce3a5d3263b157e05 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Mon, 29 Jun 2026 14:05:57 +0200 Subject: [PATCH 09/10] adding hints --- theories/borel_hierarchy.v | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index d642eecd9c..bec77858c9 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -103,9 +103,15 @@ Proof. rewrite singleton_bigcap; apply: bigcap_measurable => // k _. by apply: sub_sigma_algebra; exact: ball_open. Qed. +#[local] Hint Resolve measurable1 : core. End borel_normedModType. +#[global] +Hint Extern 0 (measurable [set _]) => solve [apply: measurable1] : core. +#[global] Hint Extern 0 (measurable (_ @^-1` [set _])) => + solve [apply: measurable_funPTI; exact: measurable1] : core. + #[non_forgetful_inheritance] HB.instance Definition _ (R : realType) (V : normedModType R) := Measurable.copy V (borel_type V). From eb062702962c2108279a84069914ac0eefcd3c2d Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Mon, 29 Jun 2026 15:33:46 +0200 Subject: [PATCH 10/10] move new lemmas from borel_hierarchy to new file measurable_topology also renames bT -> rT --- CHANGELOG_UNRELEASED.md | 6 +-- _CoqProject | 1 + theories/borel_hierarchy.v | 38 +------------- .../simple_functions.v | 30 +++++------ theories/measure_theory/measurable_function.v | 5 +- theories/measure_theory/measurable_topology.v | 52 +++++++++++++++++++ 6 files changed, 76 insertions(+), 56 deletions(-) create mode 100644 theories/measure_theory/measurable_topology.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a19f959434..421944ebc3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -15,13 +15,13 @@ + lemmas `zerofctE`, `onefctE` ### Added -- in `borel_hierarchy.v`: - + definition `borel_type` +- new file `measurable_topology.v`: + + definition `borelType` + lemmas `singleton_bigcap`, `measurable1` - in `simple_functions.v`: + lemmas `mem_sfun_comp_pair`, `sfun_submod_closed` - + `{sfun aT >-> borel_type V}` is an `lmodType` when `V` is a `normedModType` + + `{sfun aT >-> rT}` is an `lmodType` when `rT` is a `normedModType` - in `set_interval.v`: + lemmas `setU_itvob1`, `setU_1itvob` diff --git a/_CoqProject b/_CoqProject index f0b745c7f6..98873fe72a 100644 --- a/_CoqProject +++ b/_CoqProject @@ -99,6 +99,7 @@ theories/derive.v theories/numfun.v theories/measure_theory/measurable_structure.v +theories/measure_theory/measurable_topology.v theories/measure_theory/measure_function.v theories/measure_theory/counting_measure.v theories/measure_theory/dirac_measure.v diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index bec77858c9..9fc7243db5 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -1,5 +1,4 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) -From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat algebra. From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import reals topology normedtype sequences. @@ -21,7 +20,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import Order.TTheory GRing.Theory Num.Theory. Import numFieldNormedType.Exports. Local Open Scope classical_set_scope. @@ -81,41 +80,6 @@ Qed. End irrational_Gdelta. -Definition borel_type (T : topologicalType) := g_sigma_algebraType (@open T). - -Section borel_normedModType. -Local Open Scope ring_scope. -Context {R : realType} {V : normedModType R}. - -Lemma singleton_bigcap (x : V) : - [set x] = \bigcap_(k : nat) ball x (k.+1%:R)^-1. -Proof. -apply/seteqP; split => [_ -> k _|y xy]. - by rewrite -ball_normE/= subrr normr0 invr_gt0 ltr0n. -apply/eqP; rewrite eq_sym -subr_eq0 -normr_eq0 eq_le normr_ge0 andbT. -apply/ler_addgt0Pl => e e0; rewrite addr0. -have := xy (truncn e^-1) I; rewrite -ball_normE/= => /ltW/le_trans; apply. -by rewrite invf_ple ?posrE ?ltr0n ?invr_gt0//; apply/ltW/truncnS_gt. -Qed. - -Lemma measurable1 (x : borel_type V) : measurable [set x]. -Proof. -rewrite singleton_bigcap; apply: bigcap_measurable => // k _. -by apply: sub_sigma_algebra; exact: ball_open. -Qed. -#[local] Hint Resolve measurable1 : core. - -End borel_normedModType. - -#[global] -Hint Extern 0 (measurable [set _]) => solve [apply: measurable1] : core. -#[global] Hint Extern 0 (measurable (_ @^-1` [set _])) => - solve [apply: measurable_funPTI; exact: measurable1] : core. - -#[non_forgetful_inheritance] -HB.instance Definition _ (R : realType) (V : normedModType R) := - Measurable.copy V (borel_type V). - Lemma not_rational_Gdelta (R : realType) : ~ Gdelta (@rational R). Proof. apply/forall2NP => A; apply/not_andP => -[oA ratrA]. diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 4ae209cfbd..51487b50b6 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -6,7 +6,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality reals fsbigop ereal topology tvs. From mathcomp Require Import normedtype sequences real_interval esum measure. From mathcomp Require Import lebesgue_measure numfun realfun measurable_realfun. -From mathcomp Require Import borel_hierarchy. +From mathcomp Require Import measurable_function measurable_topology. (**md**************************************************************************) (* # Simple functions *) @@ -74,8 +74,8 @@ Local Open Scope ring_scope. Module HBSimple. HB.structure Definition SimpleFun d d' - (aT : sigmaRingType d) (bT : sigmaRingType d') := - {f of @isMeasurableFun d d' aT bT f & @FiniteImage aT bT f}. + (aT : sigmaRingType d) (rT : sigmaRingType d') := + {f of @isMeasurableFun d d' aT rT f & @FiniteImage aT rT f}. End HBSimple. @@ -97,8 +97,8 @@ Notation "{ 'nnsfun' aT >-> T }" := Notation "[ 'nnsfun' 'of' f ]" := [the {nnsfun _ >-> _} of f] : form_scope. Section sfun_pred. -Context {d d'} {aT : sigmaRingType d} {bT : sigmaRingType d'}. -Definition sfun : {pred _ -> _} := [predI @mfun _ _ aT bT & fimfun]. +Context {d d'} {aT : sigmaRingType d} {rT : sigmaRingType d'}. +Definition sfun : {pred _ -> _} := [predI @mfun _ _ aT rT & fimfun]. Definition sfun_key : pred_key sfun. Proof. exact. Qed. Canonical sfun_keyed := KeyedPred sfun_key. Lemma sub_sfun_mfun : {subset sfun <= mfun}. Proof. by move=> x /andP[]. Qed. @@ -106,16 +106,16 @@ Lemma sub_sfun_fimfun : {subset sfun <= fimfun}. Proof. by move=> x /andP[]. Qed End sfun_pred. Section sfun. -Context {d d'} {aT : measurableType d} {bT : sigmaRingType d'}. -Notation T := {sfun aT >-> bT}. -Notation sfun := (@sfun _ _ aT bT). +Context {d d'} {aT : measurableType d} {rT : sigmaRingType d'}. +Notation T := {sfun aT >-> rT}. +Notation sfun := (@sfun _ _ aT rT). Section Sub. -Context (f : aT -> bT) (fP : f \in sfun). +Context (f : aT -> rT) (fP : f \in sfun). Definition sfun_Sub1_subproof := - @isMeasurableFun.Build d d' aT bT 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 bT f (set_mem (sub_sfun_fimfun fP)). + @FiniteImage.Build aT rT f (set_mem (sub_sfun_fimfun fP)). Import HBSimple. @@ -139,15 +139,15 @@ Proof. by []. Qed. HB.instance Definition _ := isSub.Build _ _ T sfun_rect sfun_valP. -Lemma sfuneqP (f g : {sfun aT >-> bT}) : f = g <-> f =1 g. +Lemma sfuneqP (f g : {sfun aT >-> rT}) : f = g <-> f =1 g. Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. -HB.instance Definition _ := [Choice of {sfun aT >-> bT} by <:]. +HB.instance Definition _ := [Choice of {sfun aT >-> rT} by <:]. (* NB: already in cardinality.v *) -HB.instance Definition _ x : @FImFun aT bT (cst x) := FImFun.on (cst x). +HB.instance Definition _ x : @FImFun aT rT (cst x) := FImFun.on (cst x). -Definition cst_sfun x : {sfun aT >-> bT} := cst x. +Definition cst_sfun x : {sfun aT >-> rT} := cst x. Lemma cst_sfunE x : @cst_sfun x =1 cst x. Proof. by []. Qed. diff --git a/theories/measure_theory/measurable_function.v b/theories/measure_theory/measurable_function.v index 061d3b958c..9080b4c129 100644 --- a/theories/measure_theory/measurable_function.v +++ b/theories/measure_theory/measurable_function.v @@ -5,7 +5,7 @@ From mathcomp Require Import all_ssreflect_compat algebra. From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality reals. From mathcomp Require Import ereal topology normedtype. -From mathcomp Require Import sequences measurable_structure. +From mathcomp Require Import sequences measurable_structure measurable_topology. (**md**************************************************************************) (* # Measurable Functions *) @@ -68,6 +68,9 @@ Proof. by move=> mY; rewrite -[f @^-1` _]setTI; exact: measurable_funP. Qed. #[deprecated(since="mathcomp-analysis 1.13.0", note="renamed to `measurable_funPTI`")] Notation measurable_sfunP := measurable_funPTI (only parsing). +#[global] Hint Extern 0 (measurable (_ @^-1` [set _])) => + solve [apply: measurable_funPTI; exact: measurable1] : core. + Section mfun_pred. Context {d d'} {aT : sigmaRingType d} {rT : sigmaRingType d'}. Definition mfun : {pred aT -> rT} := mem [set f | measurable_fun setT f]. diff --git a/theories/measure_theory/measurable_topology.v b/theories/measure_theory/measurable_topology.v new file mode 100644 index 0000000000..0671cdca15 --- /dev/null +++ b/theories/measure_theory/measurable_topology.v @@ -0,0 +1,52 @@ +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect_compat algebra finmap. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import boolp classical_sets functions cardinality reals topology. +From mathcomp Require Import measurable_structure normedtype. + +Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. + +Definition borelType (T : topologicalType) := g_sigma_algebraType (@open T). + +Section borel_normedModType. +Local Open Scope ring_scope. +Context {R : realType} {V : normedModType R}. + +Lemma singleton_bigcap (x : V) : + [set x] = \bigcap_(k : nat) ball x (k.+1%:R)^-1. +Proof. +apply/seteqP; split => [_ -> k _|y xy]. + by rewrite -ball_normE/= subrr normr0 invr_gt0 ltr0n. +apply/eqP; rewrite eq_sym -subr_eq0 -normr_eq0 eq_le normr_ge0 andbT. +apply/ler_addgt0Pl => e e0; rewrite addr0. +have := xy (truncn e^-1) I; rewrite -ball_normE/= => /ltW/le_trans; apply. +by rewrite invf_ple ?posrE ?ltr0n ?invr_gt0//; apply/ltW/truncnS_gt. +Qed. + +Lemma measurable1 (x : borelType V) : measurable [set x]. +Proof. +rewrite singleton_bigcap; apply: bigcap_measurable => // k _. +by apply: sub_sigma_algebra; exact: ball_open. +Qed. +#[local] Hint Resolve measurable1 : core. + +End borel_normedModType. + +#[global] +Hint Extern 0 (measurable [set _]) => solve [apply: measurable1] : core. + +#[non_forgetful_inheritance] +HB.instance Definition _ (R : realType) (V : normedModType R) := + Measurable.copy V (borelType V). + +