Theory "lebesgue"

Parents measure

Signature

Constant	Type
RADON_F	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> extreal) -> bool
RADON_F_integrals	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> extreal -> bool
finite_space_integral	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> extreal) -> extreal
fn_seq	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> extreal) -> num -> α -> extreal
fn_seq_integral	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> extreal) -> num -> extreal
integrable	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> extreal) -> bool
integral	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> extreal) -> extreal
max_fn_seq	:(num -> α -> extreal) -> num -> α -> extreal
measure_absolutely_continuous	:((α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real)) reln
negative_set	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> bool
pos_fn_integral	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> extreal) -> extreal
pos_simple_fn_integral	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (num -> bool) -> (num -> α -> bool) -> (num -> real) -> extreal
prod_measure	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (β -> bool) # ((β -> bool) -> bool) # ((β -> bool) -> real) -> (α # β -> bool) -> real
prod_measure3	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (β -> bool) # ((β -> bool) -> bool) # ((β -> bool) -> real) -> (γ -> bool) # ((γ -> bool) -> bool) # ((γ -> bool) -> real) -> (α # β # γ -> bool) -> real
prod_measure_space	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (β -> bool) # ((β -> bool) -> bool) # ((β -> bool) -> real) -> (α # β -> bool) # ((α # β -> bool) -> bool) # ((α # β -> bool) -> real)
prod_measure_space3	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (β -> bool) # ((β -> bool) -> bool) # ((β -> bool) -> real) -> (γ -> bool) # ((γ -> bool) -> bool) # ((γ -> bool) -> real) -> (α # β # γ -> bool) # ((α # β # γ -> bool) -> bool) # ((α # β # γ -> bool) -> real)
prod_sets3	:((α -> bool) -> bool) -> ((β -> bool) -> bool) -> ((γ -> bool) -> bool) -> (α # β # γ -> bool) -> bool
psfis	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> extreal) -> extreal -> bool
psfs	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> extreal) -> (num -> bool) # (num -> α -> bool) # (num -> real) -> bool
seq_sup	:(extreal -> bool) -> num -> extreal
signed_measure_space	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool

Definitions

pos_simple_fn_integral_def

|- ∀m s a x.
     pos_simple_fn_integral m s a x =
     Normal (SIGMA (λi. x i * measure m (a i)) s)

psfs_def

|- ∀m f. psfs m f = {(s,a,x) | pos_simple_fn m f s a x}

psfis_def

|- ∀m f.
     psfis m f = IMAGE (λ(s,a,x). pos_simple_fn_integral m s a x) (psfs m f)

pos_fn_integral_def

|- ∀m f. pos_fn_integral m f = sup {r | ∃g. r ∈ psfis m g ∧ ∀x. g x ≤ f x}

integral_def

|- ∀m f.
     integral m f =
     pos_fn_integral m (fn_plus f) − pos_fn_integral m (fn_minus f)

integrable_def

|- ∀m f.
     integrable m f ⇔
     f ∈ measurable (m_space m,measurable_sets m) Borel ∧
     pos_fn_integral m (fn_plus f) ≠ PosInf ∧
     pos_fn_integral m (fn_minus f) ≠ PosInf

finite_space_integral_def

|- ∀m f.
     finite_space_integral m f =
     SIGMA (λr. r * Normal (measure m (PREIMAGE f {r} ∩ m_space m)))
       (IMAGE f (m_space m))

prod_measure_def

|- ∀m0 m1.
     prod_measure m0 m1 =
     (λa.
        real
          (integral m0
             (λs0. Normal (measure m1 (PREIMAGE (λs1. (s0,s1)) a)))))

prod_measure_space_def

|- ∀m0 m1.
     prod_measure_space m0 m1 =
     (m_space m0 × m_space m1,
      subsets
        (sigma (m_space m0 × m_space m1)
           (prod_sets (measurable_sets m0) (measurable_sets m1))),
      prod_measure m0 m1)

prod_sets3_def

|- ∀a b c. prod_sets3 a b c = {s × (t × u) | s ∈ a ∧ t ∈ b ∧ u ∈ c}

prod_measure3_def

|- ∀m0 m1 m2.
     prod_measure3 m0 m1 m2 = prod_measure m0 (prod_measure_space m1 m2)

prod_measure_space3_def

|- ∀m0 m1 m2.
     prod_measure_space3 m0 m1 m2 =
     (m_space m0 × (m_space m1 × m_space m2),
      subsets
        (sigma (m_space m0 × (m_space m1 × m_space m2))
           (prod_sets3 (measurable_sets m0) (measurable_sets m1)
              (measurable_sets m2))),prod_measure3 m0 m1 m2)

fn_seq_def

|- ∀m f.
     fn_seq m f =
     (λn x.
        SIGMA
          (λk.
             &k / 2 pow n *
             indicator_fn
               {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 * indicator_fn {x | x ∈ m_space m ∧ 2 pow n ≤ f x} x)

fn_seq_integral_def

|- ∀m f.
     fn_seq_integral m f =
     (λn.
        Normal
          (SIGMA
             (λ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}))

seq_sup_def

|- (∀P. seq_sup P 0 = @r. r ∈ P ∧ sup P < r + 1) ∧
   ∀P n.
     seq_sup P (SUC n) =
     @r.
       r ∈ P ∧ sup P < r + Normal ((1 / 2) pow SUC n) ∧ seq_sup P n < r ∧
       r < sup P

max_fn_seq_def

|- (∀g x. max_fn_seq g 0 x = g 0 x) ∧
   ∀g n x. max_fn_seq g (SUC n) x = max (max_fn_seq g n x) (g (SUC n) x)

signed_measure_space_def

|- ∀m.
     signed_measure_space m ⇔
     sigma_algebra (m_space m,measurable_sets m) ∧ countably_additive m

negative_set_def

|- ∀m A.
     negative_set m A ⇔
     A ∈ measurable_sets m ∧
     ∀s. s ∈ measurable_sets m ∧ s ⊆ A ⇒ measure m s ≤ 0

RADON_F_def

|- ∀m v.
     RADON_F m v =
     {f |
      f ∈ measurable (m_space m,measurable_sets m) Borel ∧ (∀x. 0 ≤ f x) ∧
      ∀A.
        A ∈ measurable_sets m ⇒
        pos_fn_integral m (λx. f x * indicator_fn A x) ≤ Normal (measure v A)}

RADON_F_integrals_def

|- ∀m v.
     RADON_F_integrals m v =
     {r | ∃f. (r = pos_fn_integral m f) ∧ f ∈ RADON_F m v}

measure_absolutely_continuous_def

|- ∀m v.
     measure_absolutely_continuous m v ⇔
     ∀A. A ∈ measurable_sets m ∧ (measure v A = 0) ⇒ (measure m A = 0)

Theorems

pos_simple_fn_integral_present

|- ∀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 = SIGMA (λi. Normal (z i) * indicator_fn (c i) t) k)) ∧
       (∀t.
          t ∈ m_space m ⇒
          (g t = SIGMA (λi. Normal (z' i) * indicator_fn (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)

psfis_present

|- ∀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 = SIGMA (λi. Normal (z i) * indicator_fn (c i) t) k)) ∧
       (∀t.
          t ∈ m_space m ⇒
          (g t = SIGMA (λi. Normal (z' i) * indicator_fn (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)

pos_simple_fn_thm1

|- ∀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))

pos_simple_fn_le

|- ∀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_cmul

|- ∀m f z.
     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

|- ∀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_add

|- ∀m f g.
     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

|- ∀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_indicator

|- ∀m A.
     measure_space m ∧ A ∈ measurable_sets m ⇒
     ∃s a x. pos_simple_fn m (indicator_fn A) s a x

pos_simple_fn_indicator_alt

|- ∀m s.
     measure_space m ∧ s ∈ measurable_sets m ⇒
     pos_simple_fn m (indicator_fn 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_max

|- ∀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

|- ∀m f s a x.
     pos_simple_fn m f s a x ⇒ ∀x. x ∈ m_space m ⇒ f x ≠ NegInf ∧ f x ≠ PosInf

pos_simple_fn_integral_add

|- ∀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

|- ∀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))

psfis_add

|- ∀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)

pos_simple_fn_integral_mono

|- ∀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

psfis_mono

|- ∀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

pos_simple_fn_integral_unique

|- ∀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)

psfis_unique

|- ∀m f a b. measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m f ⇒ (a = b)

pos_simple_fn_integral_indicator

|- ∀m A.
     measure_space m ∧ A ∈ measurable_sets m ⇒
     ∃s a x.
       pos_simple_fn m (indicator_fn A) s a x ∧
       (pos_simple_fn_integral m s a x = Normal (measure m A))

psfis_indicator

|- ∀m A.
     measure_space m ∧ A ∈ measurable_sets m ⇒
     Normal (measure m A) ∈ psfis m (indicator_fn A)

pos_simple_fn_integral_cmul

|- ∀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)

psfis_cmul

|- ∀m f a z.
     measure_space m ∧ a ∈ psfis m f ∧ 0 ≤ z ⇒
     Normal z * a ∈ psfis m (λx. Normal z * f x)

pos_simple_fn_integral_cmul_alt

|- ∀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)

IN_psfis

|- ∀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

|- ∀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)

psfis_pos

|- ∀m f a. measure_space m ∧ a ∈ psfis m f ⇒ ∀x. x ∈ m_space m ⇒ 0 ≤ f x

pos_simple_fn_integral_zero

|- ∀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

|- ∀m 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)

psfis_zero

|- ∀m a. measure_space m ⇒ (a ∈ psfis m (λx. 0) ⇔ (a = 0))

pos_simple_fn_integral_not_infty

|- ∀m s a x.
     pos_simple_fn_integral m s a x ≠ NegInf ∧
     pos_simple_fn_integral m s a x ≠ PosInf

psfis_not_infty

|- ∀m f a. a ∈ psfis m f ⇒ a ≠ NegInf ∧ a ≠ PosInf

pos_simple_fn_integral_sum

|- ∀m f s a x P.
     measure_space m ∧ (∀i. i ∈ P ⇒ pos_simple_fn m (f i) s a (x i)) ∧
     FINITE P ∧ P ≠ ∅ ⇒
     pos_simple_fn m (λt. SIGMA (λi. f i t) P) s a (λi. SIGMA (λj. x j i) P) ∧
     (pos_simple_fn_integral m s a (λj. SIGMA (λi. x i j) P) =
      SIGMA (λi. pos_simple_fn_integral m s a (x i)) P)

pos_simple_fn_integral_sum_alt

|- ∀m f s a x P.
     measure_space m ∧ (∀i. i ∈ P ⇒ pos_simple_fn m (f i) (s i) (a i) (x i)) ∧
     FINITE P ∧ P ≠ ∅ ⇒
     ∃c k z.
       pos_simple_fn m (λt. SIGMA (λi. f i t) P) k c z ∧
       (pos_simple_fn_integral m k c z =
        SIGMA (λi. pos_simple_fn_integral m (s i) (a i) (x i)) P)

psfis_sum

|- ∀m f a P.
     measure_space m ∧ (∀i. i ∈ P ⇒ a i ∈ psfis m (f i)) ∧ FINITE P ⇒
     SIGMA a P ∈ psfis m (λt. SIGMA (λi. f i t) P)

psfis_intro

|- ∀m a x P.
     measure_space m ∧ (∀i. i ∈ P ⇒ a i ∈ measurable_sets m) ∧
     (∀i. i ∈ P ⇒ 0 ≤ x i) ∧ FINITE P ⇒
     Normal (SIGMA (λi. x i * measure m (a i)) P) ∈
     psfis m (λt. SIGMA (λi. Normal (x i) * indicator_fn (a i) t) P)

pos_simple_fn_integral_sub

|- ∀m f s a x g s' b y.
     measure_space m ∧ (∀x. g x ≤ f x) ∧ (∀x. g x ≠ PosInf) ∧
     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)

psfis_sub

|- ∀m f g a b.
     measure_space m ∧ (∀x. g x ≤ f x) ∧ (∀x. g x ≠ PosInf) ∧ a ∈ psfis m f ∧
     b ∈ psfis m g ⇒
     a − b ∈ psfis m (λx. f x − g x)

pos_fn_integral_pos_simple_fn

|- ∀m f s a x.
     measure_space m ∧ pos_simple_fn m f s a x ⇒
     (pos_fn_integral m f = pos_simple_fn_integral m s a x)

pos_fn_integral_mspace

|- ∀m f.
     measure_space m ∧ (∀x. 0 ≤ f x) ⇒
     (pos_fn_integral m f =
      pos_fn_integral m (λx. f x * indicator_fn (m_space m) x))

pos_fn_integral_zero

|- ∀m. measure_space m ⇒ (pos_fn_integral m (λx. 0) = 0)

pos_fn_integral_mono

|- ∀f g. (∀x. 0 ≤ f x ∧ f x ≤ g x) ⇒ pos_fn_integral m f ≤ pos_fn_integral m g

pos_fn_integral_mono_mspace

|- ∀m f g.
     measure_space m ∧ (∀x. x ∈ m_space m ⇒ g x ≤ f x) ∧ (∀x. 0 ≤ f x) ∧
     (∀x. 0 ≤ g x) ⇒
     pos_fn_integral m g ≤ pos_fn_integral m f

pos_fn_integral_pos

|- ∀m f. measure_space m ∧ (∀x. 0 ≤ f x) ⇒ 0 ≤ pos_fn_integral m f

pos_fn_integral_cmul

|- ∀f c.
     measure_space m ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ∧ 0 ≤ c ⇒
     (pos_fn_integral m (λx. Normal c * f x) = Normal c * pos_fn_integral m f)

pos_fn_integral_indicator

|- ∀m s.
     measure_space m ∧ s ∈ measurable_sets m ⇒
     (pos_fn_integral m (indicator_fn s) = Normal (measure m s))

pos_fn_integral_cmul_indicator

|- ∀m s c.
     measure_space m ∧ s ∈ measurable_sets m ∧ 0 ≤ c ⇒
     (pos_fn_integral m (λx. Normal c * indicator_fn s x) =
      Normal (c * measure m s))

pos_fn_integral_sum_cmul_indicator

|- ∀m s a x.
     measure_space m ∧ FINITE s ∧ (∀i. i ∈ s ⇒ 0 ≤ x i) ∧
     (∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ⇒
     (pos_fn_integral m
        (λt. SIGMA (λi. Normal (x i) * indicator_fn (a i) t) s) =
      Normal (SIGMA (λi. x i * measure m (a i)) s))

lebesgue_monotone_convergence_lemma

|- ∀m f fi g r'.
     measure_space m ∧
     (∀i. fi i ∈ measurable (m_space m,measurable_sets m) Borel) ∧
     (∀x. mono_increasing (λi. fi i x)) ∧
     (∀x. x ∈ m_space m ⇒ (sup (IMAGE (λi. fi i x) 𝕌(:num)) = f x)) ∧
     r' ∈ psfis m g ∧ (∀x. g x ≤ f x) ∧ (∀i x. 0 ≤ fi i x) ⇒
     r' ≤ sup (IMAGE (λi. pos_fn_integral m (fi i)) 𝕌(:num))

lebesgue_monotone_convergence

|- ∀m f fi.
     measure_space m ∧
     (∀i. fi i ∈ measurable (m_space m,measurable_sets m) Borel) ∧
     (∀i x. 0 ≤ fi i x) ∧ (∀x. 0 ≤ f x) ∧ (∀x. mono_increasing (λi. fi i x)) ∧
     (∀x. x ∈ m_space m ⇒ (sup (IMAGE (λi. fi i x) 𝕌(:num)) = f x)) ⇒
     (pos_fn_integral m f =
      sup (IMAGE (λi. pos_fn_integral m (fi i)) 𝕌(:num)))

lebesgue_monotone_convergence_subset

|- ∀m f fi A.
     measure_space m ∧
     (∀i. fi i ∈ measurable (m_space m,measurable_sets m) Borel) ∧
     (∀i x. 0 ≤ fi i x) ∧ (∀x. 0 ≤ f x) ∧
     (∀x. x ∈ m_space m ⇒ (sup (IMAGE (λi. fi i x) 𝕌(:num)) = f x)) ∧
     (∀x. mono_increasing (λi. fi i x)) ∧ A ∈ measurable_sets m ⇒
     (pos_fn_integral m (λx. f x * indicator_fn A x) =
      sup
        (IMAGE (λi. pos_fn_integral m (λx. fi i x * indicator_fn A x))
           𝕌(:num)))

lemma_fn_1

|- ∀m f n x k.
     x ∈ m_space m ∧ k ∈ count (4 ** n) ∧ &k / 2 pow n ≤ f x ∧
     f x < (&k + 1) / 2 pow n ⇒
     (fn_seq m f n x = &k / 2 pow n)

lemma_fn_2

|- ∀m f n x. x ∈ m_space m ∧ 2 pow n ≤ f x ⇒ (fn_seq m f n x = 2 pow n)

lemma_fn_3

|- ∀m f n x.
     x ∈ m_space m ∧ 0 ≤ f x ⇒
     2 pow n ≤ f x ∨
     ∃k. k ∈ count (4 ** n) ∧ &k / 2 pow n ≤ f x ∧ f x < (&k + 1) / 2 pow n

lemma_fn_4

|- ∀m f n x. x ∉ m_space m ⇒ (fn_seq m f n x = 0)

lemma_fn_5

|- ∀m f n x. 0 ≤ f x ⇒ 0 ≤ fn_seq m f n x

lemma_fn_mono_increasing

|- ∀m f x. 0 ≤ f x ⇒ mono_increasing (λn. fn_seq m f n x)

lemma_fn_upper_bounded

|- ∀m f n x. 0 ≤ f x ⇒ fn_seq m f n x ≤ f x

lemma_fn_sup

|- ∀m f x.
     x ∈ m_space m ∧ 0 ≤ f x ⇒
     (sup (IMAGE (λn. fn_seq m f n x) 𝕌(:num)) = f x)

lemma_fn_in_psfis

|- ∀m f n.
     (∀x. 0 ≤ f x) ∧ measure_space m ∧
     f ∈ measurable (m_space m,measurable_sets m) Borel ⇒
     fn_seq_integral m f n ∈ psfis m (fn_seq m f n)

integral_sequence

|- ∀m f.
     (∀x. 0 ≤ f x) ∧ measure_space m ∧
     f ∈ measurable (m_space m,measurable_sets m) Borel ⇒
     (pos_fn_integral m f =
      sup (IMAGE (λi. pos_fn_integral m (fn_seq m f i)) 𝕌(:num)))

measurable_sequence

|- ∀m f.
     measure_space m ∧ f ∈ measurable (m_space m,measurable_sets m) Borel ⇒
     (∃fi ri.
        (∀x. mono_increasing (λi. fi i x)) ∧
        (∀x.
           x ∈ m_space m ⇒ (sup (IMAGE (λi. fi i x) 𝕌(:num)) = fn_plus f x)) ∧
        (∀i. ri i ∈ psfis m (fi i)) ∧ (∀i x. fi i x ≤ fn_plus f x) ∧
        (∀i x. 0 ≤ fi i x) ∧
        (pos_fn_integral m (fn_plus f) =
         sup (IMAGE (λi. pos_fn_integral 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)) = fn_minus f x)) ∧
       (∀i. vi i ∈ psfis m (gi i)) ∧ (∀i x. gi i x ≤ fn_minus f x) ∧
       (∀i x. 0 ≤ gi i x) ∧
       (pos_fn_integral m (fn_minus f) =
        sup (IMAGE (λi. pos_fn_integral m (gi i)) 𝕌(:num)))

pos_fn_integral_add

|- ∀m f g.
     measure_space m ∧ (∀x. 0 ≤ f x ∧ 0 ≤ g x) ∧
     f ∈ measurable (m_space m,measurable_sets m) Borel ∧
     g ∈ measurable (m_space m,measurable_sets m) Borel ⇒
     (pos_fn_integral m (λx. f x + g x) =
      pos_fn_integral m f + pos_fn_integral m g)

pos_fn_integral_sum

|- ∀m f s.
     FINITE s ∧ measure_space m ∧ (∀i. i ∈ s ⇒ ∀x. 0 ≤ f i x) ∧
     (∀i. i ∈ s ⇒ f i ∈ measurable (m_space m,measurable_sets m) Borel) ⇒
     (pos_fn_integral m (λx. SIGMA (λi. f i x) s) =
      SIGMA (λi. pos_fn_integral m (f i)) s)

pos_fn_integral_disjoint_sets

|- ∀m f s t.
     measure_space m ∧ DISJOINT s t ∧ s ∈ measurable_sets m ∧
     t ∈ measurable_sets m ∧
     f ∈ measurable (m_space m,measurable_sets m) Borel ∧ (∀x. 0 ≤ f x) ⇒
     (pos_fn_integral m (λx. f x * indicator_fn (s ∪ t) x) =
      pos_fn_integral m (λx. f x * indicator_fn s x) +
      pos_fn_integral m (λx. f x * indicator_fn t x))

pos_fn_integral_disjoint_sets_sum

|- ∀m f s a.
     FINITE s ∧ measure_space m ∧ (∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ∧
     (∀x. 0 ≤ f x) ∧ (∀i j. i ∈ s ∧ j ∈ s ∧ i ≠ j ⇒ DISJOINT (a i) (a j)) ∧
     f ∈ measurable (m_space m,measurable_sets m) Borel ⇒
     (pos_fn_integral m (λx. f x * indicator_fn (BIGUNION (IMAGE a s)) x) =
      SIGMA (λi. pos_fn_integral m (λx. f x * indicator_fn (a i) x)) s)

pos_fn_integral_split

|- ∀m f s.
     measure_space m ∧ s ∈ measurable_sets m ∧ (∀x. 0 ≤ f x) ∧
     f ∈ measurable (m_space m,measurable_sets m) Borel ⇒
     (pos_fn_integral m f =
      pos_fn_integral m (λx. f x * indicator_fn s x) +
      pos_fn_integral m (λx. f x * indicator_fn (m_space m DIFF s) x))

pos_fn_integral_cmul_infty

|- ∀m s.
     measure_space m ∧ s ∈ measurable_sets m ⇒
     (pos_fn_integral m (λx. PosInf * indicator_fn s x) =
      PosInf * Normal (measure m s))

pos_fn_integral_suminf

|- ∀m f.
     measure_space m ∧ (∀i x. 0 ≤ f i x) ∧
     (∀i. f i ∈ measurable (m_space m,measurable_sets m) Borel) ⇒
     (pos_fn_integral m (λx. suminf (λi. f i x)) =
      suminf (λi. pos_fn_integral m (f i)))

integral_pos_fn

|- ∀m f.
     measure_space m ∧ (∀x. 0 ≤ f x) ⇒ (integral m f = pos_fn_integral m f)

integrable_pos

|- ∀m f.
     measure_space m ∧ (∀x. 0 ≤ f x) ⇒
     (integrable m f ⇔
      f ∈ measurable (m_space m,measurable_sets m) Borel ∧
      pos_fn_integral m f ≠ PosInf)

integrable_infty

|- ∀m f s.
     measure_space m ∧ integrable m f ∧ s ∈ measurable_sets m ∧
     (∀x. x ∈ s ⇒ (f x = PosInf)) ⇒
     (measure m s = 0)

integrable_infty_null

|- ∀m f.
     measure_space m ∧ integrable m f ⇒
     null_set m {x | x ∈ m_space m ∧ (f x = PosInf)}

integrable_bounded

|- ∀m f g.
     measure_space m ∧ integrable m f ∧
     g ∈ measurable (m_space m,measurable_sets m) Borel ∧
     (∀x. abs (g x) ≤ f x) ⇒
     integrable m g

integrable_fn_plus

|- ∀m f. measure_space m ∧ integrable m f ⇒ integrable m (fn_plus f)

integrable_fn_minus

|- ∀m f. measure_space m ∧ integrable m f ⇒ integrable m (fn_minus f)

integrable_const

|- ∀m c. measure_space m ⇒ integrable m (λx. Normal c)

integrable_zero

|- ∀m c. measure_space m ⇒ integrable m (λx. 0)

integrable_plus_minus

|- ∀m f.
     measure_space m ⇒
     (integrable m f ⇔
      f ∈ measurable (m_space m,measurable_sets m) Borel ∧
      integrable m (fn_plus f) ∧ integrable m (fn_minus f))

integrable_add_pos

|- ∀m f g.
     measure_space m ∧ integrable m f ∧ integrable m g ∧ (∀x. 0 ≤ f x) ∧
     (∀x. 0 ≤ g x) ⇒
     integrable m (λx. f x + g x)

integrable_add_lemma

|- ∀m f g.
     measure_space m ∧ integrable m f ∧ integrable m g ⇒
     integrable m (λx. fn_plus f x + fn_plus g x) ∧
     integrable m (λx. fn_minus f x + fn_minus g x)

integrable_add

|- ∀m f1 f2.
     measure_space m ∧ integrable m f1 ∧ integrable m f2 ⇒
     integrable m (λx. f1 x + f2 x)

integrable_cmul

|- ∀m f c.
     measure_space m ∧ integrable m f ⇒ integrable m (λx. Normal c * f x)

integrable_sub

|- ∀m f1 f2.
     measure_space m ∧ integrable m f1 ∧ integrable m f2 ⇒
     integrable m (λx. f1 x − f2 x)

integrable_indicator

|- ∀m s.
     measure_space m ∧ s ∈ measurable_sets m ⇒ integrable m (indicator_fn s)

integrable_not_infty

|- ∀m f.
     measure_space m ∧ integrable m f ∧ (∀x. 0 ≤ f x) ⇒
     ∃g.
       integrable m g ∧ (∀x. 0 ≤ g x) ∧ (∀x. x ∈ m_space m ⇒ g x ≠ PosInf) ∧
       (integral m f = integral m g)

integrable_not_infty_alt

|- ∀m f.
     measure_space m ∧ integrable m f ∧ (∀x. 0 ≤ f x) ⇒
     integrable m (λx. if f x = PosInf then 0 else f x) ∧
     (integral m f = integral m (λx. if f x = PosInf then 0 else f x))

integrable_not_infty_alt2

|- ∀m f.
     measure_space m ∧ integrable m f ∧ (∀x. 0 ≤ f x) ⇒
     integrable m (λx. if f x = PosInf then 0 else f x) ∧
     (pos_fn_integral m f =
      pos_fn_integral m (λx. if f x = PosInf then 0 else f x))

integrable_not_infty_alt3

|- ∀m f.
     measure_space m ∧ integrable m f ⇒
     integrable m (λx. if (f x = NegInf) ∨ (f x = PosInf) then 0 else f x) ∧
     (integral m f =
      integral m (λx. if (f x = NegInf) ∨ (f x = PosInf) then 0 else f x))

integral_indicator

|- ∀m s.
     measure_space m ∧ s ∈ measurable_sets m ⇒
     (integral m (indicator_fn s) = Normal (measure m s))

integral_add_lemma

|- ∀m f f1 f2.
     measure_space m ∧ integrable m f ∧ integrable m f1 ∧ integrable m f2 ∧
     (f = (λx. f1 x − f2 x)) ∧ (∀x. 0 ≤ f1 x) ∧ (∀x. 0 ≤ f2 x) ⇒
     (integral m f = pos_fn_integral m f1 − pos_fn_integral m f2)

integral_add

|- ∀m f g.
     measure_space m ∧ integrable m f ∧ integrable m g ⇒
     (integral m (λx. f x + g x) = integral m f + integral m g)

integral_cmul

|- ∀m f c.
     measure_space m ∧ integrable m f ⇒
     (integral m (λx. Normal c * f x) = Normal c * integral m f)

integral_cmul_indicator

|- ∀m s c.
     measure_space m ∧ s ∈ measurable_sets m ⇒
     (integral m (λx. Normal c * indicator_fn s x) = Normal (c * measure m s))

integral_zero

|- ∀m. measure_space m ⇒ (integral m (λx. 0) = 0)

integral_mspace

|- ∀m f.
     measure_space m ⇒
     (integral m f = integral m (λx. f x * indicator_fn (m_space m) x))

integral_mono

|- ∀m f1 f2.
     measure_space m ∧ (∀t. t ∈ m_space m ⇒ f1 t ≤ f2 t) ⇒
     integral m f1 ≤ integral m f2

finite_space_integral_reduce

|- ∀m f.
     measure_space m ∧ f ∈ measurable (m_space m,measurable_sets m) Borel ∧
     (∀x. x ∈ m_space m ⇒ f x ≠ NegInf ∧ f x ≠ PosInf) ∧ FINITE (m_space m) ⇒
     (integral m f = finite_space_integral m f)

finite_support_integral_reduce

|- ∀m f.
     measure_space m ∧ f ∈ measurable (m_space m,measurable_sets m) Borel ∧
     (∀x. x ∈ m_space m ⇒ f x ≠ NegInf ∧ f x ≠ PosInf) ∧
     FINITE (IMAGE f (m_space m)) ⇒
     (integral m f = finite_space_integral m f)

finite_space_POW_integral_reduce

|- ∀m f.
     measure_space m ∧ (POW (m_space m) = measurable_sets m) ∧
     FINITE (m_space m) ∧ (∀x. x ∈ m_space m ⇒ f x ≠ NegInf ∧ f x ≠ PosInf) ⇒
     (integral m f = SIGMA (λx. f x * Normal (measure m {x})) (m_space m))

finite_POW_prod_measure_reduce

|- ∀m0 m1.
     measure_space m0 ∧ measure_space m1 ∧ FINITE (m_space m0) ∧
     FINITE (m_space m1) ∧ (POW (m_space m0) = measurable_sets m0) ∧
     (POW (m_space m1) = measurable_sets m1) ⇒
     ∀a0 a1.
       a0 ∈ measurable_sets m0 ∧ a1 ∈ measurable_sets m1 ⇒
       (prod_measure m0 m1 (a0 × a1) = measure m0 a0 * measure m1 a1)

measure_space_finite_prod_measure_POW1

|- ∀m0 m1.
     measure_space m0 ∧ measure_space m1 ∧ FINITE (m_space m0) ∧
     FINITE (m_space m1) ∧ (POW (m_space m0) = measurable_sets m0) ∧
     (POW (m_space m1) = measurable_sets m1) ⇒
     measure_space (prod_measure_space m0 m1)

measure_space_finite_prod_measure_POW2

|- ∀m0 m1.
     measure_space m0 ∧ measure_space m1 ∧ FINITE (m_space m0) ∧
     FINITE (m_space m1) ∧ (POW (m_space m0) = measurable_sets m0) ∧
     (POW (m_space m1) = measurable_sets m1) ⇒
     measure_space
       (m_space m0 × m_space m1,POW (m_space m0 × m_space m1),
        prod_measure m0 m1)

finite_prod_measure_space_POW

|- ∀s1 s2 u v.
     FINITE s1 ∧ FINITE s2 ⇒
     (prod_measure_space (s1,POW s1,u) (s2,POW s2,v) =
      (s1 × s2,POW (s1 × s2),prod_measure (s1,POW s1,u) (s2,POW s2,v)))

finite_POW_prod_measure_reduce3

|- ∀m0 m1 m2.
     measure_space m0 ∧ measure_space m1 ∧ measure_space m2 ∧
     FINITE (m_space m0) ∧ FINITE (m_space m1) ∧ FINITE (m_space m2) ∧
     (POW (m_space m0) = measurable_sets m0) ∧
     (POW (m_space m1) = measurable_sets m1) ∧
     (POW (m_space m2) = measurable_sets m2) ⇒
     ∀a0 a1 a2.
       a0 ∈ measurable_sets m0 ∧ a1 ∈ measurable_sets m1 ∧
       a2 ∈ measurable_sets m2 ⇒
       (prod_measure3 m0 m1 m2 (a0 × (a1 × a2)) =
        measure m0 a0 * measure m1 a1 * measure m2 a2)

measure_space_finite_prod_measure_POW3

|- ∀m0 m1 m2.
     measure_space m0 ∧ measure_space m1 ∧ measure_space m2 ∧
     FINITE (m_space m0) ∧ FINITE (m_space m1) ∧ FINITE (m_space m2) ∧
     (POW (m_space m0) = measurable_sets m0) ∧
     (POW (m_space m1) = measurable_sets m1) ∧
     (POW (m_space m2) = measurable_sets m2) ⇒
     measure_space
       (m_space m0 × (m_space m1 × m_space m2),
        POW (m_space m0 × (m_space m1 × m_space m2)),prod_measure3 m0 m1 m2)

finite_prod_measure_space_POW3

|- ∀s1 s2 s3 u v w.
     FINITE s1 ∧ FINITE s2 ∧ FINITE s3 ⇒
     (prod_measure_space3 (s1,POW s1,u) (s2,POW s2,v) (s3,POW s3,w) =
      (s1 × (s2 × s3),POW (s1 × (s2 × s3)),
       prod_measure3 (s1,POW s1,u) (s2,POW s2,v) (s3,POW s3,w)))

seq_sup_def_compute

|- (∀P. seq_sup P 0 = @r. r ∈ P ∧ sup P < r + 1) ∧
   (∀P n.
      seq_sup P (NUMERAL (BIT1 n)) =
      @r.
        r ∈ P ∧ sup P < r + Normal ((1 / 2) pow NUMERAL (BIT1 n)) ∧
        seq_sup P (NUMERAL (BIT1 n) − 1) < r ∧ r < sup P) ∧
   ∀P n.
     seq_sup P (NUMERAL (BIT2 n)) =
     @r.
       r ∈ P ∧ sup P < r + Normal ((1 / 2) pow NUMERAL (BIT2 n)) ∧
       seq_sup P (NUMERAL (BIT1 n)) < r ∧ r < sup P

EXTREAL_SUP_SEQ

|- ∀P.
     (∃x. P x) ∧ (∃z. z ≠ PosInf ∧ ∀x. P x ⇒ x ≤ z) ⇒
     ∃x.
       (∀n. x n ∈ P) ∧ (∀n. x n ≤ x (SUC n)) ∧ (sup (IMAGE x 𝕌(:num)) = sup P)

EXTREAL_SUP_FUN_SEQ_IMAGE

|- ∀P P' f.
     (∃x. P x) ∧ (∃z. z ≠ PosInf ∧ ∀x. P x ⇒ x ≤ z) ∧ (P = IMAGE f P') ⇒
     ∃g. (∀n. g n ∈ P') ∧ (sup (IMAGE (λn. f (g n)) 𝕌(:num)) = sup P)

max_fn_seq_def_compute

|- (∀g x. max_fn_seq g 0 x = g 0 x) ∧
   (∀g n x.
      max_fn_seq g (NUMERAL (BIT1 n)) x =
      max (max_fn_seq g (NUMERAL (BIT1 n) − 1) x) (g (NUMERAL (BIT1 n)) x)) ∧
   ∀g n x.
     max_fn_seq g (NUMERAL (BIT2 n)) x =
     max (max_fn_seq g (NUMERAL (BIT1 n)) x) (g (NUMERAL (BIT2 n)) x)

max_fn_seq_mono

|- ∀g n x. max_fn_seq g n x ≤ max_fn_seq g (SUC n) x

EXTREAL_SUP_FUN_SEQ_MONO_IMAGE

|- ∀P P'.
     (∃x. P x) ∧ (∃z. z ≠ PosInf ∧ ∀x. P x ⇒ x ≤ z) ∧ (P = IMAGE f P') ∧
     (∀g1 g2. g1 ∈ P' ∧ g2 ∈ P' ∧ (∀x. g1 x ≤ g2 x) ⇒ f g1 ≤ f g2) ∧
     (∀g1 g2. g1 ∈ P' ∧ g2 ∈ P' ⇒ (λx. max (g1 x) (g2 x)) ∈ P') ⇒
     ∃g.
       (∀n. g n ∈ P') ∧ (∀x n. g n x ≤ g (SUC n) x) ∧
       (sup (IMAGE (λn. f (g n)) 𝕌(:num)) = sup P)

lemma_radon_max_in_F

|- ∀f g m v.
     measure_space m ∧ measure_space v ∧ (m_space v = m_space m) ∧
     (measurable_sets v = measurable_sets m) ∧ f ∈ RADON_F m v ∧
     g ∈ RADON_F m v ⇒
     (λx. max (f x) (g x)) ∈ RADON_F m v

lemma_radon_seq_conv_sup

|- ∀f m v.
     measure_space m ∧ measure_space v ∧ (m_space v = m_space m) ∧
     (measurable_sets v = measurable_sets m) ⇒
     ∃f_n.
       (∀n. f_n n ∈ RADON_F m v) ∧ (∀x n. f_n n x ≤ f_n (SUC n) x) ∧
       (sup (IMAGE (λn. pos_fn_integral m (f_n n)) 𝕌(:num)) =
        sup (RADON_F_integrals m v))

RN_lemma1

|- ∀m v e.
     measure_space m ∧ measure_space v ∧ 0 < e ∧ (m_space v = m_space m) ∧
     (measurable_sets v = measurable_sets m) ⇒
     ∃A.
       A ∈ measurable_sets m ∧
       measure m (m_space m) − measure v (m_space m) ≤
       measure m A − measure v A ∧
       ∀B. B ∈ measurable_sets m ∧ B ⊆ A ⇒ -e < measure m B − measure v B

RN_lemma2

|- ∀m v.
     measure_space m ∧ measure_space v ∧ (m_space v = m_space m) ∧
     (measurable_sets v = measurable_sets m) ⇒
     ∃A.
       A ∈ measurable_sets m ∧
       measure m (m_space m) − measure v (m_space m) ≤
       measure m A − measure v A ∧
       ∀B. B ∈ measurable_sets m ∧ B ⊆ A ⇒ 0 ≤ measure m B − measure v B

Radon_Nikodym

|- ∀m v.
     measure_space m ∧ measure_space v ∧ (m_space v = m_space m) ∧
     (measurable_sets v = measurable_sets m) ∧
     measure_absolutely_continuous v m ⇒
     ∃f.
       f ∈ measurable (m_space m,measurable_sets m) Borel ∧ (∀x. 0 ≤ f x) ∧
       ∀A.
         A ∈ measurable_sets m ⇒
         (pos_fn_integral m (λx. f x * indicator_fn A x) =
          Normal (measure v A))

Radon_Nikodym2

|- ∀m v.
     measure_space m ∧ measure_space v ∧ (m_space v = m_space m) ∧
     (measurable_sets v = measurable_sets m) ∧
     measure_absolutely_continuous v m ⇒
     ∃f.
       f ∈ measurable (m_space m,measurable_sets m) Borel ∧ (∀x. 0 ≤ f x) ∧
       (∀x. f x ≠ PosInf) ∧
       ∀A.
         A ∈ measurable_sets m ⇒
         (pos_fn_integral m (λx. f x * indicator_fn A x) =
          Normal (measure v A))