Theory lebesgue_measure

⊢ ∀k. closed_interval k ⇔ ∃a b. k = interval [(a,b)]

⊢ ∀X. integrable_sets X = {E | indicator E integrable_on X}

⊢ lebesgue =
  (𝕌(:real),{A | ∀n. indicator A integrable_on line n},
   (λA. sup {Normal (integral (line n) (indicator A)) | n ∈ 𝕌(:num)}))

⊢ ∀s t. nonoverlapping s t ⇔ DISJOINT (interior s) (interior t)

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

⊢ ∀f n.
    real_fn_seq_integral f n =
    ∑
      (λk.
           &k / 2 pow n *
           lambda' {x | &k / 2 pow n ≤ f x ∧ f x < (&k + 1) / 2 pow n})
      (count (4 ** n)) + 2 pow n * lambda' {x | 2 pow n ≤ f x}

⊢ countable 𝕌(:int)

⊢ ∀f f' g a b.
    a ≤ b ∧
    (∀x. x ∈ interval [(a,b)] ⇒
         (f has_vector_derivative f' x) (at x within interval [(a,b)])) ∧
    f' ∈ borel_measurable borel ∧
    (∀x. g x = f' x * indicator (interval [(a,b)]) x) ∧
    (integrable lborel (Normal ∘ g) ∨ g absolutely_integrable_on 𝕌(:real)) ⇒
    ∫ lborel (Normal ∘ g) = Normal (f b − f a)

⊢ ∀f i s t.
    FINITE t ∧ (∀a. a ∈ t ⇒ (f a has_integral i a) s) ⇒
    ((λx. ∑ (λa. f a x) t) has_integral ∑ i t) s

⊢ ∀f t.
    FINITE t ∧ (∀s. s ∈ t ⇒ f integrable_on s) ∧
    (∀s s'. s ∈ t ∧ s' ∈ t ∧ s ≠ s' ⇒ negligible (s ∩ s')) ⇒
    f integrable_on BIGUNION t ∧
    integral (BIGUNION t) f = sum t (λs. integral s f)

⊢ ∀f s y. (f has_integral y) s ⇒ integral s f = y

⊢ ∀f g s.
    f integrable_on s ∧ g integrable_on s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧
    (∀x. x ∈ s ⇒ 0 ≤ g x) ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
    integral s f ≤ integral s g

⊢ ∀f s. f integrable_on s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ integral s f

⊢ ∀s. (∀n. negligible (s n)) ⇒ negligible (BIGUNION (IMAGE s 𝕌(:num)))

⊢ 𝕌(:real) =
  BIGUNION
    (IMAGE (λi. interval [(real_of_int i,real_of_int i + 1)]) 𝕌(:int))

⊢ 𝕌(:real) =
  BIGUNION
    (IMAGE (λn. interval [(-&SUC n,-&n)] ∪ interval [(&n,&SUC n)]) 𝕌(:num))

⊢ ∀A X.
    indicator A absolutely_integrable_on X ⇔ indicator A integrable_on X

⊢ ∀E e.
    E ∈ measurable_sets lebesgue ∧ 0 < e ⇒
    ∃J. (∀i. closed_interval (J i)) ∧
        (∀i j. i ≠ j ⇒ nonoverlapping (J i) (J j)) ∧
        E ⊆ BIGUNION (IMAGE J 𝕌(:num)) ∧
        lmeasure E ≤ suminf (lmeasure ∘ J) ∧
        suminf (lmeasure ∘ J) ≤ lmeasure E + Normal e

⊢ ∀f. f ∈ borel_measurable (space borel,subsets borel) ⇒
      f ∈ borel_measurable (measurable_space lebesgue)

⊢ ∀f. f ∈ borel_measurable borel ⇒
      f ∈ borel_measurable (measurable_space lebesgue)

⊢ ∀s. s ∈ subsets borel ⇒ s ∈ measurable_sets lebesgue

⊢ ∀s. s ∈ null_set lborel ⇒ negligible s

⊢ null_set lborel ⊆ null_set lebesgue

⊢ closed_interval k ⇒ closed k

⊢ ∀s. closed_interval s ⇒ s ∈ measurable_sets lebesgue

⊢ closed_interval (interval [(a,b)])

⊢ ∀s t.
    closed_interval s ∧ closed_interval t ⇒
    (negligible (s ∩ t) ⇔ nonoverlapping s t)

⊢ ∀a b c d.
    a < b ∧ c < d ⇒
    (nonoverlapping (interval [(a,b)]) (interval [(c,d)]) ⇔ b ≤ c ∨ d ≤ a)

⊢ countably_additive lebesgue

⊢ ∀g E.
    gauge 𝕌(:real) g ∧ E ≠ ∅ ⇒
    ∃J t.
      (∀i. closed_interval (J i) ∧ t i ∈ E ∩ J i ∧
           J i ⊆ cball (t i,g (t i))) ∧
      (∀i j. J i ≠ J j ⇒ nonoverlapping (J i) (J j)) ∧
      E ⊆ BIGUNION (IMAGE J 𝕌(:num))

⊢ ∀g E.
    gauge g ∧ E ≠ ∅ ⇒
    ∃J t.
      (∀i. closed_interval (J i) ∧ t i ∈ E ∩ J i ∧ J i ⊆ g (t i)) ∧
      (∀i j. i ≠ j ⇒ nonoverlapping (J i) (J j)) ∧
      E ⊆ BIGUNION (IMAGE J 𝕌(:num))

⊢ ∀s y.
    s ∈ measurable_sets lebesgue ∧ lmeasure s = Normal y ⇒
    (indicator s has_integral y) 𝕌(:real)

⊢ ∀s. s ∈ measurable_sets lebesgue ∧ lmeasure s ≠ +∞ ⇒
      (indicator s has_integral real (lmeasure s)) 𝕌(:real)

⊢ ∀s y.
    s ∈ measurable_sets lebesgue ∧ lmeasure s = Normal y ⇒
    indicator s integrable_on 𝕌(:real) ∧
    integral 𝕌(:real) (indicator s) = y

⊢ ∀f. (Normal ∘ f)⁻ = Normal ∘ f⁻

⊢ ∀f. (Normal ∘ f)⁺ = Normal ∘ f⁺

⊢ ∀m f n x. fn_seq m (Normal ∘ f) n x = Normal (real_fn_seq m f n x)

⊢ ∀f n.
    f ∈ borel_measurable borel ∧ (∀x. 0 ≤ f x) ∧
    ∫⁺ lborel (Normal ∘ f) ≠ +∞ ⇒
    fn_seq_integral lborel (Normal ∘ f) n =
    Normal (real_fn_seq_integral f n)

⊢ ∀f n.
    f ∈ borel_measurable borel ∧ (∀x. 0 ≤ f x) ∧ f integrable_on 𝕌(:real) ⇒
    fn_seq_integral lborel (Normal ∘ f) n =
    Normal (real_fn_seq_integral f n)

⊢ ∀m f.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ∧
    (∀x. x ∈ m_space m ⇒ 0 ≤ f x) ⇒
    mono_increasing (fn_seq_integral m f)

⊢ ∀m f n.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ⇒
    0 ≤ fn_seq_integral m f n

⊢ ∀s A x.
    (indicator (s ∩ A) has_integral x) 𝕌(:real) ⇔
    (indicator s has_integral x) A

⊢ ∀E y. (indicator E has_integral y) 𝕌(:real) ⇒ lmeasure E = Normal y

⊢ ∀E y s.
    E ∈ measurable_sets lebesgue ∧ E ⊆ s ⇒
    (indicator E has_integral y) s ⇒
    lmeasure E = Normal y

⊢ ∀a b n.
    (indicator (interval [(a,b)]) has_integral
     content (interval [(a,b)] ∩ line n)) (line n)

⊢ ∀A. (∀n. indicator A integrable_on line n) ⇒ A ∈ measurable_sets lebesgue

⊢ ∀A n. A ∈ measurable_sets lebesgue ⇒ indicator A integrable_on line n

⊢ ∀s A.
    indicator (s ∩ A) integrable_on 𝕌(:real) ⇔ indicator s integrable_on A

⊢ ∀E y.
    E ∈ integrable_sets 𝕌(:real) ⇒
    lmeasure E = Normal (integral 𝕌(:real) (indicator E))

⊢ ∀E. indicator E integrable_on 𝕌(:real) ⇒ E ∈ measurable_sets lebesgue

⊢ ∀s. s ∈ integrable_sets 𝕌(:real) ⇒
      (indicator s has_integral real (lmeasure s)) 𝕌(:real)

⊢ ∀s. s ∈ integrable_sets 𝕌(:real) ⇔
      s ∈ measurable_sets lebesgue ∧ lmeasure s ≠ +∞

⊢ integrable_sets 𝕌(:real) ⊆ measurable_sets lebesgue

⊢ ∀s A. integral 𝕌(:real) (indicator (s ∩ A)) = integral A (indicator s)

⊢ ∀E y.
    E ∈ integrable_sets 𝕌(:real) ⇒
    lmeasure E ≠ +∞ ∧ integral 𝕌(:real) (indicator E) = real (lmeasure E)

⊢ ∀A. integral A (λx. 1) = integral 𝕌(:real) (indicator A)

⊢ ∀s. s ∈ subsets borel ⇒ lambda s = lmeasure s

⊢ measurable_sets lborel ⊆ measurable_sets lebesgue

⊢ ∀s t.
    s ∈ measurable_sets lebesgue ∧ t ∈ measurable_sets lebesgue ∧
    negligible (s ∩ t) ⇒
    lmeasure (s ∪ t) = lmeasure s + lmeasure t

⊢ ∀E e.
    E ∈ measurable_sets lebesgue ∧ 0 < e ⇒
    ∃s. s ∈ subsets borel ∧ E ⊆ s ∧ lmeasure E ≤ lambda s ∧
        lambda s ≤ lmeasure E + Normal e

⊢ ∀E e.
    E ∈ measurable_sets lebesgue ∧ 0 < e ⇒
    ∃s. fsigma s ∧ E ⊆ s ∧ lmeasure E ≤ lambda s ∧
        lambda s ≤ lmeasure E + Normal e

⊢ ∀a b. a ≤ b ⇒ lmeasure (interval [(a,b)]) = Normal (b − a)

⊢ ∀a b. lmeasure (interval [(a,b)]) = Normal (content (interval [(a,b)]))

⊢ ∀f s.
    f ∈ (𝕌(:num) → measurable_sets lebesgue) ∧
    (∀i j. i ≠ j ⇒ negligible (f i ∩ f j)) ∧ s = BIGUNION (IMAGE f 𝕌(:num)) ⇒
    suminf (lmeasure ∘ f) = lmeasure s

⊢ lmeasure ∅ = 0

⊢ ∀f. f ∈ borel_measurable borel ⇒
      (integrable lborel (Normal ∘ f) ⇔ f absolutely_integrable_on 𝕌(:real))

⊢ ∀f. integrable lborel (Normal ∘ f) ⇒
      f absolutely_integrable_on 𝕌(:real) ∧
      ∫ lborel (Normal ∘ f) = Normal (integral 𝕌(:real) f)

⊢ ∀f. f ∈ borel_measurable borel ∧ f absolutely_integrable_on 𝕌(:real) ⇒
      integrable lborel (Normal ∘ f) ∧
      ∫ lborel (Normal ∘ f) = Normal (integral 𝕌(:real) f)

⊢ ∀f. f ∈ borel_measurable borel ∧ (∀x. 0 ≤ f x) ∧
      ∫⁺ lborel (Normal ∘ f) ≠ +∞ ⇒
      f integrable_on 𝕌(:real) ∧
      ∫⁺ lborel (Normal ∘ f) = Normal (integral 𝕌(:real) f)

⊢ ∀f. f ∈ borel_measurable borel ∧ (∀x. 0 ≤ f x) ∧ f integrable_on 𝕌(:real) ⇒
      ∫⁺ lborel (Normal ∘ f) = Normal (integral 𝕌(:real) f)

⊢ ∀f. f ∈ borel_measurable borel ∧ (∀x. 0 ≤ f x) ∧
      bounded (IMAGE f 𝕌(:real)) ∧ ∫⁺ lborel (Normal ∘ f) ≠ +∞ ⇒
      f integrable_on 𝕌(:real) ∧
      ∫⁺ lborel (Normal ∘ f) = Normal (integral 𝕌(:real) f)

⊢ ∀f. f ∈ borel_measurable borel ∧ f integrable_on 𝕌(:real) ∧
      (∀x. 0 ≤ f x) ∧ bounded (IMAGE f 𝕌(:real)) ⇒
      ∫⁺ lborel (Normal ∘ f) = Normal (integral 𝕌(:real) f)

⊢ ∀s. s ∈ subsets borel ⇒ lmeasure s = lambda s

⊢ ∀s. negligible s ⇒ lmeasure s = 0

⊢ ∀a b. a ≤ b ⇒ lmeasure (interval (a,b)) = Normal (b − a)

⊢ ∀c. lmeasure {c} = 0

⊢ ∀A x.
    ((λk. indicator (BIGUNION {A i | i < k}) x) ⟶
     indicator (BIGUNION {A i | i ∈ 𝕌(:num)}) x) sequentially

⊢ ∀s. negligible s ⇒ lmeasure s = 0

⊢ ∀A m.
    A ∈ measurable_sets lebesgue ∧ 0 ≤ m ⇒
    (lmeasure A = Normal m ⇔
     ((λn. integral (line n) (indicator A)) ⟶ m) sequentially)

⊢ lmeasure =
  (λA. sup {Normal (integral (line n) (indicator A)) | n ∈ 𝕌(:num)})

⊢ measure_space lebesgue

⊢ ∀s. negligible s ⇔ s ∈ null_set lebesgue

⊢ ∀E e.
    negligible E ∧ 0 < e ⇒
    ∃s. s ∈ subsets borel ∧ E ⊆ s ∧ lambda s ≤ Normal e

⊢ ∀E. negligible E ⇒ ∃N. N ∈ null_set lborel ∧ E ⊆ N

⊢ ∀E. E ∈ null_set lebesgue ⇒ ∃N. N ∈ null_set lborel ∧ E ⊆ N

⊢ ∀s. s ∈ measurable_sets lebesgue ⇒ (negligible s ⇔ lmeasure s = 0)

⊢ ∀s. negligible s ⇒ s ∈ measurable_sets lebesgue

⊢ ∀s t. nonoverlapping s t ⇔ nonoverlapping t s

⊢ nonoverlapping s ∅ ∧ nonoverlapping ∅ s

⊢ ∀s t u v. nonoverlapping s t ∧ u ⊆ s ∧ v ⊆ t ⇒ nonoverlapping u v

⊢ ∀m f n.
    measure_space m ∧ f ∈ Borel_measurable (measurable_space m) ⇒
    ∫⁺ m (fn_seq m f n) = fn_seq_integral m f n

⊢ positive lebesgue

⊢ ∀f. f⁻ = (λx. 1 / 2 * (abs (f x) − f x))

⊢ ∀f. f⁺ = (λx. 1 / 2 * (f x + abs (f x)))

⊢ ∀m f n x. real_fn_seq m f n x = real (fn_seq m (Normal ∘ f) n x)

⊢ ∀f n.
    f ∈ borel_measurable borel ∧ (∀x. 0 ≤ f x) ∧
    ∫⁺ lborel (Normal ∘ f) ≠ +∞ ⇒
    (real_fn_seq lborel f n has_integral real_fn_seq_integral f n) 𝕌(:real)

⊢ ∀f n.
    f ∈ borel_measurable borel ∧ (∀x. 0 ≤ f x) ∧ f integrable_on 𝕌(:real) ⇒
    (real_fn_seq lborel f n has_integral real_fn_seq_integral f n) 𝕌(:real)

⊢ ∀f n.
    f ∈ borel_measurable borel ∧ (∀x. 0 ≤ f x) ∧
    ∫⁺ lborel (Normal ∘ f) ≠ +∞ ⇒
    real_fn_seq_integral f n = real (fn_seq_integral lborel (Normal ∘ f) n)

⊢ ∀f n.
    f ∈ borel_measurable borel ∧ (∀x. 0 ≤ f x) ∧ f integrable_on 𝕌(:real) ⇒
    fn_seq_integral lborel (Normal ∘ f) n ≠ +∞ ∧
    real_fn_seq_integral f n = real (fn_seq_integral lborel (Normal ∘ f) n)

⊢ ∀f. f ∈ borel_measurable borel ∧ (∀x. 0 ≤ f x) ∧
      ∫⁺ lborel (Normal ∘ f) ≠ +∞ ⇒
      mono_increasing (real_fn_seq_integral f)

⊢ ∀f. f ∈ borel_measurable borel ∧ (∀x. 0 ≤ f x) ∧ f integrable_on 𝕌(:real) ⇒
      mono_increasing (real_fn_seq_integral f)

⊢ ∀f n. f ∈ borel_measurable borel ⇒ 0 ≤ real_fn_seq_integral f n

⊢ measurable_sets lebesgue = {A | ∀n. indicator A integrable_on line n}

⊢ sigma_algebra (𝕌(:real),{A | ∀n. indicator A integrable_on line n})

⊢ m_space lebesgue = 𝕌(:real)