Zulip Chat Archive

Stream: maths

Topic: Integrals in other systems?

Yury G. Kudryashov (Jan 31 2022 at 17:20):

I have a question to people who use Isabelle/Coq: what definition of the integral do these systems (or their most popular libraries) use (a) in dimension one (i.e., integrals over intervals); (b) in higher dimension (integrals over boxes and other sets in $\mathbb R^n$ )?

Patrick Massot (Jan 31 2022 at 17:23):

Sébastien often says that Isabelle couldn't choose an integral and this is a pain.

Yury G. Kudryashov (Jan 31 2022 at 17:58):

More precisely: which integrals do they use for Green's formula / divergence theorem?

Yury G. Kudryashov (Jan 31 2022 at 18:06):

Semi-offtopic: it turns out that I've reinvented a wheel in #9496: the integral I used to prove the divergence theorem is called GP-integral and was introduced by Mawhin in 1981.

Wenda Li (Jan 31 2022 at 18:24):

In Isabelle, it is the latter -- most of the integral libraries are developed for Euclidean space. For example, a lemma to establish the equivalence between Lebesgue integral and Gauge integral is of the following form:

lemma has_integral_integral_lebesgue_on:
  fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
  assumes "integrable (lebesgue_on S) f" "S ∈ sets lebesgue"
  shows "(f has_integral (integral⇧L (lebesgue_on S) f)) S"

For Green's theorem, the partial derivative is defined as follows:

definition has_partial_vector_derivative:: "(('a::euclidean_space) ⇒ 'b::euclidean_space) ⇒ 'a ⇒ ( 'b) ⇒ ('a) ⇒ bool" where
  "has_partial_vector_derivative F base_vec F' a
        ≡ ((λx. F( (a - ((a ∙ base_vec) *⇩R base_vec)) + x *⇩R base_vec ))
                has_vector_derivative F') (at (a ∙ base_vec))"

while the final result is in R^2.

Yury G. Kudryashov (Jan 31 2022 at 18:33):

Which Gauge integral do they use?

Yury G. Kudryashov (Jan 31 2022 at 18:33):

What do they assume in the Green's theorem?

Yury G. Kudryashov (Jan 31 2022 at 18:34):

(I mean, beyond differentiability of the function)

Yury G. Kudryashov (Jan 31 2022 at 18:34):

Possibly, I should learn to read Isabelle but I doubt I can do it before the ITP deadline.

Wenda Li (Jan 31 2022 at 18:36):

Yury G. Kudryashov said:

Which Gauge integral do they use?

It is Henstock–Kurzweil integral. I am not sure if there is another Gauge integral...

Yury G. Kudryashov (Jan 31 2022 at 18:37):

There is more than one generalization of H.-K. to higher dimensions.

Yury G. Kudryashov (Jan 31 2022 at 18:39):

And they require different assumptions in the Green's formula.

Yury G. Kudryashov (Jan 31 2022 at 18:39):

https://www.sciencedirect.com/science/article/pii/B9780444502636500142

Wenda Li (Jan 31 2022 at 18:40):

Yury G. Kudryashov said:

There is more than one generalization of H.-K. to higher dimensions.

I see. Here is the definition of Gauge integral in Isabelle:

definition has_integral :: "('n::euclidean_space ⇒ 'b::real_normed_vector) ⇒ 'b ⇒ 'n set ⇒ bool"
  (infixr "has'_integral" 46)
  where "(f has_integral I) s ⟷
    (if ∃a b. s = cbox a b
      then ((λp. ∑(x,k)∈p. content k *⇩R f x) ⤏ I) (division_filter s)
      else (∀e>0. ∃B>0. ∀a b. ball 0 B ⊆ cbox a b ⟶
        (∃z. ((λp. ∑(x,k)∈p. content k *⇩R (if x ∈ s then f x else 0)) ⤏ z) (division_filter (cbox a b)) ∧
          norm (z - I) < e)))"

Is it the most general form?

Yury G. Kudryashov (Jan 31 2022 at 18:40):

:up: Quite a few generalizations of H.-K. are listed in Sec. 4.5

Yury G. Kudryashov (Jan 31 2022 at 18:41):

What is the division_filter? Could you please share a link to this definition on some docs website?

Wenda Li (Jan 31 2022 at 18:46):

Here is the theory file for defining HK integral: https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Henstock_Kurzweil_Integration.html
And the one for formulating Green's theorem: https://www.isa-afp.org/browser_info/current/AFP/Green/Green.html.
I was told the Green's theorem formulation was not entirely satisfactory though.

Yury G. Kudryashov (Jan 31 2022 at 18:50):

I see that their assumptions imply integrability of partial derivatives.

Yury G. Kudryashov (Jan 31 2022 at 18:54):

A few minutes of reading Isabelle docs and I already miss mathlib-style docstrings.

Yury G. Kudryashov (Jan 31 2022 at 19:26):

What about Coq?

Wenda Li (Jan 31 2022 at 19:35):

I am not Coq expert but my impression is that they are mostly using Riemann integrals, and Coquelicot (http://coquelicot.saclay.inria.fr) is probably one of their most popular library for analysis.