Measurable function results to canonise.

Jared Yeager · mn200 · commit aaef1212e0f2 · 2026-01-12T11:56:41.000+11:00
diff --git a/src/probability/borelScript.sml b/src/probability/borelScript.sml
@@ -8934,6 +8934,19 @@ Proof
       MATCH_MP_TAC borel_measurable_real_set >> art [] ]
 QED
 
+(* A different version of this also exists in Martingale,
+   but it can proved here, and this form is more consistent with other results.
+- Jared
+*)
+
+Theorem IN_MEASURABLE_BOREL_FROM_PROD_SIGMA':
+    ∀a b f. sigma_algebra a ∧ sigma_algebra b ∧ f ∈ Borel_measurable (a × b) ⇒
+        (∀y. y ∈ space b ⇒ (λx. f (x,y)) ∈ Borel_measurable a) ∧
+        (∀x. x ∈ space a ⇒ (λy. f (x,y)) ∈ Borel_measurable b)
+Proof
+    rpt gen_tac >> DISCH_TAC >> irule IN_MEASURABLE_FROM_PROD_SIGMA >> simp[SIGMA_ALGEBRA_BOREL]
+QED
+
 (* References:
 
   [1] Schilling, R.L.: Measures, Integrals and Martingales (Second Edition).
diff --git a/src/probability/real_borelScript.sml b/src/probability/real_borelScript.sml
@@ -3997,6 +3997,165 @@ Proof
         MATCH_MP_TAC hyperbola_lemma4 >> art [] ] ]
 QED
 
+(* ------------------------------------------------------------------------- *)
+(*  More Measurability Results                                               *)
+(* ------------------------------------------------------------------------- *)
+
+(*
+These are the results from my own accumulated library for borel measurable functions
+that I believe stand on their own as something useful for future users.
+- Jared Yeager
+*)
+
+(* This first batch of results has to do with sets derived from borel measurable
+   functions being measurable sets
+*)
+
+Theorem in_borel_measurable_ge_imp:
+    ∀a f. sigma_algebra a ∧ f ∈ borel_measurable a ⇒
+        ∀c. {x | c ≤ f x} ∩ space a ∈ subsets a
+Proof
+    rw[] >> drule_all_then mp_tac $ cj 2 $ SRULE [AND_IMP_INTRO] $ iffLR in_borel_measurable_ge >>
+    rw[INTER_DEF] >> pop_assum $ qspec_then ‘c’ mp_tac >>
+    qmatch_goalsub_abbrev_tac ‘s ∈ _ ⇒ t ∈ _’ >> ‘s = t’ suffices_by simp[] >>
+    simp[EXTENSION,Abbr ‘s’,Abbr ‘t’] >> metis_tac[]
+QED
+
+Theorem in_borel_measurable_gt_imp:
+    ∀a f. sigma_algebra a ∧ f ∈ borel_measurable a ⇒
+        ∀c. {x | c < f x} ∩ space a ∈ subsets a
+Proof
+    rw[] >> drule_all_then mp_tac $ cj 2 $ SRULE [AND_IMP_INTRO] $ iffLR in_borel_measurable_gr >>
+    rw[INTER_DEF] >> pop_assum $ qspec_then ‘c’ mp_tac >>
+    qmatch_goalsub_abbrev_tac ‘s ∈ _ ⇒ t ∈ _’ >> ‘s = t’ suffices_by simp[] >>
+    simp[EXTENSION,Abbr ‘s’,Abbr ‘t’] >> metis_tac[]
+QED
+
+Theorem in_borel_measurable_le_imp:
+    ∀a f. sigma_algebra a ∧ f ∈ borel_measurable a ⇒
+        ∀c. {x | f x ≤ c} ∩ space a ∈ subsets a
+Proof
+    rw[] >> drule_all_then mp_tac $ cj 2 $ SRULE [AND_IMP_INTRO] $ iffLR in_borel_measurable_le >>
+    rw[INTER_DEF] >> pop_assum $ qspec_then ‘c’ mp_tac >>
+    qmatch_goalsub_abbrev_tac ‘s ∈ _ ⇒ t ∈ _’ >> ‘s = t’ suffices_by simp[] >>
+    simp[EXTENSION,Abbr ‘s’,Abbr ‘t’] >> metis_tac[]
+QED
+
+Theorem in_borel_measurable_lt_imp:
+    ∀a f. sigma_algebra a ∧ f ∈ borel_measurable a ⇒
+        ∀c. {x | f x < c} ∩ space a ∈ subsets a
+Proof
+    rw[] >> drule_all_then mp_tac $ cj 2 $ SRULE [AND_IMP_INTRO] $ iffLR in_borel_measurable_less >>
+    rw[INTER_DEF] >> pop_assum $ qspec_then ‘c’ mp_tac >>
+    qmatch_goalsub_abbrev_tac ‘s ∈ _ ⇒ t ∈ _’ >> ‘s = t’ suffices_by simp[] >>
+    simp[EXTENSION,Abbr ‘s’,Abbr ‘t’] >> metis_tac[]
+QED
+
+Theorem in_borel_measurable_le2_imp:
+    ∀a f g. sigma_algebra a ∧ f ∈ borel_measurable a ∧ g ∈ borel_measurable a ⇒
+        {x | f x ≤ g x} ∩ space a ∈ subsets a
+Proof
+    rw[] >> qspecl_then [‘a’,‘f’,‘g’] mp_tac in_borel_measurable_le2 >> simp[INTER_DEF] >>
+    qmatch_goalsub_abbrev_tac ‘s ∈ _ ⇒ t ∈ _’ >> ‘s = t’ suffices_by simp[] >>
+    simp[EXTENSION,Abbr ‘s’,Abbr ‘t’] >> metis_tac[]
+QED
+
+Theorem in_borel_measurable_lt2_imp:
+    ∀a f g. sigma_algebra a ∧ f ∈ borel_measurable a ∧ g ∈ borel_measurable a ⇒
+        {x | f x < g x} ∩ space a ∈ subsets a
+Proof
+    rw[] >> qspecl_then [‘a’,‘f’,‘g’] mp_tac in_borel_measurable_lt2 >> simp[INTER_DEF] >>
+    qmatch_goalsub_abbrev_tac ‘s ∈ _ ⇒ t ∈ _’ >> ‘s = t’ suffices_by simp[] >>
+    simp[EXTENSION,Abbr ‘s’,Abbr ‘t’] >> metis_tac[]
+QED
+
+(* This second batch of results has to do with functions being borel measurable *)
+
+(* name conflict *)
+Theorem in_borel_measurable_ainv':
+    ∀a f g. sigma_algebra a ∧ f ∈ borel_measurable a ∧
+        (∀x. x ∈ space a ⇒ g x = -f x) ⇒ g ∈ borel_measurable a
+Proof
+    rw[] >> irule $ INST_TYPE [“:β”|->“:γ”] IN_MEASURABLE_COMP >>
+    qexistsl [‘borel’,‘f’,‘λx. -x’] >> simp[] >>
+    irule in_borel_measurable_mul >> simp[sigma_algebra_borel,space_borel] >>
+    qexistsl [‘λx. -1r’,‘I’] >>
+    simp[sigma_algebra_borel,MEASURABLE_I,borel_measurable_sets,borel_measurable_const]
+QED
+
+Theorem in_borel_measurable_abs:
+    ∀a f g. sigma_algebra a ∧ f ∈ borel_measurable a ∧
+        (∀x. x ∈ space a ⇒ g x = abs (f x)) ⇒ g ∈ borel_measurable a
+Proof
+    rw[] >> irule $ INST_TYPE [“:β”|->“:γ”] IN_MEASURABLE_COMP >>
+    qexistsl [‘borel’,‘f’,‘abs’] >> simp[] >>
+    ‘abs = λr:real. max (I r) ((λrr. -rr) r)’ by (
+        simp[FUN_EQ_THM,abs,max_def] >> strip_tac >> Cases_on ‘0 ≤ r’ >> simp[]
+        >- (Cases_on ‘r = 0’ >> simp[] >> ‘0 < r’ by simp[REAL_LT_LE] >>
+            ‘¬(r ≤ -r)’ suffices_by simp[] >> simp[REAL_NOT_LE])
+        >- (‘r ≤ -r’ suffices_by simp[] >> gs[REAL_NOT_LE])) >>
+    pop_assum SUBST1_TAC >> irule in_borel_measurable_max >>
+    simp[sigma_algebra_borel,MEASURABLE_I] >>
+    irule in_borel_measurable_ainv' >> simp[sigma_algebra_borel] >>
+    qexists ‘I’ >> simp[sigma_algebra_borel,MEASURABLE_I]
+QED
+
+Theorem in_borel_measurable_sum:
+    ∀a f g s. FINITE s ∧ sigma_algebra a ∧ (∀i. i ∈ s ⇒ f i ∈ borel_measurable a) ∧
+        (∀x. x ∈ space a ⇒ g x = REAL_SUM_IMAGE (λi. f i x) s) ⇒ g ∈ borel_measurable a
+Proof
+    simp[Once $ GSYM AND_IMP_INTRO] >> rpt gen_tac >> map_every qid_spec_tac [‘f’,‘g’] >>
+    simp[RIGHT_FORALL_IMP_THM] >> Induct_on ‘s’ >> rw[]
+    >- (irule in_borel_measurable_const >> simp[] >> qexists ‘0’ >> simp[]) >>
+    gs[REAL_SUM_IMAGE_THM] >> irule in_borel_measurable_add >> simp[] >>
+    qexistsl [‘f e’,‘λx. REAL_SUM_IMAGE (λi. f i x) (s DELETE e)’] >> simp[] >>
+    last_x_assum irule >> qexists ‘f’ >> simp[DELETE_NON_ELEMENT_RWT]
+QED
+
+Theorem in_borel_measurable_inv:
+    ∀a f g. sigma_algebra a ∧ f ∈ borel_measurable a ∧
+        (∀x. x ∈ space a ⇒ g x = (f x)⁻¹) ⇒ g ∈ borel_measurable a
+Proof
+    rw[] >> irule $ INST_TYPE [“:β”|->“:γ”] IN_MEASURABLE_COMP >>
+    qexistsl [‘borel’,‘f’,‘λx. x⁻¹’] >> simp[] >>
+    simp[sigma_algebra_borel,in_borel_measurable_le,FUNSET,space_borel] >>
+    qx_gen_tac ‘c’ >> Cases_on ‘c < 0’
+    >- (‘{x | x⁻¹ ≤ c} = {x | c⁻¹ ≤ x ∧ x < 0}’ suffices_by
+            simp[borel_measurable_sets,Excl "RMUL_LEQNORM"] >>
+        rw[EXTENSION] >> Cases_on ‘x < 0’ >> simp[REAL_NEG_NZ,nonzerop_EQ1_I] >>
+        gs[REAL_NOT_LT,REAL_NOT_LE] >> irule REAL_LTE_TRANS >>
+        qexists ‘0’ >> simp[]) >>
+    reverse $ gs[REAL_NOT_LT,Once REAL_LE_LT]
+    >- (‘{x | x⁻¹ ≤ 0r} = {x | x ≤ 0}’ suffices_by simp[borel_measurable_sets] >>
+        rw[EXTENSION,REAL_LE_LT]) >>
+    ‘{x | x⁻¹ ≤ c} = {x | x ≤ 0} ∪ {x | c⁻¹ ≤ x}’ suffices_by (
+        disch_then SUBST1_TAC >> irule SIGMA_ALGEBRA_UNION >>
+        simp[sigma_algebra_borel,borel_measurable_sets,Excl "RMUL_LEQNORM"]) >>
+    rw[EXTENSION] >> Cases_on ‘x ≤ 0’ >> simp[]
+    >- (irule REAL_LE_TRANS >> qexists ‘0’ >> gs[REAL_LE_LT]) >>
+    gs[REAL_NOT_LE] >> simp[REAL_POS_NZ,nonzerop_EQ1_I]
+QED
+
+Theorem in_borel_measurable_div:
+    ∀a f g h. sigma_algebra a ∧ f ∈ borel_measurable a ∧ g ∈ borel_measurable a ∧
+        (∀x. x ∈ space a ⇒ h x = f x / g x) ⇒ h ∈ borel_measurable a
+Proof
+    rw[] >> irule in_borel_measurable_mul >> simp[real_div] >>
+    qexistsl [‘f’,‘λx. (g x)⁻¹’] >> simp[] >>
+    irule in_borel_measurable_inv >> simp[] >> qexists ‘g’ >> simp[]
+QED
+
+Theorem in_borel_measurable_pow:
+    ∀a n f g.
+       sigma_algebra a ∧ f ∈ borel_measurable a ∧
+       (∀x. x ∈ space a ⇒ g x = (f x) pow n) ⇒
+       g ∈ borel_measurable a
+Proof
+    Induct_on ‘n’ >> rw[pow] >- (metis_tac[in_borel_measurable_const]) >>
+    irule in_borel_measurable_mul >> simp[] >> qexistsl [‘f’,‘λx. f x pow n’] >>
+    simp[] >> last_x_assum $ irule_at Any >> simp[] >> qexists ‘f’ >> simp[]
+QED
+
 (* References:
 
   [1] Schilling, R.L.: Measures, Integrals and Martingales (Second Edition).
diff --git a/src/probability/sigma_algebraScript.sml b/src/probability/sigma_algebraScript.sml
@@ -6117,6 +6117,122 @@ Proof
     dxrule_then (qspec_then `sp` mp_tac) DYNKIN_MONOTONE >> dxrule DYNKIN_STABLE >> simp[]
 QED
 
+(* ------------------------------------------------------------------------- *)
+(*  More Measurability Results                                               *)
+(* ------------------------------------------------------------------------- *)
+
+(*
+These are the results from my own accumulated library for general measurable functions
+that I believe stand on their own as something useful for future users.
+- Jared Yeager
+*)
+
+(* We have constant functions are measurable for borel/Borel later,
+   but not for generic spaces. *)
+Theorem MEASURABLE_CONST:
+    ∀a b c. sigma_algebra a ∧ c ∈ space b ⇒ (λx. c) ∈ measurable a b
+Proof
+    rw[measurable_def,FUNSET] >> Cases_on ‘c ∈ s’ >>
+    simp[PREIMAGE_def,SIGMA_ALGEBRA_SPACE,SIGMA_ALGEBRA_EMPTY]
+QED
+
+Theorem IN_MEASURABLE_CONST:
+    ∀a b c f. sigma_algebra a ∧ c ∈ space b ∧ (∀x. x ∈ space a ⇒ f x = c) ⇒ f ∈ measurable a b
+Proof
+    rw[] >> irule IN_MEASURABLE_EQ >> irule_at Any MEASURABLE_CONST >>
+    simp[] >> last_x_assum $ irule_at Any >> simp[]
+QED
+
+(* Helper lemmas for the next result *)
+
+Theorem SUBSETS_PROD_SIGMA:
+    ∀a b. subsets (a × b) =
+        BIGINTER {s | prod_sets (subsets a) (subsets b) ⊆ s ∧ sigma_algebra (space a × space b,s)}
+Proof
+    simp[prod_sigma_def,sigma_def]
+QED
+
+Theorem SIGMA_ALGEBRA_SUBSET_CLASS:
+    ∀a. sigma_algebra a ⇒ subset_class (space a) (subsets a)
+Proof
+    simp[SIGMA_ALGEBRA]
+QED
+
+Theorem PROD_SIGMA_X_SLICE:
+    ∀a b s y. sigma_algebra a ∧ subset_class (space b) (subsets b) ∧
+        s ∈ subsets (a × b) ⇒ {x | (x,y) ∈ s} ∈ subsets a
+Proof
+    rw[] >> `sigma_algebra (a × b)` by (irule SIGMA_ALGEBRA_PROD_SIGMA >> simp[SIGMA_ALGEBRA_SUBSET_CLASS]) >>
+    REVERSE $ Cases_on `y ∈ space b`
+    >- (dxrule_all_then mp_tac SIGMA_ALGEBRA_SUBSET_SPACE >> simp[SUBSET_DEF,SPACE_PROD_SIGMA] >> strip_tac >>
+        `{x | (x,y) ∈ s} = ∅` suffices_by simp[SIGMA_ALGEBRA_EMPTY] >> simp[EXTENSION] >> qx_gen_tac `x` >>
+        CCONTR_TAC >> fs[] >> first_x_assum $ dxrule_then mp_tac >> simp[]) >>
+    fs[SUBSETS_PROD_SIGMA] >>
+    first_x_assum $ qspec_then `subsets (a × b) ∩ {t | {x | (x,y) ∈ t} ∈ subsets a}` $
+        irule o cj 2 o SIMP_RULE (srw_ss ()) [] >>
+    simp[SIGMA_ALGEBRA_ALT_SPACE] >> rpt CONJ_TAC
+    >- (dxrule_then mp_tac SIGMA_ALGEBRA_SUBSET_CLASS >> simp[subset_class_def,SPACE_PROD_SIGMA])
+    >- (dxrule_then mp_tac SIGMA_ALGEBRA_SPACE >> simp[SPACE_PROD_SIGMA])
+    >- (simp[SIGMA_ALGEBRA_SPACE])
+    >- (NTAC 2 strip_tac >> NTAC 2 $ dxrule_all_then mp_tac SIGMA_ALGEBRA_COMPL >>
+        simp[SPACE_PROD_SIGMA,DIFF_DEF])
+    >- (simp[FUNSET_INTER] >> NTAC 2 strip_tac >> simp[SIGMA_ALGEBRA_ENUM] >>
+        qspecl_then [`a`,`λn. {x | (x,y) ∈ f n}`] mp_tac SIGMA_ALGEBRA_ENUM >> fs[FUNSET] >>
+        qmatch_abbrev_tac `s ∈ _ ⇒ t ∈ _` >> `s = t` suffices_by simp[] >> UNABBREV_ALL_TAC >>
+        simp[EXTENSION,IN_BIGUNION_IMAGE] >> qx_gen_tac `x` >> metis_tac[])
+    >- (simp[prod_sets_def,SUBSET_DEF] >> rw[] >> rename [`s × t`] >> Cases_on `y ∈ t`
+        >- (`{x | (x,y) ∈ s × t} = s` suffices_by simp[] >> simp[EXTENSION])
+        >- (`{x | (x,y) ∈ s × t} = ∅` suffices_by simp[SIGMA_ALGEBRA_EMPTY] >> simp[EXTENSION]))
+    >- (simp[prod_sigma_def,SIGMA_SUBSET_SUBSETS])
+QED
+
+Theorem PROD_SIGMA_Y_SLICE:
+    ∀a b s x. subset_class (space a) (subsets a) ∧ sigma_algebra b ∧
+        s ∈ subsets (a × b) ⇒ {y | (x,y) ∈ s} ∈ subsets b
+Proof
+    rw[] >> `sigma_algebra (a × b)` by (irule SIGMA_ALGEBRA_PROD_SIGMA >> simp[SIGMA_ALGEBRA_SUBSET_CLASS]) >>
+    REVERSE $ Cases_on `x ∈ space a`
+    >- (dxrule_all_then mp_tac SIGMA_ALGEBRA_SUBSET_SPACE >> simp[SUBSET_DEF,SPACE_PROD_SIGMA] >> strip_tac >>
+        `{y | (x,y) ∈ s} = ∅` suffices_by simp[SIGMA_ALGEBRA_EMPTY] >> simp[EXTENSION] >> qx_gen_tac `y` >>
+        CCONTR_TAC >> fs[] >> first_x_assum $ dxrule_then mp_tac >> simp[]) >>
+    fs[SUBSETS_PROD_SIGMA] >>
+    first_x_assum $ qspec_then `subsets (a × b) ∩ {t | {y | (x,y) ∈ t} ∈ subsets b}` $
+        irule o cj 2 o SIMP_RULE (srw_ss ()) [] >>
+    simp[SIGMA_ALGEBRA_ALT_SPACE] >> rpt CONJ_TAC
+    >- (dxrule_then mp_tac SIGMA_ALGEBRA_SUBSET_CLASS >> simp[subset_class_def,SPACE_PROD_SIGMA])
+    >- (dxrule_then mp_tac SIGMA_ALGEBRA_SPACE >> simp[SPACE_PROD_SIGMA])
+    >- (simp[SIGMA_ALGEBRA_SPACE])
+    >- (NTAC 2 strip_tac >> NTAC 2 $ dxrule_all_then mp_tac SIGMA_ALGEBRA_COMPL >>
+        simp[SPACE_PROD_SIGMA,DIFF_DEF])
+    >- (simp[FUNSET_INTER] >> NTAC 2 strip_tac >> simp[SIGMA_ALGEBRA_ENUM] >>
+        qspecl_then [`b`,`λn. {y | (x,y) ∈ f n}`] mp_tac SIGMA_ALGEBRA_ENUM >> fs[FUNSET] >>
+        qmatch_abbrev_tac `s ∈ _ ⇒ t ∈ _` >> `s = t` suffices_by simp[] >> UNABBREV_ALL_TAC >>
+        simp[EXTENSION,IN_BIGUNION_IMAGE] >> qx_gen_tac `y` >> metis_tac[])
+    >- (simp[prod_sets_def,SUBSET_DEF] >> rw[] >> rename [`s × t`] >> Cases_on `x ∈ s`
+        >- (`{y | (x,y) ∈ s × t} = t` suffices_by simp[] >> simp[EXTENSION])
+        >- (`{y | (x,y) ∈ s × t} = ∅` suffices_by simp[SIGMA_ALGEBRA_EMPTY] >> simp[EXTENSION]))
+    >- (simp[prod_sigma_def,SIGMA_SUBSET_SUBSETS])
+QED
+
+(* IN_MEASURABLE_PROD_SIGMA tells us that pairing measurable functions gives a measurable
+   function.
+   This gives us that fixing a variable in a measurable function gives a measurable function.
+   As before, there is a IN_MEASURABLE_BOREL_FROM_PROD_SIGMA later, but this is more general.
+*)
+Theorem IN_MEASURABLE_FROM_PROD_SIGMA:
+    ∀a b c f. sigma_algebra a ∧ sigma_algebra b ∧ sigma_algebra c ∧ f ∈ measurable (a × b) c ⇒
+        (∀y. y ∈ space b ⇒ (λx. f (x,y)) ∈ measurable a c) ∧
+        (∀x. x ∈ space a ⇒ (λy. f (x,y)) ∈ measurable b c)
+Proof
+    rw[measurable_def,FUNSET,FORALL_PROD,IN_SPACE_PROD_SIGMA] >>
+    first_x_assum $ dxrule_then assume_tac
+    >| [dxrule_at_then Any (qspec_then ‘y’ mp_tac) PROD_SIGMA_X_SLICE,
+        dxrule_at_then Any (qspec_then ‘x’ mp_tac) PROD_SIGMA_Y_SLICE] >>
+    simp[SIGMA_ALGEBRA_SUBSET_CLASS] >>
+    qmatch_goalsub_abbrev_tac ‘t ∈ _ ⇒ r ∈ _’ >> ‘t = r’ suffices_by simp[] >>
+    simp[Abbr ‘t’,Abbr ‘r’,EXTENSION,IN_SPACE_PROD_SIGMA]
+QED
+
 (* References:
 
   [1] Hurd, J.: Formal verification of probabilistic algorithms. University of
