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
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) ∂μ)
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
⊢ ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖

Tactic:
replace ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖ := ha_bound x hx
-- 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
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) ∂μ)
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
rw rw₁ :
  ‖‖x - x₀‖⁻¹ • (F x a - F x₀ a) - HSMul.hSMul (β := E) ‖x - x₀‖⁻¹ ((F' a : (a : H) → E) (x - x₀) : E)‖ =
    ‖‖x - x₀‖⁻¹ • (F x a - F x₀ a) - HSMul.hSMul (β := E) ‖x - x₀‖⁻¹ ((F' a : (a : H) → E) (x - x₀) : E)‖
⊢ ‖‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E)‖ =
    ‖‖x - x₀‖⁻¹ • (F x a - F x₀ a) - HSMul.hSMul (β := E) ‖x - x₀‖⁻¹ ((F' a : (a : H) → E) (x - x₀) : E)‖

Tactic:
rw [smul_sub]

Premises used: smul_sub
-- 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
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) ∂μ)
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
⊢ ‖‖x - x₀‖⁻¹ • (F x a - F x₀ a) - HSMul.hSMul (β := E) ‖x - x₀‖⁻¹ ((F' a : (a : H) → E) (x - x₀) : E)‖ ≤
    ‖‖x - x₀‖⁻¹ • (F x a - F x₀ a)‖ + ‖HSMul.hSMul (β := E) ‖x - x₀‖⁻¹ ((F' a : (a : H) → E) (x - x₀) : E)‖

Tactic:
norm_sub_le _ _

Premises used: norm_sub_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
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) ∂μ)
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
ht ht₁ : 0 ≤ ‖x - x₀‖⁻¹
⊢ ‖‖x - x₀‖⁻¹ • (F x a - F x₀ a)‖ + ‖HSMul.hSMul (β := E) ‖x - x₀‖⁻¹ ((F' a : (a : H) → E) (x - x₀) : E)‖ =
    ‖x - x₀‖⁻¹ * ‖F x a - F x₀ a‖ + ‖x - x₀‖⁻¹ * norm.{u_3} (E := E) ((F' a : (a : H) → E) (x - x₀) : E)

Tactic:
rw [norm_smul_of_nonneg, norm_smul_of_nonneg]

Premises used: norm_smul_of_nonneg
-- 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
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) ∂μ)
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
⊢ 0 ≤ ‖x - x₀‖⁻¹

Tactic:
nneg _
-- 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
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) ∂μ)
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
⊢ 0 ≤ ‖x - x₀‖⁻¹

Tactic:
exact nneg _
-- 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
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) ∂μ)
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
h₂ : norm.{u_3} (E := E) ((F' a : (a : H) → E) (x - x₀) : E) ≤ ‖F' a‖ * ‖x - x₀‖
⊢ ‖x - x₀‖⁻¹ * ‖F x a - F x₀ a‖ + ‖x - x₀‖⁻¹ * norm.{u_3} (E := E) ((F' a : (a : H) → E) (x - x₀) : E) ≤
    ‖x - x₀‖⁻¹ * (b a * ‖x - x₀‖) + ‖x - x₀‖⁻¹ * (‖F' a‖ * ‖x - x₀‖)

Tactic:
gcongr
-- 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
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) ∂μ)
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
⊢ norm.{u_3} (E := E) ((F' a : (a : H) → E) (x - x₀) : E) ≤ ‖F' a‖ * ‖x - x₀‖

Tactic:
(F' a).le_opNorm _

Premises used: ContinuousLinearMap.le_opNorm
-- 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
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) ∂μ)
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
⊢ norm.{u_3} (E := E) ((F' a : (a : H) → E) (x - x₀) : E) ≤ ‖F' a‖ * ‖x - x₀‖

Tactic:
exact (F' a).le_opNorm _

Premises used: ContinuousLinearMap.le_opNorm
-- 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
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) ∂μ)
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
⊢ ‖x - x₀‖⁻¹ * (b a * ‖x - x₀‖) + ‖x - x₀‖⁻¹ * (‖F' a‖ * ‖x - x₀‖) ≤ b a + ‖F' a‖

Tactic:
?_
-- 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
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) ∂μ)
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
pos : ‖x - x₀‖⁻¹ * (b a * ‖x - x₀‖) + ‖x - x₀‖⁻¹ * (‖F' a‖ * ‖x - x₀‖) ≤ b a + ‖F' a‖
⊢ ‖‖x - x₀‖⁻¹ • HSub.hSub (β := E) (F x a - F x₀ a) ((F' a : (a : H) → E) (x - x₀) : E)‖ ≤ b a + ‖F' a‖

Tactic:
calc
      ‖‖x - x₀‖⁻¹ • (F x a - F x₀ a - F' a (x - x₀))‖ =
          ‖‖x - x₀‖⁻¹ • (F x a - F x₀ a) - ‖x - x₀‖⁻¹ • F' a (x - x₀)‖ := by rw [smul_sub]
      _ ≤ ‖‖x - x₀‖⁻¹ • (F x a - F x₀ a)‖ + ‖‖x - x₀‖⁻¹ • F' a (x - x₀)‖ := norm_sub_le _ _
      _ = ‖x - x₀‖⁻¹ * ‖F x a - F x₀ a‖ + ‖x - x₀‖⁻¹ * ‖F' a (x - x₀)‖ := by
        rw [norm_smul_of_nonneg, norm_smul_of_nonneg] <;> exact nneg _
      _ ≤ ‖x - x₀‖⁻¹ * (b a * ‖x - x₀‖) + ‖x - x₀‖⁻¹ * (‖F' a‖ * ‖x - x₀‖) := by
        gcongr; exact (F' a).le_opNorm _
      _ ≤ b a + ‖F' a‖ := ?_

Premises used: Norm.norm, HMul.hMul, norm_sub_le, HSub.hSub, DFunLike.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
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) ∂μ)
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
pos : b a * ‖x - x₀‖ / ‖x - x₀‖ + ‖F' a‖ * ‖x - x₀‖ / ‖x - x₀‖ ≤ b a + ‖F' a‖
⊢ ‖x - x₀‖⁻¹ * (b a * ‖x - x₀‖) + ‖x - x₀‖⁻¹ * (‖F' a‖ * ‖x - x₀‖) ≤ b a + ‖F' a‖

Tactic:
simp only [← div_eq_inv_mul]

Premises used: div_eq_inv_mul
-- 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
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) ∂μ)
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
pos : 0 ≤ ‖x - x₀‖
pos₁ : b a * ‖x - x₀‖ ≤ b a * ‖x - x₀‖
pos₂ : 0 ≤ ‖x - x₀‖
pos₃ : 0 ≤ ‖F' a‖
pos₄ : ‖F' a‖ * ‖x - x₀‖ ≤ ‖F' a‖ * ‖x - x₀‖
⊢ b a * ‖x - x₀‖ / ‖x - x₀‖ + ‖F' a‖ * ‖x - x₀‖ / ‖x - x₀‖ ≤ b a + ‖F' a‖

Tactic:
apply_rules [add_le_add, div_le_of_le_mul₀]

Premises used: div_le_of_le_mul₀, add_le_add
-- 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
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) ∂μ)
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
⊢ 0 ≤ ‖x - x₀‖

Tactic:
positivity