awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : ¬CompleteSpace E
hH : Nontrivial H
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
have this : ¬CompleteSpace (H →L[𝕜] E)
Tactic: have : ¬(CompleteSpace (H →L[𝕜] E)) := by
        simpa [SeparatingDual.completeSpace_continuousLinearMap_iff] using hE
-- 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
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : ¬CompleteSpace E
hH : Nontrivial H
this : ¬CompleteSpace (H →L[𝕜] E)
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
have neg : HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ 0) 0 x₀
Tactic: simp only [integral, hE, ↓reduceDIte, this]
-- 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
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
have h_ball : ball x₀ ε ∈ 𝓝 x₀
Tactic: have h_ball : ball x₀ ε ∈ 𝓝 x₀ := ball_mem_nhds x₀ ε_pos
-- 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
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
⊢ ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
have apply : ball x₀ ε ⊆
  {x : H |
    (fun (x : H) ↦
        ‖x - x₀‖⁻¹ *
            ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
                ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
          norm.{u_3} (E := E)
            (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ))
      x}
Tactic: apply mem_of_superset (ball_mem_nhds _ ε_pos)
-- 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
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
x : H
x_in : x ∈ ball x₀ ε
⊢ Membership.mem (γ := Set H)
    {x : H |
      ‖x - x₀‖⁻¹ *
          ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
              ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
        norm.{u_3} (E := E)
          (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)}
    x
have hf : Integrable (F x) μ
Tactic: rw [Set.mem_setOf_eq, ← norm_smul_of_nonneg (nneg _), integral_smul, integral_sub, integral_sub,
      ← ContinuousLinearMap.integral_apply 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
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
x : H
x_in : x ∈ ball x₀ ε
hf : Integrable (F x) μ
hg : Integrable (F x₀) μ
⊢ Membership.mem (γ := Set H)
    {x : H |
      ‖x - x₀‖⁻¹ *
          ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
              ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
        norm.{u_3} (E := E)
          (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)}
    x
have hf₁ : Integrable.{u_3, u_1} (ε := E) (fun (a : α) ↦ F x a - F x₀ a) μ
Tactic: rw [Set.mem_setOf_eq, ← norm_smul_of_nonneg (nneg _), integral_smul, integral_sub, integral_sub,
      ← ContinuousLinearMap.integral_apply 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
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
x : H
x_in : x ∈ ball x₀ ε
hf : Integrable (F x) μ
hg : Integrable (F x₀) μ
hf₁ : Integrable.{u_3, u_1} (ε := E) (fun (a : α) ↦ F x a - F x₀ a) μ
⊢ Membership.mem (γ := Set H)
    {x : H |
      ‖x - x₀‖⁻¹ *
          ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
              ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
        norm.{u_3} (E := E)
          (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)}
    x
have hg₁ : Integrable.{u_3, u_1} (ε := E) (fun (a : α) ↦ (F' a : (a : H) → E) (x - x₀)) μ
Tactic: rw [Set.mem_setOf_eq, ← norm_smul_of_nonneg (nneg _), integral_smul, integral_sub, integral_sub,
      ← ContinuousLinearMap.integral_apply hF'_int]
-- 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
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
have this : ∀ᶠ (x : H) in 𝓝 x₀,
  ‖x - x₀‖⁻¹ *
      ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
          ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
    norm.{u_3} (E := E)
      (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
Tactic: have : ∀ᶠ x in 𝓝 x₀, ‖x - x₀‖⁻¹ * ‖((∫ a, F x a ∂μ) - ∫ a, F x₀ a ∂μ) - (∫ a, F' a ∂μ) (x - x₀)‖ =
      ‖∫ a, ‖x - x₀‖⁻¹ • (F x a - F x₀ a - F' a (x - x₀)) ∂μ‖ := by
    apply mem_of_superset (ball_mem_nhds _ ε_pos)
    intro x x_in; simp only
    rw [Set.mem_setOf_eq, ← norm_smul_of_nonneg (nneg _), integral_smul, integral_sub, integral_sub,
      ← ContinuousLinearMap.integral_apply hF'_int]
    exacts [hF_int' x x_in, hF_int, (hF_int' x x_in).sub hF_int,
      hF'_int.apply_continuousLinearMap _]
-- 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
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
⊢ HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
have pos : Tendsto.{u_4, u_3} (β := E)
  (fun (x : H) ↦ ∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
  (𝓝 x₀) (𝓝 (∫ (a : α), ‖x₀ - x₀‖⁻¹ • HSub.hSub (β := E) (F x₀ a - F x₀ a) ((F' a : (a : H) → E) (x₀ - x₀) : E) ∂μ))
Tactic: rw [hasFDerivAt_iff_tendsto, tendsto_congr' this, ← tendsto_zero_iff_norm_tendsto_zero, ←
    show (∫ a : α, ‖x₀ - x₀‖⁻¹ • (F x₀ a - F x₀ a - (F' a) (x₀ - x₀)) ∂μ) = 0 by simp]
-- 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
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
⊢ Tendsto.{u_4, u_3} (β := E)
    (fun (x : H) ↦ ∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
    (𝓝 x₀) (𝓝 (∫ (a : α), ‖x₀ - x₀‖⁻¹ • HSub.hSub (β := E) (F x₀ a - F x₀ a) ((F' a : (a : H) → E) (x₀ - x₀) : E) ∂μ))
have pos : ∀ᶠ (n : H) in 𝓝 x₀,
  AEStronglyMeasurable.{u_1, u_3} (β := E)
    (fun (a : α) ↦ ‖n - x₀‖⁻¹ • HSub.hSub (β := E) (F n a - F x₀ a) ((F' a : (a : H) → E) (n - x₀) : E)) μ
Tactic: apply tendsto_integral_filter_of_dominated_convergence
-- 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
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
pos :
  ∀ᶠ (n : H) in 𝓝 x₀,
    AEStronglyMeasurable.{u_1, u_3} (β := E)
      (fun (a : α) ↦ ‖n - x₀‖⁻¹ • HSub.hSub (β := E) (F n a - F x₀ a) ((F' a : (a : H) → E) (n - x₀) : E)) μ
⊢ Tendsto.{u_4, u_3} (β := E)
    (fun (x : H) ↦ ∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
    (𝓝 x₀) (𝓝 (∫ (a : α), ‖x₀ - x₀‖⁻¹ • HSub.hSub (β := E) (F x₀ a - F x₀ a) ((F' a : (a : H) → E) (x₀ - x₀) : E) ∂μ))
have pos₁ : ∀ᶠ (n : H) in 𝓝 x₀,
  ∀ᵐ (a : α) ∂μ, ‖‖n - x₀‖⁻¹ • HSub.hSub (β := E) (F n a - F x₀ a) ((F' a : (a : H) → E) (n - x₀) : E)‖ ≤ b a + ‖F' a‖
Tactic: apply tendsto_integral_filter_of_dominated_convergence
-- 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
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
pos :
  ∀ᶠ (n : H) in 𝓝 x₀,
    AEStronglyMeasurable.{u_1, u_3} (β := E)
      (fun (a : α) ↦ ‖n - x₀‖⁻¹ • HSub.hSub (β := E) (F n a - F x₀ a) ((F' a : (a : H) → E) (n - x₀) : E)) μ
pos₁ :
  ∀ᶠ (n : H) in 𝓝 x₀,
    ∀ᵐ (a : α) ∂μ, ‖‖n - x₀‖⁻¹ • HSub.hSub (β := E) (F n a - F x₀ a) ((F' a : (a : H) → E) (n - x₀) : E)‖ ≤ b a + ‖F' a‖
⊢ Tendsto.{u_4, u_3} (β := E)
    (fun (x : H) ↦ ∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
    (𝓝 x₀) (𝓝 (∫ (a : α), ‖x₀ - x₀‖⁻¹ • HSub.hSub (β := E) (F x₀ a - F x₀ a) ((F' a : (a : H) → E) (x₀ - x₀) : E) ∂μ))
have pos₂ : Integrable (ε := ℝ) (fun (a : α) ↦ b a + ‖F' a‖) μ
Tactic: apply tendsto_integral_filter_of_dominated_convergence
-- 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
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt.{u_2, u_4, u_3} (𝕜 := 𝕜) (F := E) (fun (x : H) ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun (a : α) ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ *
        ‖HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (a : α), F x a ∂μ) (∫ (a : α), F x₀ a ∂μ))
            ((∫ (a : α), F' a ∂μ : (a : H) → E) (x - x₀) : E)‖ =
      norm.{u_3} (E := E)
        (∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
pos :
  ∀ᶠ (n : H) in 𝓝 x₀,
    AEStronglyMeasurable.{u_1, u_3} (β := E)
      (fun (a : α) ↦ ‖n - x₀‖⁻¹ • HSub.hSub (β := E) (F n a - F x₀ a) ((F' a : (a : H) → E) (n - x₀) : E)) μ
pos₁ :
  ∀ᶠ (n : H) in 𝓝 x₀,
    ∀ᵐ (a : α) ∂μ, ‖‖n - x₀‖⁻¹ • HSub.hSub (β := E) (F n a - F x₀ a) ((F' a : (a : H) → E) (n - x₀) : E)‖ ≤ b a + ‖F' a‖
pos₂ : Integrable (ε := ℝ) (fun (a : α) ↦ b a + ‖F' a‖) μ
⊢ Tendsto.{u_4, u_3} (β := E)
    (fun (x : H) ↦ ∫ (a : α), ‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E) ∂μ)
    (𝓝 x₀) (𝓝 (∫ (a : α), ‖x₀ - x₀‖⁻¹ • HSub.hSub (β := E) (F x₀ a - F x₀ a) ((F' a : (a : H) → E) (x₀ - x₀) : E) ∂μ))
have pos₃ : ∀ᵐ (a : α) ∂μ,
  Tendsto (fun (n : H) ↦ ‖n - x₀‖⁻¹ • HSub.hSub (β := E) (F n a - F x₀ a) ((F' a : (a : H) → E) (n - x₀) : E)) (𝓝 x₀)
    (𝓝 (‖x₀ - x₀‖⁻¹ • HSub.hSub (β := E) (F x₀ a - F x₀ a) ((F' a : (a : H) → E) (x₀ - x₀) : E)))
Tactic: apply tendsto_integral_filter_of_dominated_convergence