Gluing Henstock integrals along a finite box partition

A gauge can prevent tags from crossing the faces of a fixed finite partition. Refinement then preserves the Henstock condition, allowing genuinely conditional integrals on the pieces to glue.

theorem BoxIntegral.Box.mem_Icc_of_coe_eq_inf {ι : Type u_1} {A B C : Box ι} {x : ι → ℝ} (h : ↑C = ↑A ⊓ ↑B) (hxA : x ∈ Box.Icc A) (hxB : x ∈ Box.Icc B) : x ∈ Box.Icc C

A point in both closed boxes lies in the closed box representing their intersection.

theorem BoxIntegral.TaggedPrepartition.infPrepartition_tag_of_mem {ι : Type u_1} {I K : Box ι} {π : TaggedPrepartition I} {p : Prepartition I} {A : Box ι} (hA : A ∈ π) (hK : K ∈ p.restrict A) : (π.infPrepartition p).tag K = π.tag A

In the refinement π.infPrepartition p, any box K ∈ p.restrict A inherits the tag of the box A ∈ π containing it.

theorem BoxIntegral.Prepartition.exists_gauge_tag_mem_Icc {ι : Type u_1} {I : Box ι} [Fintype ι] (p : Prepartition I) : ∃ (r : (ι → ℝ) → ↑(Set.Ioi 0)), ∀ (x z : ι → ℝ), z ∈ Metric.closedBall x ↑(r x) → ∀ J ∈ p, z ∈ Box.Icc J → x ∈ Box.Icc J

A finite box prepartition admits a gauge preventing tags from crossing its faces.

theorem BoxIntegral.Prepartition.infPrepartition_tag_mem_Icc_of_gauge {ι : Type u_1} {I J K : Box ι} [Fintype ι] (p : Prepartition I) {π : TaggedPrepartition I} {r : (ι → ℝ) → ↑(Set.Ioi 0)} (hr : ∀ (x z : ι → ℝ), z ∈ Metric.closedBall x ↑(r x) → ∀ J ∈ p, z ∈ Box.Icc J → x ∈ Box.Icc J) (hπ : π.IsSubordinate r) (hJ : J ∈ p) (hK : K ∈ π.restrict J) : (π.infPrepartition p).tag K ∈ Box.Icc J

Refinement tags remain in the fixed piece when its gauge prevents face crossing.

theorem BoxIntegral.Prepartition.isHenstock_infPrepartition_of_gauge {ι : Type u_1} {I : Box ι} [Fintype ι] (p : Prepartition I) {π : TaggedPrepartition I} {r : (ι → ℝ) → ↑(Set.Ioi 0)} (hr : ∀ (x z : ι → ℝ), z ∈ Metric.closedBall x ↑(r x) → ∀ J ∈ p, z ∈ Box.Icc J → x ∈ Box.Icc J) (hπ : π.IsSubordinate r) (hH : π.IsHenstock) : (π.infPrepartition p).IsHenstock

A gauge preventing face crossing preserves the Henstock condition under refinement.

theorem TauCeti.BoxIntegral.hasIntegral_Henstock_of_partition {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {I : BoxIntegral.Box ι} [Fintype ι] {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} (p : BoxIntegral.Prepartition I) (hp : p.IsPartition) (y : BoxIntegral.Box ι → F) (hy : ∀ J ∈ p, BoxIntegral.HasIntegral J BoxIntegral.IntegrationParams.Henstock f vol (y J)) : BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.Henstock f vol (∑ J ∈ p.boxes, y J)

Genuine Henstock integrals on the members of a finite box partition glue to an integral on the entire box. No absolute-integrability or primitive hypothesis is used.