Theory "real_lebesgue"

Parents real_measure

Signature

Constant	Type
RN_deriv	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> ((α -> bool) -> real) -> α -> real
countable_space_integral	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> real) -> real
finite_space_integral	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> real) -> real
fn_minus	:(α -> real) -> α -> real
fn_plus	:(α -> real) -> α -> real
integrable	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> real) -> bool
integral	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> real) -> real
mon_upclose	:(num -> num -> α -> real) -> num -> α -> real
mon_upclose_help	:num -> (β -> num -> α -> real) -> β -> α -> real
mono_increasing	:(num -> real) -> bool
nnfis	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> real) -> real -> bool
nonneg	:(α -> real) -> bool
pos_fn_integral	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> real) -> real
pos_simple_fn	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> real) -> (num -> bool) -> (num -> α -> bool) -> (num -> real) -> bool
pos_simple_fn_integral	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (β -> bool) -> (β -> α -> bool) -> (β -> real) -> real
prod_measure	:(α -> 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)
psfis	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> real) -> real -> bool
psfs	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> real) -> (num -> bool) # (num -> α -> bool) # (num -> real) -> bool
upclose	:(α -> real) -> (α -> real) -> α -> real

Definitions

RN_deriv_def

⊢ ∀m v.
    RN_deriv m v =
    @f. measure_space m ∧ measure_space (m_space m,measurable_sets m,v) ∧
        f ∈ borel_measurable (m_space m,measurable_sets m) ∧
        ∀a. a ∈ measurable_sets m ⇒ (integral m (λx. f x * 𝟙 a x) = v a)

countable_space_integral_def

⊢ ∀m f.
    countable_space_integral m f =
    (let
       e = enumerate (IMAGE f (m_space m))
     in
       suminf ((λr. r * measure m (PREIMAGE f {r} ∩ m_space m)) ∘ e))

finite_space_integral_def

⊢ ∀m f.
    finite_space_integral m f =
    ∑ (λr. r * measure m (PREIMAGE f {r} ∩ m_space m)) (IMAGE f (m_space m))

fn_minus_def

⊢ ∀f. f⁻ = (λx. if 0 ≤ f x then 0 else -f x)

fn_plus_def

⊢ ∀f. fn_plus f = (λx. if 0 ≤ f x then f x else 0)

integrable_def

⊢ ∀m f.
    integrable m f ⇔
    measure_space m ∧ (∃x. x ∈ nnfis m (fn_plus f)) ∧ ∃y. y ∈ nnfis m f⁻

integral_def

⊢ ∀m f. integral m f = (@i. i ∈ nnfis m (fn_plus f)) − @j. j ∈ nnfis m f⁻

mon_upclose_def

⊢ ∀u m. mon_upclose u m = mon_upclose_help m u m

mon_upclose_help_def

⊢ (∀u m. mon_upclose_help 0 u m = u m 0) ∧
  ∀n u m.
    mon_upclose_help (SUC n) u m =
    upclose (u m (SUC n)) (mon_upclose_help n u m)

mono_increasing_def

⊢ ∀f. mono_increasing f ⇔ ∀m n. m ≤ n ⇒ f m ≤ f n

nnfis_def

⊢ ∀m f.
    nnfis m f =
    {y |
     ∃u x. mono_convergent u f (m_space m) ∧ (∀n. x n ∈ psfis m (u n)) ∧ x ⟶ y}

nonneg_def

⊢ ∀f. nonneg f ⇔ ∀x. 0 ≤ f x

pos_fn_integral_def

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

pos_simple_fn_def

⊢ ∀m f s a x.
    pos_simple_fn m f s a x ⇔
    (∀t. 0 ≤ f t) ∧ (∀t. t ∈ m_space m ⇒ (f t = ∑ (λi. x i * 𝟙 (a i) t) s)) ∧
    (∀i. i ∈ s ⇒ a i ∈ measurable_sets m) ∧ (∀i. 0 ≤ x i) ∧ FINITE s ∧
    (∀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

⊢ ∀m s a x. pos_simple_fn_integral m s a x = ∑ (λi. x i * measure m (a i)) s

prod_measure_def

⊢ ∀m0 m1.
    prod_measure m0 m1 =
    (λa. integral m0 (λs0. 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)

psfis_def

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

psfs_def

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

upclose_def

⊢ ∀f g. upclose f g = (λt. max (f t) (g t))

Theorems

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)

borel_measurable_mon_conv_psfis

⊢ ∀m f.
    measure_space m ∧ f ∈ borel_measurable (m_space m,measurable_sets m) ∧
    (∀t. t ∈ m_space m ⇒ 0 ≤ f t) ⇒
    ∃u x. mono_convergent u f (m_space m) ∧ ∀n. x n ∈ psfis m (u n)

countable_space_integral_reduce

⊢ ∀m f p n.
    measure_space m ∧ positive m ∧
    f ∈ borel_measurable (m_space m,measurable_sets m) ∧
    COUNTABLE (IMAGE f (m_space m)) ∧
    INFINITE (IMAGE (fn_plus f) (m_space m)) ∧
    INFINITE (IMAGE f⁻ (m_space m)) ∧
    (λr. r * measure m (PREIMAGE f⁻ {r} ∩ m_space m)) ∘
    enumerate (IMAGE f⁻ (m_space m)) sums n ∧
    (λr. r * measure m (PREIMAGE (fn_plus f) {r} ∩ m_space m)) ∘
    enumerate (IMAGE (fn_plus f) (m_space m)) sums p ⇒
    (integral m f = p − n)

finite_POW_RN_deriv_reduce

⊢ ∀m v.
    measure_space m ∧ FINITE (m_space m) ∧
    measure_space (m_space m,measurable_sets m,v) ∧
    (POW (m_space m) = measurable_sets m) ∧
    (∀x. (measure m {x} = 0) ⇒ (v {x} = 0)) ⇒
    ∀x. x ∈ m_space m ∧ measure m {x} ≠ 0 ⇒
        (RN_deriv m v x = v {x} / measure m {x})

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)

finite_integral_on_set

⊢ ∀m f a.
    measure_space m ∧ FINITE (m_space m) ∧
    f ∈ borel_measurable (m_space m,measurable_sets m) ∧ a ∈ measurable_sets m ⇒
    (integral m (λx. f x * 𝟙 a x) =
     ∑ (λr. r * measure m (PREIMAGE f {r} ∩ a)) (IMAGE f a))

finite_space_POW_integral_reduce

⊢ ∀m f.
    measure_space m ∧ (POW (m_space m) = measurable_sets m) ∧
    FINITE (m_space m) ⇒
    (integral m f = ∑ (λx. f x * measure m {x}) (m_space m))

finite_space_integral_reduce

⊢ ∀m f.
    measure_space m ∧ f ∈ borel_measurable (m_space m,measurable_sets m) ∧
    FINITE (m_space m) ⇒
    (integral m f = finite_space_integral m f)

fn_plus_fn_minus_borel_measurable

⊢ ∀f m.
    measure_space m ∧ f ∈ borel_measurable (m_space m,measurable_sets m) ⇒
    fn_plus f ∈ borel_measurable (m_space m,measurable_sets m) ∧
    f⁻ ∈ borel_measurable (m_space m,measurable_sets m)

fn_plus_fn_minus_borel_measurable_iff

⊢ ∀f m.
    measure_space m ⇒
    (f ∈ borel_measurable (m_space m,measurable_sets m) ⇔
     fn_plus f ∈ borel_measurable (m_space m,measurable_sets m) ∧
     f⁻ ∈ borel_measurable (m_space m,measurable_sets m))

indicator_fn_split

⊢ ∀r s b.
    FINITE r ∧ (BIGUNION (IMAGE b r) = s) ∧
    (∀i j. i ∈ r ∧ j ∈ r ∧ i ≠ j ⇒ DISJOINT (b i) (b j)) ⇒
    ∀a. a ⊆ s ⇒ (𝟙 a = (λx. ∑ (λi. 𝟙 (a ∩ b i) x) r))

integral_add

⊢ ∀m f g.
    integrable m f ∧ integrable m g ⇒
    integrable m (λt. f t + g t) ∧
    (integral m (λt. f t + g t) = integral m f + integral m g)

integral_borel_measurable

⊢ ∀m f. integrable m f ⇒ f ∈ borel_measurable (m_space m,measurable_sets m)

integral_cmul_indicator

⊢ ∀m s c.
    measure_space m ∧ s ∈ measurable_sets m ⇒
    (integral m (λx. c * 𝟙 s x) = c * measure m s)

integral_indicator_fn

⊢ ∀m a.
    measure_space m ∧ a ∈ measurable_sets m ⇒
    (integral m (𝟙 a) = measure m a) ∧ integrable m (𝟙 a)

integral_mono

⊢ ∀m f g.
    integrable m f ∧ integrable m g ∧ (∀t. t ∈ m_space m ⇒ f t ≤ g t) ⇒
    integral m f ≤ integral m g

integral_times

⊢ ∀m f a.
    integrable m f ⇒
    integrable m (λt. a * f t) ∧ (integral m (λt. a * f t) = a * integral m f)

integral_zero

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

markov_ineq

⊢ ∀m f a n.
    integrable m f ∧ 0 < a ∧ integrable m (λx. abs (f x) pow n) ⇒
    measure m (PREIMAGE f {y | a ≤ y} ∩ m_space m) ≤
    integral m (λx. abs (f x) pow n) / a pow n

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)

measure_split

⊢ ∀r b m.
    measure_space m ∧ FINITE r ∧ (BIGUNION (IMAGE b r) = m_space m) ∧
    (∀i j. i ∈ r ∧ j ∈ r ∧ i ≠ j ⇒ DISJOINT (b i) (b j)) ∧
    (∀i. i ∈ r ⇒ b i ∈ measurable_sets m) ⇒
    ∀a. a ∈ measurable_sets m ⇒ (measure m a = ∑ (λi. measure m (a ∩ b i)) r)

mon_upclose_help_compute

⊢ (∀u m. mon_upclose_help 0 u m = u m 0) ∧
  (∀n u m.
     mon_upclose_help (NUMERAL (BIT1 n)) u m =
     upclose (u m (NUMERAL (BIT1 n)))
       (mon_upclose_help (NUMERAL (BIT1 n) − 1) u m)) ∧
  ∀n u m.
    mon_upclose_help (NUMERAL (BIT2 n)) u m =
    upclose (u m (NUMERAL (BIT2 n))) (mon_upclose_help (NUMERAL (BIT1 n)) u m)

mon_upclose_psfis

⊢ ∀m u.
    measure_space m ∧ (∀n n'. ∃a. a ∈ psfis m (u n n')) ⇒
    ∃c. ∀n. c n ∈ psfis m (mon_upclose u n)

mono_increasing_converges_to_sup

⊢ ∀f r.
    (∀i. 0 ≤ f i) ∧ mono_increasing f ∧ f ⟶ r ⇒ (r = sup (IMAGE f 𝕌(:num)))

nnfis_add

⊢ ∀f g m a b.
    measure_space m ∧ a ∈ nnfis m f ∧ b ∈ nnfis m g ⇒
    a + b ∈ nnfis m (λw. f w + g w)

nnfis_borel_measurable

⊢ ∀m f a.
    measure_space m ∧ a ∈ nnfis m f ⇒
    f ∈ borel_measurable (m_space m,measurable_sets m)

nnfis_dom_conv

⊢ ∀m f g b.
    measure_space m ∧ f ∈ borel_measurable (m_space m,measurable_sets m) ∧
    b ∈ nnfis m g ∧ (∀t. t ∈ m_space m ⇒ f t ≤ g t) ∧
    (∀t. t ∈ m_space m ⇒ 0 ≤ f t) ⇒
    ∃a. a ∈ nnfis m f ∧ a ≤ b

nnfis_integral

⊢ ∀m f a.
    measure_space m ∧ a ∈ nnfis m f ⇒ integrable m f ∧ (integral m f = a)

nnfis_minus_nnfis_integral

⊢ ∀m f g a b.
    measure_space m ∧ a ∈ nnfis m f ∧ b ∈ nnfis m g ⇒
    integrable m (λt. f t − g t) ∧ (integral m (λt. f t − g t) = a − b)

nnfis_mon_conv

⊢ ∀f m h x y.
    measure_space m ∧ mono_convergent f h (m_space m) ∧
    (∀n. x n ∈ nnfis m (f n)) ∧ x ⟶ y ⇒
    y ∈ nnfis m h

nnfis_mono

⊢ ∀f g m a b.
    measure_space m ∧ a ∈ nnfis m f ∧ b ∈ nnfis m g ∧
    (∀w. w ∈ m_space m ⇒ f w ≤ g w) ⇒
    a ≤ b

nnfis_pos_on_mspace

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

nnfis_times

⊢ ∀f m a z.
    measure_space m ∧ a ∈ nnfis m f ∧ 0 ≤ z ⇒ z * a ∈ nnfis m (λw. z * f w)

nnfis_unique

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

pos_psfis

⊢ ∀r m f. measure_space m ∧ r ∈ psfis m f ⇒ 0 ≤ r

pos_simple_fn_integral_REAL_SUM_IMAGE

⊢ ∀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 ⇒
    ∃s' a' x'.
      pos_simple_fn m (λt. ∑ (λi. f i t) P) s' a' x' ∧
      (pos_simple_fn_integral m s' a' x' =
       ∑ (λi. pos_simple_fn_integral m (s i) (a i) (x i)) P)

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_indicator

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

⊢ ∀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. f x ≤ g x) ⇒
    pos_simple_fn_integral m s a x ≤ pos_simple_fn_integral m s' b y

pos_simple_fn_integral_mono_on_mspace

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

⊢ ∀m f s a x.
    measure_space m ∧ pos_simple_fn m f s a x ⇒
    ∀z. 0 ≤ z ⇒
        ∃s' b y.
          pos_simple_fn m (λx. z * f x) s' b y ∧
          (pos_simple_fn_integral m s' b y =
           z * pos_simple_fn_integral m s a x)

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 = ∑ (λi. z i * 𝟙 (c i) t) k)) ∧
      (∀t. t ∈ m_space m ⇒ (g t = ∑ (λi. 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 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) ∧ (∀i. 0 ≤ z i) ∧ ∀i. 0 ≤ z' i

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_REAL_SUM_IMAGE

⊢ ∀m f a P.
    measure_space m ∧ (∀i. i ∈ P ⇒ a i ∈ psfis m (f i)) ∧ FINITE P ⇒
    ∑ a P ∈ psfis m (λt. ∑ (λi. f i t) P)

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)

psfis_borel_measurable

⊢ ∀m f a.
    measure_space m ∧ a ∈ psfis m f ⇒
    f ∈ borel_measurable (m_space m,measurable_sets m)

psfis_equiv

⊢ ∀f g a m.
    measure_space m ∧ a ∈ psfis m f ∧ (∀t. 0 ≤ g t) ∧
    (∀t. t ∈ m_space m ⇒ (f t = g t)) ⇒
    a ∈ psfis m g

psfis_indicator

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

psfis_intro

⊢ ∀m a x P.
    measure_space m ∧ (∀i. i ∈ P ⇒ a i ∈ measurable_sets m) ∧ (∀i. 0 ≤ x i) ∧
    FINITE P ⇒
    ∑ (λi. x i * measure m (a i)) P ∈ psfis m (λt. ∑ (λi. x i * 𝟙 (a i) t) P)

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_mono_conv_mono

⊢ ∀m f u x y r s.
    measure_space m ∧ mono_convergent u f (m_space m) ∧
    (∀n. x n ∈ psfis m (u n)) ∧ (∀m n. m ≤ n ⇒ x m ≤ x n) ∧ x ⟶ y ∧
    r ∈ psfis m s ∧ (∀a. a ∈ m_space m ⇒ s a ≤ f a) ⇒
    r ≤ y

psfis_mult

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

psfis_nnfis

⊢ ∀m f a. measure_space m ∧ a ∈ psfis m f ⇒ a ∈ nnfis m f

psfis_nonneg

⊢ ∀m f a. a ∈ psfis m f ⇒ nonneg f

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 = ∑ (λi. z i * 𝟙 (c i) t) k)) ∧
      (∀t. t ∈ m_space m ⇒ (g t = ∑ (λi. 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 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) ∧ (∀i. 0 ≤ z i) ∧ ∀i. 0 ≤ z' i

psfis_unique

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

upclose_psfis

⊢ ∀f g a b m.
    measure_space m ∧ a ∈ psfis m f ∧ b ∈ psfis m g ⇒
    ∃c. c ∈ psfis m (upclose f g)