[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖f y - a - ↑f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : Box.distortion I ≤ c
⊢ ‖(∏ j : Fin (n + 1), (Box.upper I j - Box.lower I j)) • ↑f' (Pi.single i 1) -
        (integral (Box.face I i) ⊥ (f ∘ Fin.insertNth i (Box.upper I i)) BoxAdditiveMap.volume -
          integral (Box.face I i) ⊥ (f ∘ Fin.insertNth i (Box.lower I i)) BoxAdditiveMap.volume)‖ ≤
    2 * ε * ↑c * ∏ j : Fin (n + 1), (Box.upper I j - Box.lower I j)
[PROOFSTEP]
set e : ℝ → (Fin n → ℝ) → (Fin (n + 1) → ℝ) :=
  i.insertNth (α := fun _ ↦ ℝ)
    /- **Plan of the proof**. The difference of the integrals of the affine function
        `fun y ↦ a + f' (y - x)` over the faces `x i = I.upper i` and `x i = I.lower i` is equal to the
        volume of `I` multiplied by `f' (Pi.single i 1)`, so it suffices to show that the integral of
        `f y - a - f' (y - x)` over each of these faces is less than or equal to `ε * c * vol I`. We
        integrate a function of the norm `≤ ε * diam I.Icc` over a box of volume
        `∏ j ≠ i, (I.upper j - I.lower j)`. Since `diam I.Icc ≤ c * (I.upper i - I.lower i)`, we get the
        required estimate.  -/
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖f y - a - ↑f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
⊢ ‖(∏ j : Fin (n + 1), (Box.upper I j - Box.lower I j)) • ↑f' (Pi.single i 1) -
        (integral (Box.face I i) ⊥ (f ∘ e (Box.upper I i)) BoxAdditiveMap.volume -
          integral (Box.face I i) ⊥ (f ∘ e (Box.lower I i)) BoxAdditiveMap.volume)‖ ≤
    2 * ε * ↑c * ∏ j : Fin (n + 1), (Box.upper I j - Box.lower I j)
[PROOFSTEP]
have Hl : I.lower i ∈ Icc (I.lower i) (I.upper i) := Set.left_mem_Icc.2 (I.lower_le_upper i)
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖f y - a - ↑f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
⊢ ‖(∏ j : Fin (n + 1), (Box.upper I j - Box.lower I j)) • ↑f' (Pi.single i 1) -
        (integral (Box.face I i) ⊥ (f ∘ e (Box.upper I i)) BoxAdditiveMap.volume -
          integral (Box.face I i) ⊥ (f ∘ e (Box.lower I i)) BoxAdditiveMap.volume)‖ ≤
    2 * ε * ↑c * ∏ j : Fin (n + 1), (Box.upper I j - Box.lower I j)
[PROOFSTEP]
have Hu : I.upper i ∈ Icc (I.lower i) (I.upper i) := Set.right_mem_Icc.2 (I.lower_le_upper i)
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖f y - a - ↑f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
⊢ ‖(∏ j : Fin (n + 1), (Box.upper I j - Box.lower I j)) • ↑f' (Pi.single i 1) -
        (integral (Box.face I i) ⊥ (f ∘ e (Box.upper I i)) BoxAdditiveMap.volume -
          integral (Box.face I i) ⊥ (f ∘ e (Box.lower I i)) BoxAdditiveMap.volume)‖ ≤
    2 * ε * ↑c * ∏ j : Fin (n + 1), (Box.upper I j - Box.lower I j)
[PROOFSTEP]
have Hi : ∀ x ∈ Icc (I.lower i) (I.upper i), Integrable.{0, u, u} (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume :=
  fun x hx => integrable_of_continuousOn _ (Box.continuousOn_face_Icc hfc hx) volume
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖f y - a - ↑f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hi :
  ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → Integrable (Box.face I i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
⊢ ‖(∏ j : Fin (n + 1), (Box.upper I j - Box.lower I j)) • ↑f' (Pi.single i 1) -
        (integral (Box.face I i) ⊥ (f ∘ e (Box.upper I i)) BoxAdditiveMap.volume -
          integral (Box.face I i) ⊥ (f ∘ e (Box.lower I i)) BoxAdditiveMap.volume)‖ ≤
    2 * ε * ↑c * ∏ j : Fin (n + 1), (Box.upper I j - Box.lower I j)
[PROOFSTEP]
have :
  ∀ y ∈ Box.Icc (I.face i),
    ‖f' (Pi.single i (I.upper i - I.lower i)) - (f (e (I.upper i) y) - f (e (I.lower i) y))‖ ≤
      2 * ε * diam (Box.Icc I) :=
  fun y hy ↦ by
  set g := fun y => f y - a - f' (y - x) with hg
  change ∀ y ∈ (Box.Icc I), ‖g y‖ ≤ ε * ‖y - x‖ at hε 
  clear_value g; obtain rfl : f = fun y => a + f' (y - x) + g y := by simp [hg]
  convert_to ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤ _
  · congr 1
    have := Fin.insertNth_sub_same (α := fun _ ↦ ℝ) i (I.upper i) (I.lower i) y
    simp only [← this, f'.map_sub]; abel
  · have : ∀ z ∈ Icc (I.lower i) (I.upper i), e z y ∈ (Box.Icc I) := fun z hz => I.mapsTo_insertNth_face_Icc hz hy
    replace hε : ∀ y ∈ (Box.Icc I), ‖g y‖ ≤ ε * diam (Box.Icc I)
    · intro y hy
      refine' (hε y hy).trans (mul_le_mul_of_nonneg_left _ h0.le)
      rw [← dist_eq_norm]
      exact dist_le_diam_of_mem I.isCompact_Icc.bounded hy hxI
    rw [two_mul, add_mul]
    exact norm_sub_le_of_le (hε _ (this _ Hl)) (hε _ (this _ Hu))
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖f y - a - ↑f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hi :
  ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → Integrable (Box.face I i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
⊢ ‖↑f' (Pi.single i (Box.upper I i - Box.lower I i)) - (f (e (Box.upper I i) y) - f (e (Box.lower I i) y))‖ ≤
    2 * ε * diam (↑Box.Icc I)
[PROOFSTEP]
set g := fun y => f y - a - f' (y - x) with hg
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖f y - a - ↑f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hi :
  ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → Integrable (Box.face I i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E := fun y => f y - a - ↑f' (y - x)
hg : g = fun y => f y - a - ↑f' (y - x)
⊢ ‖↑f' (Pi.single i (Box.upper I i - Box.lower I i)) - (f (e (Box.upper I i) y) - f (e (Box.lower I i) y))‖ ≤
    2 * ε * diam (↑Box.Icc I)
[PROOFSTEP]
change ∀ y ∈ (Box.Icc I), ‖g y‖ ≤ ε * ‖y - x‖ at hε 
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hi :
  ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → Integrable (Box.face I i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E := fun y => f y - a - ↑f' (y - x)
hg : g = fun y => f y - a - ↑f' (y - x)
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * ‖y - x‖
⊢ ‖↑f' (Pi.single i (Box.upper I i - Box.lower I i)) - (f (e (Box.upper I i) y) - f (e (Box.lower I i) y))‖ ≤
    2 * ε * diam (↑Box.Icc I)
[PROOFSTEP]
clear_value g
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hi :
  ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → Integrable (Box.face I i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E
hg : g = fun y => f y - a - ↑f' (y - x)
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * ‖y - x‖
⊢ ‖↑f' (Pi.single i (Box.upper I i - Box.lower I i)) - (f (e (Box.upper I i) y) - f (e (Box.lower I i) y))‖ ≤
    2 * ε * diam (↑Box.Icc I)
[PROOFSTEP]
obtain rfl : f = fun y => a + f' (y - x) + g y := by simp [hg]
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hi :
  ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → Integrable (Box.face I i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E
hg : g = fun y => f y - a - ↑f' (y - x)
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * ‖y - x‖
⊢ f = fun y => a + ↑f' (y - x) + g y
[PROOFSTEP]
simp [hg]
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y => a + ↑f' (y - x) + g y) (↑Box.Icc I)
Hi :
  ∀ (x_1 : ℝ),
    x_1 ∈ Set.Icc (Box.lower I i) (Box.upper I i) →
      Integrable (Box.face I i) ⊥ ((fun y => a + ↑f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + ↑f' (y - x) + g y) y - a - ↑f' (y - x)
⊢ ‖↑f' (Pi.single i (Box.upper I i - Box.lower I i)) -
        ((fun y => a + ↑f' (y - x) + g y) (e (Box.upper I i) y) -
          (fun y => a + ↑f' (y - x) + g y) (e (Box.lower I i) y))‖ ≤
    2 * ε * diam (↑Box.Icc I)
[PROOFSTEP]
convert_to ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤ _
[GOAL]
case h.e'_3
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y => a + ↑f' (y - x) + g y) (↑Box.Icc I)
Hi :
  ∀ (x_1 : ℝ),
    x_1 ∈ Set.Icc (Box.lower I i) (Box.upper I i) →
      Integrable (Box.face I i) ⊥ ((fun y => a + ↑f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + ↑f' (y - x) + g y) y - a - ↑f' (y - x)
⊢ ‖↑f' (Pi.single i (Box.upper I i - Box.lower I i)) -
        ((fun y => a + ↑f' (y - x) + g y) (e (Box.upper I i) y) -
          (fun y => a + ↑f' (y - x) + g y) (e (Box.lower I i) y))‖ =
    ‖g (e (Box.lower I i) y) - g (e (Box.upper I i) y)‖
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_3.e_a
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y => a + ↑f' (y - x) + g y) (↑Box.Icc I)
Hi :
  ∀ (x_1 : ℝ),
    x_1 ∈ Set.Icc (Box.lower I i) (Box.upper I i) →
      Integrable (Box.face I i) ⊥ ((fun y => a + ↑f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + ↑f' (y - x) + g y) y - a - ↑f' (y - x)
⊢ ↑f' (Pi.single i (Box.upper I i - Box.lower I i)) -
      ((fun y => a + ↑f' (y - x) + g y) (e (Box.upper I i) y) -
        (fun y => a + ↑f' (y - x) + g y) (e (Box.lower I i) y)) =
    g (e (Box.lower I i) y) - g (e (Box.upper I i) y)
[PROOFSTEP]
have := Fin.insertNth_sub_same (α := fun _ ↦ ℝ) i (I.upper i) (I.lower i) y
[GOAL]
case h.e'_3.e_a
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y => a + ↑f' (y - x) + g y) (↑Box.Icc I)
Hi :
  ∀ (x_1 : ℝ),
    x_1 ∈ Set.Icc (Box.lower I i) (Box.upper I i) →
      Integrable (Box.face I i) ⊥ ((fun y => a + ↑f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + ↑f' (y - x) + g y) y - a - ↑f' (y - x)
this :
  Fin.insertNth i (Box.upper I i) y - Fin.insertNth i (Box.lower I i) y = Pi.single i (Box.upper I i - Box.lower I i)
⊢ ↑f' (Pi.single i (Box.upper I i - Box.lower I i)) -
      ((fun y => a + ↑f' (y - x) + g y) (e (Box.upper I i) y) -
        (fun y => a + ↑f' (y - x) + g y) (e (Box.lower I i) y)) =
    g (e (Box.lower I i) y) - g (e (Box.upper I i) y)
[PROOFSTEP]
simp only [← this, f'.map_sub]
[GOAL]
case h.e'_3.e_a
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y => a + ↑f' (y - x) + g y) (↑Box.Icc I)
Hi :
  ∀ (x_1 : ℝ),
    x_1 ∈ Set.Icc (Box.lower I i) (Box.upper I i) →
      Integrable (Box.face I i) ⊥ ((fun y => a + ↑f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + ↑f' (y - x) + g y) y - a - ↑f' (y - x)
this :
  Fin.insertNth i (Box.upper I i) y - Fin.insertNth i (Box.lower I i) y = Pi.single i (Box.upper I i - Box.lower I i)
⊢ ↑f' (Fin.insertNth i (Box.upper I i) y) - ↑f' (Fin.insertNth i (Box.lower I i) y) -
      (a + (↑f' (Fin.insertNth i (Box.upper I i) y) - ↑f' x) + g (Fin.insertNth i (Box.upper I i) y) -
        (a + (↑f' (Fin.insertNth i (Box.lower I i) y) - ↑f' x) + g (Fin.insertNth i (Box.lower I i) y))) =
    g (Fin.insertNth i (Box.lower I i) y) - g (Fin.insertNth i (Box.upper I i) y)
[PROOFSTEP]
abel
[GOAL]
case h.e'_3.e_a
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y => a + ↑f' (y - x) + g y) (↑Box.Icc I)
Hi :
  ∀ (x_1 : ℝ),
    x_1 ∈ Set.Icc (Box.lower I i) (Box.upper I i) →
      Integrable (Box.face I i) ⊥ ((fun y => a + ↑f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + ↑f' (y - x) + g y) y - a - ↑f' (y - x)
this :
  Fin.insertNth i (Box.upper I i) y - Fin.insertNth i (Box.lower I i) y = Pi.single i (Box.upper I i - Box.lower I i)
⊢ ↑f' (Fin.insertNth i (Box.upper I i) y) - ↑f' (Fin.insertNth i (Box.lower I i) y) -
      (a + (↑f' (Fin.insertNth i (Box.upper I i) y) - ↑f' x) + g (Fin.insertNth i (Box.upper I i) y) -
        (a + (↑f' (Fin.insertNth i (Box.lower I i) y) - ↑f' x) + g (Fin.insertNth i (Box.lower I i) y))) =
    g (Fin.insertNth i (Box.lower I i) y) - g (Fin.insertNth i (Box.upper I i) y)
[PROOFSTEP]
abel
[GOAL]
case convert_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y => a + ↑f' (y - x) + g y) (↑Box.Icc I)
Hi :
  ∀ (x_1 : ℝ),
    x_1 ∈ Set.Icc (Box.lower I i) (Box.upper I i) →
      Integrable (Box.face I i) ⊥ ((fun y => a + ↑f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + ↑f' (y - x) + g y) y - a - ↑f' (y - x)
⊢ ‖g (e (Box.lower I i) y) - g (e (Box.upper I i) y)‖ ≤ 2 * ε * diam (↑Box.Icc I)
[PROOFSTEP]
have : ∀ z ∈ Icc (I.lower i) (I.upper i), e z y ∈ (Box.Icc I) := fun z hz => I.mapsTo_insertNth_face_Icc hz hy
[GOAL]
case convert_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y => a + ↑f' (y - x) + g y) (↑Box.Icc I)
Hi :
  ∀ (x_1 : ℝ),
    x_1 ∈ Set.Icc (Box.lower I i) (Box.upper I i) →
      Integrable (Box.face I i) ⊥ ((fun y => a + ↑f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + ↑f' (y - x) + g y) y - a - ↑f' (y - x)
this : ∀ (z : ℝ), z ∈ Set.Icc (Box.lower I i) (Box.upper I i) → e z y ∈ ↑Box.Icc I
⊢ ‖g (e (Box.lower I i) y) - g (e (Box.upper I i) y)‖ ≤ 2 * ε * diam (↑Box.Icc I)
[PROOFSTEP]
replace hε : ∀ y ∈ (Box.Icc I), ‖g y‖ ≤ ε * diam (Box.Icc I)
[GOAL]
case hε
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y => a + ↑f' (y - x) + g y) (↑Box.Icc I)
Hi :
  ∀ (x_1 : ℝ),
    x_1 ∈ Set.Icc (Box.lower I i) (Box.upper I i) →
      Integrable (Box.face I i) ⊥ ((fun y => a + ↑f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + ↑f' (y - x) + g y) y - a - ↑f' (y - x)
this : ∀ (z : ℝ), z ∈ Set.Icc (Box.lower I i) (Box.upper I i) → e z y ∈ ↑Box.Icc I
⊢ ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * diam (↑Box.Icc I)
[PROOFSTEP]
intro y hy
[GOAL]
case hε
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
y✝ : Fin n → ℝ
hy✝ : y✝ ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y => a + ↑f' (y - x) + g y) (↑Box.Icc I)
Hi :
  ∀ (x_1 : ℝ),
    x_1 ∈ Set.Icc (Box.lower I i) (Box.upper I i) →
      Integrable (Box.face I i) ⊥ ((fun y => a + ↑f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + ↑f' (y - x) + g y) y - a - ↑f' (y - x)
this : ∀ (z : ℝ), z ∈ Set.Icc (Box.lower I i) (Box.upper I i) → e z y✝ ∈ ↑Box.Icc I
y : Fin (n + 1) → ℝ
hy : y ∈ ↑Box.Icc I
⊢ ‖g y‖ ≤ ε * diam (↑Box.Icc I)
[PROOFSTEP]
refine' (hε y hy).trans (mul_le_mul_of_nonneg_left _ h0.le)
[GOAL]
case hε
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
y✝ : Fin n → ℝ
hy✝ : y✝ ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y => a + ↑f' (y - x) + g y) (↑Box.Icc I)
Hi :
  ∀ (x_1 : ℝ),
    x_1 ∈ Set.Icc (Box.lower I i) (Box.upper I i) →
      Integrable (Box.face I i) ⊥ ((fun y => a + ↑f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + ↑f' (y - x) + g y) y - a - ↑f' (y - x)
this : ∀ (z : ℝ), z ∈ Set.Icc (Box.lower I i) (Box.upper I i) → e z y✝ ∈ ↑Box.Icc I
y : Fin (n + 1) → ℝ
hy : y ∈ ↑Box.Icc I
⊢ ‖y - x‖ ≤ diam (↑Box.Icc I)
[PROOFSTEP]
rw [← dist_eq_norm]
[GOAL]
case hε
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
y✝ : Fin n → ℝ
hy✝ : y✝ ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y => a + ↑f' (y - x) + g y) (↑Box.Icc I)
Hi :
  ∀ (x_1 : ℝ),
    x_1 ∈ Set.Icc (Box.lower I i) (Box.upper I i) →
      Integrable (Box.face I i) ⊥ ((fun y => a + ↑f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + ↑f' (y - x) + g y) y - a - ↑f' (y - x)
this : ∀ (z : ℝ), z ∈ Set.Icc (Box.lower I i) (Box.upper I i) → e z y✝ ∈ ↑Box.Icc I
y : Fin (n + 1) → ℝ
hy : y ∈ ↑Box.Icc I
⊢ dist y x ≤ diam (↑Box.Icc I)
[PROOFSTEP]
exact dist_le_diam_of_mem I.isCompact_Icc.bounded hy hxI
[GOAL]
case convert_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E
hfc : ContinuousOn (fun y => a + ↑f' (y - x) + g y) (↑Box.Icc I)
Hi :
  ∀ (x_1 : ℝ),
    x_1 ∈ Set.Icc (Box.lower I i) (Box.upper I i) →
      Integrable (Box.face I i) ⊥ ((fun y => a + ↑f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + ↑f' (y - x) + g y) y - a - ↑f' (y - x)
this : ∀ (z : ℝ), z ∈ Set.Icc (Box.lower I i) (Box.upper I i) → e z y ∈ ↑Box.Icc I
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * diam (↑Box.Icc I)
⊢ ‖g (e (Box.lower I i) y) - g (e (Box.upper I i) y)‖ ≤ 2 * ε * diam (↑Box.Icc I)
[PROOFSTEP]
rw [two_mul, add_mul]
[GOAL]
case convert_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
g : (Fin (n + 1) → ℝ) → E
hfc : ContinuousOn (fun y => a + ↑f' (y - x) + g y) (↑Box.Icc I)
Hi :
  ∀ (x_1 : ℝ),
    x_1 ∈ Set.Icc (Box.lower I i) (Box.upper I i) →
      Integrable (Box.face I i) ⊥ ((fun y => a + ↑f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + ↑f' (y - x) + g y) y - a - ↑f' (y - x)
this : ∀ (z : ℝ), z ∈ Set.Icc (Box.lower I i) (Box.upper I i) → e z y ∈ ↑Box.Icc I
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖g y‖ ≤ ε * diam (↑Box.Icc I)
⊢ ‖g (e (Box.lower I i) y) - g (e (Box.upper I i) y)‖ ≤ ε * diam (↑Box.Icc I) + ε * diam (↑Box.Icc I)
[PROOFSTEP]
exact norm_sub_le_of_le (hε _ (this _ Hl)) (hε _ (this _ Hu))
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖f y - a - ↑f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hi :
  ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → Integrable (Box.face I i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ (y : Fin n → ℝ),
    y ∈ ↑Box.Icc (Box.face I i) →
      ‖↑f' (Pi.single i (Box.upper I i - Box.lower I i)) - (f (e (Box.upper I i) y) - f (e (Box.lower I i) y))‖ ≤
        2 * ε * diam (↑Box.Icc I)
⊢ ‖(∏ j : Fin (n + 1), (Box.upper I j - Box.lower I j)) • ↑f' (Pi.single i 1) -
        (integral (Box.face I i) ⊥ (f ∘ e (Box.upper I i)) BoxAdditiveMap.volume -
          integral (Box.face I i) ⊥ (f ∘ e (Box.lower I i)) BoxAdditiveMap.volume)‖ ≤
    2 * ε * ↑c * ∏ j : Fin (n + 1), (Box.upper I j - Box.lower I j)
[PROOFSTEP]
calc
  ‖(∏ j, (I.upper j - I.lower j)) • f' (Pi.single i 1) -
          (integral (I.face i) ⊥ (f ∘ e (I.upper i)) BoxAdditiveMap.volume -
            integral (I.face i) ⊥ (f ∘ e (I.lower i)) BoxAdditiveMap.volume)‖ =
      ‖integral.{0, u, u} (I.face i) ⊥
          (fun x : Fin n → ℝ => f' (Pi.single i (I.upper i - I.lower i)) - (f (e (I.upper i) x) - f (e (I.lower i) x)))
          BoxAdditiveMap.volume‖ :=
    by
    rw [← integral_sub (Hi _ Hu) (Hi _ Hl), ← Box.volume_face_mul i, mul_smul, ← Box.volume_apply, ←
      BoxAdditiveMap.toSMul_apply, ← integral_const, ← BoxAdditiveMap.volume, ←
      integral_sub (integrable_const _) ((Hi _ Hu).sub (Hi _ Hl))]
    simp only [(· ∘ ·), Pi.sub_def, ← f'.map_smul, ← Pi.single_smul', smul_eq_mul, mul_one]
  _ ≤ (volume (I.face i : Set (Fin n → ℝ))).toReal * (2 * ε * c * (I.upper i - I.lower i)) := by
    -- The hard part of the estimate was done above, here we just replace `diam I.Icc`
          -- with `c * (I.upper i - I.lower i)`
    refine' norm_integral_le_of_le_const (fun y hy => (this y hy).trans _) volume
    rw [mul_assoc (2 * ε)]
    exact mul_le_mul_of_nonneg_left (I.diam_Icc_le_of_distortion_le i hc) (mul_nonneg zero_le_two h0.le)
  _ = 2 * ε * c * ∏ j, (I.upper j - I.lower j) :=
    by
    rw [← Measure.toBoxAdditive_apply, Box.volume_apply, ← I.volume_face_mul i]
    ac_rfl
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖f y - a - ↑f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hi :
  ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → Integrable (Box.face I i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ (y : Fin n → ℝ),
    y ∈ ↑Box.Icc (Box.face I i) →
      ‖↑f' (Pi.single i (Box.upper I i - Box.lower I i)) - (f (e (Box.upper I i) y) - f (e (Box.lower I i) y))‖ ≤
        2 * ε * diam (↑Box.Icc I)
⊢ ‖(∏ j : Fin (n + 1), (Box.upper I j - Box.lower I j)) • ↑f' (Pi.single i 1) -
        (integral (Box.face I i) ⊥ (f ∘ e (Box.upper I i)) BoxAdditiveMap.volume -
          integral (Box.face I i) ⊥ (f ∘ e (Box.lower I i)) BoxAdditiveMap.volume)‖ =
    ‖integral (Box.face I i) ⊥
        (fun x =>
          ↑f' (Pi.single i (Box.upper I i - Box.lower I i)) - (f (e (Box.upper I i) x) - f (e (Box.lower I i) x)))
        BoxAdditiveMap.volume‖
[PROOFSTEP]
rw [← integral_sub (Hi _ Hu) (Hi _ Hl), ← Box.volume_face_mul i, mul_smul, ← Box.volume_apply, ←
  BoxAdditiveMap.toSMul_apply, ← integral_const, ← BoxAdditiveMap.volume, ←
  integral_sub (integrable_const _) ((Hi _ Hu).sub (Hi _ Hl))]
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖f y - a - ↑f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hi :
  ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → Integrable (Box.face I i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ (y : Fin n → ℝ),
    y ∈ ↑Box.Icc (Box.face I i) →
      ‖↑f' (Pi.single i (Box.upper I i - Box.lower I i)) - (f (e (Box.upper I i) y) - f (e (Box.lower I i) y))‖ ≤
        2 * ε * diam (↑Box.Icc I)
⊢ ‖integral (Box.face I i) ⊥
        ((fun x => (Box.upper I i - Box.lower I i) • ↑f' (Pi.single i 1)) -
          (f ∘ e (Box.upper I i) - f ∘ e (Box.lower I i)))
        BoxAdditiveMap.volume‖ =
    ‖integral (Box.face I i) ⊥
        (fun x =>
          ↑f' (Pi.single i (Box.upper I i - Box.lower I i)) - (f (e (Box.upper I i) x) - f (e (Box.lower I i) x)))
        BoxAdditiveMap.volume‖
[PROOFSTEP]
simp only [(· ∘ ·), Pi.sub_def, ← f'.map_smul, ← Pi.single_smul', smul_eq_mul, mul_one]
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖f y - a - ↑f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hi :
  ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → Integrable (Box.face I i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ (y : Fin n → ℝ),
    y ∈ ↑Box.Icc (Box.face I i) →
      ‖↑f' (Pi.single i (Box.upper I i - Box.lower I i)) - (f (e (Box.upper I i) y) - f (e (Box.lower I i) y))‖ ≤
        2 * ε * diam (↑Box.Icc I)
⊢ ‖integral (Box.face I i) ⊥
        (fun x =>
          ↑f' (Pi.single i (Box.upper I i - Box.lower I i)) - (f (e (Box.upper I i) x) - f (e (Box.lower I i) x)))
        BoxAdditiveMap.volume‖ ≤
    ENNReal.toReal (↑↑volume ↑(Box.face I i)) * (2 * ε * ↑c * (Box.upper I i - Box.lower I i))
[PROOFSTEP]
refine' norm_integral_le_of_le_const (fun y hy => (this y hy).trans _) volume
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖f y - a - ↑f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hi :
  ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → Integrable (Box.face I i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ (y : Fin n → ℝ),
    y ∈ ↑Box.Icc (Box.face I i) →
      ‖↑f' (Pi.single i (Box.upper I i - Box.lower I i)) - (f (e (Box.upper I i) y) - f (e (Box.lower I i) y))‖ ≤
        2 * ε * diam (↑Box.Icc I)
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
⊢ 2 * ε * diam (↑Box.Icc I) ≤ 2 * ε * ↑c * (Box.upper I i - Box.lower I i)
[PROOFSTEP]
rw [mul_assoc (2 * ε)]
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖f y - a - ↑f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hi :
  ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → Integrable (Box.face I i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ (y : Fin n → ℝ),
    y ∈ ↑Box.Icc (Box.face I i) →
      ‖↑f' (Pi.single i (Box.upper I i - Box.lower I i)) - (f (e (Box.upper I i) y) - f (e (Box.lower I i) y))‖ ≤
        2 * ε * diam (↑Box.Icc I)
y : Fin n → ℝ
hy : y ∈ ↑Box.Icc (Box.face I i)
⊢ 2 * ε * diam (↑Box.Icc I) ≤ 2 * ε * (↑c * (Box.upper I i - Box.lower I i))
[PROOFSTEP]
exact mul_le_mul_of_nonneg_left (I.diam_Icc_le_of_distortion_le i hc) (mul_nonneg zero_le_two h0.le)
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖f y - a - ↑f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hi :
  ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → Integrable (Box.face I i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ (y : Fin n → ℝ),
    y ∈ ↑Box.Icc (Box.face I i) →
      ‖↑f' (Pi.single i (Box.upper I i - Box.lower I i)) - (f (e (Box.upper I i) y) - f (e (Box.lower I i) y))‖ ≤
        2 * ε * diam (↑Box.Icc I)
⊢ ENNReal.toReal (↑↑volume ↑(Box.face I i)) * (2 * ε * ↑c * (Box.upper I i - Box.lower I i)) =
    2 * ε * ↑c * ∏ j : Fin (n + 1), (Box.upper I j - Box.lower I j)
[PROOFSTEP]
rw [← Measure.toBoxAdditive_apply, Box.volume_apply, ← I.volume_face_mul i]
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (↑Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ ↑Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ (y : Fin (n + 1) → ℝ), y ∈ ↑Box.Icc I → ‖f y - a - ↑f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : Box.distortion I ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := Fin.insertNth i
Hl : Box.lower I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hu : Box.upper I i ∈ Set.Icc (Box.lower I i) (Box.upper I i)
Hi :
  ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → Integrable (Box.face I i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ (y : Fin n → ℝ),
    y ∈ ↑Box.Icc (Box.face I i) →
      ‖↑f' (Pi.single i (Box.upper I i - Box.lower I i)) - (f (e (Box.upper I i) y) - f (e (Box.lower I i) y))‖ ≤
        2 * ε * diam (↑Box.Icc I)
⊢ (∏ i_1 : Fin n, (Box.upper (Box.face I i) i_1 - Box.lower (Box.face I i) i_1)) *
      (2 * ε * ↑c * (Box.upper I i - Box.lower I i)) =
    2 * ε * ↑c *
      ((∏ j : Fin n, (Box.upper (Box.face I i) j - Box.lower (Box.face I i) j)) * (Box.upper I i - Box.lower I i))
[PROOFSTEP]
ac_rfl
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
⊢ HasIntegral I GP (fun x => ↑(f' x) (Pi.single i 1)) BoxAdditiveMap.volume
    (integral (Box.face I i) GP (fun x => f (Fin.insertNth i (Box.upper I i) x)) BoxAdditiveMap.volume -
      integral (Box.face I i) GP (fun x => f (Fin.insertNth i (Box.lower I i) x)) BoxAdditiveMap.volume)
[PROOFSTEP]
have Hc : ContinuousOn f (Box.Icc I) := fun x hx ↦
  by
  by_cases hxs : x ∈ s
  exacts [Hs x hxs, (Hd x ⟨hx, hxs⟩).continuousWithinAt]
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I
⊢ ContinuousWithinAt f (↑Box.Icc I) x
[PROOFSTEP]
by_cases hxs : x ∈ s
[GOAL]
case pos
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I
hxs : x ∈ s
⊢ ContinuousWithinAt f (↑Box.Icc I) x
case neg
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I
hxs : ¬x ∈ s
⊢ ContinuousWithinAt f (↑Box.Icc I) x
[PROOFSTEP]
exacts [Hs x hxs, (Hd x ⟨hx, hxs⟩).continuousWithinAt]
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
⊢ HasIntegral I GP (fun x => ↑(f' x) (Pi.single i 1)) BoxAdditiveMap.volume
    (integral (Box.face I i) GP (fun x => f (Fin.insertNth i (Box.upper I i) x)) BoxAdditiveMap.volume -
      integral (Box.face I i) GP (fun x => f (Fin.insertNth i (Box.lower I i) x)) BoxAdditiveMap.volume)
[PROOFSTEP]
set fI : ℝ → Box (Fin n) → E := fun y J => integral.{0, u, u} J GP (fun x => f (i.insertNth y x)) BoxAdditiveMap.volume
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
⊢ HasIntegral I GP (fun x => ↑(f' x) (Pi.single i 1)) BoxAdditiveMap.volume
    (integral (Box.face I i) GP (fun x => f (Fin.insertNth i (Box.upper I i) x)) BoxAdditiveMap.volume -
      integral (Box.face I i) GP (fun x => f (Fin.insertNth i (Box.lower I i) x)) BoxAdditiveMap.volume)
[PROOFSTEP]
set fb : Icc (I.lower i) (I.upper i) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x =>
  (integrable_of_continuousOn GP (Box.continuousOn_face_Icc Hc x.2) volume).toBoxAdditive
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
⊢ HasIntegral I GP (fun x => ↑(f' x) (Pi.single i 1)) BoxAdditiveMap.volume
    (integral (Box.face I i) GP (fun x => f (Fin.insertNth i (Box.upper I i) x)) BoxAdditiveMap.volume -
      integral (Box.face I i) GP (fun x => f (Fin.insertNth i (Box.lower I i) x)) BoxAdditiveMap.volume)
[PROOFSTEP]
set F : Fin (n + 1) →ᵇᵃ[I] E := BoxAdditiveMap.upperSubLower I i fI fb fun x _ J => rfl
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
⊢ HasIntegral I GP (fun x => ↑(f' x) (Pi.single i 1)) BoxAdditiveMap.volume
    (integral (Box.face I i) GP (fun x => f (Fin.insertNth i (Box.upper I i) x)) BoxAdditiveMap.volume -
      integral (Box.face I i) GP (fun x => f (Fin.insertNth i (Box.lower I i) x)) BoxAdditiveMap.volume)
[PROOFSTEP]
change HasIntegral I GP (fun x => f' x (Pi.single i 1)) _ (F I)
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
⊢ HasIntegral I GP (fun x => ↑(f' x) (Pi.single i 1)) BoxAdditiveMap.volume (↑F I)
[PROOFSTEP]
refine' HasIntegral.of_le_Henstock_of_forall_isLittleO gp_le _ _ _ s hs _ _
[GOAL]
case refine'_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
⊢ Fin (n + 1) →ᵇᵃ[↑I] ℝ
[PROOFSTEP]
exact (volume : Measure (Fin (n + 1) → ℝ)).toBoxAdditive.restrict _ le_top
[GOAL]
case refine'_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
⊢ ∀ (J : Box (Fin (n + 1))), 0 ≤ ↑(BoxAdditiveMap.restrict (Measure.toBoxAdditive volume) ↑I (_ : ↑I ≤ ⊤)) J
[PROOFSTEP]
exact fun J => ENNReal.toReal_nonneg
[GOAL]
case refine'_3
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
⊢ ∀ (c : ℝ≥0) (x : Fin (n + 1) → ℝ),
    x ∈ ↑Box.Icc I ∩ s →
      ∀ (ε : ℝ),
        ε > 0 →
          ∃ δ,
            δ > 0 ∧
              ∀ (J : Box (Fin (n + 1))),
                J ≤ I →
                  ↑Box.Icc J ⊆ closedBall x δ →
                    x ∈ ↑Box.Icc J →
                      (GP.bDistortion = true → Box.distortion J ≤ c) →
                        dist (↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1))) (↑F J) ≤ ε
[PROOFSTEP]
intro c x hx ε ε0
[GOAL]
case refine'_3
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
⊢ ∃ δ,
    δ > 0 ∧
      ∀ (J : Box (Fin (n + 1))),
        J ≤ I →
          ↑Box.Icc J ⊆ closedBall x δ →
            x ∈ ↑Box.Icc J →
              (GP.bDistortion = true → Box.distortion J ≤ c) →
                dist (↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1))) (↑F J) ≤ ε
[PROOFSTEP]
have :
  ∀ᶠ δ in 𝓝[>] (0 : ℝ),
    δ ∈ Ioc (0 : ℝ) (1 / 2) ∧
      (∀ᵉ (y₁ ∈ closedBall x δ ∩ (Box.Icc I)) (y₂ ∈ closedBall x δ ∩ (Box.Icc I)), ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖f' x (Pi.single i 1)‖ ≤ ε / 2 :=
  by
  refine' .and _ (.and _ _)
  · exact Ioc_mem_nhdsWithin_Ioi ⟨le_rfl, one_half_pos⟩
  · rcases((nhdsWithin_hasBasis nhds_basis_closedBall _).tendsto_iff nhds_basis_closedBall).1 (Hs x hx.2) _
        (half_pos <| half_pos ε0) with ⟨δ₁, δ₁0, hδ₁⟩
    filter_upwards [Ioc_mem_nhdsWithin_Ioi ⟨le_rfl, δ₁0⟩] with δ hδ y₁ hy₁ y₂ hy₂
    have : closedBall x δ ∩ (Box.Icc I) ⊆ closedBall x δ₁ ∩ (Box.Icc I) :=
      inter_subset_inter_left _ (closedBall_subset_closedBall hδ.2)
    rw [← dist_eq_norm]
    calc
      dist (f y₁) (f y₂) ≤ dist (f y₁) (f x) + dist (f y₂) (f x) := dist_triangle_right _ _ _
      _ ≤ ε / 2 / 2 + ε / 2 / 2 := (add_le_add (hδ₁ _ <| this hy₁) (hδ₁ _ <| this hy₂))
      _ = ε / 2 := add_halves _
  · have : ContinuousWithinAt (fun δ : ℝ => (2 * δ) ^ (n + 1) * ‖f' x (Pi.single i 1)‖) (Ioi 0) 0 :=
      ((continuousWithinAt_id.const_mul _).pow _).mul_const _
    refine' this.eventually (ge_mem_nhds _)
    simpa using half_pos ε0
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
[PROOFSTEP]
refine' .and _ (.and _ _)
[GOAL]
case refine'_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0, δ ∈ Set.Ioc 0 (1 / 2)
[PROOFSTEP]
exact Ioc_mem_nhdsWithin_Ioi ⟨le_rfl, one_half_pos⟩
[GOAL]
case refine'_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    ∀ (y₁ : Fin (n + 1) → ℝ),
      y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
        ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
[PROOFSTEP]
rcases((nhdsWithin_hasBasis nhds_basis_closedBall _).tendsto_iff nhds_basis_closedBall).1 (Hs x hx.2) _
    (half_pos <| half_pos ε0) with
  ⟨δ₁, δ₁0, hδ₁⟩
[GOAL]
case refine'_2.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
δ₁ : ℝ
δ₁0 : 0 < δ₁
hδ₁ : ∀ (x_1 : Fin (n + 1) → ℝ), x_1 ∈ closedBall x δ₁ ∩ ↑Box.Icc I → f x_1 ∈ closedBall (f x) (ε / 2 / 2)
⊢ ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    ∀ (y₁ : Fin (n + 1) → ℝ),
      y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
        ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
[PROOFSTEP]
filter_upwards [Ioc_mem_nhdsWithin_Ioi ⟨le_rfl, δ₁0⟩] with δ hδ y₁ hy₁ y₂ hy₂
[GOAL]
case h
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
δ₁ : ℝ
δ₁0 : 0 < δ₁
hδ₁ : ∀ (x_1 : Fin (n + 1) → ℝ), x_1 ∈ closedBall x δ₁ ∩ ↑Box.Icc I → f x_1 ∈ closedBall (f x) (ε / 2 / 2)
δ : ℝ
hδ : δ ∈ Set.Ioc 0 δ₁
y₁ : Fin (n + 1) → ℝ
hy₁ : y₁ ∈ closedBall x δ ∩ ↑Box.Icc I
y₂ : Fin (n + 1) → ℝ
hy₂ : y₂ ∈ closedBall x δ ∩ ↑Box.Icc I
⊢ ‖f y₁ - f y₂‖ ≤ ε / 2
[PROOFSTEP]
have : closedBall x δ ∩ (Box.Icc I) ⊆ closedBall x δ₁ ∩ (Box.Icc I) :=
  inter_subset_inter_left _ (closedBall_subset_closedBall hδ.2)
[GOAL]
case h
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
δ₁ : ℝ
δ₁0 : 0 < δ₁
hδ₁ : ∀ (x_1 : Fin (n + 1) → ℝ), x_1 ∈ closedBall x δ₁ ∩ ↑Box.Icc I → f x_1 ∈ closedBall (f x) (ε / 2 / 2)
δ : ℝ
hδ : δ ∈ Set.Ioc 0 δ₁
y₁ : Fin (n + 1) → ℝ
hy₁ : y₁ ∈ closedBall x δ ∩ ↑Box.Icc I
y₂ : Fin (n + 1) → ℝ
hy₂ : y₂ ∈ closedBall x δ ∩ ↑Box.Icc I
this : closedBall x δ ∩ ↑Box.Icc I ⊆ closedBall x δ₁ ∩ ↑Box.Icc I
⊢ ‖f y₁ - f y₂‖ ≤ ε / 2
[PROOFSTEP]
rw [← dist_eq_norm]
[GOAL]
case h
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
δ₁ : ℝ
δ₁0 : 0 < δ₁
hδ₁ : ∀ (x_1 : Fin (n + 1) → ℝ), x_1 ∈ closedBall x δ₁ ∩ ↑Box.Icc I → f x_1 ∈ closedBall (f x) (ε / 2 / 2)
δ : ℝ
hδ : δ ∈ Set.Ioc 0 δ₁
y₁ : Fin (n + 1) → ℝ
hy₁ : y₁ ∈ closedBall x δ ∩ ↑Box.Icc I
y₂ : Fin (n + 1) → ℝ
hy₂ : y₂ ∈ closedBall x δ ∩ ↑Box.Icc I
this : closedBall x δ ∩ ↑Box.Icc I ⊆ closedBall x δ₁ ∩ ↑Box.Icc I
⊢ dist (f y₁) (f y₂) ≤ ε / 2
[PROOFSTEP]
calc
  dist (f y₁) (f y₂) ≤ dist (f y₁) (f x) + dist (f y₂) (f x) := dist_triangle_right _ _ _
  _ ≤ ε / 2 / 2 + ε / 2 / 2 := (add_le_add (hδ₁ _ <| this hy₁) (hδ₁ _ <| this hy₂))
  _ = ε / 2 := add_halves _
[GOAL]
case refine'_3
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0, (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
[PROOFSTEP]
have : ContinuousWithinAt (fun δ : ℝ => (2 * δ) ^ (n + 1) * ‖f' x (Pi.single i 1)‖) (Ioi 0) 0 :=
  ((continuousWithinAt_id.const_mul _).pow _).mul_const _
[GOAL]
case refine'_3
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this : ContinuousWithinAt (fun δ => (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖) (Set.Ioi 0) 0
⊢ ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0, (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
[PROOFSTEP]
refine' this.eventually (ge_mem_nhds _)
[GOAL]
case refine'_3
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this : ContinuousWithinAt (fun δ => (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖) (Set.Ioi 0) 0
⊢ (fun δ => (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖) 0 < ε / 2
[PROOFSTEP]
simpa using half_pos ε0
[GOAL]
case refine'_3
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
⊢ ∃ δ,
    δ > 0 ∧
      ∀ (J : Box (Fin (n + 1))),
        J ≤ I →
          ↑Box.Icc J ⊆ closedBall x δ →
            x ∈ ↑Box.Icc J →
              (GP.bDistortion = true → Box.distortion J ≤ c) →
                dist (↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1))) (↑F J) ≤ ε
[PROOFSTEP]
rcases this.exists with ⟨δ, ⟨hδ0, hδ12⟩, hdfδ, hδ⟩
[GOAL]
case refine'_3.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
⊢ ∃ δ,
    δ > 0 ∧
      ∀ (J : Box (Fin (n + 1))),
        J ≤ I →
          ↑Box.Icc J ⊆ closedBall x δ →
            x ∈ ↑Box.Icc J →
              (GP.bDistortion = true → Box.distortion J ≤ c) →
                dist (↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1))) (↑F J) ≤ ε
[PROOFSTEP]
refine' ⟨δ, hδ0, fun J hJI hJδ _ _ => add_halves ε ▸ _⟩
[GOAL]
case refine'_3.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
⊢ dist (↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1))) (↑F J) ≤ ε / 2 + ε / 2
[PROOFSTEP]
have Hl : J.lower i ∈ Icc (J.lower i) (J.upper i) := Set.left_mem_Icc.2 (J.lower_le_upper i)
[GOAL]
case refine'_3.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
⊢ dist (↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1))) (↑F J) ≤ ε / 2 + ε / 2
[PROOFSTEP]
have Hu : J.upper i ∈ Icc (J.lower i) (J.upper i) := Set.right_mem_Icc.2 (J.lower_le_upper i)
[GOAL]
case refine'_3.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
⊢ dist (↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1))) (↑F J) ≤ ε / 2 + ε / 2
[PROOFSTEP]
have Hi :
  ∀ x ∈ Icc (J.lower i) (J.upper i),
    Integrable.{0, u, u} (J.face i) GP (fun y => f (i.insertNth x y)) BoxAdditiveMap.volume :=
  fun x hx => integrable_of_continuousOn _ (Box.continuousOn_face_Icc (Hc.mono <| Box.le_iff_Icc.1 hJI) hx) volume
[GOAL]
case refine'_3.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hi :
  ∀ (x : ℝ),
    x ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      Integrable (Box.face J i) GP (fun y => f (Fin.insertNth i x y)) BoxAdditiveMap.volume
⊢ dist (↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1))) (↑F J) ≤ ε / 2 + ε / 2
[PROOFSTEP]
have hJδ' : Box.Icc J ⊆ closedBall x δ ∩ (Box.Icc I) := subset_inter hJδ (Box.le_iff_Icc.1 hJI)
[GOAL]
case refine'_3.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hi :
  ∀ (x : ℝ),
    x ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      Integrable (Box.face J i) GP (fun y => f (Fin.insertNth i x y)) BoxAdditiveMap.volume
hJδ' : ↑Box.Icc J ⊆ closedBall x δ ∩ ↑Box.Icc I
⊢ dist (↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1))) (↑F J) ≤ ε / 2 + ε / 2
[PROOFSTEP]
have Hmaps :
  ∀ z ∈ Icc (J.lower i) (J.upper i), MapsTo (i.insertNth z) (Box.Icc (J.face i)) (closedBall x δ ∩ (Box.Icc I)) :=
  fun z hz => (J.mapsTo_insertNth_face_Icc hz).mono Subset.rfl hJδ'
[GOAL]
case refine'_3.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hi :
  ∀ (x : ℝ),
    x ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      Integrable (Box.face J i) GP (fun y => f (Fin.insertNth i x y)) BoxAdditiveMap.volume
hJδ' : ↑Box.Icc J ⊆ closedBall x δ ∩ ↑Box.Icc I
Hmaps :
  ∀ (z : ℝ),
    z ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      MapsTo (Fin.insertNth i z) (↑Box.Icc (Box.face J i)) (closedBall x δ ∩ ↑Box.Icc I)
⊢ dist (↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1))) (↑F J) ≤ ε / 2 + ε / 2
[PROOFSTEP]
simp only [dist_eq_norm]
[GOAL]
case refine'_3.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hi :
  ∀ (x : ℝ),
    x ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      Integrable (Box.face J i) GP (fun y => f (Fin.insertNth i x y)) BoxAdditiveMap.volume
hJδ' : ↑Box.Icc J ⊆ closedBall x δ ∩ ↑Box.Icc I
Hmaps :
  ∀ (z : ℝ),
    z ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      MapsTo (Fin.insertNth i z) (↑Box.Icc (Box.face J i)) (closedBall x δ ∩ ↑Box.Icc I)
⊢ ‖↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1)) -
        ↑(BoxAdditiveMap.upperSubLower I i
              (fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume)
              (fun x =>
                Integrable.toBoxAdditive
                  (_ :
                    Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x)
                      (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))))
              (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J))
          J‖ ≤
    ε / 2 + ε / 2
[PROOFSTEP]
dsimp
[GOAL]
case refine'_3.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hi :
  ∀ (x : ℝ),
    x ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      Integrable (Box.face J i) GP (fun y => f (Fin.insertNth i x y)) BoxAdditiveMap.volume
hJδ' : ↑Box.Icc J ⊆ closedBall x δ ∩ ↑Box.Icc I
Hmaps :
  ∀ (z : ℝ),
    z ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      MapsTo (Fin.insertNth i z) (↑Box.Icc (Box.face J i)) (closedBall x δ ∩ ↑Box.Icc I)
⊢ ‖↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1)) -
        (integral (Box.face J i) GP (fun x => f (Fin.insertNth i (Box.upper J i) x)) BoxAdditiveMap.volume -
          integral (Box.face J i) GP (fun x => f (Fin.insertNth i (Box.lower J i) x)) BoxAdditiveMap.volume)‖ ≤
    ε / 2 + ε / 2
[PROOFSTEP]
rw [← integral_sub (Hi _ Hu) (Hi _ Hl)]
[GOAL]
case refine'_3.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hi :
  ∀ (x : ℝ),
    x ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      Integrable (Box.face J i) GP (fun y => f (Fin.insertNth i x y)) BoxAdditiveMap.volume
hJδ' : ↑Box.Icc J ⊆ closedBall x δ ∩ ↑Box.Icc I
Hmaps :
  ∀ (z : ℝ),
    z ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      MapsTo (Fin.insertNth i z) (↑Box.Icc (Box.face J i)) (closedBall x δ ∩ ↑Box.Icc I)
⊢ ‖↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1)) -
        integral (Box.face J i) GP
          ((fun y => f (Fin.insertNth i (Box.upper J i) y)) - fun y => f (Fin.insertNth i (Box.lower J i) y))
          BoxAdditiveMap.volume‖ ≤
    ε / 2 + ε / 2
[PROOFSTEP]
refine' (norm_sub_le _ _).trans (add_le_add _ _)
[GOAL]
case refine'_3.intro.intro.intro.intro.refine'_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hi :
  ∀ (x : ℝ),
    x ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      Integrable (Box.face J i) GP (fun y => f (Fin.insertNth i x y)) BoxAdditiveMap.volume
hJδ' : ↑Box.Icc J ⊆ closedBall x δ ∩ ↑Box.Icc I
Hmaps :
  ∀ (z : ℝ),
    z ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      MapsTo (Fin.insertNth i z) (↑Box.Icc (Box.face J i)) (closedBall x δ ∩ ↑Box.Icc I)
⊢ ‖↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1))‖ ≤ ε / 2
[PROOFSTEP]
simp_rw [BoxAdditiveMap.volume_apply, norm_smul, Real.norm_eq_abs, abs_prod]
[GOAL]
case refine'_3.intro.intro.intro.intro.refine'_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hi :
  ∀ (x : ℝ),
    x ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      Integrable (Box.face J i) GP (fun y => f (Fin.insertNth i x y)) BoxAdditiveMap.volume
hJδ' : ↑Box.Icc J ⊆ closedBall x δ ∩ ↑Box.Icc I
Hmaps :
  ∀ (z : ℝ),
    z ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      MapsTo (Fin.insertNth i z) (↑Box.Icc (Box.face J i)) (closedBall x δ ∩ ↑Box.Icc I)
⊢ (∏ x : Fin (n + 1), |Box.upper J x - Box.lower J x|) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
[PROOFSTEP]
refine' (mul_le_mul_of_nonneg_right _ <| norm_nonneg _).trans hδ
[GOAL]
case refine'_3.intro.intro.intro.intro.refine'_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hi :
  ∀ (x : ℝ),
    x ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      Integrable (Box.face J i) GP (fun y => f (Fin.insertNth i x y)) BoxAdditiveMap.volume
hJδ' : ↑Box.Icc J ⊆ closedBall x δ ∩ ↑Box.Icc I
Hmaps :
  ∀ (z : ℝ),
    z ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      MapsTo (Fin.insertNth i z) (↑Box.Icc (Box.face J i)) (closedBall x δ ∩ ↑Box.Icc I)
⊢ ∏ x : Fin (n + 1), |Box.upper J x - Box.lower J x| ≤ (2 * δ) ^ (n + 1)
[PROOFSTEP]
have : ∀ j, |J.upper j - J.lower j| ≤ 2 * δ := fun j ↦
  calc
    dist (J.upper j) (J.lower j) ≤ dist J.upper J.lower := dist_le_pi_dist _ _ _
    _ ≤ dist J.upper x + dist J.lower x := (dist_triangle_right _ _ _)
    _ ≤ δ + δ := (add_le_add (hJδ J.upper_mem_Icc) (hJδ J.lower_mem_Icc))
    _ = 2 * δ := (two_mul δ).symm
[GOAL]
case refine'_3.intro.intro.intro.intro.refine'_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this✝ :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hi :
  ∀ (x : ℝ),
    x ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      Integrable (Box.face J i) GP (fun y => f (Fin.insertNth i x y)) BoxAdditiveMap.volume
hJδ' : ↑Box.Icc J ⊆ closedBall x δ ∩ ↑Box.Icc I
Hmaps :
  ∀ (z : ℝ),
    z ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      MapsTo (Fin.insertNth i z) (↑Box.Icc (Box.face J i)) (closedBall x δ ∩ ↑Box.Icc I)
this : ∀ (j : Fin (n + 1)), |Box.upper J j - Box.lower J j| ≤ 2 * δ
⊢ ∏ x : Fin (n + 1), |Box.upper J x - Box.lower J x| ≤ (2 * δ) ^ (n + 1)
[PROOFSTEP]
calc
  ∏ j, |J.upper j - J.lower j| ≤ ∏ j : Fin (n + 1), 2 * δ := prod_le_prod (fun _ _ => abs_nonneg _) fun j _ => this j
  _ = (2 * δ) ^ (n + 1) := by simp
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this✝ :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hi :
  ∀ (x : ℝ),
    x ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      Integrable (Box.face J i) GP (fun y => f (Fin.insertNth i x y)) BoxAdditiveMap.volume
hJδ' : ↑Box.Icc J ⊆ closedBall x δ ∩ ↑Box.Icc I
Hmaps :
  ∀ (z : ℝ),
    z ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      MapsTo (Fin.insertNth i z) (↑Box.Icc (Box.face J i)) (closedBall x δ ∩ ↑Box.Icc I)
this : ∀ (j : Fin (n + 1)), |Box.upper J j - Box.lower J j| ≤ 2 * δ
⊢ ∏ j : Fin (n + 1), 2 * δ = (2 * δ) ^ (n + 1)
[PROOFSTEP]
simp
[GOAL]
case refine'_3.intro.intro.intro.intro.refine'_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hi :
  ∀ (x : ℝ),
    x ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      Integrable (Box.face J i) GP (fun y => f (Fin.insertNth i x y)) BoxAdditiveMap.volume
hJδ' : ↑Box.Icc J ⊆ closedBall x δ ∩ ↑Box.Icc I
Hmaps :
  ∀ (z : ℝ),
    z ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      MapsTo (Fin.insertNth i z) (↑Box.Icc (Box.face J i)) (closedBall x δ ∩ ↑Box.Icc I)
⊢ ‖integral (Box.face J i) GP
        ((fun y => f (Fin.insertNth i (Box.upper J i) y)) - fun y => f (Fin.insertNth i (Box.lower J i) y))
        BoxAdditiveMap.volume‖ ≤
    ε / 2
[PROOFSTEP]
refine' (norm_integral_le_of_le_const (fun y hy => hdfδ _ (Hmaps _ Hu hy) _ (Hmaps _ Hl hy)) volume).trans _
[GOAL]
case refine'_3.intro.intro.intro.intro.refine'_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hi :
  ∀ (x : ℝ),
    x ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      Integrable (Box.face J i) GP (fun y => f (Fin.insertNth i x y)) BoxAdditiveMap.volume
hJδ' : ↑Box.Icc J ⊆ closedBall x δ ∩ ↑Box.Icc I
Hmaps :
  ∀ (z : ℝ),
    z ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      MapsTo (Fin.insertNth i z) (↑Box.Icc (Box.face J i)) (closedBall x δ ∩ ↑Box.Icc I)
⊢ ENNReal.toReal (↑↑volume ↑(Box.face J i)) * (ε / 2) ≤ ε / 2
[PROOFSTEP]
refine' (mul_le_mul_of_nonneg_right _ (half_pos ε0).le).trans_eq (one_mul _)
[GOAL]
case refine'_3.intro.intro.intro.intro.refine'_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hi :
  ∀ (x : ℝ),
    x ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      Integrable (Box.face J i) GP (fun y => f (Fin.insertNth i x y)) BoxAdditiveMap.volume
hJδ' : ↑Box.Icc J ⊆ closedBall x δ ∩ ↑Box.Icc I
Hmaps :
  ∀ (z : ℝ),
    z ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      MapsTo (Fin.insertNth i z) (↑Box.Icc (Box.face J i)) (closedBall x δ ∩ ↑Box.Icc I)
⊢ ENNReal.toReal (↑↑volume ↑(Box.face J i)) ≤ 1
[PROOFSTEP]
rw [Box.coe_eq_pi, Real.volume_pi_Ioc_toReal (Box.lower_le_upper _)]
[GOAL]
case refine'_3.intro.intro.intro.intro.refine'_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ ↑Box.Icc J
x✝ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hi :
  ∀ (x : ℝ),
    x ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      Integrable (Box.face J i) GP (fun y => f (Fin.insertNth i x y)) BoxAdditiveMap.volume
hJδ' : ↑Box.Icc J ⊆ closedBall x δ ∩ ↑Box.Icc I
Hmaps :
  ∀ (z : ℝ),
    z ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      MapsTo (Fin.insertNth i z) (↑Box.Icc (Box.face J i)) (closedBall x δ ∩ ↑Box.Icc I)
⊢ ∏ i_1 : Fin n, (Box.upper (Box.face J i) i_1 - Box.lower (Box.face J i) i_1) ≤ 1
[PROOFSTEP]
refine' prod_le_one (fun _ _ => sub_nonneg.2 <| Box.lower_le_upper _ _) fun j _ => _
[GOAL]
case refine'_3.intro.intro.intro.intro.refine'_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[Set.Ioi 0] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ (y₁ : Fin (n + 1) → ℝ),
          y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
            ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ :
  ∀ (y₁ : Fin (n + 1) → ℝ),
    y₁ ∈ closedBall x δ ∩ ↑Box.Icc I →
      ∀ (y₂ : Fin (n + 1) → ℝ), y₂ ∈ closedBall x δ ∩ ↑Box.Icc I → ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖↑(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
x✝² : x ∈ ↑Box.Icc J
x✝¹ : GP.bDistortion = true → Box.distortion J ≤ c
Hl : Box.lower J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hu : Box.upper J i ∈ Set.Icc (Box.lower J i) (Box.upper J i)
Hi :
  ∀ (x : ℝ),
    x ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      Integrable (Box.face J i) GP (fun y => f (Fin.insertNth i x y)) BoxAdditiveMap.volume
hJδ' : ↑Box.Icc J ⊆ closedBall x δ ∩ ↑Box.Icc I
Hmaps :
  ∀ (z : ℝ),
    z ∈ Set.Icc (Box.lower J i) (Box.upper J i) →
      MapsTo (Fin.insertNth i z) (↑Box.Icc (Box.face J i)) (closedBall x δ ∩ ↑Box.Icc I)
j : Fin n
x✝ : j ∈ Finset.univ
⊢ Box.upper (Box.face J i) j - Box.lower (Box.face J i) j ≤ 1
[PROOFSTEP]
calc
  J.upper (i.succAbove j) - J.lower (i.succAbove j) ≤ dist (J.upper (i.succAbove j)) (J.lower (i.succAbove j)) :=
    le_abs_self _
  _ ≤ dist J.upper J.lower := (dist_le_pi_dist J.upper J.lower (i.succAbove j))
  _ ≤ dist J.upper x + dist J.lower x := (dist_triangle_right _ _ _)
  _ ≤ δ + δ := (add_le_add (hJδ J.upper_mem_Icc) (hJδ J.lower_mem_Icc))
  _ ≤ 1 / 2 + 1 / 2 := (add_le_add hδ12 hδ12)
  _ = 1 := add_halves 1
[GOAL]
case refine'_4
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
⊢ ∀ (c : ℝ≥0) (x : Fin (n + 1) → ℝ),
    x ∈ ↑Box.Icc I \ s →
      ∀ (ε : ℝ),
        ε > 0 →
          ∃ δ,
            δ > 0 ∧
              ∀ (J : Box (Fin (n + 1))),
                J ≤ I →
                  ↑Box.Icc J ⊆ closedBall x δ →
                    x ∈ ↑Box.Icc J →
                      (GP.bDistortion = true → Box.distortion J ≤ c) →
                        dist (↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1))) (↑F J) ≤
                          ε * ↑(BoxAdditiveMap.restrict (Measure.toBoxAdditive volume) ↑I (_ : ↑I ≤ ⊤)) J
[PROOFSTEP]
intro c x hx ε ε0
[GOAL]
case refine'_4
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
⊢ ∃ δ,
    δ > 0 ∧
      ∀ (J : Box (Fin (n + 1))),
        J ≤ I →
          ↑Box.Icc J ⊆ closedBall x δ →
            x ∈ ↑Box.Icc J →
              (GP.bDistortion = true → Box.distortion J ≤ c) →
                dist (↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1))) (↑F J) ≤
                  ε * ↑(BoxAdditiveMap.restrict (Measure.toBoxAdditive volume) ↑I (_ : ↑I ≤ ⊤)) J
[PROOFSTEP]
rcases exists_pos_mul_lt ε0 (2 * c) with ⟨ε', ε'0, hlt⟩
[GOAL]
case refine'_4.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * ↑c * ε' < ε
⊢ ∃ δ,
    δ > 0 ∧
      ∀ (J : Box (Fin (n + 1))),
        J ≤ I →
          ↑Box.Icc J ⊆ closedBall x δ →
            x ∈ ↑Box.Icc J →
              (GP.bDistortion = true → Box.distortion J ≤ c) →
                dist (↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1))) (↑F J) ≤
                  ε * ↑(BoxAdditiveMap.restrict (Measure.toBoxAdditive volume) ↑I (_ : ↑I ≤ ⊤)) J
[PROOFSTEP]
rcases(nhdsWithin_hasBasis nhds_basis_closedBall _).mem_iff.1 ((Hd x hx).def ε'0) with ⟨δ, δ0, Hδ⟩
[GOAL]
case refine'_4.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * ↑c * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : closedBall x δ ∩ ↑Box.Icc I ⊆ {x_1 | (fun x_2 => ‖f x_2 - f x - ↑(f' x) (x_2 - x)‖ ≤ ε' * ‖x_2 - x‖) x_1}
⊢ ∃ δ,
    δ > 0 ∧
      ∀ (J : Box (Fin (n + 1))),
        J ≤ I →
          ↑Box.Icc J ⊆ closedBall x δ →
            x ∈ ↑Box.Icc J →
              (GP.bDistortion = true → Box.distortion J ≤ c) →
                dist (↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1))) (↑F J) ≤
                  ε * ↑(BoxAdditiveMap.restrict (Measure.toBoxAdditive volume) ↑I (_ : ↑I ≤ ⊤)) J
[PROOFSTEP]
refine' ⟨δ, δ0, fun J hle hJδ hxJ hJc => _⟩
[GOAL]
case refine'_4.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * ↑c * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : closedBall x δ ∩ ↑Box.Icc I ⊆ {x_1 | (fun x_2 => ‖f x_2 - f x - ↑(f' x) (x_2 - x)‖ ≤ ε' * ‖x_2 - x‖) x_1}
J : Box (Fin (n + 1))
hle : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
hxJ : x ∈ ↑Box.Icc J
hJc : GP.bDistortion = true → Box.distortion J ≤ c
⊢ dist (↑(↑BoxAdditiveMap.volume J) (↑(f' x) (Pi.single i 1))) (↑F J) ≤
    ε * ↑(BoxAdditiveMap.restrict (Measure.toBoxAdditive volume) ↑I (_ : ↑I ≤ ⊤)) J
[PROOFSTEP]
simp only [BoxAdditiveMap.volume_apply, Box.volume_apply, dist_eq_norm]
[GOAL]
case refine'_4.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * ↑c * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : closedBall x δ ∩ ↑Box.Icc I ⊆ {x_1 | (fun x_2 => ‖f x_2 - f x - ↑(f' x) (x_2 - x)‖ ≤ ε' * ‖x_2 - x‖) x_1}
J : Box (Fin (n + 1))
hle : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
hxJ : x ∈ ↑Box.Icc J
hJc : GP.bDistortion = true → Box.distortion J ≤ c
⊢ ‖(∏ j : Fin (n + 1), (Box.upper J j - Box.lower J j)) • ↑(f' x) (Pi.single i 1) -
        ↑(BoxAdditiveMap.upperSubLower I i
              (fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume)
              (fun x =>
                Integrable.toBoxAdditive
                  (_ :
                    Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x)
                      (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume))))
              (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J))
          J‖ ≤
    ε * ↑(BoxAdditiveMap.restrict (Measure.toBoxAdditive volume) ↑I (_ : ↑I ≤ ⊤)) J
[PROOFSTEP]
refine'
  (norm_volume_sub_integral_face_upper_sub_lower_smul_le _ (Hc.mono <| Box.le_iff_Icc.1 hle) hxJ ε'0 (fun y hy => Hδ _)
        (hJc rfl)).trans
    _
[GOAL]
case refine'_4.intro.intro.intro.intro.refine'_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * ↑c * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : closedBall x δ ∩ ↑Box.Icc I ⊆ {x_1 | (fun x_2 => ‖f x_2 - f x - ↑(f' x) (x_2 - x)‖ ≤ ε' * ‖x_2 - x‖) x_1}
J : Box (Fin (n + 1))
hle : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
hxJ : x ∈ ↑Box.Icc J
hJc : GP.bDistortion = true → Box.distortion J ≤ c
y : Fin (n + 1) → ℝ
hy : y ∈ ↑Box.Icc J
⊢ y ∈ closedBall x δ ∩ ↑Box.Icc I
[PROOFSTEP]
exact ⟨hJδ hy, Box.le_iff_Icc.1 hle hy⟩
[GOAL]
case refine'_4.intro.intro.intro.intro.refine'_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * ↑c * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : closedBall x δ ∩ ↑Box.Icc I ⊆ {x_1 | (fun x_2 => ‖f x_2 - f x - ↑(f' x) (x_2 - x)‖ ≤ ε' * ‖x_2 - x‖) x_1}
J : Box (Fin (n + 1))
hle : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
hxJ : x ∈ ↑Box.Icc J
hJc : GP.bDistortion = true → Box.distortion J ≤ c
⊢ 2 * ε' * ↑c * ∏ j : Fin (n + 1), (Box.upper J j - Box.lower J j) ≤
    ε * ↑(BoxAdditiveMap.restrict (Measure.toBoxAdditive volume) ↑I (_ : ↑I ≤ ⊤)) J
[PROOFSTEP]
rw [mul_right_comm (2 : ℝ), ← Box.volume_apply]
[GOAL]
case refine'_4.intro.intro.intro.intro.refine'_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (↑Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (Fin.insertNth i y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (Box.lower I i) (Box.upper I i)) → Fin n →ᵇᵃ[↑(Box.face I i)] E :=
  fun x =>
    Integrable.toBoxAdditive
      (_ : Integrable (Box.face I i) GP (f ∘ Fin.insertNth i ↑x) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)))
F : Fin (n + 1) →ᵇᵃ[↑I] E :=
  BoxAdditiveMap.upperSubLower I i fI fb
    (_ : ∀ (x : ℝ), x ∈ Set.Icc (Box.lower I i) (Box.upper I i) → ∀ (J : Box (Fin n)), fI x J = fI x J)
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ ↑Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * ↑c * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : closedBall x δ ∩ ↑Box.Icc I ⊆ {x_1 | (fun x_2 => ‖f x_2 - f x - ↑(f' x) (x_2 - x)‖ ≤ ε' * ‖x_2 - x‖) x_1}
J : Box (Fin (n + 1))
hle : J ≤ I
hJδ : ↑Box.Icc J ⊆ closedBall x δ
hxJ : x ∈ ↑Box.Icc J
hJc : GP.bDistortion = true → Box.distortion J ≤ c
⊢ 2 * ↑c * ε' * ↑(Measure.toBoxAdditive volume) J ≤
    ε * ↑(BoxAdditiveMap.restrict (Measure.toBoxAdditive volume) ↑I (_ : ↑I ≤ ⊤)) J
[PROOFSTEP]
exact mul_le_mul_of_nonneg_right hlt.le ENNReal.toReal_nonneg
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : 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 : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
⊢ HasIntegral I GP (fun x => ∑ i : Fin (n + 1), ↑(f' x) (Pi.single i 1) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (integral (Box.face I i) GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i) BoxAdditiveMap.volume -
        integral (Box.face I i) GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i) BoxAdditiveMap.volume))
[PROOFSTEP]
refine HasIntegral.sum fun i _ => ?_
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : 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 : Set.Countable s
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ContinuousWithinAt f (↑Box.Icc I) x
Hd : ∀ (x : Fin (n + 1) → ℝ), x ∈ ↑Box.Icc I \ s → HasFDerivWithinAt f (f' x) (↑Box.Icc I) x
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ HasIntegral I GP (fun x => ↑(f' x) (Pi.single i 1) i) BoxAdditiveMap.volume
    (integral (Box.face I i) GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i) BoxAdditiveMap.volume -
      integral (Box.face I i) GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i) BoxAdditiveMap.volume)
[PROOFSTEP]
simp only [hasFDerivWithinAt_pi', continuousWithinAt_pi] at Hd Hs 
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i✝ : 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 : Set.Countable s
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
Hd :
  ∀ (x : Fin (n + 1) → ℝ),
    x ∈ ↑Box.Icc I \ s →
      ∀ (i : Fin (n + 1)),
        HasFDerivWithinAt (fun x => f x i) (ContinuousLinearMap.comp (ContinuousLinearMap.proj i) (f' x)) (↑Box.Icc I) x
Hs : ∀ (x : Fin (n + 1) → ℝ), x ∈ s → ∀ (i : Fin (n + 1)), ContinuousWithinAt (fun y => f y i) (↑Box.Icc I) x
⊢ HasIntegral I GP (fun x => ↑(f' x) (Pi.single i 1) i) BoxAdditiveMap.volume
    (integral (Box.face I i) GP (fun x => f (Fin.insertNth i (Box.upper I i) x) i) BoxAdditiveMap.volume -
      integral (Box.face I i) GP (fun x => f (Fin.insertNth i (Box.lower I i) x) i) BoxAdditiveMap.volume)
[PROOFSTEP]
exact hasIntegral_GP_pderiv I _ _ s hs (fun x hx => Hs x hx i) (fun x hx => Hd x hx i) i
