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.

Author: urkud

docs/references.bib

@@ -552,6 +552,17 @@ @Book{            GierzEtAl1980
   mrreviewer    = {James W. Lea, Jr.}
 }
 
+@Book{            Gordon55,
+  author        = {Russel A. Gordon},
+  title         = {The integrals of Lebesgue, Denjoy, Perron, and
+                   Henstock},
+  isbn          = {0-8218-3805-9},
+  year          = {1955},
+  series        = {Graduate Studies in Mathematics},
+  volume        = 4,
+  publisher     = {American Mathematical Society, Providence, R.I}
+}
+
 @Book{            gouvea1997,
   author        = {Gouv\^{e}a, Fernando Q.},
   title         = {{$p$}-adic numbers},

src/algebra/order/field.lean

@@ -582,6 +582,10 @@ begin
     ← lt_sub_iff_add_lt, sub_self_div_two, sub_self_div_two, div_lt_div_right (@zero_lt_two α _ _)]
 end
 
+lemma left_lt_add_div_two : a < (a + b) / 2 ↔ a < b := by simp [lt_div_iff, mul_two]
+
+lemma add_div_two_lt_right : (a + b) / 2 < b ↔ a < b := by simp [div_lt_iff, mul_two]
+
 /--  An inequality involving `2`. -/
 lemma sub_one_div_inv_le_two (a2 : 2 ≤ a) :
   (1 - 1 / a)⁻¹ ≤ 2 :=
@@ -643,6 +647,14 @@ end
 lemma exists_add_lt_and_pos_of_lt (h : b < a) : ∃ c : α, b + c < a ∧ 0 < c :=
 ⟨(a - b) / 2, add_sub_div_two_lt h, div_pos (sub_pos_of_lt h) zero_lt_two⟩
 
+lemma exists_pos_mul_lt {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ b * c < a :=
+begin
+  have : 0 < a / max (b + 1) 1, from div_pos h (lt_max_iff.2 (or.inr zero_lt_one)),
+  refine ⟨a / max (b + 1) 1, this, _⟩,
+  rw [← lt_div_iff this, div_div_cancel' h.ne'],
+  exact lt_max_iff.2 (or.inl $ lt_add_one _)
+end
+
 lemma le_of_forall_sub_le (h : ∀ ε > 0, b - ε ≤ a) : b ≤ a :=
 begin
   contrapose! h,