Structure lebesgueTheory
signature lebesgueTheory =
sig
type thm = Thm.thm
(* Definitions *)
val RADON_F_def : thm
val RADON_F_integrals_def : thm
val RN_deriv_def : thm
val density_def : thm
val density_measure_def : thm
val distr_def : thm
val finite_space_integral_def : thm
val fn_seq_def : thm
val fn_seq_integral_def : thm
val integrable_def : thm
val integral_def : thm
val measure_absolutely_continuous_def : thm
val norm_def : thm
val pos_fn_integral_def : thm
val pos_simple_fn_def : thm
val pos_simple_fn_integral_def : thm
val psfis_def : thm
val psfs_def : thm
(* Theorems *)
val BOREL_INDUCT : thm
val IN_MEASURABLE_BOREL_POS_SIMPLE_FN : thm
val IN_psfis : thm
val IN_psfis_eq : thm
val Radon_Nikodym : thm
val Radon_Nikodym' : thm
val Radon_Nikodym_finite : thm
val Radon_Nikodym_finite_arbitrary : thm
val Radon_Nikodym_sigma_finite : thm
val density_fn_plus : thm
val ext_suminf_cmult_indicator : thm
val finite_integrable_function_exists : thm
val finite_space_POW_integral_reduce : thm
val finite_space_integral_reduce : thm
val finite_support_integral_reduce : thm
val integrable_AE_normal : thm
val integrable_abs : thm
val integrable_abs_bound_exists : thm
val integrable_add : thm
val integrable_add_lemma : thm
val integrable_add_pos : thm
val integrable_bound_exists : thm
val integrable_bounded : thm
val integrable_cmul : thm
val integrable_const : thm
val integrable_eq : thm
val integrable_eq_AE : thm
val integrable_finite_integral : thm
val integrable_fn_minus : thm
val integrable_fn_plus : thm
val integrable_from_abs : thm
val integrable_from_bound_exists : thm
val integrable_indicator : thm
val integrable_indicator_pow : thm
val integrable_infty : thm
val integrable_infty_null : thm
val integrable_mul_indicator : thm
val integrable_normal_integral : thm
val integrable_not_infty : thm
val integrable_not_infty_alt : thm
val integrable_not_infty_alt2 : thm
val integrable_not_infty_alt3 : thm
val integrable_plus_minus : thm
val integrable_pos : thm
val integrable_sub : thm
val integrable_sum : thm
val integrable_zero : thm
val integral_abs_eq_0 : thm
val integral_abs_imp_integrable : thm
val integral_abs_pos_fn : thm
val integral_add : thm
val integral_add_lemma : thm
val integral_add_lemma' : thm
val integral_cmul : thm
val integral_cmul_indicator : thm
val integral_cmul_infty : thm
val integral_cong : thm
val integral_cong_AE : thm
val integral_const : thm
val integral_eq_0 : thm
val integral_indicator : thm
val integral_indicator_pow : thm
val integral_indicator_pow_eq : thm
val integral_mono : thm
val integral_mspace : thm
val integral_null_set : thm
val integral_pos : thm
val integral_pos_fn : thm
val integral_posinf : thm
val integral_sequence : thm
val integral_split : thm
val integral_split' : thm
val integral_sum : thm
val integral_triangle_ineq : thm
val integral_triangle_ineq' : thm
val integral_zero : thm
val lebesgue_monotone_convergence : thm
val lebesgue_monotone_convergence_AE : thm
val lebesgue_monotone_convergence_decreasing : thm
val lebesgue_monotone_convergence_subset : thm
val lemma_fn_seq_measurable : thm
val lemma_fn_seq_mono_increasing : thm
val lemma_fn_seq_positive : thm
val lemma_fn_seq_sup : thm
val markov_ineq : thm
val markov_inequality : thm
val measurable_sequence : thm
val measure_density_indicator : thm
val measure_restricted : thm
val measure_space_density : thm
val measure_space_density' : thm
val measure_space_distr : thm
val measure_subadditive_finite : thm
val pos_fn_integral_add : thm
val pos_fn_integral_cmul : thm
val pos_fn_integral_cmul_indicator : thm
val pos_fn_integral_cmul_infty : thm
val pos_fn_integral_cmult : thm
val pos_fn_integral_cmult' : thm
val pos_fn_integral_cong : thm
val pos_fn_integral_cong_AE : thm
val pos_fn_integral_density : thm
val pos_fn_integral_density' : thm
val pos_fn_integral_disjoint_sets : thm
val pos_fn_integral_disjoint_sets_sum : thm
val pos_fn_integral_eq_0 : thm
val pos_fn_integral_indicator : thm
val pos_fn_integral_infty_null : thm
val pos_fn_integral_mono : thm
val pos_fn_integral_mono_AE : thm
val pos_fn_integral_mspace : thm
val pos_fn_integral_null_set : thm
val pos_fn_integral_pos : thm
val pos_fn_integral_pos_simple_fn : thm
val pos_fn_integral_split : thm
val pos_fn_integral_sub : thm
val pos_fn_integral_sum : thm
val pos_fn_integral_sum_cmul_indicator : thm
val pos_fn_integral_suminf : thm
val pos_fn_integral_zero : thm
val pos_simple_fn_add : thm
val pos_simple_fn_add_alt : thm
val pos_simple_fn_cmul : thm
val pos_simple_fn_cmul_alt : thm
val pos_simple_fn_indicator : thm
val pos_simple_fn_indicator_alt : thm
val pos_simple_fn_integral_add : thm
val pos_simple_fn_integral_add_alt : thm
val pos_simple_fn_integral_cmul : thm
val pos_simple_fn_integral_cmul_alt : thm
val pos_simple_fn_integral_indicator : thm
val pos_simple_fn_integral_mono : thm
val pos_simple_fn_integral_not_infty : thm
val pos_simple_fn_integral_present : thm
val pos_simple_fn_integral_sub : thm
val pos_simple_fn_integral_sum : thm
val pos_simple_fn_integral_sum_alt : thm
val pos_simple_fn_integral_unique : thm
val pos_simple_fn_integral_zero : thm
val pos_simple_fn_integral_zero_alt : thm
val pos_simple_fn_le : thm
val pos_simple_fn_max : thm
val pos_simple_fn_not_infty : thm
val pos_simple_fn_thm1 : thm
val psfis_add : thm
val psfis_cmul : thm
val psfis_indicator : thm
val psfis_intro : thm
val psfis_mono : thm
val psfis_not_infty : thm
val psfis_pos : thm
val psfis_present : thm
val psfis_sub : thm
val psfis_sum : thm
val psfis_unique : thm
val psfis_zero : thm
val lebesgue_grammars : type_grammar.grammar * term_grammar.grammar
(*
[borel] Parent theory of "lebesgue"
[RADON_F_def] Definition
⊢ ∀m v.
RADON_F m v =
{f |
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
(∀x. 0 ≤ f x) ∧
∀A. A ∈ measurable_sets m ⇒ ∫⁺ m (λx. f x * 𝟙 A x) ≤ measure v A}
[RADON_F_integrals_def] Definition
⊢ ∀m v.
RADON_F_integrals m v = {r | ∃f. r = ∫⁺ m f ∧ f ∈ RADON_F m v}
[RN_deriv_def] Definition
⊢ ∀v m.
v / m =
@f. f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
(∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
∀s. s ∈ measurable_sets m ⇒ (f * m) s = v s
[density_def] Definition
⊢ ∀m f. density m f = (m_space m,measurable_sets m,f * m)
[density_measure_def] Definition
⊢ ∀m f. f * m = (λs. ∫⁺ m (λx. f x * 𝟙 s x))
[distr_def] Definition
⊢ ∀m f. distr m f = (λs. measure m (PREIMAGE f s ∩ m_space m))
[finite_space_integral_def] Definition
⊢ ∀m f.
finite_space_integral m f =
∑ (λr. r * measure m (PREIMAGE f {r} ∩ m_space m))
(IMAGE f (m_space m))
[fn_seq_def] Definition
⊢ ∀m f.
fn_seq m f =
(λn x.
∑
(λk.
&k / 2 pow n *
𝟙
{x |
x ∈ m_space m ∧ &k / 2 pow n ≤ f x ∧
f x < (&k + 1) / 2 pow n} x) (count (4 ** n)) +
2 pow n * 𝟙 {x | x ∈ m_space m ∧ 2 pow n ≤ f x} x)
[fn_seq_integral_def] Definition
⊢ ∀m f.
fn_seq_integral m f =
(λn.
∑
(λk.
&k / 2 pow n *
measure m
{x |
x ∈ m_space m ∧ &k / 2 pow n ≤ f x ∧
f x < (&k + 1) / 2 pow n}) (count (4 ** n)) +
2 pow n * measure m {x | x ∈ m_space m ∧ 2 pow n ≤ f x})
[integrable_def] Definition
⊢ ∀m f.
integrable m f ⇔
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
∫⁺ m f⁺ ≠ +∞ ∧ ∫⁺ m f⁻ ≠ +∞
[integral_def] Definition
⊢ ∀m f. ∫ m f = ∫⁺ m f⁺ − ∫⁺ m f⁻
[measure_absolutely_continuous_def] Definition
⊢ ∀v m. v ≪ m ⇔ ∀s. s ∈ measurable_sets m ∧ measure m s = 0 ⇒ v s = 0
[norm_def] Definition
⊢ ∀m u p.
norm m u p =
if p < +∞ then ∫ m (λx. abs (u x) powr p) powr p⁻¹
else inf {c | 0 < c ∧ measure m {x | c ≤ abs (u x)} = 0}
[pos_fn_integral_def] Definition
⊢ ∀m f.
∫⁺ m f =
sup {r | (∃g. r ∈ psfis m g ∧ ∀x. x ∈ m_space m ⇒ g x ≤ f x)}
[pos_simple_fn_def] Definition
⊢ ∀m f s a x.
pos_simple_fn m f s a x ⇔
(∀t. t ∈ m_space m ⇒ 0 ≤ f t) ∧
(∀t. t ∈ m_space m ⇒ f t = ∑ (λi. Normal (x i) * 𝟙 (a i) t) s) ∧
(∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ∧ FINITE s ∧
(∀i. i ∈ s ⇒ 0 ≤ x i) ∧
(∀i j. i ∈ s ∧ j ∈ s ∧ i ≠ j ⇒ DISJOINT (a i) (a j)) ∧
BIGUNION (IMAGE a s) = m_space m
[pos_simple_fn_integral_def] Definition
⊢ ∀m s a x.
pos_simple_fn_integral m s a x =
∑ (λi. Normal (x i) * measure m (a i)) s
[psfis_def] Definition
⊢ ∀m f.
psfis m f =
IMAGE (λ(s,a,x). pos_simple_fn_integral m s a x) (psfs m f)
[psfs_def] Definition
⊢ ∀m f. psfs m f = {(s,a,x) | pos_simple_fn m f s a x}
[BOREL_INDUCT] Theorem
⊢ ∀f m P.
measure_space m ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
(∀x. 0 ≤ f x) ∧
(∀f g.
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
g ∈ Borel_measurable (m_space m,measurable_sets m) ∧
(∀x. x ∈ m_space m ⇒ f x = g x) ∧ P f ⇒
P g) ∧ (∀A. A ∈ measurable_sets m ⇒ P (𝟙 A)) ∧
(∀f c.
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧ 0 ≤ c ∧
(∀x. 0 ≤ f x) ∧ P f ⇒
P (λx. c * f x)) ∧
(∀f g.
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
g ∈ Borel_measurable (m_space m,measurable_sets m) ∧
(∀x. 0 ≤ f x) ∧ P f ∧ (∀x. 0 ≤ g x) ∧ P g ⇒
P (λx. f x + g x)) ∧
(∀u. (∀i. u i ∈ Borel_measurable (m_space m,measurable_sets m)) ∧
(∀i x. 0 ≤ u i x) ∧ (∀x. mono_increasing (λi. u i x)) ∧
(∀i. P (u i)) ⇒
P (λx. sup (IMAGE (λi. u i x) 𝕌(:num)))) ⇒
P f
[IN_MEASURABLE_BOREL_POS_SIMPLE_FN] Theorem
⊢ ∀m f.
measure_space m ∧ (∃s a x. pos_simple_fn m f s a x) ⇒
f ∈ Borel_measurable (m_space m,measurable_sets m)
[IN_psfis] Theorem
⊢ ∀m r f.
r ∈ psfis m f ⇒
∃s a x.
pos_simple_fn m f s a x ∧ r = pos_simple_fn_integral m s a x
[IN_psfis_eq] Theorem
⊢ ∀m r f.
r ∈ psfis m f ⇔
∃s a x.
pos_simple_fn m f s a x ∧ r = pos_simple_fn_integral m s a x
[Radon_Nikodym] Theorem
⊢ ∀m v.
measure_space m ∧ sigma_finite m ∧
measure_space (m_space m,measurable_sets m,v) ∧ v ≪ m ⇒
∃f. f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
(∀x. 0 ≤ f x) ∧ ∀s. s ∈ measurable_sets m ⇒ (f * m) s = v s
[Radon_Nikodym'] Theorem
⊢ ∀m v.
measure_space m ∧ sigma_finite m ∧
measure_space (m_space m,measurable_sets m,v) ∧ v ≪ m ⇒
∃f. f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
(∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
∀s. s ∈ measurable_sets m ⇒ (f * m) s = v s
[Radon_Nikodym_finite] Theorem
⊢ ∀M N.
measure_space M ∧ measure_space N ∧ m_space M = m_space N ∧
measurable_sets M = measurable_sets N ∧
measure M (m_space M) ≠ +∞ ∧ measure N (m_space N) ≠ +∞ ∧
measure N ≪ M ⇒
∃f. f ∈ Borel_measurable (m_space M,measurable_sets M) ∧
(∀x. 0 ≤ f x) ∧
∀A. A ∈ measurable_sets M ⇒
∫⁺ M (λx. f x * 𝟙 A x) = measure N A
[Radon_Nikodym_finite_arbitrary] Theorem
⊢ ∀M N.
measure_space M ∧ measure_space N ∧ m_space M = m_space N ∧
measurable_sets M = measurable_sets N ∧
measure M (m_space M) ≠ +∞ ∧ measure N ≪ M ⇒
∃f. f ∈ Borel_measurable (m_space M,measurable_sets M) ∧
(∀x. 0 ≤ f x) ∧
∀A. A ∈ measurable_sets M ⇒
∫⁺ M (λx. f x * 𝟙 A x) = measure N A
[Radon_Nikodym_sigma_finite] Theorem
⊢ ∀M N.
measure_space M ∧ measure_space N ∧ m_space M = m_space N ∧
measurable_sets M = measurable_sets N ∧ sigma_finite M ∧
measure N ≪ M ⇒
∃f. f ∈ Borel_measurable (m_space M,measurable_sets M) ∧
(∀x. 0 ≤ f x) ∧
∀A. A ∈ measurable_sets M ⇒
∫⁺ M (λx. f x * 𝟙 A x) = measure N A
[density_fn_plus] Theorem
⊢ ∀M f.
density M f⁺ =
(m_space M,measurable_sets M,(λA. ∫⁺ M (λx. max 0 (f x * 𝟙 A x))))
[ext_suminf_cmult_indicator] Theorem
⊢ ∀A f x i.
disjoint_family A ∧ x ∈ A i ∧ (∀i. 0 ≤ f i) ⇒
suminf (λn. f n * 𝟙 (A n) x) = f i
[finite_integrable_function_exists] Theorem
⊢ ∀m. measure_space m ∧ sigma_finite m ⇒
∃h. h ∈ Borel_measurable (m_space m,measurable_sets m) ∧
∫⁺ m h ≠ +∞ ∧ (∀x. x ∈ m_space m ⇒ 0 < h x ∧ h x < +∞) ∧
∀x. 0 ≤ h x
[finite_space_POW_integral_reduce] Theorem
⊢ ∀m f.
measure_space m ∧ POW (m_space m) = measurable_sets m ∧
FINITE (m_space m) ∧ (∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ∧
measure m (m_space m) < +∞ ⇒
∫ m f = ∑ (λx. f x * measure m {x}) (m_space m)
[finite_space_integral_reduce] Theorem
⊢ ∀m f.
measure_space m ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
(∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ∧ FINITE (m_space m) ∧
measure m (m_space m) < +∞ ∧ integrable m f ⇒
∫ m f = finite_space_integral m f
[finite_support_integral_reduce] Theorem
⊢ ∀m f.
measure_space m ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
(∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ∧
FINITE (IMAGE f (m_space m)) ∧ integrable m f ∧
measure m (m_space m) < +∞ ⇒
∫ m f = finite_space_integral m f
[integrable_AE_normal] Theorem
⊢ ∀m f. measure_space m ∧ integrable m f ⇒ AE x::m. f x < +∞
[integrable_abs] Theorem
⊢ ∀m f. measure_space m ∧ integrable m f ⇒ integrable m (abs ∘ f)
[integrable_abs_bound_exists] Theorem
⊢ ∀m u.
measure_space m ∧ integrable m (abs ∘ u) ⇒
∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x) ∧
∀x. x ∈ m_space m ⇒ abs (u x) ≤ w x
[integrable_add] Theorem
⊢ ∀m f g.
measure_space m ∧ integrable m f ∧ integrable m g ∧
(∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ g x ≠ −∞ ∨ f x ≠ +∞ ∧ g x ≠ +∞) ⇒
integrable m (λx. f x + g x)
[integrable_add_lemma] Theorem
⊢ ∀m f g.
measure_space m ∧ integrable m f ∧ integrable m g ⇒
integrable m (λx. f⁺ x + g⁺ x) ∧ integrable m (λx. f⁻ x + g⁻ x)
[integrable_add_pos] Theorem
⊢ ∀m f g.
measure_space m ∧ integrable m f ∧ integrable m g ∧
(∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ g x) ⇒
integrable m (λx. f x + g x)
[integrable_bound_exists] Theorem
⊢ ∀m u.
measure_space m ∧ integrable m u ⇒
∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x) ∧
∀x. x ∈ m_space m ⇒ abs (u x) ≤ w x
[integrable_bounded] Theorem
⊢ ∀m f g.
measure_space m ∧ integrable m f ∧
g ∈ Borel_measurable (m_space m,measurable_sets m) ∧
(∀x. x ∈ m_space m ⇒ abs (g x) ≤ f x) ⇒
integrable m g
[integrable_cmul] Theorem
⊢ ∀m f c.
measure_space m ∧ integrable m f ⇒
integrable m (λx. Normal c * f x)
[integrable_const] Theorem
⊢ ∀m c.
measure_space m ∧ measure m (m_space m) < +∞ ⇒
integrable m (λx. Normal c)
[integrable_eq] Theorem
⊢ ∀m f g.
measure_space m ∧ integrable m f ∧
(∀x. x ∈ m_space m ⇒ f x = g x) ⇒
integrable m g
[integrable_eq_AE] Theorem
⊢ ∀m f g.
complete_measure_space m ∧ integrable m f ∧ (AE x::m. f x = g x) ⇒
integrable m g
[integrable_finite_integral] Theorem
⊢ ∀m f. measure_space m ∧ integrable m f ⇒ ∫ m f ≠ +∞ ∧ ∫ m f ≠ −∞
[integrable_fn_minus] Theorem
⊢ ∀m f. measure_space m ∧ integrable m f ⇒ integrable m f⁻
[integrable_fn_plus] Theorem
⊢ ∀m f. measure_space m ∧ integrable m f ⇒ integrable m f⁺
[integrable_from_abs] Theorem
⊢ ∀m u.
measure_space m ∧
u ∈ Borel_measurable (m_space m,measurable_sets m) ∧
integrable m (abs ∘ u) ⇒
integrable m u
[integrable_from_bound_exists] Theorem
⊢ ∀m u.
measure_space m ∧
u ∈ Borel_measurable (m_space m,measurable_sets m) ∧
(∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x) ∧
∀x. x ∈ m_space m ⇒ abs (u x) ≤ w x) ⇒
integrable m u
[integrable_indicator] Theorem
⊢ ∀m s.
measure_space m ∧ s ∈ measurable_sets m ∧ measure m s < +∞ ⇒
integrable m (𝟙 s)
[integrable_indicator_pow] Theorem
⊢ ∀m s n.
measure_space m ∧ s ∈ measurable_sets m ∧ measure m s < +∞ ∧
0 < n ⇒
integrable m (λx. 𝟙 s x pow n)
[integrable_infty] Theorem
⊢ ∀m f s.
measure_space m ∧ integrable m f ∧ s ∈ measurable_sets m ∧
(∀x. x ∈ s ⇒ f x = +∞) ⇒
measure m s = 0
[integrable_infty_null] Theorem
⊢ ∀m f.
measure_space m ∧ integrable m f ⇒
null_set m {x | x ∈ m_space m ∧ f x = +∞}
[integrable_mul_indicator] Theorem
⊢ ∀m s f.
measure_space m ∧ s ∈ measurable_sets m ∧ measure m s < +∞ ∧
(∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ∧ integrable m f ⇒
integrable m (λx. f x * 𝟙 s x)
[integrable_normal_integral] Theorem
⊢ ∀m f. measure_space m ∧ integrable m f ⇒ ∃r. ∫ m f = Normal r
[integrable_not_infty] Theorem
⊢ ∀m f.
measure_space m ∧ integrable m f ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
∃g. integrable m g ∧ (∀x. 0 ≤ g x) ∧ (∀x. g x ≠ +∞) ∧
∫ m f = ∫ m g
[integrable_not_infty_alt] Theorem
⊢ ∀m f.
measure_space m ∧ integrable m f ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
integrable m (λx. if f x = +∞ then 0 else f x) ∧
∫ m f = ∫ m (λx. if f x = +∞ then 0 else f x)
[integrable_not_infty_alt2] Theorem
⊢ ∀m f.
measure_space m ∧ integrable m f ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
integrable m (λx. if f x = +∞ then 0 else f x) ∧
∫⁺ m f = ∫⁺ m (λx. if f x = +∞ then 0 else f x)
[integrable_not_infty_alt3] Theorem
⊢ ∀m f.
measure_space m ∧ integrable m f ⇒
integrable m (λx. if f x = −∞ ∨ f x = +∞ then 0 else f x) ∧
∫ m f = ∫ m (λx. if f x = −∞ ∨ f x = +∞ then 0 else f x)
[integrable_plus_minus] Theorem
⊢ ∀m f.
measure_space m ⇒
(integrable m f ⇔
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
integrable m f⁺ ∧ integrable m f⁻)
[integrable_pos] Theorem
⊢ ∀m f.
measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
(integrable m f ⇔
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧ ∫⁺ m f ≠ +∞)
[integrable_sub] Theorem
⊢ ∀m f g.
measure_space m ∧ integrable m f ∧ integrable m g ∧
(∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ g x ≠ +∞) ⇒
integrable m (λx. f x − g x)
[integrable_sum] Theorem
⊢ ∀m f s.
FINITE s ∧ measure_space m ∧ (∀i. i ∈ s ⇒ integrable m (f i)) ∧
(∀i x. i ∈ s ∧ x ∈ m_space m ⇒ f i x ≠ +∞ ∧ f i x ≠ −∞) ⇒
integrable m (λx. ∑ (λi. f i x) s)
[integrable_zero] Theorem
⊢ ∀m c. measure_space m ⇒ integrable m (λx. 0)
[integral_abs_eq_0] Theorem
⊢ ∀m f.
measure_space m ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
(∫ m (abs ∘ f) = 0 ⇔ AE x::m. (abs ∘ f) x = 0) ∧
((AE x::m. (abs ∘ f) x = 0) ⇔
measure m {x | x ∈ m_space m ∧ f x ≠ 0} = 0)
[integral_abs_imp_integrable] Theorem
⊢ ∀m f.
measure_space m ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
∫ m (abs ∘ f) = 0 ⇒
integrable m f
[integral_abs_pos_fn] Theorem
⊢ ∀m f. measure_space m ⇒ ∫ m (abs ∘ f) = ∫⁺ m (abs ∘ f)
[integral_add] Theorem
⊢ ∀m f g.
measure_space m ∧ integrable m f ∧ integrable m g ∧
(∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ g x ≠ −∞ ∨ f x ≠ +∞ ∧ g x ≠ +∞) ⇒
∫ m (λx. f x + g x) = ∫ m f + ∫ m g
[integral_add_lemma] Theorem
⊢ ∀m f f1 f2.
measure_space m ∧ integrable m f ∧ integrable m f1 ∧
integrable m f2 ∧ (∀x. x ∈ m_space m ⇒ f x = f1 x − f2 x) ∧
(∀x. x ∈ m_space m ⇒ 0 ≤ f1 x) ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f2 x) ∧
(∀x. x ∈ m_space m ⇒ f1 x ≠ +∞ ∨ f2 x ≠ +∞) ⇒
∫ m f = ∫⁺ m f1 − ∫⁺ m f2
[integral_add_lemma'] Theorem
⊢ ∀m f f1 f2.
measure_space m ∧ integrable m f ∧ integrable m f1 ∧
integrable m f2 ∧ (∀x. x ∈ m_space m ⇒ f x = f1 x − f2 x) ∧
(∀x. x ∈ m_space m ⇒ 0 ≤ f1 x) ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f2 x) ⇒
∫ m f = ∫⁺ m f1 − ∫⁺ m f2
[integral_cmul] Theorem
⊢ ∀m f c.
measure_space m ∧ integrable m f ⇒
∫ m (λx. Normal c * f x) = Normal c * ∫ m f
[integral_cmul_indicator] Theorem
⊢ ∀m s c.
measure_space m ∧ s ∈ measurable_sets m ∧ measure m s < +∞ ⇒
∫ m (λx. Normal c * 𝟙 s x) = Normal c * measure m s
[integral_cmul_infty] Theorem
⊢ ∀m s.
measure_space m ∧ s ∈ measurable_sets m ⇒
∫ m (λx. +∞ * 𝟙 s x) = +∞ * measure m s
[integral_cong] Theorem
⊢ ∀m f g.
measure_space m ∧ (∀x. x ∈ m_space m ⇒ f x = g x) ⇒ ∫ m f = ∫ m g
[integral_cong_AE] Theorem
⊢ ∀m f g. measure_space m ∧ (AE x::m. f x = g x) ⇒ ∫ m f = ∫ m g
[integral_const] Theorem
⊢ ∀m c.
measure_space m ∧ measure m (m_space m) < +∞ ⇒
∫ m (λx. Normal c) = Normal c * measure m (m_space m)
[integral_eq_0] Theorem
⊢ ∀m f.
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
measure_space m ∧ (AE x::m. 0 ≤ f x) ⇒
(∫ m f = 0 ⇔ measure m {x | x ∈ m_space m ∧ f x ≠ 0} = 0)
[integral_indicator] Theorem
⊢ ∀m s.
measure_space m ∧ s ∈ measurable_sets m ⇒ ∫ m (𝟙 s) = measure m s
[integral_indicator_pow] Theorem
⊢ ∀m s n.
measure_space m ∧ s ∈ measurable_sets m ∧ 0 < n ⇒
∫ m (λx. 𝟙 s x pow n) = measure m s
[integral_indicator_pow_eq] Theorem
⊢ ∀m s n.
measure_space m ∧ s ∈ measurable_sets m ∧ 0 < n ⇒
∫ m (λx. 𝟙 s x pow n) = ∫ m (𝟙 s)
[integral_mono] Theorem
⊢ ∀m f1 f2.
measure_space m ∧ integrable m f1 ∧ integrable m f2 ∧
(∀x. x ∈ m_space m ⇒ f1 x ≤ f2 x) ⇒
∫ m f1 ≤ ∫ m f2
[integral_mspace] Theorem
⊢ ∀m f. measure_space m ⇒ ∫ m f = ∫ m (λx. f x * 𝟙 (m_space m) x)
[integral_null_set] Theorem
⊢ ∀m f N.
measure_space m ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
N ∈ null_set m ⇒
integrable m (λx. f x * 𝟙 N x) ∧ ∫ m (λx. f x * 𝟙 N x) = 0
[integral_pos] Theorem
⊢ ∀m f. measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒ 0 ≤ ∫ m f
[integral_pos_fn] Theorem
⊢ ∀m f.
measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒ ∫ m f = ∫⁺ m f
[integral_posinf] Theorem
⊢ ∀m. measure_space m ∧ 0 < measure m (m_space m) ⇒ ∫ m (λx. +∞) = +∞
[integral_sequence] Theorem
⊢ ∀m f.
(∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ measure_space m ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
∫⁺ m f = sup (IMAGE (λi. ∫⁺ m (fn_seq m f i)) 𝕌(:num))
[integral_split] Theorem
⊢ ∀m f s.
measure_space m ∧ s ∈ measurable_sets m ∧
(∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
∫ m f =
∫ m (λx. f x * 𝟙 s x) + ∫ m (λx. f x * 𝟙 (m_space m DIFF s) x)
[integral_split'] Theorem
⊢ ∀m f s.
measure_space m ∧ integrable m f ∧ s ∈ measurable_sets m ⇒
∫ m f =
∫ m (λx. f x * 𝟙 s x) + ∫ m (λx. f x * 𝟙 (m_space m DIFF s) x)
[integral_sum] Theorem
⊢ ∀m f s.
FINITE s ∧ measure_space m ∧ (∀i. i ∈ s ⇒ integrable m (f i)) ∧
(∀x i. i ∈ s ∧ x ∈ m_space m ⇒ f i x ≠ +∞ ∧ f i x ≠ −∞) ⇒
∫ m (λx. ∑ (λi. f i x) s) = ∑ (λi. ∫ m (f i)) s
[integral_triangle_ineq] Theorem
⊢ ∀m f.
measure_space m ∧ integrable m f ⇒ abs (∫ m f) ≤ ∫ m (abs ∘ f)
[integral_triangle_ineq'] Theorem
⊢ ∀m f.
measure_space m ∧ integrable m f ⇒ abs (∫ m f) ≤ ∫⁺ m (abs ∘ f)
[integral_zero] Theorem
⊢ ∀m. measure_space m ⇒ ∫ m (λx. 0) = 0
[lebesgue_monotone_convergence] Theorem
⊢ ∀m f fi.
measure_space m ∧
(∀i. fi i ∈ Borel_measurable (m_space m,measurable_sets m)) ∧
(∀i x. x ∈ m_space m ⇒ 0 ≤ fi i x) ∧
(∀x. x ∈ m_space m ⇒ mono_increasing (λi. fi i x)) ∧
(∀x. x ∈ m_space m ⇒ sup (IMAGE (λi. fi i x) 𝕌(:num)) = f x) ⇒
∫⁺ m f = sup (IMAGE (λi. ∫⁺ m (fi i)) 𝕌(:num))
[lebesgue_monotone_convergence_AE] Theorem
⊢ ∀m f fi.
measure_space m ∧
(∀i. fi i ∈ Borel_measurable (m_space m,measurable_sets m)) ∧
(AE x::m. ∀i. fi i x ≤ fi (SUC i) x ∧ 0 ≤ fi i x) ∧
(∀x. x ∈ m_space m ⇒ sup (IMAGE (λi. fi i x) 𝕌(:num)) = f x) ⇒
∫⁺ m f⁺ = sup (IMAGE (λi. ∫⁺ m (fi i)⁺) 𝕌(:num))
[lebesgue_monotone_convergence_decreasing] Theorem
⊢ ∀m f fi.
measure_space m ∧
(∀i. fi i ∈ Borel_measurable (m_space m,measurable_sets m)) ∧
(∀i x. x ∈ m_space m ⇒ 0 ≤ fi i x ∧ fi i x < +∞) ∧
(∀i. ∫⁺ m (fi i) ≠ +∞) ∧
(∀x. x ∈ m_space m ⇒ mono_decreasing (λi. fi i x)) ∧
(∀x. x ∈ m_space m ⇒ inf (IMAGE (λi. fi i x) 𝕌(:num)) = f x) ⇒
∫⁺ m f = inf (IMAGE (λi. ∫⁺ m (fi i)) 𝕌(:num))
[lebesgue_monotone_convergence_subset] Theorem
⊢ ∀m f fi A.
measure_space m ∧
(∀i. fi i ∈ Borel_measurable (m_space m,measurable_sets m)) ∧
(∀i x. x ∈ m_space m ⇒ 0 ≤ fi i x) ∧
(∀x. x ∈ m_space m ⇒ sup (IMAGE (λi. fi i x) 𝕌(:num)) = f x) ∧
(∀x. x ∈ m_space m ⇒ mono_increasing (λi. fi i x)) ∧
A ∈ measurable_sets m ⇒
∫⁺ m (λx. f x * 𝟙 A x) =
sup (IMAGE (λi. ∫⁺ m (λx. fi i x * 𝟙 A x)) 𝕌(:num))
[lemma_fn_seq_measurable] Theorem
⊢ ∀m f n.
measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
fn_seq m f n ∈ Borel_measurable (m_space m,measurable_sets m)
[lemma_fn_seq_mono_increasing] Theorem
⊢ ∀m f x. 0 ≤ f x ⇒ mono_increasing (λn. fn_seq m f n x)
[lemma_fn_seq_positive] Theorem
⊢ ∀m f n x. 0 ≤ f x ⇒ 0 ≤ fn_seq m f n x
[lemma_fn_seq_sup] Theorem
⊢ ∀m f x.
x ∈ m_space m ∧ 0 ≤ f x ⇒
sup (IMAGE (λn. fn_seq m f n x) 𝕌(:num)) = f x
[markov_ineq] Theorem
⊢ ∀m f c.
measure_space m ∧ integrable m f ∧ 0 < c ⇒
measure m ({x | c ≤ abs (f x)} ∩ m_space m) ≤ c⁻¹ * ∫ m (abs ∘ f)
[markov_inequality] Theorem
⊢ ∀m f a c.
measure_space m ∧ integrable m f ∧ a ∈ measurable_sets m ∧ 0 < c ⇒
measure m ({x | c ≤ abs (f x)} ∩ a) ≤
c⁻¹ * ∫ m (λx. abs (f x) * 𝟙 a x)
[measurable_sequence] Theorem
⊢ ∀m f.
measure_space m ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
(∃fi ri.
(∀x. mono_increasing (λi. fi i x)) ∧
(∀x. x ∈ m_space m ⇒ sup (IMAGE (λi. fi i x) 𝕌(:num)) = f⁺ x) ∧
(∀i. ri i ∈ psfis m (fi i)) ∧ (∀i x. fi i x ≤ f⁺ x) ∧
(∀i x. 0 ≤ fi i x) ∧
∫⁺ m f⁺ = sup (IMAGE (λi. ∫⁺ m (fi i)) 𝕌(:num))) ∧
∃gi vi.
(∀x. mono_increasing (λi. gi i x)) ∧
(∀x. x ∈ m_space m ⇒ sup (IMAGE (λi. gi i x) 𝕌(:num)) = f⁻ x) ∧
(∀i. vi i ∈ psfis m (gi i)) ∧ (∀i x. gi i x ≤ f⁻ x) ∧
(∀i x. 0 ≤ gi i x) ∧
∫⁺ m f⁻ = sup (IMAGE (λi. ∫⁺ m (gi i)) 𝕌(:num))
[measure_density_indicator] Theorem
⊢ ∀m s t.
measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
measure (density m (𝟙 s)) t = measure m (s ∩ t)
[measure_restricted] Theorem
⊢ ∀m s t.
measure_space m ∧ s ∈ measurable_sets m ∧ t ∈ measurable_sets m ⇒
measure
(m_space m,measurable_sets m,(λA. ∫⁺ m (λx. 𝟙 s x * 𝟙 A x))) t =
measure m (s ∩ t)
[measure_space_density] Theorem
⊢ ∀m f.
measure_space m ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
(∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
measure_space (density m f)
[measure_space_density'] Theorem
⊢ ∀M f.
measure_space M ∧
f ∈ Borel_measurable (m_space M,measurable_sets M) ⇒
measure_space (density M f⁺)
[measure_space_distr] Theorem
⊢ ∀M B f.
measure_space M ∧ sigma_algebra B ∧
f ∈ measurable (m_space M,measurable_sets M) B ⇒
measure_space (space B,subsets B,distr M f)
[measure_subadditive_finite] Theorem
⊢ ∀I A M.
measure_space M ∧ FINITE I ∧ IMAGE A I ⊆ measurable_sets M ⇒
measure M (BIGUNION {A i | i ∈ I}) ≤ ∑ (λi. measure M (A i)) I
[pos_fn_integral_add] Theorem
⊢ ∀m f g.
measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
(∀x. x ∈ m_space m ⇒ 0 ≤ g x) ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
g ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
∫⁺ m (λx. f x + g x) = ∫⁺ m f + ∫⁺ m g
[pos_fn_integral_cmul] Theorem
⊢ ∀m f c.
measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ 0 ≤ c ⇒
∫⁺ m (λx. Normal c * f x) = Normal c * ∫⁺ m f
[pos_fn_integral_cmul_indicator] Theorem
⊢ ∀m s c.
measure_space m ∧ s ∈ measurable_sets m ∧ 0 ≤ c ⇒
∫⁺ m (λx. Normal c * 𝟙 s x) = Normal c * measure m s
[pos_fn_integral_cmul_infty] Theorem
⊢ ∀m s.
measure_space m ∧ s ∈ measurable_sets m ⇒
∫⁺ m (λx. +∞ * 𝟙 s x) = +∞ * measure m s
[pos_fn_integral_cmult] Theorem
⊢ ∀f c m.
measure_space m ∧ 0 ≤ c ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
∫⁺ m (λx. c * f⁺ x) = c * ∫⁺ m f⁺
[pos_fn_integral_cmult'] Theorem
⊢ ∀f c m.
measure_space m ∧ 0 ≤ c ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
∫⁺ m (λx. max 0 (c * f x)) = c * ∫⁺ m (λx. max 0 (f x))
[pos_fn_integral_cong] Theorem
⊢ ∀m u v.
measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ u x) ∧
(∀x. x ∈ m_space m ⇒ 0 ≤ v x) ∧ (∀x. x ∈ m_space m ⇒ u x = v x) ⇒
∫⁺ m u = ∫⁺ m v
[pos_fn_integral_cong_AE] Theorem
⊢ ∀m u v.
measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ u x) ∧
(∀x. x ∈ m_space m ⇒ 0 ≤ v x) ∧ (AE x::m. u x = v x) ⇒
∫⁺ m u = ∫⁺ m v
[pos_fn_integral_density] Theorem
⊢ ∀m f g.
measure_space m ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
g ∈ Borel_measurable (m_space m,measurable_sets m) ∧
(AE x::m. 0 ≤ f x) ∧ (∀x. 0 ≤ g x) ⇒
∫⁺ (density m f⁺) g = ∫⁺ m (λx. f⁺ x * g x)
[pos_fn_integral_density'] Theorem
⊢ ∀f g M.
measure_space M ∧
f ∈ Borel_measurable (m_space M,measurable_sets M) ∧
g ∈ Borel_measurable (m_space M,measurable_sets M) ∧
(AE x::M. 0 ≤ f x) ∧ (∀x. 0 ≤ g x) ⇒
∫⁺
(m_space M,measurable_sets M,
(λA. ∫⁺ M (λx. max 0 (f x * 𝟙 A x)))) (λx. max 0 (g x)) =
∫⁺ M (λx. max 0 (f x * g x))
[pos_fn_integral_disjoint_sets] Theorem
⊢ ∀m f s t.
measure_space m ∧ DISJOINT s t ∧ s ∈ measurable_sets m ∧
t ∈ measurable_sets m ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
(∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
∫⁺ m (λx. f x * 𝟙 (s ∪ t) x) =
∫⁺ m (λx. f x * 𝟙 s x) + ∫⁺ m (λx. f x * 𝟙 t x)
[pos_fn_integral_disjoint_sets_sum] Theorem
⊢ ∀m f s a.
FINITE s ∧ measure_space m ∧
(∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ∧
(∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
(∀i j. i ∈ s ∧ j ∈ s ∧ i ≠ j ⇒ DISJOINT (a i) (a j)) ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
∫⁺ m (λx. f x * 𝟙 (BIGUNION (IMAGE a s)) x) =
∑ (λi. ∫⁺ m (λx. f x * 𝟙 (a i) x)) s
[pos_fn_integral_eq_0] Theorem
⊢ ∀m f.
measure_space m ∧ nonneg f ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
(∫⁺ m f = 0 ⇔ measure m {x | x ∈ m_space m ∧ f x ≠ 0} = 0)
[pos_fn_integral_indicator] Theorem
⊢ ∀m s.
measure_space m ∧ s ∈ measurable_sets m ⇒
∫⁺ m (𝟙 s) = measure m s
[pos_fn_integral_infty_null] Theorem
⊢ ∀m f.
measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧ ∫⁺ m f ≠ +∞ ⇒
null_set m {x | x ∈ m_space m ∧ f x = +∞}
[pos_fn_integral_mono] Theorem
⊢ ∀m f g.
(∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ (∀x. x ∈ m_space m ⇒ f x ≤ g x) ⇒
∫⁺ m f ≤ ∫⁺ m g
[pos_fn_integral_mono_AE] Theorem
⊢ ∀m u v.
measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ u x) ∧
(∀x. x ∈ m_space m ⇒ 0 ≤ v x) ∧ (AE x::m. u x ≤ v x) ⇒
∫⁺ m u ≤ ∫⁺ m v
[pos_fn_integral_mspace] Theorem
⊢ ∀m f.
measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
∫⁺ m f = ∫⁺ m (λx. f x * 𝟙 (m_space m) x)
[pos_fn_integral_null_set] Theorem
⊢ ∀m f N.
measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ N ∈ null_set m ⇒
∫⁺ m (λx. f x * 𝟙 N x) = 0
[pos_fn_integral_pos] Theorem
⊢ ∀m f. measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒ 0 ≤ ∫⁺ m f
[pos_fn_integral_pos_simple_fn] Theorem
⊢ ∀m f s a x.
measure_space m ∧ pos_simple_fn m f s a x ⇒
∫⁺ m f = pos_simple_fn_integral m s a x
[pos_fn_integral_split] Theorem
⊢ ∀m f s.
measure_space m ∧ s ∈ measurable_sets m ∧
(∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ⇒
∫⁺ m f =
∫⁺ m (λx. f x * 𝟙 s x) + ∫⁺ m (λx. f x * 𝟙 (m_space m DIFF s) x)
[pos_fn_integral_sub] Theorem
⊢ ∀m f g.
measure_space m ∧
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
g ∈ Borel_measurable (m_space m,measurable_sets m) ∧
(∀x. x ∈ m_space m ⇒ 0 ≤ g x) ∧ (∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧
(∀x. x ∈ m_space m ⇒ g x ≠ +∞) ∧ ∫⁺ m g ≠ +∞ ⇒
∫⁺ m (λx. f x − g x) = ∫⁺ m f − ∫⁺ m g
[pos_fn_integral_sum] Theorem
⊢ ∀m f s.
FINITE s ∧ measure_space m ∧
(∀i. i ∈ s ⇒ ∀x. x ∈ m_space m ⇒ 0 ≤ f i x) ∧
(∀i. i ∈ s ⇒ f i ∈ Borel_measurable (m_space m,measurable_sets m)) ⇒
∫⁺ m (λx. ∑ (λi. f i x) s) = ∑ (λi. ∫⁺ m (f i)) s
[pos_fn_integral_sum_cmul_indicator] Theorem
⊢ ∀m s a x.
measure_space m ∧ FINITE s ∧ (∀i. i ∈ s ⇒ 0 ≤ x i) ∧
(∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ⇒
∫⁺ m (λt. ∑ (λi. Normal (x i) * 𝟙 (a i) t) s) =
∑ (λi. Normal (x i) * measure m (a i)) s
[pos_fn_integral_suminf] Theorem
⊢ ∀m f.
measure_space m ∧ (∀i x. x ∈ m_space m ⇒ 0 ≤ f i x) ∧
(∀i. f i ∈ Borel_measurable (m_space m,measurable_sets m)) ⇒
∫⁺ m (λx. suminf (λi. f i x)) = suminf (λi. ∫⁺ m (f i))
[pos_fn_integral_zero] Theorem
⊢ ∀m. measure_space m ⇒ ∫⁺ m (λx. 0) = 0
[pos_simple_fn_add] Theorem
⊢ ∀m f g s a x s' a' x'.
measure_space m ∧ pos_simple_fn m f s a x ∧
pos_simple_fn m g s' a' x' ⇒
∃s'' a'' x''. pos_simple_fn m (λt. f t + g t) s'' a'' x''
[pos_simple_fn_add_alt] Theorem
⊢ ∀m f g s a x y.
measure_space m ∧ pos_simple_fn m f s a x ∧
pos_simple_fn m g s a y ⇒
pos_simple_fn m (λt. f t + g t) s a (λi. x i + y i)
[pos_simple_fn_cmul] Theorem
⊢ ∀m f z s a x.
measure_space m ∧ pos_simple_fn m f s a x ∧ 0 ≤ z ⇒
∃s' a' x'. pos_simple_fn m (λt. Normal z * f t) s' a' x'
[pos_simple_fn_cmul_alt] Theorem
⊢ ∀m f s a x z.
measure_space m ∧ 0 ≤ z ∧ pos_simple_fn m f s a x ⇒
pos_simple_fn m (λt. Normal z * f t) s a (λi. z * x i)
[pos_simple_fn_indicator] Theorem
⊢ ∀m A.
measure_space m ∧ A ∈ measurable_sets m ⇒
∃s a x. pos_simple_fn m (𝟙 A) s a x
[pos_simple_fn_indicator_alt] Theorem
⊢ ∀m s.
measure_space m ∧ s ∈ measurable_sets m ⇒
pos_simple_fn m (𝟙 s) {0; 1}
(λi. if i = 0 then m_space m DIFF s else s)
(λi. if i = 0 then 0 else 1)
[pos_simple_fn_integral_add] Theorem
⊢ ∀m f s a x g s' b y.
measure_space m ∧ pos_simple_fn m f s a x ∧
pos_simple_fn m g s' b y ⇒
∃s'' c z.
pos_simple_fn m (λx. f x + g x) s'' c z ∧
pos_simple_fn_integral m s a x +
pos_simple_fn_integral m s' b y =
pos_simple_fn_integral m s'' c z
[pos_simple_fn_integral_add_alt] Theorem
⊢ ∀m f s a x g y.
measure_space m ∧ pos_simple_fn m f s a x ∧
pos_simple_fn m g s a y ⇒
pos_simple_fn_integral m s a x + pos_simple_fn_integral m s a y =
pos_simple_fn_integral m s a (λi. x i + y i)
[pos_simple_fn_integral_cmul] Theorem
⊢ ∀m f s a x z.
measure_space m ∧ pos_simple_fn m f s a x ∧ 0 ≤ z ⇒
pos_simple_fn m (λx. Normal z * f x) s a (λi. z * x i) ∧
pos_simple_fn_integral m s a (λi. z * x i) =
Normal z * pos_simple_fn_integral m s a x
[pos_simple_fn_integral_cmul_alt] Theorem
⊢ ∀m f s a x z.
measure_space m ∧ 0 ≤ z ∧ pos_simple_fn m f s a x ⇒
∃s' a' x'.
pos_simple_fn m (λt. Normal z * f t) s' a' x' ∧
pos_simple_fn_integral m s' a' x' =
Normal z * pos_simple_fn_integral m s a x
[pos_simple_fn_integral_indicator] Theorem
⊢ ∀m A.
measure_space m ∧ A ∈ measurable_sets m ⇒
∃s a x.
pos_simple_fn m (𝟙 A) s a x ∧
pos_simple_fn_integral m s a x = measure m A
[pos_simple_fn_integral_mono] Theorem
⊢ ∀m f s a x g s' b y.
measure_space m ∧ pos_simple_fn m f s a x ∧
pos_simple_fn m g s' b y ∧ (∀x. x ∈ m_space m ⇒ f x ≤ g x) ⇒
pos_simple_fn_integral m s a x ≤ pos_simple_fn_integral m s' b y
[pos_simple_fn_integral_not_infty] Theorem
⊢ ∀m f s a x.
measure_space m ∧ pos_simple_fn m f s a x ⇒
pos_simple_fn_integral m s a x ≠ −∞
[pos_simple_fn_integral_present] Theorem
⊢ ∀m f s a x g s' b y.
measure_space m ∧ pos_simple_fn m f s a x ∧
pos_simple_fn m g s' b y ⇒
∃z z' c k.
(∀t. t ∈ m_space m ⇒ f t = ∑ (λi. Normal (z i) * 𝟙 (c i) t) k) ∧
(∀t. t ∈ m_space m ⇒ g t = ∑ (λi. Normal (z' i) * 𝟙 (c i) t) k) ∧
pos_simple_fn_integral m s a x = pos_simple_fn_integral m k c z ∧
pos_simple_fn_integral m s' b y =
pos_simple_fn_integral m k c z' ∧ FINITE k ∧
(∀i. i ∈ k ⇒ 0 ≤ z i) ∧ (∀i. i ∈ k ⇒ 0 ≤ z' i) ∧
(∀i j. i ∈ k ∧ j ∈ k ∧ i ≠ j ⇒ DISJOINT (c i) (c j)) ∧
(∀i. i ∈ k ⇒ c i ∈ measurable_sets m) ∧
BIGUNION (IMAGE c k) = m_space m
[pos_simple_fn_integral_sub] Theorem
⊢ ∀m f s a x g s' b y.
measure_space m ∧ measure m (m_space m) ≠ +∞ ∧
(∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧
(∀x. x ∈ m_space m ⇒ g x ≠ +∞) ∧ pos_simple_fn m f s a x ∧
pos_simple_fn m g s' b y ⇒
∃s'' c z.
pos_simple_fn m (λx. f x − g x) s'' c z ∧
pos_simple_fn_integral m s a x −
pos_simple_fn_integral m s' b y =
pos_simple_fn_integral m s'' c z
[pos_simple_fn_integral_sum] Theorem
⊢ ∀m f s a x P.
measure_space m ∧ (∀i. i ∈ P ⇒ pos_simple_fn m (f i) s a (x i)) ∧
(∀i t. i ∈ P ⇒ f i t ≠ −∞) ∧ FINITE P ∧ P ≠ ∅ ⇒
pos_simple_fn m (λt. ∑ (λi. f i t) P) s a (λi. ∑ (λj. x j i) P) ∧
pos_simple_fn_integral m s a (λj. ∑ (λi. x i j) P) =
∑ (λi. pos_simple_fn_integral m s a (x i)) P
[pos_simple_fn_integral_sum_alt] Theorem
⊢ ∀m f s a x P.
measure_space m ∧
(∀i. i ∈ P ⇒ pos_simple_fn m (f i) (s i) (a i) (x i)) ∧
(∀i t. i ∈ P ⇒ f i t ≠ −∞) ∧ FINITE P ∧ P ≠ ∅ ⇒
∃c k z.
pos_simple_fn m (λt. ∑ (λi. f i t) P) k c z ∧
pos_simple_fn_integral m k c z =
∑ (λi. pos_simple_fn_integral m (s i) (a i) (x i)) P
[pos_simple_fn_integral_unique] Theorem
⊢ ∀m f s a x s' b y.
measure_space m ∧ pos_simple_fn m f s a x ∧
pos_simple_fn m f s' b y ⇒
pos_simple_fn_integral m s a x = pos_simple_fn_integral m s' b y
[pos_simple_fn_integral_zero] Theorem
⊢ ∀m s a x.
measure_space m ∧ pos_simple_fn m (λt. 0) s a x ⇒
pos_simple_fn_integral m s a x = 0
[pos_simple_fn_integral_zero_alt] Theorem
⊢ ∀m g s a x.
measure_space m ∧ pos_simple_fn m g s a x ∧
(∀x. x ∈ m_space m ⇒ g x = 0) ⇒
pos_simple_fn_integral m s a x = 0
[pos_simple_fn_le] Theorem
⊢ ∀m f g s a x x' i.
measure_space m ∧ pos_simple_fn m f s a x ∧
pos_simple_fn m g s a x' ∧ (∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧
i ∈ s ∧ a i ≠ ∅ ⇒
Normal (x' i) ≤ Normal (x i)
[pos_simple_fn_max] Theorem
⊢ ∀m f s a x g s' b y.
measure_space m ∧ pos_simple_fn m f s a x ∧
pos_simple_fn m g s' b y ⇒
∃s'' a'' x''. pos_simple_fn m (λx. max (f x) (g x)) s'' a'' x''
[pos_simple_fn_not_infty] Theorem
⊢ ∀m f s a x.
pos_simple_fn m f s a x ⇒ ∀x. x ∈ m_space m ⇒ f x ≠ −∞ ∧ f x ≠ +∞
[pos_simple_fn_thm1] Theorem
⊢ ∀m f s a x i y.
measure_space m ∧ pos_simple_fn m f s a x ∧ i ∈ s ∧ y ∈ a i ⇒
f y = Normal (x i)
[psfis_add] Theorem
⊢ ∀m f g a b.
measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m g ⇒
a + b ∈ psfis m (λx. f x + g x)
[psfis_cmul] Theorem
⊢ ∀m f a z.
measure_space m ∧ a ∈ psfis m f ∧ 0 ≤ z ⇒
Normal z * a ∈ psfis m (λx. Normal z * f x)
[psfis_indicator] Theorem
⊢ ∀m A.
measure_space m ∧ A ∈ measurable_sets m ⇒
measure m A ∈ psfis m (𝟙 A)
[psfis_intro] Theorem
⊢ ∀m a x P.
measure_space m ∧ (∀i. i ∈ P ⇒ a i ∈ measurable_sets m) ∧
(∀i. i ∈ P ⇒ 0 ≤ x i) ∧ FINITE P ⇒
∑ (λi. Normal (x i) * measure m (a i)) P ∈
psfis m (λt. ∑ (λi. Normal (x i) * 𝟙 (a i) t) P)
[psfis_mono] Theorem
⊢ ∀m f g a b.
measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m g ∧
(∀x. x ∈ m_space m ⇒ f x ≤ g x) ⇒
a ≤ b
[psfis_not_infty] Theorem
⊢ ∀m f a. measure_space m ∧ a ∈ psfis m f ⇒ a ≠ −∞
[psfis_pos] Theorem
⊢ ∀m f a.
measure_space m ∧ a ∈ psfis m f ⇒ ∀x. x ∈ m_space m ⇒ 0 ≤ f x
[psfis_present] Theorem
⊢ ∀m f g a b.
measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m g ⇒
∃z z' c k.
(∀t. t ∈ m_space m ⇒ f t = ∑ (λi. Normal (z i) * 𝟙 (c i) t) k) ∧
(∀t. t ∈ m_space m ⇒ g t = ∑ (λi. Normal (z' i) * 𝟙 (c i) t) k) ∧
a = pos_simple_fn_integral m k c z ∧
b = pos_simple_fn_integral m k c z' ∧ FINITE k ∧
(∀i. i ∈ k ⇒ 0 ≤ z i) ∧ (∀i. i ∈ k ⇒ 0 ≤ z' i) ∧
(∀i j. i ∈ k ∧ j ∈ k ∧ i ≠ j ⇒ DISJOINT (c i) (c j)) ∧
(∀i. i ∈ k ⇒ c i ∈ measurable_sets m) ∧
BIGUNION (IMAGE c k) = m_space m
[psfis_sub] Theorem
⊢ ∀m f g a b.
measure_space m ∧ measure m (m_space m) ≠ +∞ ∧
(∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧
(∀x. x ∈ m_space m ⇒ g x ≠ +∞) ∧ a ∈ psfis m f ∧ b ∈ psfis m g ⇒
a − b ∈ psfis m (λx. f x − g x)
[psfis_sum] Theorem
⊢ ∀m f a P.
measure_space m ∧ (∀i. i ∈ P ⇒ a i ∈ psfis m (f i)) ∧
(∀i t. i ∈ P ⇒ f i t ≠ −∞) ∧ FINITE P ⇒
∑ a P ∈ psfis m (λt. ∑ (λi. f i t) P)
[psfis_unique] Theorem
⊢ ∀m f a b. measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m f ⇒ a = b
[psfis_zero] Theorem
⊢ ∀m a. measure_space m ⇒ (a ∈ psfis m (λx. 0) ⇔ a = 0)
*)
end
HOL 4, Kananaskis-14