[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (Measure.restrict μ (Ι a b))
h_lip : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → LipschitzOnWith (↑Real.nnabs (bound t)) (fun x => F x t) (ball x₀ ε)
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasFDerivAt (fun x => F x t) (F' t) x₀
⊢ IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
[PROOFSTEP]
rw [← ae_restrict_iff' measurableSet_uIoc] at h_lip h_diff
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (Measure.restrict μ (Ι a b))
h_lip : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), LipschitzOnWith (↑Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), HasFDerivAt (fun x_1 => F x_1 x) (F' x) x₀
⊢ IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
[PROOFSTEP]
simp only [intervalIntegrable_iff] at hF_int bound_integrable ⊢
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF'_meas : AEStronglyMeasurable F' (Measure.restrict μ (Ι a b))
h_lip : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), LipschitzOnWith (↑Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
h_diff : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), HasFDerivAt (fun x_1 => F x_1 x) (F' x) x₀
hF_int : IntegrableOn (F x₀) (Ι a b)
bound_integrable : IntegrableOn bound (Ι a b)
⊢ IntegrableOn F' (Ι a b) ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
[PROOFSTEP]
simp only [intervalIntegral_eq_integral_uIoc]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF'_meas : AEStronglyMeasurable F' (Measure.restrict μ (Ι a b))
h_lip : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), LipschitzOnWith (↑Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
h_diff : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), HasFDerivAt (fun x_1 => F x_1 x) (F' x) x₀
hF_int : IntegrableOn (F x₀) (Ι a b)
bound_integrable : IntegrableOn bound (Ι a b)
⊢ IntegrableOn F' (Ι a b) ∧
    HasFDerivAt (fun x => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ)
      ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' t ∂μ) x₀
[PROOFSTEP]
have := hasFDerivAt_integral_of_dominated_loc_of_lip ε_pos hF_meas hF_int hF'_meas h_lip bound_integrable h_diff
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF'_meas : AEStronglyMeasurable F' (Measure.restrict μ (Ι a b))
h_lip : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), LipschitzOnWith (↑Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
h_diff : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), HasFDerivAt (fun x_1 => F x_1 x) (F' x) x₀
hF_int : IntegrableOn (F x₀) (Ι a b)
bound_integrable : IntegrableOn bound (Ι a b)
this : Integrable F' ∧ HasFDerivAt (fun x => ∫ (a : ℝ) in Ι a b, F x a ∂μ) (∫ (a : ℝ) in Ι a b, F' a ∂μ) x₀
⊢ IntegrableOn F' (Ι a b) ∧
    HasFDerivAt (fun x => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ)
      ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' t ∂μ) x₀
[PROOFSTEP]
exact ⟨this.1, this.2.const_smul _⟩
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (Measure.restrict μ (Ι a b))
h_bound : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ (x : H), x ∈ ball x₀ ε → ‖F' x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ (x : H), x ∈ ball x₀ ε → HasFDerivAt (fun x => F x t) (F' x t) x
⊢ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
[PROOFSTEP]
rw [← ae_restrict_iff' measurableSet_uIoc] at h_bound h_diff
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (Measure.restrict μ (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ∀ (x_1 : H), x_1 ∈ ball x₀ ε → ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ∀ (x_1 : H), x_1 ∈ ball x₀ ε → HasFDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1
⊢ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
[PROOFSTEP]
simp only [intervalIntegrable_iff] at hF_int bound_integrable
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF'_meas : AEStronglyMeasurable (F' x₀) (Measure.restrict μ (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ∀ (x_1 : H), x_1 ∈ ball x₀ ε → ‖F' x_1 x‖ ≤ bound x
h_diff :
  ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ∀ (x_1 : H), x_1 ∈ ball x₀ ε → HasFDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1
hF_int : IntegrableOn (F x₀) (Ι a b)
bound_integrable : IntegrableOn bound (Ι a b)
⊢ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
[PROOFSTEP]
simp only [intervalIntegral_eq_integral_uIoc]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF'_meas : AEStronglyMeasurable (F' x₀) (Measure.restrict μ (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ∀ (x_1 : H), x_1 ∈ ball x₀ ε → ‖F' x_1 x‖ ≤ bound x
h_diff :
  ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ∀ (x_1 : H), x_1 ∈ ball x₀ ε → HasFDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1
hF_int : IntegrableOn (F x₀) (Ι a b)
bound_integrable : IntegrableOn bound (Ι a b)
⊢ HasFDerivAt (fun x => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ)
    ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' x₀ t ∂μ) x₀
[PROOFSTEP]
exact
  (hasFDerivAt_integral_of_dominated_of_fderiv_le ε_pos hF_meas hF_int hF'_meas h_bound bound_integrable
        h_diff).const_smul
    _
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (Measure.restrict μ (Ι a b))
h_lipsch : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → LipschitzOnWith (↑Real.nnabs (bound t)) (fun x => F x t) (ball x₀ ε)
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasDerivAt (fun x => F x t) (F' t) x₀
⊢ IntervalIntegrable F' μ a b ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
[PROOFSTEP]
rw [← ae_restrict_iff' measurableSet_uIoc] at h_lipsch h_diff
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (Measure.restrict μ (Ι a b))
h_lipsch :
  ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), LipschitzOnWith (↑Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), HasDerivAt (fun x_1 => F x_1 x) (F' x) x₀
⊢ IntervalIntegrable F' μ a b ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
[PROOFSTEP]
simp only [intervalIntegrable_iff] at hF_int bound_integrable ⊢
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF'_meas : AEStronglyMeasurable F' (Measure.restrict μ (Ι a b))
h_lipsch :
  ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), LipschitzOnWith (↑Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
h_diff : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), HasDerivAt (fun x_1 => F x_1 x) (F' x) x₀
hF_int : IntegrableOn (F x₀) (Ι a b)
bound_integrable : IntegrableOn bound (Ι a b)
⊢ IntegrableOn F' (Ι a b) ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
[PROOFSTEP]
simp only [intervalIntegral_eq_integral_uIoc]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF'_meas : AEStronglyMeasurable F' (Measure.restrict μ (Ι a b))
h_lipsch :
  ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), LipschitzOnWith (↑Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
h_diff : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), HasDerivAt (fun x_1 => F x_1 x) (F' x) x₀
hF_int : IntegrableOn (F x₀) (Ι a b)
bound_integrable : IntegrableOn bound (Ι a b)
⊢ IntegrableOn F' (Ι a b) ∧
    HasDerivAt (fun x => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ)
      ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' t ∂μ) x₀
[PROOFSTEP]
have := hasDerivAt_integral_of_dominated_loc_of_lip ε_pos hF_meas hF_int hF'_meas h_lipsch bound_integrable h_diff
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : 𝕜 → ℝ → E
F' : ℝ → E
x₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF'_meas : AEStronglyMeasurable F' (Measure.restrict μ (Ι a b))
h_lipsch :
  ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), LipschitzOnWith (↑Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
h_diff : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), HasDerivAt (fun x_1 => F x_1 x) (F' x) x₀
hF_int : IntegrableOn (F x₀) (Ι a b)
bound_integrable : IntegrableOn bound (Ι a b)
this : Integrable F' ∧ HasDerivAt (fun x => ∫ (a : ℝ) in Ι a b, F x a ∂μ) (∫ (a : ℝ) in Ι a b, F' a ∂μ) x₀
⊢ IntegrableOn F' (Ι a b) ∧
    HasDerivAt (fun x => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ)
      ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' t ∂μ) x₀
[PROOFSTEP]
exact ⟨this.1, this.2.const_smul _⟩
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (Measure.restrict μ (Ι a b))
h_bound : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ (x : 𝕜), x ∈ ball x₀ ε → ‖F' x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ (x : 𝕜), x ∈ ball x₀ ε → HasDerivAt (fun x => F x t) (F' x t) x
⊢ IntervalIntegrable (F' x₀) μ a b ∧
    HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
[PROOFSTEP]
rw [← ae_restrict_iff' measurableSet_uIoc] at h_bound h_diff
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (Measure.restrict μ (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ∀ (x_1 : 𝕜), x_1 ∈ ball x₀ ε → ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ∀ (x_1 : 𝕜), x_1 ∈ ball x₀ ε → HasDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1
⊢ IntervalIntegrable (F' x₀) μ a b ∧
    HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
[PROOFSTEP]
simp only [intervalIntegrable_iff] at hF_int bound_integrable ⊢
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF'_meas : AEStronglyMeasurable (F' x₀) (Measure.restrict μ (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ∀ (x_1 : 𝕜), x_1 ∈ ball x₀ ε → ‖F' x_1 x‖ ≤ bound x
h_diff :
  ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ∀ (x_1 : 𝕜), x_1 ∈ ball x₀ ε → HasDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1
hF_int : IntegrableOn (F x₀) (Ι a b)
bound_integrable : IntegrableOn bound (Ι a b)
⊢ IntegrableOn (F' x₀) (Ι a b) ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
[PROOFSTEP]
simp only [intervalIntegral_eq_integral_uIoc]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF'_meas : AEStronglyMeasurable (F' x₀) (Measure.restrict μ (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ∀ (x_1 : 𝕜), x_1 ∈ ball x₀ ε → ‖F' x_1 x‖ ≤ bound x
h_diff :
  ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ∀ (x_1 : 𝕜), x_1 ∈ ball x₀ ε → HasDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1
hF_int : IntegrableOn (F x₀) (Ι a b)
bound_integrable : IntegrableOn bound (Ι a b)
⊢ IntegrableOn (F' x₀) (Ι a b) ∧
    HasDerivAt (fun x => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ)
      ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' x₀ t ∂μ) x₀
[PROOFSTEP]
have := hasDerivAt_integral_of_dominated_loc_of_deriv_le ε_pos hF_meas hF_int hF'_meas h_bound bound_integrable h_diff
[GOAL]
𝕜 : Type u_1
inst✝⁶ : IsROrC 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (Measure.restrict μ (Ι a b))
hF'_meas : AEStronglyMeasurable (F' x₀) (Measure.restrict μ (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ∀ (x_1 : 𝕜), x_1 ∈ ball x₀ ε → ‖F' x_1 x‖ ≤ bound x
h_diff :
  ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ∀ (x_1 : 𝕜), x_1 ∈ ball x₀ ε → HasDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1
hF_int : IntegrableOn (F x₀) (Ι a b)
bound_integrable : IntegrableOn bound (Ι a b)
this : Integrable (F' x₀) ∧ HasDerivAt (fun n => ∫ (a : ℝ) in Ι a b, F n a ∂μ) (∫ (a : ℝ) in Ι a b, F' x₀ a ∂μ) x₀
⊢ IntegrableOn (F' x₀) (Ι a b) ∧
    HasDerivAt (fun x => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ)
      ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' x₀ t ∂μ) x₀
[PROOFSTEP]
exact ⟨this.1, this.2.const_smul _⟩