awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a b : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) 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 : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ s, ‖F' x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x t) (F' x t) x
h_bound₁ : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
⊢ IntervalIntegrable bound μ a b

Tactic:
rw [← ae_restrict_iff' measurableSet_uIoc] at h_bound 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
a b : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) 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 : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ s, ‖F' x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) ↦ F x t) (F' x t) x
h_bound₁ : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable₁ : IntervalIntegrable bound μ a b
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, HasDerivAt (fun (x_2 : 𝕜) ↦ F x_2 x) (F' x_1 x) x_1

Tactic:
rw [← ae_restrict_iff' measurableSet_uIoc] at h_bound 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
a b : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) 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 (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, HasDerivAt (fun (x_2 : 𝕜) ↦ F x_2 x) (F' x_1 x) x_1
simp :
  ∀ (hF_int : IntegrableOn (F x₀) (Ι a b) μ) (bound_integrable : IntegrableOn bound (Ι a b) μ),
    IntegrableOn (F' x₀) (Ι a b) μ ∧
      HasDerivAt.{u_1, u_2} (F := E) (fun (x : 𝕜) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
⊢ IntervalIntegrable (F' x₀) μ a b ∧
    HasDerivAt.{u_1, u_2} (F := E) (fun (x : 𝕜) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀

Tactic:
simp only [intervalIntegrable_iff] at hF_int bound_integrable ⊢

Premises used: intervalIntegrable_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
a b : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, HasDerivAt (fun (x_2 : 𝕜) ↦ F x_2 x) (F' x_1 x) x_1
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
simp :
  IntegrableOn (F' x₀) (Ι a b) μ ∧
    HasDerivAt (fun (x : 𝕜) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F x t ∂μ))
      (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F' x₀ t ∂μ)) x₀
⊢ IntegrableOn (F' x₀) (Ι a b) μ ∧
    HasDerivAt.{u_1, u_2} (F := E) (fun (x : 𝕜) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀

Tactic:
simp only [intervalIntegral_eq_integral_uIoc]

Premises used: intervalIntegral.intervalIntegral_eq_integral_uIoc
-- 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
a b : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, HasDerivAt (fun (x_2 : 𝕜) ↦ F x_2 x) (F' x_1 x) x_1
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
⊢ Integrable (F' x₀) (μ.restrict (Ι a b)) ∧
    HasDerivAt.{u_1, u_2} (F := E) (fun (n : 𝕜) ↦ ∫ (a : ℝ) in Ι a b, F n a ∂μ) (∫ (a : ℝ) in Ι a b, F' x₀ a ∂μ) x₀

Tactic:
have := hasDerivAt_integral_of_dominated_loc_of_deriv_le hs hF_meas hF_int hF'_meas h_bound
    bound_integrable h_diff
-- 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
a b : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, HasDerivAt (fun (x_2 : 𝕜) ↦ F x_2 x) (F' x_1 x) x_1
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
this :
  Integrable (F' x₀) (μ.restrict (Ι a b)) ∧
    HasDerivAt.{u_1, u_2} (F := E) (fun (n : 𝕜) ↦ ∫ (a : ℝ) in Ι a b, F n a ∂μ) (∫ (a : ℝ) in Ι a b, F' x₀ a ∂μ) x₀
⊢ IntegrableOn (F' x₀) (Ι a b) μ ∧
    HasDerivAt (fun (x : 𝕜) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F x t ∂μ))
      (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F' x₀ t ∂μ)) x₀

Tactic:
⟨this.1, this.2.const_smul _⟩

Premises used: HasDerivAt.const_smul, And.right, And.left, And.intro
-- 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
a b : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ s, HasDerivAt (fun (x_2 : 𝕜) ↦ F x_2 x) (F' x_1 x) x_1
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
this :
  Integrable (F' x₀) (μ.restrict (Ι a b)) ∧
    HasDerivAt.{u_1, u_2} (F := E) (fun (n : 𝕜) ↦ ∫ (a : ℝ) in Ι a b, F n a ∂μ) (∫ (a : ℝ) in Ι a b, F' x₀ a ∂μ) x₀
⊢ IntegrableOn (F' x₀) (Ι a b) μ ∧
    HasDerivAt (fun (x : 𝕜) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F x t ∂μ))
      (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F' x₀ t ∂μ)) x₀

Tactic:
exact ⟨this.1, this.2.const_smul _⟩
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
hf : LipschitzWith C f
v : E
⊢ MemLp (ε := ℝ) (fun (x : E) ↦ lineDeriv ℝ f x v) ∞ μ

Tactic:
memLp_top_of_bound (aestronglyMeasurable_lineDeriv hf.continuous μ)
    (C * ‖v‖) (.of_forall fun _x ↦ norm_lineDeriv_le_of_lipschitz ℝ hf)

Premises used: Norm.norm, MeasureTheory.memLp_top_of_bound, Real, HMul.hMul, aestronglyMeasurable_lineDeriv, norm_lineDeriv_le_of_lipschitz, Filter.Eventually.of_forall, LipschitzWith.continuous, NNReal.toReal
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (S := ℝ) 1 v
suffices : ∀ (p : E), ∀ᵐ (t : ℝ), LineDifferentiableAt ℝ f (p + t • v) v
⊢ ∀ᵐ (p : E) ∂μ, LineDifferentiableAt ℝ f p v

Tactic:
suffices A : ∀ p, ∀ᵐ (t : ℝ) ∂volume, LineDifferentiableAt ℝ f (p + t • v) v from
    ae_mem_of_ae_add_linearMap_mem L.toLinearMap volume μ
      (measurableSet_lineDifferentiableAt hf.continuous) A
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (S := ℝ) 1 v
p : E
⊢ ∀ᵐ (s : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s

Tactic:
have : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (fun t ↦ f (p + t • v)) s :=
    (hf.comp ((LipschitzWith.const p).add L.lipschitz)).ae_differentiableAt_real
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (S := ℝ) 1 v
p : E
this : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
h : ∀ (s : ℝ) (hs : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s), LineDifferentiableAt ℝ f (p + s • v) v
⊢ ∀ᵐ (t : ℝ), LineDifferentiableAt ℝ f (p + t • v) v

Tactic:
filter_upwards [this] with s hs
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (S := ℝ) 1 v
p : E
this : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
s : ℝ
hs : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
⊢ DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) (s + 0)

Tactic:
simpa using hs
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (S := ℝ) 1 v
p : E
this : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
s : ℝ
hs : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
⊢ DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) (s + 0)

Tactic:
have h's : DifferentiableAt ℝ (fun t ↦ f (p + t • v)) (s + 0) := by simpa using hs
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (S := ℝ) 1 v
p : E
this : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
s : ℝ
hs : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
h's : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) (s + 0)
⊢ DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ s + t) 0

Tactic:
have : DifferentiableAt ℝ (fun t ↦ s + t) 0 := differentiableAt_id.const_add _
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (S := ℝ) 1 v
p : E
this_1 : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
s : ℝ
hs : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
h's : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) (s + 0)
this : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ s + t) 0
⊢ DifferentiableAt ℝ (E := ℝ) (F := ℝ) ((fun (t : ℝ) ↦ f (p + t • v)) ∘ HAdd.hAdd s) 0

Tactic:
h's.comp 0 this

Premises used: DifferentiableAt.comp, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (S := ℝ) 1 v
p : E
this_1 : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
s : ℝ
hs : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
h's : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) (s + 0)
this : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ s + t) 0
h : ∀ (t : ℝ), f (p + s • v + t • v) = ((fun (t : ℝ) ↦ f (p + t • v)) ∘ HAdd.hAdd s) t
⊢ DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + s • v + t • v)) 0

Tactic:
convert! h's.comp 0 this with _ t

Premises used: DifferentiableAt.comp, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (S := ℝ) 1 v
p : E
this_1 : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
s : ℝ
hs : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) s
h's : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ f (p + t • v)) (s + 0)
this : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ s + t) 0
t : ℝ
⊢ f (p + s • v + t • v) = ((fun (t : ℝ) ↦ f (p + t • v)) ∘ HAdd.hAdd s) t

Tactic:
simp only [add_assoc, Function.comp_apply, add_smul]

Premises used: add_assoc, add_smul, Function.comp_apply
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
⊢ LocallyIntegrable (ε := ℝ) (fun (x : E) ↦ lineDeriv ℝ f x v) μ

Tactic:
(hf.memLp_lineDeriv v).locallyIntegrable le_top

Premises used: MeasureTheory.MemLp.locallyIntegrable, LipschitzWith.memLp_lineDeriv, le_top
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
hF_meas : ∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) μ
h_bound : ∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ᵐ (a : E) ∂μ, ‖n⁻¹ • (f (a + n • v) - f a) * g a‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g a‖
bound_integrable : Integrable (ε := ℝ) (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) μ
h_lim : ∀ᵐ (a : E) ∂μ, Tendsto (fun (n : ℝ) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) (𝓝[>] 0) (𝓝 (lineDeriv ℝ f a v * g a))
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))

Tactic:
apply tendsto_integral_filter_of_dominated_convergence (fun x ↦ (C * ‖v‖) * ‖g x‖)

Premises used: Norm.norm, HMul.hMul, MeasureTheory.tendsto_integral_filter_of_dominated_convergence, NNReal.toReal
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
hF_meas : ∀ (t : ℝ), AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ t⁻¹ • (f (a + t • v) - f a) * g a) μ
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) μ

Tactic:
filter_upwards with t
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
apply : AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ t⁻¹ • (f (a + t • v) - f a)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ t⁻¹ • (f (a + t • v) - f a) * g a) μ

Tactic:
apply AEStronglyMeasurable.mul ?_ hg.aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
apply : AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v) - f x) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : E) ↦ t⁻¹ • (f (a + t • v) - f a)) μ

Tactic:
apply aestronglyMeasurable_const.smul

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.AEStronglyMeasurable.smul
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
apply : AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v) - f x) μ

Tactic:
apply AEStronglyMeasurable.sub _ hf.continuous.measurable.aestronglyMeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.sub, Measurable.aestronglyMeasurable, LipschitzWith.continuous, Continuous.measurable
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
hf₁ : AEMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v)) μ

Tactic:
apply AEMeasurable.aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
⊢ AEMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v)) μ

Tactic:
hf.continuous.measurable.comp_aemeasurable' (aemeasurable_id'.add_const _)

Premises used: AEMeasurable.add_const, Measurable.comp_aemeasurable', LipschitzWith.continuous, aemeasurable_id', Continuous.measurable
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
⊢ AEMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v)) μ

Tactic:
exact hf.continuous.measurable.comp_aemeasurable' (aemeasurable_id'.add_const _)

Premises used: AEMeasurable.add_const, Measurable.comp_aemeasurable', LipschitzWith.continuous, aemeasurable_id', Continuous.measurable
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
h : ∀ (ht : 0 < t), ∀ᵐ (a : E) ∂μ, ‖t⁻¹ • (f (a + t • v) - f a) * g a‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g a‖
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) t → ∀ᵐ (a : E) ∂μ, ‖t⁻¹ • (f (a + t • v) - f a) * g a‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g a‖

Tactic:
(ht : 0 < t)
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
h : ∀ (t : ℝ) (ht : 0 < t), ∀ᵐ (a : E) ∂μ, ‖t⁻¹ • (f (a + t • v) - f a) * g a‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g a‖
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ᵐ (a : E) ∂μ, ‖n⁻¹ • (f (a + n • v) - f a) * g a‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g a‖

Tactic:
filter_upwards [self_mem_nhdsWithin] with t (ht : 0 < t)

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
ht : 0 < t
h : ∀ (x : E), ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g x‖
⊢ ∀ᵐ (a : E) ∂μ, ‖t⁻¹ • (f (a + t • v) - f a) * g a‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g a‖

Tactic:
filter_upwards with x
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
ht : 0 < t
x : E
⊢ ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ = t⁻¹ * ‖f (x + t • v) - f x‖ * ‖g x‖

Tactic:
simp [norm_mul, ht.le]

Premises used: LT.lt.le, norm_mul
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
ht : 0 < t
x : E
hbc : ‖f (x + t • v) - f x‖ ≤ (↑C : ℝ) * ‖x + t • v - x‖
⊢ t⁻¹ * ‖f (x + t • v) - f x‖ * ‖g x‖ ≤ t⁻¹ * ((↑C : ℝ) * ‖x + t • v - x‖) * ‖g x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
ht : 0 < t
x : E
⊢ ‖f (x + t • v) - f x‖ ≤ (↑C : ℝ) * ‖x + t • v - x‖

Tactic:
LipschitzWith.norm_sub_le hf (x + t • v) x

Premises used: LipschitzWith.norm_sub_le, HAdd.hAdd, HSMul.hSMul
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
ht : 0 < t
x : E
⊢ ‖f (x + t • v) - f x‖ ≤ (↑C : ℝ) * ‖x + t • v - x‖

Tactic:
exact LipschitzWith.norm_sub_le hf (x + t • v) x

Premises used: LipschitzWith.norm_sub_le, HAdd.hAdd, HSMul.hSMul