-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
Hd :
  ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Ioo : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivAt (𝕜 := ℝ) f (f' x) x
Hi :
  IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : Fin (n + 1) → ℝ) ↦
      ∑ i : Fin (n + 1),
        (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i)
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) volume
J : ℕ →o Box (Fin (n + 1))
hJ_sub :
  ∀ (n_1 : ℕ),
    Subset (α := Set (Fin (n + 1) → ℝ))
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
          ((J : (a : ℕ) → Box (Fin (n + 1))) n_1 : Box (Fin (n + 1))) :
        Set (Fin (n + 1) → ℝ))
      ((Box.Ioo : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ))
hJl :
  ∀ (x : Fin (n + 1)),
    Tendsto (fun (i : ℕ) ↦ (Box.lower ∘ (⇑J : (a : ℕ) → Box (Fin (n + 1)))) i x) atTop (𝓝 (I.lower x))
hJu :
  ∀ (x : Fin (n + 1)),
    Tendsto (fun (i : ℕ) ↦ (Box.upper ∘ (⇑J : (a : ℕ) → Box (Fin (n + 1)))) i x) atTop (𝓝 (I.upper x))
hJ_sub' :
  ∀ (k : ℕ),
    Subset (α := Set (Fin (n + 1) → ℝ))
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
          ((J : (a : ℕ) → Box (Fin (n + 1))) k : Box (Fin (n + 1))) :
        Set (Fin (n + 1) → ℝ))
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ))
hJ_le : ∀ (k : ℕ), (J : (a : ℕ) → Box (Fin (n + 1))) k ≤ I
HcJ :
  ∀ (k : ℕ),
    ContinuousOn f
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
        ((J : (a : ℕ) → Box (Fin (n + 1))) k : Box (Fin (n + 1))))
HdJ :
  ∀ (k : ℕ) (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
              ((J : (a : ℕ) → Box (Fin (n + 1))) k : Box (Fin (n + 1))) \
            s :
          Set (Fin (n + 1) → ℝ))
        x →
      HasFDerivWithinAt (𝕜 := ℝ) f (f' x)
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
          ((J : (a : ℕ) → Box (Fin (n + 1))) k : Box (Fin (n + 1))))
        x
HiJ :
  ∀ (k : ℕ),
    IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : Fin (n + 1) → ℝ) ↦
        ∑ i : Fin (n + 1),
          (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i)
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
        ((J : (a : ℕ) → Box (Fin (n + 1))) k : Box (Fin (n + 1))))
      volume
HJ_eq :
  ∀ (k : ℕ),
    Eq.{u + 1} (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume
          ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ))
            ((J : (a : ℕ) → Box (Fin (n + 1))) k : Box (Fin (n + 1)))))
        fun (x : Fin (n + 1) → ℝ) ↦
        ∑ i : Fin (n + 1),
          (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i)
      (∑ i : Fin (n + 1),
        HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
            (Measure.restrict volume
              ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (Box.face ((J : (a : ℕ) → Box (Fin (n + 1))) k) i)))
            fun (x : Fin n → ℝ) ↦
            f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (Box.upper ((J : (a : ℕ) → Box (Fin (n + 1))) k) i) x) i)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
            (Measure.restrict volume
              ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (Box.face ((J : (a : ℕ) → Box (Fin (n + 1))) k) i)))
            fun (x : Fin n → ℝ) ↦
            f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (Box.lower ((J : (a : ℕ) → Box (Fin (n + 1))) k) i) x) i))
i : Fin (n + 1)
c : ℕ → ℝ
d : ℝ
hc : ∀ (k : ℕ), c k ∈ Set.Icc (I.lower i) (I.upper i)
hcd : Tendsto c atTop (𝓝 d)
hd : d ∈ Set.Icc (I.lower i) (I.upper i)
Hic :
  ∀ (k : ℕ),
    IntegrableOn.{0, u} (ε := E) (mα := MeasurableSpace.pi (X := fun (j : Fin n) ↦ ℝ))
      (fun (x : (j : Fin n) → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (c k) x) i)
      ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i)) volume
Hid :
  IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : (j : Fin n) → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) d x) i)
    ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i)) volume
H :
  Tendsto.{0, u} (β := E)
    (fun (k : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume
          ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (Box.face ((J : (a : ℕ) → Box (Fin (n + 1))) k) i)))
        fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) d x) i)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i))) fun (x : Fin n → ℝ) ↦
        f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) d x) i))
ε : ℝ
εpos : 0 < ε
hvol_pos : ∀ (J : Box (Fin n)), LT.lt (α := ℝ) 0 (∏ j : Fin n, (J.upper j - J.lower j))
δ : ℝ
δpos : δ > 0
hδ :
  ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) x →
      ∀ (y : Fin (n + 1) → ℝ),
        Membership.mem (γ := Set (Fin (n + 1) → ℝ))
            ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) y →
          dist x y ≤ δ → dist (f x) (f y) ≤ ε / ∏ j : Fin n, ((I.face i).upper j - (I.face i).lower j)
k : ℕ
hk : dist (c k) d < δ
Hsub :
  Subset (α := Set (Fin n → ℝ))
    ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (Box.face ((J : (a : ℕ) → Box (Fin (n + 1))) k) i) :
      Set (Fin n → ℝ))
    ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i) : Set (Fin n → ℝ))
x :
  norm.{u} (E := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume
          ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (Box.face ((J : (a : ℕ) → Box (Fin (n + 1))) k) i)))
        fun (x : Fin n → ℝ) ↦
        f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) d x) i -
          f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (c k) x) i) ≤
    (ε / ∏ j : Fin n, ((I.face i).upper j - (I.face i).lower j)) *
      ENNReal.toReal
        ((volume : (a : Set (Fin n → ℝ)) → ENNReal)
          ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (Box.face ((J : (a : ℕ) → Box (Fin (n + 1))) k) i) :
            Set (Fin n → ℝ)))
x₁ :
  (ε / ∏ j : Fin n, ((I.face i).upper j - (I.face i).lower j)) *
      ENNReal.toReal
        ((volume : (a : Set (Fin n → ℝ)) → ENNReal)
          ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (Box.face ((J : (a : ℕ) → Box (Fin (n + 1))) k) i) :
            Set (Fin n → ℝ))) ≤
    ε
⊢ norm.{u} (E := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume
          ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (Box.face ((J : (a : ℕ) → Box (Fin (n + 1))) k) i)))
        fun (a : (j : Fin n) → ℝ) ↦
        f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) d a) i -
          f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (c k) a) i) ≤
    ε

Tactic:
calc
    ‖∫ x in Box.Icc ((J k).face i), f (i.insertNth d x) i - f (i.insertNth (c k) x) i‖ ≤
        (ε / ∏ j, ((I.face i).upper j - (I.face i).lower j)) *
          (volume (Box.Icc ((J k).face i))).toReal := by
      refine norm_setIntegral_le_of_norm_le_const (((J k).face i).measure_Icc_lt_top _)
        fun x hx => ?_
      rw [← dist_eq_norm]
      calc
        dist (f (i.insertNth d x) i) (f (i.insertNth (c k) x) i) ≤
            dist (f (i.insertNth d x)) (f (i.insertNth (c k) x)) :=
          dist_le_pi_dist (f (i.insertNth d x)) (f (i.insertNth (c k) x)) i
        _ ≤ ε / ∏ j, ((I.face i).upper j - (I.face i).lower j) :=
          hδ _ (I.mapsTo_insertNth_face_Icc hd <| Hsub hx) _
            (I.mapsTo_insertNth_face_Icc (hc _) <| Hsub hx) ?_
      rw [Fin.dist_insertNth_insertNth, dist_self, dist_comm]
      exact max_le hk.le δpos.lt.le
    _ ≤ ε := by
      rw [Box.Icc_def, Real.volume_Icc_pi_toReal ((J k).face i).lower_le_upper,
        ← le_div_iff₀ (hvol_pos _)]
      gcongr
      exacts [hvol_pos _, fun _ _ ↦ sub_nonneg.2 (Box.lower_le_upper _ _),
        (hJ_sub' _ (J _).upper_mem_Icc).2 _, (hJ_sub' _ (J _).lower_mem_Icc).1 _]

Premises used: BoxIntegral.Box.face, Finset.univ, BoxIntegral.Box.Icc, HSub.hSub, BoxIntegral.Box.upper, HDiv.hDiv, Finset.prod, BoxIntegral.Box.lower, ENNReal.toReal, MeasureTheory.MeasureSpace.volume, DFunLike.coe