-- Module: Mathlib.Analysis.BoxIntegral.Basic
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
this :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x →
      oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x < ENNReal.ofReal ε₁
r : ℝ
r0 : r > 0
hr :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x →
      ediam (f '' (eball x (ENNReal.ofReal r) ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) ≤ ENNReal.ofReal ε₁
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ :
  l.MemBaseSet I c₁
    ((fun (x : ℝ≥0) (x_1 : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) (r / 2) ⋯)
      c₁)
    π₁
h₁p : π₁.IsPartition
h₂ :
  l.MemBaseSet I c₂
    ((fun (x : ℝ≥0) (x_1 : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) (r / 2) ⋯)
      c₂)
    π₂
h₂p : π₂.IsPartition
μI : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t₁ : (J : Box ι) → ι → ℝ := fun (J : Box ι) ↦ (π₁.infPrepartition π₂.toPrepartition).tag J
t₂ : (J : Box ι) → ι → ℝ := fun (J : Box ι) ↦ (π₂.infPrepartition π₁.toPrepartition).tag J
B : Finset (Box ι) := (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes
let let₁ let₂ :
  norm.{v} (E := E)
      (∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
        HSMul.hSMul (α := ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) x : ℝ)
          (f ((π₁.infPrepartition π₂.toPrepartition).tag x) - f ((π₂.infPrepartition π₁.toPrepartition).tag x))) ≤
    ε
let₃ :
  let B' := {J ∈ B | (↑J : Set (ι → ℝ)) ⊆ U};
  ∀ (hB' : B' ⊆ B),
    norm.{v} (E := E)
        (∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
          HSMul.hSMul (α := ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) x : ℝ)
            (f ((π₁.infPrepartition π₂.toPrepartition).tag x) - f ((π₂.infPrepartition π₁.toPrepartition).tag x))) ≤
      ε
let₄ :
  let B' := {J ∈ B | (↑J : Set (ι → ℝ)) ⊆ U};
  ∀ (hB' : B' ⊆ B)
    (μJ_ne_top : ∀ J ∈ B, Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑J : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    norm.{v} (E := E)
        (∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
          HSMul.hSMul (α := ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) x : ℝ)
            (f ((π₁.infPrepartition π₂.toPrepartition).tag x) - f ((π₂.infPrepartition π₁.toPrepartition).tag x))) ≤
      ε
let₅ :
  let B' := {J ∈ B | (↑J : Set (ι → ℝ)) ⊆ U};
  ∀ (hB' : B' ⊆ B)
    (μJ_ne_top : ∀ J ∈ B, Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑J : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (un : ∀ S ⊆ B, ⋃ J ∈ S, (↑J : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))),
    norm.{v} (E := E)
        (∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
          HSMul.hSMul (α := ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) x : ℝ)
            (f ((π₁.infPrepartition π₂.toPrepartition).tag x) - f ((π₂.infPrepartition π₁.toPrepartition).tag x))) ≤
      ε
let₆ :
  let B' := {J ∈ B | (↑J : Set (ι → ℝ)) ⊆ U};
  ∀ (hB' : B' ⊆ B)
    (μJ_ne_top : ∀ J ∈ B, Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑J : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (un : ∀ S ⊆ B, ⋃ J ∈ S, (↑J : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))),
    ‖HAdd.hAdd (α := E)
          (∑ x ∈ B \ B',
            HSMul.hSMul (α := ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) x : ℝ)
              (f ((π₁.infPrepartition π₂.toPrepartition).tag x) - f ((π₂.infPrepartition π₁.toPrepartition).tag x)))
          (∑ x ∈ B',
            HSMul.hSMul (α := ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) x : ℝ)
              (f ((π₁.infPrepartition π₂.toPrepartition).tag x) - f ((π₂.infPrepartition π₁.toPrepartition).tag x)))‖ ≤
      ε / 2 + ε / 2
let₇ :
  let B' := {J ∈ B | (↑J : Set (ι → ℝ)) ⊆ U};
  ∀ (hB' : B' ⊆ B)
    (μJ_ne_top : ∀ J ∈ B, Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑J : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (un : ∀ S ⊆ B, ⋃ J ∈ S, (↑J : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))),
    norm.{v} (E := E)
        (∑ x ∈ B \ B',
          HSMul.hSMul (α := ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) x : ℝ)
            (f ((π₁.infPrepartition π₂.toPrepartition).tag x) - f ((π₂.infPrepartition π₁.toPrepartition).tag x))) ≤
      ε / 2
let₈ let₉ :
  let B' := {J ∈ B | (↑J : Set (ι → ℝ)) ⊆ U};
  ∀ (hB' : B' ⊆ B)
    (μJ_ne_top : ∀ J ∈ B, Ne (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑J : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (un : ∀ S ⊆ B, ⋃ J ∈ S, (↑J : Set (ι → ℝ)) ⊆ (↑I : Set (ι → ℝ))),
    norm.{v} (E := E)
        (∑ x ∈ B',
          HSMul.hSMul (α := ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) x : ℝ)
            (f ((π₁.infPrepartition π₂.toPrepartition).tag x) - f ((π₂.infPrepartition π₁.toPrepartition).tag x))) ≤
      ε / 2
⊢ norm.{v} (E := E)
      (∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
        HSMul.hSMul (α := ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) x : ℝ)
          (f ((π₁.infPrepartition π₂.toPrepartition).tag x) - f ((π₂.infPrepartition π₁.toPrepartition).tag x))) ≤
    ε

Tactic:
classical
  let B' := {J ∈ B | J.toSet ⊆ U}
  have hB' : B' ⊆ B := B.filter_subset (fun J ↦ J.toSet ⊆ U)
  have μJ_ne_top : ∀ J ∈ B, μ J ≠ ⊤ :=
    fun J hJ ↦ lt_top_iff_ne_top.1 <| lt_of_le_of_lt (μ.mono (Prepartition.le_of_mem' _ J hJ)) μI
  have un : ∀ S ⊆ B, ⋃ J ∈ S, J.toSet ⊆ I.toSet :=
    fun S hS ↦ iUnion_subset_iff.2 (fun J ↦ iUnion_subset_iff.2 fun hJ ↦ le_of_mem' _ J (hS hJ))
  rw [← sum_sdiff hB', ← add_halves ε]
  apply le_trans (norm_add_le _ _) (add_le_add ?_ ?_)
  /- If a box J is not contained within U, then the oscillation of f on J is small, which bounds
     the contribution of J to the overall sum. -/
  · have : ∀ J ∈ B \ B', ‖μ.toBoxAdditive J • (f (t₁ J) - f (t₂ J))‖ ≤ μ.toBoxAdditive J * ε₁ := by
      intro J hJ
      rw [Finset.mem_sdiff, B.mem_filter, not_and] at hJ
      rw [norm_smul, μ.toBoxAdditive_apply, Real.norm_of_nonneg measureReal_nonneg]
      gcongr _ * ?_
      obtain ⟨x, xJ, xnU⟩ : ∃ x ∈ J, x ∉ U := Set.not_subset.1 (hJ.2 hJ.1)
      have hx : x ∈ Box.Icc I \ U := ⟨Box.coe_subset_Icc ((le_of_mem' _ J hJ.1) xJ), xnU⟩
      have ineq : edist (f (t₁ J)) (f (t₂ J)) ≤ ediam (f '' (ball x r ∩ (Box.Icc I))) := by
        apply edist_le_ediam_of_mem <;>
          refine Set.mem_image_of_mem f ⟨?_, tag_mem_Icc _ J⟩ <;>
          refine closedBall_subset_ball (div_two_lt_of_pos r0) <| mem_closedBall_comm.1 ?_
        · exact h₁.isSubordinate.infPrepartition π₂.toPrepartition J hJ.1 (Box.coe_subset_Icc xJ)
        · exact h₂.isSubordinate.infPrepartition π₁.toPrepartition J
            ((π₁.mem_infPrepartition_comm).1 hJ.1) (Box.coe_subset_Icc xJ)
      rw [← Metric.eball_ofReal] at ineq
      simpa only [edist_le_ofReal (le_of_lt ε₁0), dist_eq_norm, hJ.1] using ineq.trans (hr x hx)
    refine (norm_sum_le _ _).trans <| (sum_le_sum this).trans ?_
    rw [← sum_mul]
    trans μ.toBoxAdditive I * ε₁; swap
    · linarith
    simp_rw [mul_le_mul_iff_left₀ ε₁0, μ.toBoxAdditive_apply]
    refine le_trans ?_ <| toReal_mono (lt_top_iff_ne_top.1 μI) <| μ.mono <| un (B \ B') sdiff_subset
    simp_rw [measureReal_def]
    rw [← toReal_sum (fun J hJ ↦ μJ_ne_top J (mem_sdiff.1 hJ).1), ← Finset.tsum_subtype]
    refine (toReal_mono <| ne_of_lt <| lt_of_le_of_lt (μ.mono <| un (B \ B') sdiff_subset) μI) ?_
    refine le_of_eq (measure_biUnion (countable_toSet _) ?_ (fun J _ ↦ J.measurableSet_coe)).symm
    exact fun J hJ J' hJ' hJJ' ↦ pairwiseDisjoint _ (mem_sdiff.1 hJ).1 (mem_sdiff.1 hJ').1 hJJ'
  -- The contribution of the boxes contained within U is bounded because f is bounded and μ U < ε₂.
  · have : ∀ J ∈ B', ‖μ.toBoxAdditive J • (f (t₁ J) - f (t₂ J))‖ ≤ μ.toBoxAdditive J * (2 * C) := by
      intro J _
      rw [norm_smul, μ.toBoxAdditive_apply, Real.norm_of_nonneg measureReal_nonneg, two_mul]
      gcongr
      apply norm_sub_le_of_le <;> exact hC _ (TaggedPrepartition.tag_mem_Icc _ J)
    apply (norm_sum_le_of_le B' this).trans
    simp_rw [← sum_mul, μ.toBoxAdditive_apply, measureReal_def,
      ← toReal_sum (fun J hJ ↦ μJ_ne_top J (hB' hJ))]
    suffices (∑ J ∈ B', μ J).toReal ≤ ε₂ by
      linarith [mul_le_mul_of_nonneg_right this <| (mul_nonneg_iff_of_pos_left two_pos).2 C0]
    rw [← toReal_ofReal (le_of_lt ε₂0)]
    refine toReal_mono ofReal_ne_top (le_trans ?_ (le_of_lt hU))
    trans μ' (⋃ J ∈ B', J)
    · simp only [μ', μ.restrict_eq_self <| (un _ hB').trans I.coe_subset_Icc]
      exact le_of_eq <| Eq.symm <| measure_biUnion_finset
        (fun J hJ K hK hJK ↦ pairwiseDisjoint _ (hB' hJ) (hB' hK) hJK) fun J _ ↦ J.measurableSet_coe
    · apply μ'.mono
      simp_rw [iUnion_subset_iff]
      exact fun J hJ ↦ (mem_filter.1 hJ).2

Premises used: MeasureTheory.measure_biUnion, add_halves, Set.iUnion_subset_iff, MeasureTheory.OuterMeasure.mono, add_le_add, le_of_lt, norm_add_le, lt_top_iff_ne_top, MeasureTheory.Measure.toBoxAdditive, ENNReal.toReal_ofReal, MeasureTheory.Measure.toOuterMeasure, And.right, MeasureTheory.Measure.toBoxAdditive_apply, Iff.mp, Finset.countable_toSet, Finset.mem_filter, MeasureTheory.measureReal_def, Finset.sum_le_sum, ENNReal.ofReal_ne_top, LE.le.trans, le_of_eq, mul_le_mul_iff_left₀, Eq.symm, ENNReal.toReal_mono, DFunLike.coe, Finset.tsum_subtype, norm_sum_le, MeasureTheory.Measure.restrict_eq_self, Finset.sum_mul, le_trans