awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_4
inst_2 : NormedAddCommGroup H
x₀ : H
s : Set H
inst_3 : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
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' x₀) (μ.restrict (Ι a b))
h_bound :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, HasFDerivAt (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, HasFDerivAt (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1
⊢ HasFDerivAt.{0, u_4, u_3} (𝕜 := ℝ) (F := E) (fun (x : H) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ)
    (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
have hF'_meas₁ : AEStronglyMeasurable (F' x₀) (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable (F' x₀) (μ.restrict (Set.Ioc b a))
Tactic: simp_rw [AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff, eventually_and] at hF_meas hF'_meas
Cleared hypotheses: hF_meas, hF'_meas
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_4
inst_2 : NormedAddCommGroup H
x₀ : H
s : Set H
inst_3 : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
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' x₀) (μ.restrict (Ι a b))
h_bound :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, HasFDerivAt (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, HasFDerivAt (fun (x_2 : H) ↦ F x_2 x) (F' x_1 x) x_1
hF'_meas₁ :
  AEStronglyMeasurable (F' x₀) (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable (F' x₀) (μ.restrict (Set.Ioc b a))
⊢ HasFDerivAt.{0, u_4, u_3} (𝕜 := ℝ) (F := E) (fun (x : H) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ)
    (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
have hF_meas₁ : (∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc a b))) ∧
  ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc b a))
Tactic: simp_rw [AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff, eventually_and] at hF_meas hF'_meas
Cleared hypotheses: hF_meas, hF'_meas
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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 μ
h_diff : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun (x : 𝕜) ↦ F x a) (F' a) x₀
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1
⊢ Integrable F' μ ∧ HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
have 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₀
Tactic: replace h_diff : ∀ᵐ a ∂μ, HasFDerivAt (F · a) (L (F' a)) x₀ :=
    h_diff.mono fun x hx ↦ hx.hasFDerivAt
Cleared hypotheses: h_diff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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₀
⊢ Integrable F' μ ∧ HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
have hm : AEStronglyMeasurable (β := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
Tactic: have hm : AEStronglyMeasurable (L ∘ F') μ := L.continuous.comp_aestronglyMeasurable hF'_meas
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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') μ
⊢ Integrable F' μ ∧ HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
have hF'_int : Integrable (ε := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
Tactic: obtain ⟨hF'_int, key⟩ := hasFDerivAt_integral_of_dominated_loc_of_lip
    hs hF_meas hF_int hm h_lipsch bound_integrable h_diff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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') μ
hF'_int : Integrable (ε := 𝕜 →L[𝕜] E) ((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') μ
⊢ Integrable F' μ ∧ HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
have 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₀
Tactic: obtain ⟨hF'_int, key⟩ := hasFDerivAt_integral_of_dominated_loc_of_lip
    hs hF_meas hF_int hm h_lipsch bound_integrable h_diff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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') μ
hF'_int : Integrable (ε := 𝕜 →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₀
⊢ Integrable F' μ
have hF'_int₁ : Integrable (ε := ℝ) (fun (a : α) ↦ norm (E := 𝕜 →L[𝕜] E) (((⇑L : (a : E) → 𝕜 →L[𝕜] E) ∘ F') a)) μ
Tactic: rw [← integrable_norm_iff hm] at hF'_int
Cleared hypotheses: hF'_int, key
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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') μ
hF'_int : Integrable (ε := 𝕜 →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₀
⊢ Integrable F' μ ∧ HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
have hF'_int₁ : Integrable F' μ
Tactic: replace hF'_int : Integrable F' μ := by
    rw [← integrable_norm_iff hm] at hF'_int
    simpa [L, (· ∘ ·), integrable_norm_iff hF'_meas] using hF'_int
Cleared hypotheses: hF'_int
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (goal)
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' μ
⊢ Integrable F' μ ∧ HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
have refine : HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
Tactic: refine ⟨hF'_int, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (goal)
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' μ
⊢ HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
have pos : ∀ (hE : CompleteSpace E), HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (goal)
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₀
⊢ HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
have neg : ∀ (hE : ¬CompleteSpace E), HasDerivAt.{u_2, u_3} (F := E) (fun (x : 𝕜) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (goal)
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
⊢ Integrable (F' x₀) μ ∧ HasDerivAt.{u_2, u_3} (F := E) (fun (n : 𝕜) ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
have 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₀
Tactic: rcases Metric.mem_nhds_iff.1 hs with ⟨ε, ε_pos, hε⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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
⊢ Integrable (F' x₀) μ ∧ HasDerivAt.{u_2, u_3} (F := E) (fun (n : 𝕜) ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
have x₀_in : x₀ ∈ ball x₀ ε
Tactic: have x₀_in : x₀ ∈ ball x₀ ε := mem_ball_self ε_pos
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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₀ ε
⊢ Integrable (F' x₀) μ ∧ HasDerivAt.{u_2, u_3} (F := E) (fun (n : 𝕜) ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
have diff_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)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (goal)
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₀ ε)
have 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₀ ε)
Tactic: apply (h_diff.and h_bound).mono
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (goal)
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₀ ε)
have refine : ∀ (x : 𝕜) (x_in : x ∈ ball x₀ ε), ‖F' x a‖₊ ≤ (Real.nnabs : (a : ℝ) → NNReal) (bound a)
Tactic: refine (convex_ball _ _).lipschitzOnWith_of_nnnorm_hasDerivWithin_le
      (fun x x_in ↦ (ha_deriv x (hε x_in)).hasDerivWithinAt) fun x x_in ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (goal)
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‖₊ ≤ (Real.nnabs : (a : ℝ) → NNReal) (bound a)
have rw : ‖F' x a‖ ≤ |bound a|
Tactic: rw [← NNReal.coe_le_coe, coe_nnnorm, Real.coe_nnabs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntegral (hypothesis)
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₀
⊢ Integrable (F' x₀) μ ∧ HasDerivAt.{u_2, u_3} (F := E) (fun (n : 𝕜) ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
have this : ∀ᵐ (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 _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ParametricIntervalIntegral (hypothesis)
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₀
⊢ 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₀
have 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
Tactic: rw [← ae_restrict_iff' measurableSet_uIoc] at h_lip h_diff
Cleared hypotheses: h_lip, bound_integrable, h_diff