awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch :
  ∀ᵐ (a : α) ∂μ, LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) s
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1
h_diff :
  ∀ᵐ (a : α) ∂μ,
    HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ F x a) ((L : (a : E) → 𝕜 →L[𝕜] E) (F' a)) x₀
hm : AEStronglyMeasurable (β := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
key :
  HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ)
    (∫ (a : α), ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') a ∂μ) x₀
hF'_int : Integrable F' μ
refine : HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
⊢ Integrable F' μ ∧ HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
refine ⟨hF'_int, ?_⟩
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch :
  ∀ᵐ (a : α) ∂μ, LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) s
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1
h_diff :
  ∀ᵐ (a : α) ∂μ,
    HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ F x a) ((L : (a : E) → 𝕜 →L[𝕜] E) (F' a)) x₀
hm : AEStronglyMeasurable (β := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
key :
  HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ)
    (∫ (a : α), ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') a ∂μ) x₀
hF'_int : Integrable F' μ
pos :
  ∀ (hE : CompleteSpace E), HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
neg :
  ∀ (hE : ¬CompleteSpace E), HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
⊢ HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch :
  ∀ᵐ (a : α) ∂μ, LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) s
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1
h_diff :
  ∀ᵐ (a : α) ∂μ,
    HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ F x a) ((L : (a : E) → 𝕜 →L[𝕜] E) (F' a)) x₀
hm : AEStronglyMeasurable (β := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
key :
  HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ)
    (∫ (a : α), ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') a ∂μ) x₀
hF'_int : Integrable F' μ
hE : ¬CompleteSpace E
⊢ HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
simpa [integral, hE] using hasDerivAt_const x₀ 0

Premises used: hasDerivAt_const, MeasureTheory.integral, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch :
  ∀ᵐ (a : α) ∂μ, LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) s
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1
h_diff :
  ∀ᵐ (a : α) ∂μ,
    HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ F x a) ((L : (a : E) → 𝕜 →L[𝕜] E) (F' a)) x₀
hm : AEStronglyMeasurable (β := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
key :
  HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ)
    (∫ (a : α), ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') a ∂μ) x₀
hF'_int : Integrable F' μ
hE : CompleteSpace E
⊢ HasFDerivAt.{u_2, u_2, u_3} (𝕜 := 𝕜) (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ)
    (ContinuousLinearMap.toSpanSingleton 𝕜 (∫ (a : α), F' a ∂μ)) x₀

Tactic:
simpa only [(· ∘ ·), ContinuousLinearMap.integral_comp_comm _ hF'_int] using key

Premises used: Function.comp, ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
rcases :
  ∀ (ε : ℝ) (ε_pos : ε > 0) (hε : ball x₀ ε ⊆ s),
    Integrable (F' x₀) μ ∧ HasDerivAt.{u_2, u_3} (F := E) (fun (n : 𝕜) ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
⊢ Integrable (F' x₀) μ ∧ HasDerivAt.{u_2, u_3} (F := E) (fun (n : 𝕜) ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀

Tactic:
rcases Metric.mem_nhds_iff.1 hs with ⟨ε, ε_pos, hε⟩

Premises used: Metric.mem_nhds_iff, Iff.mp
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
⊢ x₀ ∈ ball x₀ ε

Tactic:
have x₀_in : x₀ ∈ ball x₀ ε := mem_ball_self ε_pos
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
⊢ ∀ᵐ (a : α) ∂μ, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x₀ a) x₀

Tactic:
have diff_x₀ : ∀ᵐ a ∂μ, HasDerivAt (F · a) (F' x₀ a) x₀ :=
    h_diff.mono fun a ha ↦ ha x₀ (hε x₀_in)
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x₀ a) x₀
apply :
  ∀ (x : α),
    ((∀ x_1 ∈ s, HasDerivAt (fun (x_2 : 𝕜) ↦ F x_2 x) (F' x_1 x) x_1) ∧ ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x) →
      LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : 𝕜) ↦ F x_1 x)
        (ball x₀ ε)
⊢ ∀ᵐ (a : α) ∂μ,
    LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) (ball x₀ ε)

Tactic:
apply (h_diff.and h_bound).mono

Premises used: Filter.Eventually.and, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
⊢ LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) (ball x₀ ε)

Tactic:
(convex_ball _ _).lipschitzOnWith_of_nnnorm_hasDerivWithin_le
      (fun x x_in ↦ (ha_deriv x (hε x_in)).hasDerivWithinAt) fun x x_in ↦ ?_

Premises used: HasDerivAt.hasDerivWithinAt, Convex.lipschitzOnWith_of_nnnorm_hasDerivWithin_le
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
refine : ∀ (x : 𝕜) (x_in : x ∈ ball x₀ ε), ‖F' x a‖₊ ≤ (Real.nnabs : (a : ℝ) → NNReal) (bound a)
⊢ LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) (ball x₀ ε)

Tactic:
refine (convex_ball _ _).lipschitzOnWith_of_nnnorm_hasDerivWithin_le
      (fun x x_in ↦ (ha_deriv x (hε x_in)).hasDerivWithinAt) fun x x_in ↦ ?_

Premises used: HasDerivAt.hasDerivWithinAt, Convex.lipschitzOnWith_of_nnnorm_hasDerivWithin_le
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
x : 𝕜
x_in : x ∈ ball x₀ ε
rw : ‖F' x a‖ ≤ |bound a|
⊢ ‖F' x a‖₊ ≤ (Real.nnabs : (a : ℝ) → NNReal) (bound a)

Tactic:
rw [← NNReal.coe_le_coe, coe_nnnorm, Real.coe_nnabs]

Premises used: Real.coe_nnabs, coe_nnnorm, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
x : 𝕜
x_in : x ∈ ball x₀ ε
⊢ ‖F' x a‖ ≤ |bound a|

Tactic:
(ha_bound x (hε x_in)).trans (le_abs_self _)

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
x : 𝕜
x_in : x ∈ ball x₀ ε
⊢ ‖F' x a‖ ≤ |bound a|

Tactic:
exact (ha_bound x (hε x_in)).trans (le_abs_self _)

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x₀ a) x₀
⊢ ∀ᵐ (a : α) ∂μ,
    LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) (ball x₀ ε)

Tactic:
have : ∀ᵐ a ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x : 𝕜 ↦ F x a) (ball x₀ ε) := by
    apply (h_diff.and h_bound).mono
    rintro a ⟨ha_deriv, ha_bound⟩
    refine (convex_ball _ _).lipschitzOnWith_of_nnnorm_hasDerivWithin_le
      (fun x x_in ↦ (ha_deriv x (hε x_in)).hasDerivWithinAt) fun x x_in ↦ ?_
    rw [← NNReal.coe_le_coe, coe_nnnorm, Real.coe_nnabs]
    exact (ha_bound x (hε x_in)).trans (le_abs_self _)
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x₀ a) x₀
this :
  ∀ᵐ (a : α) ∂μ,
    LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) (ball x₀ ε)
⊢ Integrable (F' x₀) μ ∧ HasDerivAt.{u_2, u_3} (F := E) (fun (n : 𝕜) ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀

Tactic:
hasDerivAt_integral_of_dominated_loc_of_lip (ball_mem_nhds x₀ ε_pos) hF_meas hF_int
    hF'_meas this bound_integrable diff_x₀

Premises used: hasDerivAt_integral_of_dominated_loc_of_lip, Metric.ball_mem_nhds
-- Module: Mathlib.Analysis.Calculus.ParametricIntegral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst_1 : RCLike 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' x₀ a) x₀
this :
  ∀ᵐ (a : α) ∂μ,
    LipschitzOnWith.{u_2, u_3} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound a)) (fun (x : 𝕜) ↦ F x a) (ball x₀ ε)
⊢ Integrable (F' x₀) μ ∧ HasDerivAt.{u_2, u_3} (F := E) (fun (n : 𝕜) ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀

Tactic:
exact hasDerivAt_integral_of_dominated_loc_of_lip (ball_mem_nhds x₀ ε_pos) hF_meas hF_int
    hF'_meas this bound_integrable diff_x₀

Premises used: hasDerivAt_integral_of_dominated_loc_of_lip, Metric.ball_mem_nhds
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
H : Type u_3
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lip :
  ∀ᵐ (t : ℝ) ∂μ,
    t ∈ Ι a b → LipschitzOnWith.{u_3, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound t)) (fun (x : H) ↦ F x t) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x t) (F' t) x₀
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_3, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s

Tactic:
rw [← ae_restrict_iff' measurableSet_uIoc] at h_lip h_diff

Premises used: measurableSet_uIoc, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
H : Type u_3
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lip :
  ∀ᵐ (t : ℝ) ∂μ,
    t ∈ Ι a b → LipschitzOnWith.{u_3, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound t)) (fun (x : H) ↦ F x t) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x t) (F' t) x₀
h_lip₁ :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_3, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s
⊢ IntervalIntegrable bound μ a b

Tactic:
rw [← ae_restrict_iff' measurableSet_uIoc] at h_lip h_diff

Premises used: measurableSet_uIoc, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
H : Type u_3
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lip :
  ∀ᵐ (t : ℝ) ∂μ,
    t ∈ Ι a b → LipschitzOnWith.{u_3, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound t)) (fun (x : H) ↦ F x t) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x t) (F' t) x₀
h_lip₁ :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_3, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s
bound_integrable₁ : IntervalIntegrable bound μ a b
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀

Tactic:
rw [← ae_restrict_iff' measurableSet_uIoc] at h_lip h_diff

Premises used: measurableSet_uIoc, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
H : Type u_3
inst_4 : NormedAddCommGroup H
inst_5 : NormedSpace 𝕜 H
s : Set H
a b : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lip :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b),
    LipschitzOnWith.{u_3, u_2} (β := E) ((Real.nnabs : (a : ℝ) → NNReal) (bound x)) (fun (x_1 : H) ↦ F x_1 x) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x_1 : H) ↦ F x_1 x) (F' x) x₀
simp :
  ∀ (hF_int : IntegrableOn (F x₀) (Ι a b) μ) (bound_integrable : IntegrableOn bound (Ι a b) μ),
    IntegrableOn F' (Ι a b) μ ∧
      HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ)
        (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
⊢ IntervalIntegrable F' μ a b ∧
    HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ)
      (∫ (t : ℝ) in a..b, F' t ∂μ) x₀

Tactic:
simp only [intervalIntegrable_iff] at hF_int bound_integrable ⊢

Premises used: intervalIntegrable_iff