Theory "real_borel"

Signature

Constant	Type
borel	:real algebra
box	:real -> real -> real -> bool
indicator_fn	:(α -> bool) -> α -> real
line	:num -> real -> bool
mr2	:(real # real) metric
real_rat_set	:real -> bool
right_open_interval	:real -> real -> real -> bool
right_open_intervals	:real algebra

Definitions

borel

⊢ borel = sigma 𝕌(:real) {s | open s}

box

⊢ ∀a b. box a b = {x | a < x ∧ x < b}

indicator_fn_def

⊢ ∀s. 𝟙 s = (λx. if x ∈ s then 1 else 0)

line

⊢ ∀n. line n = {x | -&n ≤ x ∧ x ≤ &n}

mr2

⊢ mr2 = metric (λ((x1,x2),y1,y2). sqrt ((x1 − y1)² + (x2 − y2)²))

real_rat_set_def

⊢ q_set =
  {x | ∃a b. (x = &a / &b) ∧ 0 < &b} ∪ {x | ∃a b. (x = -(&a / &b)) ∧ 0 < &b}

right_open_interval

⊢ ∀a b. right_open_interval a b = {x | a ≤ x ∧ x < b}

right_open_intervals

⊢ right_open_intervals = (𝕌(:real),{right_open_interval a b | T})

Theorems

ADD_IN_QSET

⊢ ∀x y. x ∈ q_set ∧ y ∈ q_set ⇒ x + y ∈ q_set

BALL_IN_LINE

⊢ ∀n. ball (0,&n) ⊆ line n

BIGUNION_IMAGE_QSET

⊢ ∀a f.
    sigma_algebra a ∧ f ∈ (q_set → subsets a) ⇒
    BIGUNION (IMAGE f q_set) ∈ subsets a

CLG_UBOUND

⊢ ∀x. 0 ≤ x ⇒ &clg x < x + 1

DIV_IN_QSET

⊢ ∀x y. x ∈ q_set ∧ y ∈ q_set ∧ y ≠ 0 ⇒ x / y ∈ q_set

IMAGE_FST_CROSS_INTERVAL

⊢ ∀a b c d.
    c < d ⇒ (IMAGE FST (interval (a,b) × interval (c,d)) = interval (a,b))

IMAGE_SND_CROSS_INTERVAL

⊢ ∀a b c d.
    a < b ⇒ (IMAGE SND (interval (a,b) × interval (c,d)) = interval (c,d))

INV_IN_QSET

⊢ ∀x. x ∈ q_set ∧ x ≠ 0 ⇒ 1 / x ∈ q_set

ISMET_R2

⊢ ismet (λ((x1,x2),y1,y2). sqrt ((x1 − y1)² + (x2 − y2)²))

LINE_MONO

⊢ ∀n N. n ≤ N ⇒ line n ⊆ line N

LINE_MONO_EQ

⊢ ∀n N. line n ⊆ line N ⇔ n ≤ N

LINE_MONO_SUC

⊢ ∀n. line n ⊆ line (SUC n)

MR2_DEF

⊢ ∀x1 x2 y1 y2. dist mr2 ((x1,x2),y1,y2) = sqrt ((x1 − y1)² + (x2 − y2)²)

MUL_IN_QSET

⊢ ∀x y. x ∈ q_set ∧ y ∈ q_set ⇒ x * y ∈ q_set

NON_NEG_REAL_RAT_DENSE

⊢ ∀x y. 0 ≤ x ∧ x < y ⇒ ∃m n. x < &m / &n ∧ &m / &n < y

NUM_IN_QSET

⊢ ∀n. &n ∈ q_set ∧ -&n ∈ q_set

OPP_IN_QSET

⊢ ∀x. x ∈ q_set ⇒ -x ∈ q_set

QSET_COUNTABLE

⊢ COUNTABLE q_set

Q_DENSE_IN_REAL

⊢ ∀x y. x < y ⇒ ∃r. r ∈ q_set ∧ x < r ∧ r < y

Q_DENSE_IN_REAL_LEMMA

⊢ ∀x y. 0 ≤ x ∧ x < y ⇒ ∃r. r ∈ q_set ∧ x < r ∧ r < y

REAL_IN_LINE

⊢ ∀x. ∃n. x ∈ line n

REAL_RAT_DENSE

⊢ ∀x y. x < y ⇒ ∃r. r ∈ q_set ∧ x < r ∧ r < y

REAL_SING_BIGINTER

⊢ ∀c. {c} =
      BIGINTER
        (IMAGE (λn. {x | c − (1 / 2) pow n ≤ x ∧ x < c + (1 / 2) pow n})
           𝕌(:num))

SUB_IN_QSET

⊢ ∀x y. x ∈ q_set ∧ y ∈ q_set ⇒ x − y ∈ q_set

borel_2d

⊢ borel × borel = sigma 𝕌(:real # real) {s | open_in (mtop mr2) s}

borel_2d_alt_box

⊢ borel × borel = sigma 𝕌(:real # real) {box a b × box c d | T}

borel_closed

⊢ ∀A. closed A ⇒ A ∈ subsets borel

borel_comp

⊢ ∀A. A ∈ subsets borel ⇒ 𝕌(:real) DIFF A ∈ subsets borel

borel_def

⊢ borel = sigma 𝕌(:real) (IMAGE (λa. {x | x ≤ a}) 𝕌(:real))

borel_eq_box

⊢ borel = sigma 𝕌(:real) (IMAGE (λ(a,b). box a b) 𝕌(:real # real))

borel_eq_ge_le

⊢ borel = sigma 𝕌(:real) (IMAGE (λ(a,b). {x | a ≤ x ∧ x ≤ b}) 𝕌(:real # real))

borel_eq_ge_less

⊢ borel = sigma 𝕌(:real) (IMAGE (λ(a,b). {x | a ≤ x ∧ x < b}) 𝕌(:real # real))

borel_eq_gr

⊢ borel = sigma 𝕌(:real) (IMAGE (λa. {x | a < x}) 𝕌(:real))

borel_eq_gr_le

⊢ borel = sigma 𝕌(:real) (IMAGE (λ(a,b). {x | a < x ∧ x ≤ b}) 𝕌(:real # real))

borel_eq_gr_less

⊢ borel = sigma 𝕌(:real) (IMAGE (λ(a,b). {x | a < x ∧ x < b}) 𝕌(:real # real))

borel_eq_le

⊢ borel = sigma 𝕌(:real) (IMAGE (λa. {x | x ≤ a}) 𝕌(:real))

borel_eq_less

⊢ borel = sigma 𝕌(:real) (IMAGE (λa. {x | x < a}) 𝕌(:real))

borel_eq_sigmaI1

⊢ ∀X A f.
    (borel = sigma 𝕌(:real) X) ∧
    (∀x. x ∈ X ⇒ x ∈ subsets (sigma 𝕌(:real) (IMAGE f A))) ∧
    (∀i. i ∈ A ⇒ f i ∈ subsets borel) ⇒
    (borel = sigma 𝕌(:real) (IMAGE f A))

borel_eq_sigmaI2

⊢ ∀G f A B.
    (borel = sigma 𝕌(:real) (IMAGE (λ(i,j). G i j) B)) ∧
    (∀i j.
       (i,j) ∈ B ⇒ G i j ∈ subsets (sigma 𝕌(:real) (IMAGE (λ(i,j). f i j) A))) ∧
    (∀i j. (i,j) ∈ A ⇒ f i j ∈ subsets borel) ⇒
    (borel = sigma 𝕌(:real) (IMAGE (λ(i,j). f i j) A))

borel_eq_sigmaI3

⊢ ∀f A X.
    (borel = sigma 𝕌(:real) X) ∧
    (∀x. x ∈ X ⇒ x ∈ subsets (sigma 𝕌(:real) (IMAGE (λ(i,j). f i j) A))) ∧
    (∀i j. (i,j) ∈ A ⇒ f i j ∈ subsets borel) ⇒
    (borel = sigma 𝕌(:real) (IMAGE (λ(i,j). f i j) A))

borel_eq_sigmaI4

⊢ ∀G f A.
    (borel = sigma 𝕌(:real) (IMAGE (λ(i,j). G i j) A)) ∧
    (∀i j. (i,j) ∈ A ⇒ G i j ∈ subsets (sigma 𝕌(:real) (IMAGE f 𝕌(:γ)))) ∧
    (∀i. f i ∈ subsets borel) ⇒
    (borel = sigma 𝕌(:real) (IMAGE f 𝕌(:γ)))

borel_eq_sigmaI5

⊢ ∀G f.
    (borel = sigma 𝕌(:real) (IMAGE G 𝕌(:α))) ∧
    (∀i. G i ∈ subsets (sigma 𝕌(:real) (IMAGE (λ(i,j). f i j) 𝕌(:β # γ)))) ∧
    (∀i j. f i j ∈ subsets borel) ⇒
    (borel = sigma 𝕌(:real) (IMAGE (λ(i,j). f i j) 𝕌(:β # γ)))

borel_line

⊢ ∀n. line n ∈ subsets borel

borel_measurable_const

⊢ ∀M c. sigma_algebra M ⇒ (λx. c) ∈ borel_measurable M

borel_measurable_image

⊢ ∀f M x. f ∈ borel_measurable M ⇒ PREIMAGE f {x} ∩ space M ∈ subsets M

borel_measurable_indicator

⊢ ∀s a. sigma_algebra s ∧ a ∈ subsets s ⇒ 𝟙 a ∈ borel_measurable s

borel_measurable_sets

⊢ (∀a. {x | x < a} ∈ subsets borel) ∧ (∀a. {x | x ≤ a} ∈ subsets borel) ∧
  (∀a. {x | a < x} ∈ subsets borel) ∧ (∀a. {x | a ≤ x} ∈ subsets borel) ∧
  (∀a b. {x | a < x ∧ x < b} ∈ subsets borel) ∧
  (∀a b. {x | a < x ∧ x ≤ b} ∈ subsets borel) ∧
  (∀a b. {x | a ≤ x ∧ x < b} ∈ subsets borel) ∧
  (∀a b. {x | a ≤ x ∧ x ≤ b} ∈ subsets borel) ∧ (∀c. {c} ∈ subsets borel) ∧
  ∀c. {x | x ≠ c} ∈ subsets borel

borel_measurable_sets_ge

⊢ ∀a. {x | a ≤ x} ∈ subsets borel

borel_measurable_sets_ge_le

⊢ ∀a b. {x | a ≤ x ∧ x ≤ b} ∈ subsets borel

borel_measurable_sets_ge_less

⊢ ∀a b. {x | a ≤ x ∧ x < b} ∈ subsets borel

borel_measurable_sets_gr

⊢ ∀a. {x | a < x} ∈ subsets borel

borel_measurable_sets_gr_le

⊢ ∀a b. {x | a < x ∧ x ≤ b} ∈ subsets borel

borel_measurable_sets_gr_less

⊢ ∀a b. {x | a < x ∧ x < b} ∈ subsets borel

borel_measurable_sets_le

⊢ ∀a. {x | x ≤ a} ∈ subsets borel

borel_measurable_sets_less

⊢ ∀a. {x | x < a} ∈ subsets borel

borel_measurable_sets_not_sing

⊢ ∀c. {x | x ≠ c} ∈ subsets borel

borel_measurable_sets_sing

⊢ ∀c. {c} ∈ subsets borel

borel_open

⊢ ∀A. open A ⇒ A ∈ subsets borel

borel_sigma_sets_subset

⊢ ∀A. A ⊆ subsets borel ⇒ sigma_sets 𝕌(:real) A ⊆ subsets borel

borel_singleton

⊢ ∀A x. A ∈ subsets borel ⇒ x INSERT A ∈ subsets borel

box_alt

⊢ ∀a b. box a b = interval (a,b)

box_open_in_mr2

⊢ ∀a b c d. open_in (mtop mr2) (interval (a,b) × interval (c,d))

countable_real_rat_set

⊢ COUNTABLE q_set

in_borel_measurable

⊢ ∀f s.
    f ∈ borel_measurable s ⇔
    sigma_algebra s ∧
    ∀s'.
      s' ∈ subsets (sigma 𝕌(:real) (IMAGE (λa. {x | x ≤ a}) 𝕌(:real))) ⇒
      PREIMAGE f s' ∩ space s ∈ subsets s

in_borel_measurable_add

⊢ ∀a f g h.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧ g ∈ borel_measurable a ∧
    (∀x. x ∈ space a ⇒ (h x = f x + g x)) ⇒
    h ∈ borel_measurable a

in_borel_measurable_borel

⊢ ∀f M.
    f ∈ borel_measurable M ⇔
    sigma_algebra M ∧
    ∀s. s ∈ subsets borel ⇒ PREIMAGE f s ∩ space M ∈ subsets M

in_borel_measurable_cmul

⊢ ∀a f g z.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧
    (∀x. x ∈ space a ⇒ (g x = z * f x)) ⇒
    g ∈ borel_measurable a

in_borel_measurable_const

⊢ ∀a k f.
    sigma_algebra a ∧ (∀x. x ∈ space a ⇒ (f x = k)) ⇒ f ∈ borel_measurable a

in_borel_measurable_ge

⊢ ∀f m.
    f ∈ borel_measurable m ⇔
    sigma_algebra m ∧ f ∈ (space m → 𝕌(:real)) ∧
    ∀a. {w | w ∈ space m ∧ a ≤ f w} ∈ subsets m

in_borel_measurable_gr

⊢ ∀f m.
    f ∈ borel_measurable m ⇔
    sigma_algebra m ∧ f ∈ (space m → 𝕌(:real)) ∧
    ∀a. {w | w ∈ space m ∧ a < f w} ∈ subsets m

in_borel_measurable_le

⊢ ∀f m.
    f ∈ borel_measurable m ⇔
    sigma_algebra m ∧ f ∈ (space m → 𝕌(:real)) ∧
    ∀a. {w | w ∈ space m ∧ f w ≤ a} ∈ subsets m

in_borel_measurable_less

⊢ ∀f m.
    f ∈ borel_measurable m ⇔
    sigma_algebra m ∧ f ∈ (space m → 𝕌(:real)) ∧
    ∀a. {w | w ∈ space m ∧ f w < a} ∈ subsets m

in_borel_measurable_mul

⊢ ∀a f g h.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧ g ∈ borel_measurable a ∧
    (∀x. x ∈ space a ⇒ (h x = f x * g x)) ⇒
    h ∈ borel_measurable a

in_borel_measurable_open

⊢ ∀f M.
    f ∈ borel_measurable M ⇔
    sigma_algebra M ∧
    ∀s. s ∈ subsets (sigma 𝕌(:real) {s | open s}) ⇒
        PREIMAGE f s ∩ space M ∈ subsets M

in_borel_measurable_sqr

⊢ ∀a f g.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧
    (∀x. x ∈ space a ⇒ (g x = (f x)²)) ⇒
    g ∈ borel_measurable a

in_borel_measurable_sub

⊢ ∀a f g h.
    sigma_algebra a ∧ f ∈ borel_measurable a ∧ g ∈ borel_measurable a ∧
    (∀x. x ∈ space a ⇒ (h x = f x − g x)) ⇒
    h ∈ borel_measurable a

in_right_open_interval

⊢ ∀a b x. x ∈ right_open_interval a b ⇔ a ≤ x ∧ x < b

in_right_open_intervals

⊢ ∀s. s ∈ subsets right_open_intervals ⇔ ∃a b. s = right_open_interval a b

in_right_open_intervals_nonempty

⊢ ∀s. s ≠ ∅ ∧ s ∈ subsets right_open_intervals ⇔
      ∃a b. a < b ∧ (s = right_open_interval a b)

line_closed

⊢ ∀n. closed (line n)

open_UNION_box

⊢ ∀M. open M ⇒ (M = BIGUNION {box a b | box a b ⊆ M})

open_UNION_rational_box

⊢ ∀M. open M ⇒ (M = BIGUNION {box a b | a ∈ q_set ∧ b ∈ q_set ∧ box a b ⊆ M})

q_set_def

⊢ q_set =
  {x | ∃a b. (x = &a / &b) ∧ 0 < &b} ∪ {x | ∃a b. (x = -(&a / &b)) ∧ 0 < &b}

rational_boxes

⊢ ∀x e.
    0 < e ⇒ ∃a b. a ∈ q_set ∧ b ∈ q_set ∧ x ∈ box a b ∧ box a b ⊆ ball (x,e)

right_open_interval_11

⊢ ∀a b c d.
    a < b ∧ c < d ⇒
    ((right_open_interval a b = right_open_interval c d) ⇔ (a = c) ∧ (b = d))

right_open_interval_DISJOINT

⊢ ∀a b c d.
    a ≤ b ∧ b ≤ c ∧ c ≤ d ⇒
    DISJOINT (right_open_interval a b) (right_open_interval c d)

right_open_interval_DISJOINT_imp

⊢ ∀a b c d.
    a < b ∧ c < d ∧
    DISJOINT (right_open_interval a b) (right_open_interval c d) ⇒
    b ≤ c ∨ d ≤ a

right_open_interval_between_bounds

⊢ ∀x a b.
    x ∈ right_open_interval a b ⇔
    interval_lowerbound (right_open_interval a b) ≤ x ∧
    x < interval_upperbound (right_open_interval a b)

right_open_interval_disjoint

⊢ ∀a b c d.
    a ≤ b ∧ b ≤ c ∧ c ≤ d ⇒
    disjoint {right_open_interval a b; right_open_interval c d}

right_open_interval_empty

⊢ ∀a b. (right_open_interval a b = ∅) ⇔ ¬(a < b)

right_open_interval_empty_eq

⊢ ∀a b. (a = b) ⇒ (right_open_interval a b = ∅)

right_open_interval_in_intervals

⊢ ∀a b. right_open_interval a b ∈ subsets right_open_intervals

right_open_interval_inter

⊢ ∀a b c d.
    right_open_interval a b ∩ right_open_interval c d =
    right_open_interval (max a c) (min b d)

right_open_interval_interior

⊢ ∀a b. a < b ⇒ a ∈ right_open_interval a b

right_open_interval_lowerbound

⊢ ∀a b. a < b ⇒ (interval_lowerbound (right_open_interval a b) = a)

right_open_interval_two_bounds

⊢ ∀a b.
    interval_lowerbound (right_open_interval a b) ≤
    interval_upperbound (right_open_interval a b)

right_open_interval_union

⊢ ∀a b c d.
    a < b ∧ c < d ∧ a ≤ d ∧ c ≤ b ⇒
    (right_open_interval a b ∪ right_open_interval c d =
     right_open_interval (min a c) (max b d))

right_open_interval_union_imp

⊢ ∀a b c d.
    a < b ∧ c < d ∧
    right_open_interval a b ∪ right_open_interval c d ∈
    subsets right_open_intervals ⇒
    a ≤ d ∧ c ≤ b

right_open_interval_upperbound

⊢ ∀a b. a < b ⇒ (interval_upperbound (right_open_interval a b) = b)

right_open_intervals_semiring

⊢ semiring right_open_intervals

right_open_intervals_sigma_borel

⊢ sigma (space right_open_intervals) (subsets right_open_intervals) = borel

right_open_intervals_subset_borel

⊢ subsets right_open_intervals ⊆ subsets borel

sigma_algebra_borel

⊢ sigma_algebra borel

sigma_algebra_borel_2d

⊢ sigma_algebra (borel × borel)

sigma_ge_gr

⊢ ∀f A.
    sigma_algebra A ∧ (∀a. {w | w ∈ space A ∧ a ≤ f w} ∈ subsets A) ⇒
    ∀a. {w | w ∈ space A ∧ a < f w} ∈ subsets A

sigma_gr_le

⊢ ∀f A.
    sigma_algebra A ∧ (∀a. {w | w ∈ space A ∧ a < f w} ∈ subsets A) ⇒
    ∀a. {w | w ∈ space A ∧ f w ≤ a} ∈ subsets A

sigma_le_less

⊢ ∀f A.
    sigma_algebra A ∧ (∀a. {w | w ∈ space A ∧ f w ≤ a} ∈ subsets A) ⇒
    ∀a. {w | w ∈ space A ∧ f w < a} ∈ subsets A

sigma_less_ge

⊢ ∀f A.
    sigma_algebra A ∧ (∀a. {w | w ∈ space A ∧ f w < a} ∈ subsets A) ⇒
    ∀a. {w | w ∈ space A ∧ a ≤ f w} ∈ subsets A

space_borel

⊢ space borel = 𝕌(:real)

space_in_borel

⊢ 𝕌(:real) ∈ subsets borel