Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hc : ∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : 2 * μ.toBoxAdditive I * ε₁ < ε
C : ℝ
hC : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) := {x | x ∈ Box.Icc I ∧ ¬ContinuousWithinAt f (Box.Icc I) x}
μ' : Measure (ι → ℝ) := μ.restrict (Box.Icc I)
μ'D : μ' D = 0
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : μ' U < ENNReal.ofReal ε₂
comp : IsCompact (Box.Icc I \ U)
this : ∀ x ∈ Box.Icc I \ U, oscillationWithin f (Box.Icc I) x < ENNReal.ofReal ε₁
r : ℝ
r0 : r > 0
hr : ∀ x ∈ Box.Icc I \ U, ediam (f '' (eball x (ENNReal.ofReal r) ∩ Box.Icc I)) ≤ ENNReal.ofReal ε₁
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₁) π₁
h₁p : π₁.IsPartition
h₂ : l.MemBaseSet I c₂ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₂) π₂
h₂p : π₂.IsPartition
μI : μ ↑I < ∞
t₁ : Box ι → ι → ℝ := fun J ↦ (π₁.infPrepartition π₂.toPrepartition).tag J
t₂ : Box ι → ι → ℝ := fun J ↦ (π₂.infPrepartition π₁.toPrepartition).tag J
B : Finset (Box ι) := (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes
B' : Finset (Box ι) := {J ∈ B | ↑J ⊆ U}
hB' : B' ⊆ B
μJ_ne_top : ∀ J ∈ B, μ ↑J ≠ ∞
un : ∀ S ⊆ B, ⋃ J ∈ S, ↑J ⊆ ↑I
⊢ ‖∑ x ∈ B \ B',
        μ.toBoxAdditive x •
          (f ((π₁.infPrepartition π₂.toPrepartition).tag x) - f ((π₂.infPrepartition π₁.toPrepartition).tag x))‖ ≤
    ε / 2

Tactic:
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'

Goal state after: