chore(analysis/box_integral): use GP instead of bot (#15939)

This is how this integral is called in the original paper.

src/analysis/box_integral/divergence_theorem.lean

@@ -18,8 +18,8 @@ equal to the sum of integrals of `f` over the faces of `I` taken with appropriat
 
 To make the proof work, we had to ban tagged partitions with “long and thin” boxes. More precisely,
 we use the following generalization of one-dimensional Henstock-Kurzweil integral to functions
-defined on a box in `ℝⁿ` (it corresponds to the value `⊥` of `box_integral.integration_params` in
-the definition of `box_integral.has_integral`).
+defined on a box in `ℝⁿ` (it corresponds to the value `box_integral.integration_params.GP = ⊥` of
+`box_integral.integration_params` in the definition of `box_integral.has_integral`).
 
 We say that `f : ℝⁿ → E` has integral `y : E` over a box `I ⊆ ℝⁿ` if for an arbitrarily small
 positive `ε` and an arbitrarily large `c`, there exists a function `r : ℝⁿ → (0, ∞)` such that for
@@ -40,6 +40,7 @@ Henstock-Kurzweil integral, integral, Stokes theorem, divergence theorem
 
 open_locale classical big_operators nnreal ennreal topological_space box_integral
 open continuous_linear_map (lsmul) filter set finset metric
+  box_integral.integration_params (GP GP_le)
 noncomputable theory
 
 universes u
@@ -139,12 +140,12 @@ we allow `f` to be non-differentiable (but still continuous) at a countable set
 TODO: If `n > 0`, then the condition at `x ∈ s` can be replaced by a much weaker estimate but this
 requires either better integrability theorems, or usage of a filter depending on the countable set
 `s` (we need to ensure that none of the faces of a partition contain a point from `s`). -/
-lemma has_integral_bot_pderiv (f : ℝⁿ⁺¹ → E) (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] E) (s : set ℝⁿ⁺¹)
+lemma has_integral_GP_pderiv (f : ℝⁿ⁺¹ → E) (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] E) (s : set ℝⁿ⁺¹)
   (hs : s.countable) (Hs : ∀ x ∈ s, continuous_within_at f I.Icc x)
   (Hd : ∀ x ∈ I.Icc \ s, has_fderiv_within_at f (f' x) I.Icc x) (i : fin (n + 1)) :
-  has_integral.{0 u u} I ⊥ (λ x, f' x (pi.single i 1)) box_additive_map.volume
-    (integral.{0 u u} (I.face i) ⊥ (λ x, f (i.insert_nth (I.upper i) x)) box_additive_map.volume -
-      integral.{0 u u} (I.face i) ⊥ (λ x, f (i.insert_nth (I.lower i) x))
+  has_integral.{0 u u} I GP (λ x, f' x (pi.single i 1)) box_additive_map.volume
+    (integral.{0 u u} (I.face i) GP (λ x, f (i.insert_nth (I.upper i) x)) box_additive_map.volume -
+      integral.{0 u u} (I.face i) GP (λ x, f (i.insert_nth (I.lower i) x))
         box_additive_map.volume) :=
 begin
   /- Note that `f` is continuous on `I.Icc`, hence it is integrable on the faces of all boxes
@@ -155,13 +156,14 @@ begin
     by_cases hxs : x ∈ s,
     exacts [Hs x hxs, (Hd x ⟨hx, hxs⟩).continuous_within_at] },
   set fI : ℝ → box (fin n) → E := λ y J,
-    integral.{0 u u} J ⊥ (λ x, f (i.insert_nth y x)) box_additive_map.volume,
+    integral.{0 u u} J GP (λ x, f (i.insert_nth y x)) box_additive_map.volume,
   set fb : Icc (I.lower i) (I.upper i) → fin n →ᵇᵃ[↑(I.face i)] E :=
-    λ x, (integrable_of_continuous_on ⊥ (box.continuous_on_face_Icc Hc x.2) volume).to_box_additive,
+    λ x, (integrable_of_continuous_on GP (box.continuous_on_face_Icc Hc x.2)
+      volume).to_box_additive,
   set F : fin (n + 1) →ᵇᵃ[I] E := box_additive_map.upper_sub_lower I i fI fb (λ x hx J, rfl),
   /- Thus our statement follows from some local estimates. -/
-  change has_integral I ⊥ (λ x, f' x (pi.single i 1)) _ (F I),
-  refine has_integral_of_le_Henstock_of_forall_is_o bot_le _ _ _ s hs _ _,
+  change has_integral I GP (λ x, f' x (pi.single i 1)) _ (F I),
+  refine has_integral_of_le_Henstock_of_forall_is_o GP_le _ _ _ s hs _ _,
   { /- We use the volume as an upper estimate. -/
     exact (volume : measure ℝⁿ⁺¹).to_box_additive.restrict _ le_top },
   { exact λ J, ennreal.to_real_nonneg },
@@ -193,7 +195,7 @@ begin
     have Hl : J.lower i ∈ Icc (J.lower i) (J.upper i) := set.left_mem_Icc.2 (J.lower_le_upper i),
     have Hu : J.upper i ∈ Icc (J.lower i) (J.upper i) := set.right_mem_Icc.2 (J.lower_le_upper i),
     have Hi : ∀ x ∈ Icc (J.lower i) (J.upper i),
-      integrable.{0 u u} (J.face i) ⊥ (λ y, f (i.insert_nth x y)) box_additive_map.volume,
+      integrable.{0 u u} (J.face i) GP (λ y, f (i.insert_nth x y)) box_additive_map.volume,
       from λ x hx, integrable_of_continuous_on _
         (box.continuous_on_face_Icc (Hc.mono $ box.le_iff_Icc.1 hJI) hx) volume,
     have hJδ' : J.Icc ⊆ closed_ball x δ ∩ I.Icc,
@@ -250,20 +252,20 @@ the sum of integrals of `f` over the faces of `I` taken with appropriate signs.
 
 More precisely, we use a non-standard generalization of the Henstock-Kurzweil integral and
 we allow `f` to be non-differentiable (but still continuous) at a countable set of points. -/
-lemma has_integral_bot_divergence_of_forall_has_deriv_within_at
+lemma has_integral_GP_divergence_of_forall_has_deriv_within_at
   (f : ℝⁿ⁺¹ → Eⁿ⁺¹) (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹) (s : set ℝⁿ⁺¹) (hs : s.countable)
   (Hs : ∀ x ∈ s, continuous_within_at f I.Icc x)
   (Hd : ∀ x ∈ I.Icc \ s, has_fderiv_within_at f (f' x) I.Icc x) :
-  has_integral.{0 u u} I ⊥ (λ x, ∑ i, f' x (pi.single i 1) i)
+  has_integral.{0 u u} I GP (λ x, ∑ i, f' x (pi.single i 1) i)
     box_additive_map.volume
-    (∑ i, (integral.{0 u u} (I.face i) ⊥ (λ x, f (i.insert_nth (I.upper i) x) i)
+    (∑ i, (integral.{0 u u} (I.face i) GP (λ x, f (i.insert_nth (I.upper i) x) i)
       box_additive_map.volume -
-      integral.{0 u u} (I.face i) ⊥ (λ x, f (i.insert_nth (I.lower i) x) i)
+      integral.{0 u u} (I.face i) GP (λ x, f (i.insert_nth (I.lower i) x) i)
         box_additive_map.volume)) :=
 begin
   refine has_integral_sum (λ i hi, _), clear hi,
   simp only [has_fderiv_within_at_pi', continuous_within_at_pi] at Hd Hs,
-  convert has_integral_bot_pderiv I _ _ s hs (λ x hx, Hs x hx i) (λ x hx, Hd x hx i) i
+  convert has_integral_GP_pderiv I _ _ s hs (λ x hx, Hs x hx i) (λ x hx, Hd x hx i) i
 end
 
 end box_integral

src/analysis/box_integral/partition/filter.lean

@@ -41,7 +41,8 @@ The structure `box_integral.integration_params` has 3 boolean fields with the fo
 
 * `bDistortion`: the value `tt` means that `r` can depend on the maximal ratio of sides of the same
   box of a partition. Presence of this case make quite a few proofs harder but we can prove the
-  divergence theorem only for the filter `⊥ = {bRiemann := ff, bHenstock := tt, bDistortion := tt}`.
+  divergence theorem only for the filter
+  `box_integral.integration_params.GP = ⊥ = {bRiemann := ff, bHenstock := tt, bDistortion := tt}`.
 
 ### Well-known sets of parameters
 
@@ -67,15 +68,15 @@ the library.
   that we allow tags to be outside of their boxes; the tags still have to be in the ambient closed
   box, and the partition still has to be subordinate to a function.
 
-* `⊥` (`bRiemann = ff`, `bHenstock = tt`, `bDistortion = tt`): this is the least integration theory
-  in our list, i.e., all functions integrable in any other theory is integrable in this one as well.
-  This is a non-standard generalization of the Henstock-Kurzweil integral to higher dimension.
-  In dimension one, it generates the same filter as `Henstock`. In higher dimension, this
-  generalization defines an integration theory such that the divergence of any Fréchet
-  differentiable function `f` is integrable, and its integral is equal to the sum of integrals of
-  `f` over the faces of the box, taken with appropriate signs.
+* `box_integral.integration_params.GP = ⊥` (`bRiemann = ff`, `bHenstock = tt`, `bDistortion = tt`):
+  this is the least integration theory in our list, i.e., all functions integrable in any other
+  theory is integrable in this one as well.  This is a non-standard generalization of the
+  Henstock-Kurzweil integral to higher dimension.  In dimension one, it generates the same filter as
+  `Henstock`. In higher dimension, this generalization defines an integration theory such that the
+  divergence of any Fréchet differentiable function `f` is integrable, and its integral is equal to
+  the sum of integrals of `f` over the faces of the box, taken with appropriate signs.
 
-  A function `f` is `⊥`-integrable if for any `ε > 0` and `c : ℝ≥0` there exists
+  A function `f` is `GP`-integrable if for any `ε > 0` and `c : ℝ≥0` there exists
   `r : (ι → ℝ) → {x : ℝ | 0 < x}` such that for any tagged partition `π` subordinate to `r`, if each
   tag belongs to the corresponding closed box and for each box `J ∈ π`, the maximal ratio of its
   sides is less than or equal to `c`, then the integral sum of `f` over `π` is `ε`-close to the
@@ -183,7 +184,8 @@ used in the definition of a box-integrable function.
 
 * `bDistortion`: the value `tt` means that `r` can depend on the maximal ratio of sides of the same
   box of a partition. Presence of this case makes quite a few proofs harder but we can prove the
-  divergence theorem only for the filter `⊥ = {bRiemann := ff, bHenstock := tt, bDistortion := tt}`.
+  divergence theorem only for the filter
+  `box_integral.integration_params.GP = ⊥ = {bRiemann := ff, bHenstock := tt, bDistortion := tt}`.
 -/
 @[ext] structure integration_params : Type :=
 (bRiemann bHenstock bDistortion : bool)
@@ -209,9 +211,10 @@ def iso_prod : integration_params ≃o bool × boolᵒᵈ × boolᵒᵈ :=
 instance : bounded_order integration_params :=
 iso_prod.symm.to_galois_insertion.lift_bounded_order
 
-/-- The value `⊥` (`bRiemann = ff`, `bHenstock = tt`, `bDistortion = tt`) corresponds to a
-generalization of the Henstock integral such that the Divergence theorem holds true without
-additional integrability assumptions, see the module docstring for details. -/
+/-- The value
+`box_integral.integration_params.GP = ⊥` (`bRiemann = ff`, `bHenstock = tt`, `bDistortion = tt`)
+corresponds to a generalization of the Henstock integral such that the Divergence theorem holds true
+without additional integrability assumptions, see the module docstring for details. -/
 instance : inhabited integration_params := ⟨⊥⟩
 
 instance : decidable_rel ((≤) : integration_params → integration_params → Prop) :=
@@ -239,10 +242,18 @@ discontinuous) positive function `r`; the tags may be outside of the correspondi
 (but still inside the ambient closed box `I.Icc`). -/
 def McShane : integration_params := ⟨ff, ff, ff⟩
 
+/-- The `box_integral.integration_params` corresponding to the generalized Perron integral. In the
+corresponding filter, we require that the tagged partition is subordinate to a (possibly,
+discontinuous) positive function `r` and each tag belongs to the corresponding closed box. We also
+require an upper estimate on the distortion of all boxes of the partition. -/
+def GP : integration_params := ⊥
+
 lemma Henstock_le_Riemann : Henstock ≤ Riemann := dec_trivial
 
 lemma Henstock_le_McShane : Henstock ≤ McShane := dec_trivial
 
+lemma GP_le : GP ≤ l := bot_le
+
 /-- The predicate corresponding to a base set of the filter defined by an
 `integration_params`. It says that
 

src/measure_theory/integral/divergence_theorem.lean

@@ -69,13 +69,13 @@ section
 ### Divergence theorem for functions on `ℝⁿ⁺¹ = fin (n + 1) → ℝ`.
 
 In this section we use the divergence theorem for a Henstock-Kurzweil-like integral
-`box_integral.has_integral_bot_divergence_of_forall_has_deriv_within_at` to prove the divergence
+`box_integral.has_integral_GP_divergence_of_forall_has_deriv_within_at` to prove the divergence
 theorem for Bochner integral. The divergence theorem for Bochner integral
 `measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable` assumes that the function
 itself is continuous on a closed box, differentiable at all but countably many points of its
 interior, and the divergence is integrable on the box.
 
-This statement differs from `box_integral.has_integral_bot_divergence_of_forall_has_deriv_within_at`
+This statement differs from `box_integral.has_integral_GP_divergence_of_forall_has_deriv_within_at`
 in several aspects.
 
 * We use Bochner integral instead of a Henstock-Kurzweil integral. This modification is done in
@@ -93,7 +93,7 @@ in several aspects.
 
 /-- An auxiliary lemma for
 `measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable`. This is exactly
-`box_integral.has_integral_bot_divergence_of_forall_has_deriv_within_at` reformulated for the
+`box_integral.has_integral_GP_divergence_of_forall_has_deriv_within_at` reformulated for the
 Bochner integral. -/
 lemma integral_divergence_of_has_fderiv_within_at_off_countable_aux₁ (I : box (fin (n + 1)))
   (f : ℝⁿ⁺¹ → Eⁿ⁺¹) (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹) (s : set ℝⁿ⁺¹) (hs : s.countable)
@@ -106,7 +106,7 @@ lemma integral_divergence_of_has_fderiv_within_at_off_countable_aux₁ (I : box
 begin
   simp only [← set_integral_congr_set_ae (box.coe_ae_eq_Icc _)],
   have A := ((Hi.mono_set box.coe_subset_Icc).has_box_integral ⊥ rfl),
-  have B := has_integral_bot_divergence_of_forall_has_deriv_within_at I f f' (s ∩ I.Icc)
+  have B := has_integral_GP_divergence_of_forall_has_deriv_within_at I f f' (s ∩ I.Icc)
     (hs.mono (inter_subset_left _ _)) (λ x hx, Hc _ hx.2)
     (λ x hx, Hd _ ⟨hx.1, λ h, hx.2 ⟨h, hx.1⟩⟩),
   rw continuous_on_pi at Hc,