Skip to content

Parameter-Dependent Integrals #1737

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
mn200 merged 2 commits into from
Dec 3, 2025
Merged

Parameter-Dependent Integrals #1737

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9a1d2d5
Parameter-Dependent Integrals
binghe Nov 28, 2025
944388e
Higher Differentiable Lemma
binghe Nov 29, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 10 additions & 6 deletions examples/CCS/MultivariateScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2472,7 +2472,8 @@ Proof
(MP_TAC o (Q.SPECL [`l`, `E1`]) o (MATCH_MP WEAK_EQUIV_TRANS_label)) \\
RW_TAC std_ss [] \\
MP_TAC (Q.SPECL [`Xs`, `Es`, `Ps`, `Qs`]
unique_solution_of_rooted_contractions_lemma) >> RW_TAC std_ss [] \\
unique_solution_of_rooted_contractions_lemma) \\
RW_TAC std_ss [] \\
POP_ASSUM (MP_TAC o (Q.SPEC `C`)) >> RW_TAC std_ss [] \\
POP_ASSUM K_TAC (* !R. EPS _ R ==> _ *) \\
POP_ASSUM (MP_TAC o (Q.SPECL [`l`, `E2`])) >> RW_TAC std_ss [] \\
Expand All @@ -2490,7 +2491,8 @@ Proof
(MP_TAC o (Q.SPECL [`l`, `E2`]) o (MATCH_MP WEAK_EQUIV_TRANS_label)) \\
RW_TAC std_ss [] \\
MP_TAC (Q.SPECL [`Xs`, `Es`, `Qs`, `Ps`]
unique_solution_of_rooted_contractions_lemma) >> RW_TAC std_ss [] \\
unique_solution_of_rooted_contractions_lemma) \\
RW_TAC std_ss [] \\
POP_ASSUM (MP_TAC o (Q.SPEC `C`)) >> RW_TAC std_ss [] \\
POP_ASSUM K_TAC (* !R. EPS _ R ==> _ *) \\
POP_ASSUM (MP_TAC o (Q.SPECL [`l`, `E2'`])) >> RW_TAC std_ss [] \\
Expand All @@ -2504,15 +2506,16 @@ Proof
IMP_RES_TAC contracts_IMP_WEAK_EQUIV \\
PROVE_TAC [WEAK_EQUIV_TRANS],
(* goal 3 (of 4) *)
Q.PAT_X_ASSUM `WEAK_EQUIV E' (CCS_SUBST (from Xs Ps) C)`
Q.PAT_X_ASSUM `WEAK_EQUIV E' (CCS_SUBST (fromPairs Xs Ps) C)`
(MP_TAC o (Q.SPEC `E1`) o (MATCH_MP WEAK_EQUIV_TRANS_tau)) \\
RW_TAC std_ss [] \\
IMP_RES_TAC EPS_IMP_WEAK_TRANS (* 2 sub-goals here *)
>- (Q.EXISTS_TAC `E''` >> REWRITE_TAC [EPS_REFL] \\
Q.EXISTS_TAC `C` >> art []) \\
Q.PAT_X_ASSUM `EPS _ E2` K_TAC \\
MP_TAC (Q.SPECL [`Xs`, `Es`, `Ps`, `Qs`]
unique_solution_of_rooted_contractions_lemma) >> RW_TAC std_ss [] \\
unique_solution_of_rooted_contractions_lemma) \\
RW_TAC std_ss [] \\
POP_ASSUM (MP_TAC o (Q.SPEC `C`)) >> RW_TAC std_ss [] \\
Q.PAT_X_ASSUM `!l R. WEAK_TRANS _ (label l) R => _` K_TAC \\
POP_ASSUM (MP_TAC o (Q.SPEC `E2`)) >> RW_TAC std_ss [] \\
Expand All @@ -2526,15 +2529,16 @@ Proof
IMP_RES_TAC contracts_IMP_WEAK_EQUIV \\
PROVE_TAC [WEAK_EQUIV_TRANS],
(* goal 4 (of 4) *)
Q.PAT_X_ASSUM `WEAK_EQUIV E'' (CCS_SUBST (from Xs Qs) C)`
Q.PAT_X_ASSUM `WEAK_EQUIV E'' (CCS_SUBST (fromPairs Xs Qs) C)`
(MP_TAC o (Q.SPEC `E2`) o (MATCH_MP WEAK_EQUIV_TRANS_tau)) \\
RW_TAC std_ss [] \\
IMP_RES_TAC EPS_IMP_WEAK_TRANS (* 2 sub-goals here *)
>- (Q.EXISTS_TAC `E'` >> REWRITE_TAC [EPS_REFL] \\
Q.EXISTS_TAC `C` >> art []) \\
Q.PAT_X_ASSUM `EPS _ E2'` K_TAC \\
MP_TAC (Q.SPECL [`Xs`, `Es`, `Qs`, `Ps`]
unique_solution_of_rooted_contractions_lemma) >> RW_TAC std_ss [] \\
unique_solution_of_rooted_contractions_lemma) \\
RW_TAC std_ss [] \\
POP_ASSUM (MP_TAC o (Q.SPEC `C`)) >> RW_TAC std_ss [] \\
Q.PAT_X_ASSUM `!l R. WEAK_TRANS _ (label l) R => _` K_TAC \\
POP_ASSUM (MP_TAC o (Q.SPEC `E2'`)) >> RW_TAC std_ss [] \\
Expand Down
126 changes: 126 additions & 0 deletions examples/probability/distributionScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6662,6 +6662,132 @@ Proof
>> simp [Abbr ‘g’]
QED

(* ------------------------------------------------------------------------- *)
(* Parameter-Dependent Integrals (Part of Chapter 12 of [5]) Gauge version *)
(* ------------------------------------------------------------------------- *)

(* Theorem 12.4 [1, p.99] (generalized from open intervals to open sets) *)
Theorem gauge_continuity_lemma :
!u. (!t. integrable lborel (Normal o u t)) /\
(!x. (\t. u t x) continuous_on univ(:real)) /\
(?w. integrable lborel w /\
(!x. 0 <= w x /\ w x <> PosInf) /\
!t x. Normal (abs (u t x)) <= w x) ==>
(\t. integral univ(:real) (u t)) continuous_on univ(:real)
Proof
rpt STRIP_TAC
>> MP_TAC (Q.SPECL [‘lborel’, ‘u’]
(INST_TYPE [alpha |-> “:real”] continuity_univ_lemma))
>> simp [space_lborel, lborel_def]
>> impl_tac >- (Q.EXISTS_TAC ‘w’ >> art [])
>> DISCH_TAC
>> MATCH_MP_TAC CONTINUOUS_ON_EQ
>> Q.EXISTS_TAC ‘(\t. real (integral lborel (Normal o u t)))’ >> rw []
>> MP_TAC (Q.SPEC ‘u (x :real)’ (cj 2 lebesgue_eq_gauge_integral))
>> simp []
QED

Theorem gauge_differentiable_lemma :
!u. (!t. integrable lborel (Normal o u t)) /\
(!x. (\t. u t x) differentiable_on univ(:real)) /\
(?w. integrable lborel w /\
(!x. 0 <= w x /\ w x <> PosInf) /\
!t x. Normal (abs (diff1 (\t. u t x) t)) <= w x)
==> (\t. integral univ(:real) (u t)) differentiable_on univ(:real) /\
!t. integrable lborel (\x. Normal (diff1 (\t. u t x) t)) /\
diff1 (\t. integral univ(:real) (u t)) t =
integral univ(:real) (\x. diff1 (\t. u t x) t)
Proof
Q.X_GEN_TAC ‘u’ >> STRIP_TAC
>> MP_TAC (Q.SPECL [‘lborel’, ‘u’]
(INST_TYPE [alpha |-> “:real”] differentiable_univ_lemma'))
>> simp [space_lborel, lborel_def]
>> impl_tac >- (Q.EXISTS_TAC ‘w’ >> art [])
>> DISCH_THEN (STRIP_ASSUME_TAC o
SRULE [IMP_CONJ_THM, FORALL_AND_THM]) >> simp []
>> Know ‘!t. integral univ(:real) (u t) =
real (integral lborel (Normal o u t))’
>- (Q.X_GEN_TAC ‘t’ \\
MP_TAC (Q.SPEC ‘u (t :real)’ (cj 2 lebesgue_eq_gauge_integral)) \\
simp [])
>> DISCH_THEN (art o wrap)
>> Q.X_GEN_TAC ‘t’
>> Know ‘integral univ(:real) (\x. diff1 (\t. u t x) t) =
real (integral lborel (\x. Normal (diff1 (\t. u t x) t)))’
>- (MP_TAC (Q.SPEC ‘\x. diff1 (\t. u t (x :real)) t’
(cj 2 lebesgue_eq_gauge_integral)) >> simp [o_DEF])
>> Rewr
QED

Theorem gauge_higher_differentiable_lemma :
!u. (!t. integrable lborel (Normal o u t)) /\
(!n t x. higher_differentiable n (\t. u t x) t) /\
(?w. integrable lborel w /\
(!x. 0 <= w x /\ w x <> PosInf) /\
!n t x. Normal (abs (diffn n (\t. u t x) t)) <= w x)
==> !n t. higher_differentiable n (\t. integral univ(:real) (u t)) t /\
integrable lborel (\x. Normal (diffn n (\t. u t x) t)) /\
diffn n (\t. integral univ(:real) (u t)) t =
integral univ(:real) (\x. diffn n (\t. u t x) t)
Proof
Q.X_GEN_TAC ‘u’ >> STRIP_TAC
>> Induct_on ‘n’
>- (Q.X_GEN_TAC ‘t’ >> simp [limTheory.diffn_0] \\
‘(\x. u t x) = u t’ by rw [FUN_EQ_THM] \\
fs [o_DEF, limTheory.higher_differentiable_def])
>> Q.X_GEN_TAC ‘t’
>> POP_ASSUM MP_TAC
>> qabbrev_tac ‘f = \t x. diffn n (\t. u t x) t’
>> ‘!t x. diffn n (\t. u t x) t = f t x’ by rw [Abbr ‘f’, FUN_EQ_THM]
>> POP_ORW
>> ‘!t. (\x. f t x) = f t’ by rw [FUN_EQ_THM] >> POP_ORW
>> DISCH_THEN (STRIP_ASSUME_TAC o SRULE [FORALL_AND_THM])
(* applying limTheory.diffn_SUC' *)
>> Know ‘!x. diffn (SUC n) (\t. u t x) = diff1 (\t. f t x)’
>- (rw [Abbr ‘f’, Once EQ_SYM_EQ] \\
‘(\t. diffn n (\t. u t x) t) = diffn n (\t. u t x)’ by rw [FUN_EQ_THM] \\
POP_ORW \\
MATCH_MP_TAC limTheory.diffn_SUC' >> art [])
>> DISCH_TAC
(* applying gauge_differentiable_lemma on f *)
>> MP_TAC (Q.SPEC ‘f’ gauge_differentiable_lemma) >> simp [o_DEF]
>> impl_tac
>- (CONJ_TAC (* !x. (\t. f t x) differentiable_on univ(:real) *)
>- (Q.X_GEN_TAC ‘x’ \\
simp [differentiable_on, NET_WITHIN_UNIV] \\
Q.X_GEN_TAC ‘t’ \\
simp [GSYM limTheory.higher_differentiable_1_eq_differentiable] \\
Q.PAT_X_ASSUM ‘!n t x. higher_differentiable n (\t. u t x) t’
(MP_TAC o Q.GEN ‘t’ o Q.SPECL [‘SUC n’, ‘t’, ‘x’]) \\
DISCH_THEN (MP_TAC o Q.SPEC ‘t’ o
MATCH_MP limTheory.higher_differentiable_imp_1n) \\
‘diffn n (\t. u t x) = (\t. f t x)’ by rw [Abbr ‘f’, FUN_EQ_THM] \\
simp []) \\
Q.EXISTS_TAC ‘w’ >> rw [] \\
POP_ASSUM (REWRITE_TAC o wrap o Q.SPEC ‘x’ o GSYM) >> art [])
>> simp []
>> DISCH_THEN (STRIP_ASSUME_TAC o SRULE [FORALL_AND_THM])
>> qabbrev_tac ‘g = \t. integral univ(:real) (u t)’
>> Q.PAT_X_ASSUM ‘!t. diffn n g t = integral univ(:real) (f t)’
(fs o wrap o GSYM)
>> ‘(\t. diffn n g t) = diffn n g’ by rw [FUN_EQ_THM]
>> POP_ASSUM (fs o wrap)
(* stage work *)
>> Know ‘!t. higher_differentiable (SUC n) g t’
>- (rw [limTheory.higher_differentiable_def] \\
qabbrev_tac ‘h = diffn n g’ \\
‘(\t. h t) = h’ by rw [FUN_EQ_THM] >> POP_ASSUM (fs o wrap) \\
REWRITE_TAC [GSYM limTheory.higher_differentiable_1] \\
REWRITE_TAC [limTheory.higher_differentiable_1_eq_differentiable] \\
Q.PAT_X_ASSUM ‘h differentiable_on univ(:real)’ MP_TAC \\
simp [differentiable_on, NET_WITHIN_UNIV])
>> DISCH_TAC
>> simp []
>> Know ‘diffn (SUC n) g = diff1 (diffn n g)’
>- (SYM_TAC >> MATCH_MP_TAC limTheory.diffn_SUC' >> art [])
>> Rewr'
>> simp []
QED

(* ------------------------------------------------------------------------- *)
(* Moment generating function *)
Expand Down
Loading