Parameter-Dependent Integrals

[binghe]

Hi,

This PR adds two major lemmas for "Parameter-Dependent Integrals" (Chapter 12 of [1]). The first one "continuty lemma" says that if a (parameterized) function u(x,t) is continuous (w.r.t. t), so is its integration (w.r.t. x). The second "differentiable lemma" says that its integration is differentiable if itself is, i.e. the derivative operation and integration is exchangeable:

   [continuity_lemma]  Theorem (martingaleTheory)
      ⊢ ∀s m u.
          measure_space m ∧ open s ∧
          (∀t. t ∈ s ⇒ integrable m (Normal ∘ u t)) ∧
          (∀x. x ∈ m_space m ⇒ (λt. u t x) continuous_on s) ∧
          (∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x ∧ w x ≠ +∞) ∧
               ∀t x. t ∈ s ∧ x ∈ m_space m ⇒ Normal (abs (u t x)) ≤ w x) ⇒
          (λt. real (∫ m (Normal ∘ u t))) continuous_on s

   [differentiable_lemma]  Theorem (martingaleTheory)
      ⊢ ∀s m u.
          measure_space m ∧ open s ∧ connected s ∧
          (∀t. t ∈ s ⇒ integrable m (Normal ∘ u t)) ∧
          (∀x. x ∈ m_space m ⇒ (λt. u t x) differentiable_on s) ∧
          (∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x ∧ w x ≠ +∞) ∧
               ∀t x.
                 t ∈ s ∧ x ∈ m_space m ⇒
                 Normal (abs (diff1 (λt. u t x) t)) ≤ w x) ⇒
          ∀t. t ∈ s ⇒
              integrable m (λx. Normal (diff1 (λt. u t x) t)) ∧
              ((λt. real (∫ m (Normal ∘ u t))) has_vector_derivative
               real (∫ m (λx. Normal (diff1 (λt. u t x) t))))
                (at t within s)

The above theorems are based on Lebesgue integration over a general measure space. Specializing it to lborel with the equivalence between Lebesgue and Guage integration used, we have the following two practical theorems (in examples/probability/distributionTheory):

[gauge_continuity_lemma] (distributionTheory)
    ⊢ ∀u. (∀t. integrable lborel (Normal ∘ u t)) ∧
          (∀x. (λt. u t x) continuous_on 𝕌(:real)) ∧
          (∃w. integrable lborel w ∧ (∀x. 0 ≤ w x ∧ w x ≠ +∞) ∧
               ∀t x. Normal (abs (u t x)) ≤ w x) ⇒
          (λt. integral 𝕌(:real) (u t)) continuous_on 𝕌(:real)

[gauge_differentiable_lemma]
    ⊢ ∀u. (∀t. integrable lborel (Normal ∘ u t)) ∧
          (∀x. (λt. u t x) differentiable_on 𝕌(:real)) ∧
          (∃w. integrable lborel w ∧ (∀x. 0 ≤ w x ∧ w x ≠ +∞) ∧
               ∀t x. Normal (abs (diff1 (λt. u t x) t)) ≤ w x) ⇒
          ∀t. integrable lborel (λx. Normal (diff1 (λt. u t x) t)) ∧
              diff1 (λt. integral 𝕌(:real) (u t)) t =
              integral 𝕌(:real) (λx. diff1 (λt. u t x) t)

where diff1 is a new overload of diffn 1 (defined in limTheory). And from the conclusion of the 2nd lemma it's easier to see how diff1 and integral are exchanged. This lemma will play a crucial role in the remaining work of the CLT project.

This is the first time I deal with proofs involving both Lebesgue integration and derivatives. Many new lemmas are either added manually or ported from HOL-Light. The proofs essentially depend on Lebesgue Dominated Convergence, which is improved now by moving one "integrable" condition from antecedents to conclusion:

   [lebesgue_dominated_convergence]  Theorem (martingaleTheory)
      ⊢ ∀m f fi.
          measure_space m ∧ (∀i. integrable m (fi i)) ∧
          (∀i x. x ∈ m_space m ⇒ fi i x ≠ +∞ ∧ fi i x ≠ −∞) ∧
          (∀x. x ∈ m_space m ⇒ f x ≠ +∞ ∧ f x ≠ −∞) ∧
          (∀x. x ∈ m_space m ⇒
               ((λi. real (fi i x)) ⟶ real (f x)) sequentially) ∧
          (∃w. integrable m w ∧ (∀x. x ∈ m_space m ⇒ 0 ≤ w x ∧ w x ≠ +∞) ∧
               ∀i x. x ∈ m_space m ⇒ abs (fi i x) ≤ w x) ⇒
          integrable m f ∧
          ((λi. real (∫ m (fi i))) ⟶ real (∫ m f)) sequentially

One key device for proving the differentiable_lemma is the following lemma added in real_topologyTheory:

   [LIM_WITHIN_SEQUENTIALLY]  Theorem (real_topologyTheory)
      ⊢ ∀f s a l.
          (f ⟶ l) (at a within s) ⇔
          ∀x. (∀n. x n ∈ s DELETE a) ∧ (x ⟶ a) sequentially ⇒
              (f ∘ x ⟶ l) sequentially

HOL-Light has this lemma, but the porting progress was tried and failed due to some essential differences between HOL4's netsTheory and HOL-Light's nets formalization. I added some new definitions and theorems into netsTheory to try to fix the gaps. The work is not finished, but safe to merge. Now I decide to make a new proof (following another similar proof in real_topologyTheory) to save time for more important work.

--Chun

[1] Schilling, R.L.: Measures, Integrals and Martingales (Second Edition).
Cambridge University Press (2017).

[binghe]

Added further a lemma for interchanging higher-differentiation and integration:

gauge_higher_differentiable_lemma
    ⊢ ∀u. (∀t. integrable lborel (Normal ∘ u t)) ∧
          (∀n t x. higher_differentiable n (λt. u t x) t) ∧
          (∃w. integrable lborel w ∧ (∀x. 0 ≤ w x ∧ w x ≠ +∞) ∧
               ∀n t x. Normal (abs (diffn n (λt. u t x) t)) ≤ w x) ⇒
          ∀n t.
            higher_differentiable n (λt. integral 𝕌(:real) (u t)) t ∧
            integrable lborel (λx. Normal (diffn n (λt. u t x) t)) ∧
            diffn n (λt. integral 𝕌(:real) (u t)) t =
            integral 𝕌(:real) (λx. diffn n (λt. u t x) t)

[mn200]

Thanks for all the ongoing work on this!