awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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⁻¹ * ((↑C : ℝ) * ‖x + t • v - x‖) * ‖g x‖ = (↑C : ℝ) * ‖v‖ * ‖g x‖

Tactic:
simp [field, norm_smul, abs_of_nonneg ht.le]

Premises used: norm_smul, LT.lt.le, abs_of_nonneg
-- 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
calc : ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ = t⁻¹ * ‖f (x + t • v) - f x‖ * ‖g x‖
calc₁ : t⁻¹ * ‖f (x + t • v) - f x‖ * ‖g x‖ ≤ t⁻¹ * ((↑C : ℝ) * ‖x + t • v - x‖) * ‖g x‖
calc₂ : t⁻¹ * ((↑C : ℝ) * ‖x + t • v - x‖) * ‖g x‖ = (↑C : ℝ) * ‖v‖ * ‖g x‖
⊢ ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ (↑C : ℝ) * ‖v‖ * ‖g x‖

Tactic:
calc ‖t⁻¹ • (f (x + t • v) - f x) * g x‖
      = (t⁻¹ * ‖f (x + t • v) - f x‖) * ‖g x‖ := by simp [norm_mul, ht.le]
    _ ≤ (t⁻¹ * (C * ‖(x + t • v) - x‖)) * ‖g x‖ := by
      gcongr; exact LipschitzWith.norm_sub_le hf (x + t • v) x
    _ = (C * ‖v‖) * ‖g x‖ := by simp [field, norm_smul, abs_of_nonneg ht.le]

Premises used: Norm.norm, HMul.hMul, HSub.hSub, Inv.inv, HAdd.hAdd, HSMul.hSMul, 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
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) μ

Tactic:
hg.norm.const_mul _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.norm
-- 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
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) μ

Tactic:
exact hg.norm.const_mul _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.norm
-- 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 :
  ∀ (x : E) (hx : LineDifferentiableAt ℝ f x v),
    Tendsto (fun (n : ℝ) ↦ n⁻¹ • (f (x + n • v) - f x) * g x) (𝓝[>] 0) (𝓝 (lineDeriv ℝ f x v * g x))
⊢ ∀ᵐ (a : E) ∂μ, Tendsto (fun (n : ℝ) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) (𝓝[>] 0) (𝓝 (lineDeriv ℝ f a v * g a))

Tactic:
filter_upwards [hf.ae_lineDifferentiableAt v] with x hx

Premises used: LipschitzWith.ae_lineDifferentiableAt
-- 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 x : E
hx : LineDifferentiableAt ℝ f x v
⊢ Tendsto (fun (n : ℝ) ↦ n⁻¹ • (f (x + n • v) - f x) * g x) (𝓝[>] 0) (𝓝 (lineDeriv ℝ f x v * g x))

Tactic:
hx.hasLineDerivAt.tendsto_slope_zero_right.mul tendsto_const_nhds

Premises used: tendsto_const_nhds, HasLineDerivAt.tendsto_slope_zero_right, Filter.Tendsto.mul, LineDifferentiableAt.hasLineDerivAt
-- 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 x : E
hx : LineDifferentiableAt ℝ f x v
⊢ Tendsto (fun (n : ℝ) ↦ n⁻¹ • (f (x + n • v) - f x) * g x) (𝓝[>] 0) (𝓝 (lineDeriv ℝ f x v * g x))

Tactic:
exact hx.hasLineDerivAt.tendsto_slope_zero_right.mul tendsto_const_nhds

Premises used: tendsto_const_nhds, HasLineDerivAt.tendsto_slope_zero_right, Filter.Tendsto.mul, LineDifferentiableAt.hasLineDerivAt
-- 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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
⊢ IsCompact K

Tactic:
have K_compact : IsCompact K := IsCompact.cthickening h'f
-- 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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
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‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) a
bound_integrable : Integrable (ε := ℝ) (K.indicator 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
      (K.indicator (fun x ↦ (C * ‖v‖) * ‖g x‖))

Premises used: Norm.norm, HMul.hMul, Set.indicator, 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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
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: Continuous.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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
h :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t),
    ∀ᵐ (a : E) ∂μ, ‖t⁻¹ • (f (a + t • v) - f a) * g a‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) a
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ᵐ (a : E) ∂μ, ‖n⁻¹ • (f (a + n • v) - f a) * g a‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) a

Tactic:
filter_upwards [Ioc_mem_nhdsGT zero_lt_one] with t ht

Premises used: Ioc_mem_nhdsGT, zero_lt_one
-- 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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
⊢ 0 < t

Tactic:
have t_pos : 0 < t := ht.1
-- 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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
h : ∀ (x : E), ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x
⊢ ∀ᵐ (a : E) ∂μ, ‖t⁻¹ • (f (a + t • v) - f a) * g a‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) 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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
pos : ∀ (hx : x ∈ K), ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x
neg : ∀ (hx : x ∉ K), ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x
⊢ ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x

Tactic:
by_cases hx : x ∈ K
-- 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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∈ K
⊢ ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ = t⁻¹ * ‖f (x + t • v) - f x‖ * ‖g x‖

Tactic:
simp [norm_mul, t_pos.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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∈ K
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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∈ K
⊢ ‖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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∈ K
⊢ ‖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
-- 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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∈ K
⊢ t⁻¹ * ((↑C : ℝ) * ‖x + t • v - x‖) * ‖g x‖ = (↑C : ℝ) * ‖v‖ * ‖g x‖

Tactic:
simp [field, norm_smul, abs_of_nonneg t_pos.le]

Premises used: norm_smul, LT.lt.le, abs_of_nonneg
-- 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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∈ K
rw rw₁ : (↑C : ℝ) * ‖v‖ * ‖g x‖ = (↑C : ℝ) * ‖v‖ * ‖g x‖
⊢ (↑C : ℝ) * ‖v‖ * ‖g x‖ = K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x

Tactic:
rw [indicator_of_mem hx]

Premises used: Set.indicator_of_mem
-- 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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∈ K
calc : ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ = t⁻¹ * ‖f (x + t • v) - f x‖ * ‖g x‖
calc₁ : t⁻¹ * ‖f (x + t • v) - f x‖ * ‖g x‖ ≤ t⁻¹ * ((↑C : ℝ) * ‖x + t • v - x‖) * ‖g x‖
calc₂ : t⁻¹ * ((↑C : ℝ) * ‖x + t • v - x‖) * ‖g x‖ = (↑C : ℝ) * ‖v‖ * ‖g x‖
calc₃ : (↑C : ℝ) * ‖v‖ * ‖g x‖ = K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x
⊢ ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x

Tactic:
calc ‖t⁻¹ • (f (x + t • v) - f x) * g x‖
        = (t⁻¹ * ‖f (x + t • v) - f x‖) * ‖g x‖ := by simp [norm_mul, t_pos.le]
      _ ≤ (t⁻¹ * (C * ‖(x + t • v) - x‖)) * ‖g x‖ := by
        gcongr; exact LipschitzWith.norm_sub_le hf (x + t • v) x
      _ = (C * ‖v‖) * ‖g x‖ := by simp [field, norm_smul, abs_of_nonneg t_pos.le]
      _ = K.indicator (fun x ↦ (C * ‖v‖) * ‖g x‖) x := by rw [indicator_of_mem hx]

Premises used: Norm.norm, HMul.hMul, Set.indicator, HSub.hSub, Inv.inv, HAdd.hAdd, HSMul.hSMul, 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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∉ K
rw : x ∉ Function.support f
⊢ f x = 0

Tactic:
rw [← Function.notMem_support]

Premises used: Function.notMem_support
-- 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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∉ K
contrapose : ∀ (hx : x ∈ Function.support f), x ∈ K
⊢ x ∉ Function.support f

Tactic:
contrapose hx
-- 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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∈ Function.support f
⊢ x ∈ K

Tactic:
self_subset_cthickening _ (subset_tsupport _ hx)

Premises used: Set.Mem, subset_tsupport, Metric.self_subset_cthickening
-- 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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∈ Function.support f
⊢ x ∈ K

Tactic:
exact self_subset_cthickening _ (subset_tsupport _ hx)

Premises used: subset_tsupport, Metric.self_subset_cthickening
-- 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
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
t_pos : 0 < t
x : E
hx : x ∉ K
⊢ f x = 0

Tactic:
have A : f x = 0 := by
        rw [← Function.notMem_support]
        contrapose hx
        exact self_subset_cthickening _ (subset_tsupport _ hx)