Skip to content

Commit

Permalink
Added measure_space_density_of, etc.
Browse files Browse the repository at this point in the history
  • Loading branch information
@binghe
binghe committed Dec 2, 2024
1 parent 9cf4e3f commit 2bc7f1e
Show file tree
Hide file tree
Showing 2 changed files with 91 additions and 31 deletions.
83 changes: 59 additions & 24 deletions src/probability/extrealScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5738,14 +5738,17 @@ val FN_PLUS_CMUL = store_thm
>> METIS_TAC [le_mul_neg, extreal_of_num_def, extreal_le_def, lt_imp_le, extreal_lt_def,
le_antisym]);

val FN_PLUS_CMUL_full = store_thm
("FN_PLUS_CMUL_full",
``!f c. (0 <= c ==> (fn_plus (\x. c * f x) = (\x. c * fn_plus f x))) /\
(c <= 0 ==> (fn_plus (\x. c * f x) = (\x. -c * fn_minus f x)))``,
(* NOTE: This (new) lemma is more general than FN_PLUS_CMUL_full because sometimes ‘c’
depends on ‘x’. But the proof is the same.
*)
Theorem fn_plus_cmul :
!f c x. (0 <= c ==> fn_plus (\x. c * f x) x = c * fn_plus f x) /\
(c <= 0 ==> fn_plus (\x. c * f x) x = -c * fn_minus f x)
Proof
rpt GEN_TAC
>> Cases_on `c`
>- (SIMP_TAC std_ss [le_infty, extreal_not_infty, extreal_of_num_def] \\
FUN_EQ_TAC >> RW_TAC std_ss [fn_plus_def, fn_minus_def] >| (* 4 subgoals *)
RW_TAC std_ss [fn_plus_def, fn_minus_def] >| (* 4 subgoals *)
[ (* goal 1 (of 4) *)
REWRITE_TAC [neg_mul2],
(* goal 2 (of 4) *)
Expand All @@ -5759,7 +5762,7 @@ val FN_PLUS_CMUL_full = store_thm
(* goal 4 (of 4) *)
REWRITE_TAC [mul_rzero] ])
>- (SIMP_TAC std_ss [le_infty, extreal_not_infty, extreal_of_num_def] \\
FUN_EQ_TAC >> RW_TAC std_ss [fn_plus_def] >| (* 3 subgoals *)
RW_TAC std_ss [fn_plus_def] >| (* 3 subgoals *)
[ (* goal 1 (of 3) *)
`f x <= 0` by PROVE_TAC [extreal_lt_def] \\
fs [le_lt] \\
Expand All @@ -5777,7 +5780,15 @@ val FN_PLUS_CMUL_full = store_thm
METIS_TAC [FN_PLUS_CMUL],
(* goal 2 (of 2) *)
`r <= 0` by PROVE_TAC [extreal_le_eq, extreal_of_num_def] \\
METIS_TAC [FN_PLUS_CMUL] ]);
METIS_TAC [FN_PLUS_CMUL] ]
QED

Theorem FN_PLUS_CMUL_full :
!f c. (0 <= c ==> (fn_plus (\x. c * f x) = (\x. c * fn_plus f x))) /\
(c <= 0 ==> (fn_plus (\x. c * f x) = (\x. -c * fn_minus f x)))
Proof
RW_TAC std_ss [FUN_EQ_THM, fn_plus_cmul]
QED

val FN_MINUS_CMUL = store_thm
("FN_MINUS_CMUL",
Expand All @@ -5795,14 +5806,14 @@ val FN_MINUS_CMUL = store_thm
>> METIS_TAC [mul_le, extreal_of_num_def, extreal_le_def, lt_imp_le, extreal_lt_def,
le_antisym, neg_eq0, mul_comm]);

val FN_MINUS_CMUL_full = store_thm
("FN_MINUS_CMUL_full",
``!f c. (0 <= c ==> (fn_minus (\x. c * f x) = (\x. c * fn_minus f x))) /\
(c <= 0 ==> (fn_minus (\x. c * f x) = (\x. -c * fn_plus f x)))``,
Theorem fn_minus_cmul :
!f c x. (0 <= c ==> fn_minus (\x. c * f x) x = c * fn_minus f x) /\
(c <= 0 ==> fn_minus (\x. c * f x) x = -c * fn_plus f x)
Proof
rpt GEN_TAC
>> Cases_on `c`
>- (SIMP_TAC std_ss [le_infty, extreal_not_infty, extreal_of_num_def] \\
FUN_EQ_TAC >> RW_TAC std_ss [fn_plus_def, fn_minus_def] >| (* 4 subgoals *)
RW_TAC std_ss [fn_plus_def, fn_minus_def] >| (* 4 subgoals *)
[ (* goal 1 (of 4) *)
REWRITE_TAC [GSYM mul_lneg],
(* goal 2 (of 4) *)
Expand All @@ -5816,7 +5827,7 @@ val FN_MINUS_CMUL_full = store_thm
(* goal 4 (of 4) *)
REWRITE_TAC [mul_rzero] ])
>- (SIMP_TAC std_ss [le_infty, extreal_not_infty, extreal_of_num_def] \\
FUN_EQ_TAC >> RW_TAC std_ss [fn_minus_def] >| (* 4 subgoals *)
RW_TAC std_ss [fn_minus_def] >| (* 4 subgoals *)
[ (* goal 1 (of 4) *)
REWRITE_TAC [GSYM mul_rneg],
(* goal 2 (of 4) *)
Expand All @@ -5835,24 +5846,41 @@ val FN_MINUS_CMUL_full = store_thm
METIS_TAC [FN_MINUS_CMUL],
(* goal 2 (of 2) *)
`r <= 0` by PROVE_TAC [extreal_le_eq, extreal_of_num_def] \\
METIS_TAC [FN_MINUS_CMUL] ]);
METIS_TAC [FN_MINUS_CMUL] ]
QED

Theorem FN_MINUS_CMUL_full :
!f c. (0 <= c ==> (fn_minus (\x. c * f x) = (\x. c * fn_minus f x))) /\
(c <= 0 ==> (fn_minus (\x. c * f x) = (\x. -c * fn_plus f x)))
Proof
RW_TAC std_ss [FUN_EQ_THM, fn_minus_cmul]
QED

val FN_PLUS_FMUL = store_thm
("FN_PLUS_FMUL",
``!f c. (!x. 0 <= c x) ==> (fn_plus (\x. c x * f x) = (\x. c x * fn_plus f x))``,
RW_TAC std_ss [fn_plus_def, FUN_EQ_THM]
Theorem fn_plus_fmul :
!f c x. (!x. 0 <= c x) ==> fn_plus (\x. c x * f x) x = c x * fn_plus f x
Proof
rpt GEN_TAC >> DISCH_TAC
>> simp [fn_plus_def]
>> Cases_on `0 < f x`
>- (`0 <= c x * f x` by PROVE_TAC [let_mul] \\
fs [le_lt])
>> `f x <= 0` by PROVE_TAC [extreal_lt_def]
>> `c x * f x <= 0` by PROVE_TAC [mul_le]
>> `~(0 < c x * f x)` by PROVE_TAC [extreal_lt_def]
>> fs [mul_rzero]);
>> fs [mul_rzero]
QED

Theorem FN_PLUS_FMUL :
!f c. (!x. 0 <= c x) ==> fn_plus (\x. c x * f x) = (\x. c x * fn_plus f x)
Proof
RW_TAC std_ss [FUN_EQ_THM, fn_plus_fmul]
QED

val FN_MINUS_FMUL = store_thm
("FN_MINUS_FMUL",
``!f c. (!x. 0 <= c x) ==> (fn_minus (\x. c x * f x) = (\x. c x * fn_minus f x))``,
RW_TAC std_ss [fn_minus_def, FUN_EQ_THM]
Theorem fn_minus_fmul :
!f c x. (!x. 0 <= c x) ==> fn_minus (\x. c x * f x) x = c x * fn_minus f x
Proof
rpt GEN_TAC >> DISCH_TAC
>> simp [fn_minus_def]
>> Cases_on `0 < f x`
>- (`0 <= c x * f x` by PROVE_TAC [let_mul] \\
`~(c x * f x < 0)` by PROVE_TAC [extreal_lt_def] \\
Expand All @@ -5863,7 +5891,14 @@ val FN_MINUS_FMUL = store_thm
>> `~(0 < c x * f x)` by PROVE_TAC [extreal_lt_def]
>> fs [le_lt, lt_refl, mul_rzero, neg_0]
>- REWRITE_TAC [GSYM mul_rneg]
>> fs [entire, neg_0]);
>> fs [entire, neg_0]
QED

Theorem FN_MINUS_FMUL :
!f c. (!x. 0 <= c x) ==> fn_minus (\x. c x * f x) = (\x. c x * fn_minus f x)
Proof
RW_TAC std_ss [FUN_EQ_THM, fn_minus_fmul]
QED

val FN_PLUS_ADD_LE = store_thm
("FN_PLUS_ADD_LE",
Expand Down
39 changes: 32 additions & 7 deletions src/probability/lebesgueScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7340,6 +7340,37 @@ Proof
>> rw [MEASURE_SPACE_SIGMA_ALGEBRA]
QED

(* ‘density_of’ is like ‘density’ but automatically apply ‘fn_plus’, and the measure
part of the returned measure space is total returning 0 for non-measurable sets.
*)
Definition density_of :
density_of M f = (m_space M, measurable_sets M,
(\A. if A IN measurable_sets M then
pos_fn_integral M (\x. max 0 (f x * indicator_fn A x)) else 0))
End

(* This was HVG's measure_space_density *)
Theorem measure_space_density_of :
!M f. measure_space M /\ f IN measurable (m_space M, measurable_sets M) Borel
==> measure_space (density_of M f)
Proof
rpt STRIP_TAC
>> ‘measure_space (density M (fn_plus f))’ by PROVE_TAC [measure_space_density']
>> MATCH_MP_TAC measure_space_eq
>> Q.EXISTS_TAC ‘density M f^+’ >> art []
>> simp [density_of, density_def, density_measure_def]
>> rpt STRIP_TAC
>> MATCH_MP_TAC pos_fn_integral_cong >> simp [le_max1]
>> rpt STRIP_TAC
>- (MATCH_MP_TAC le_mul >> simp [FN_PLUS_POS, INDICATOR_FN_POS])
>> ‘max 0 (f x * indicator_fn s x) = (\x. f x * indicator_fn s x)^+ x’
by rw [Once max_comm, FN_PLUS_ALT]
>> POP_ORW
>> ONCE_REWRITE_TAC [mul_comm]
>> MATCH_MP_TAC fn_plus_fmul
>> simp [INDICATOR_FN_POS]
QED

val suminf_measure = prove (
``!M A. measure_space M /\ IMAGE (\i:num. A i) UNIV SUBSET measurable_sets M /\
disjoint_family A ==>
Expand Down Expand Up @@ -11132,16 +11163,10 @@ QED
(* old name *)
val sigma_algebra_iff2 = sigma_algebra_alt_pow;

Definition density_of :
density_of M f = (m_space M, measurable_sets M,
(\A. if A IN measurable_sets M then
pos_fn_integral M (\x. max 0 (f x * indicator_fn A x)) else 0))
End

(*
val RN_derivI = store_thm ("RN_derivI",
``!f M N. f IN measurable (m_space M, measurable_sets M) Borel /\
(!x. x IN measurable_seets M ==> 0 <= f x) /\
(!x. x IN m_space M ==> 0 <= f x) /\
(density M f = measure_of N) /\
measure_space M /\ measure_space N /\
(measurable_sets M = measurable_sets N) ==>
Expand Down

0 comments on commit 2bc7f1e

Please sign in to comment.