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)
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))
refine HasIntegral.sum fun i _ => ?_
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)
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)
simp only [hasFDerivWithinAt_pi', continuousWithinAt_pi] at Hd Hs
no goals
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)
exact hasIntegral_GP_pderiv I _ _ s hs (fun x hx => Hs x hx i) (fun x hx => Hd x hx i) i