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) -> (α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
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

signed_measure_space_def

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

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

RADON_F_integrals_def

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

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

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)

prod_sets3_def

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

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

prod_measure_def

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

prod_measure3_def

⊢ ∀m0 m1 m2.
      prod_measure3 m0 m1 m2 = prod_measure m0 (prod_measure_space m1 m2)

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)

pos_fn_integral_def

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

negative_set_def

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

measure_absolutely_continuous_def

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

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)

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

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

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)

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

Theorems

seq_sup_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

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

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

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

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

psfis_zero

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

psfis_unique

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

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

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)

psfis_pos

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

psfis_not_infty

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

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

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)

psfis_indicator

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

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)

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

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

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)

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

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)

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

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

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

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)

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)

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

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_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_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_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_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_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_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_fn_integral_zero

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

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

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

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_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_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_pos

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

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_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_mono

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

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

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)

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)

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)

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

max_fn_seq_mono

⊢ ∀g n x. max_fn_seq g n x ≤ max_fn_seq g (SUC n) x

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

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

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_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_mono_increasing

⊢ ∀m f x. 0 ≤ f x ⇒ mono_increasing (λn. fn_seq m f n 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)

lemma_fn_5

⊢ ∀m f n x. 0 ≤ f x ⇒ 0 ≤ fn_seq m f n x

lemma_fn_4

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

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

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

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

integral_zero

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

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

integral_pos_fn

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

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

integral_indicator

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

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_cmul

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

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)

integrable_zero

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

integrable_sub

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

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

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

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

⊢ ∀m f.
      measure_space m ∧ integrable m f ⇒
      null_set m {x | x ∈ m_space m ∧ (f x = 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_indicator

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

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_cmul

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

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

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)

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)

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

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)

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)

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

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)