Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-19 02:24 04094c4b

View on Github →

feat(analysis/box_integral): Divergence thm for a Henstock-style integral (#9496)

  • Define integrals of Riemann, McShane, and Henstock (plus a few variations).
  • Prove basic properties.
  • Prove a version of the divergence theorem for one of these integrals.
  • Prove that a Bochner integrable function is McShane integrable.

Estimated changes

added theorem
added structure
added structure box_integral.prepartition