awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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 : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v)) μ
have hf₁ : AEMeasurable (β := ℝ) (fun (x : E) ↦ f (x + t • v)) μ
Tactic: apply AEMeasurable.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ᵐ (a : E) ∂μ, ‖n⁻¹ • (f (a + n • v) - f a) * g a‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) a
have 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
Tactic: filter_upwards [Ioc_mem_nhdsGT zero_lt_one] with t ht
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (hypothesis)
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
⊢ ∀ᵐ (a : E) ∂μ, ‖t⁻¹ • (f (a + t • v) - f a) * g a‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) a
have t_pos : 0 < t
Tactic: have t_pos : 0 < t := ht.1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
⊢ ∀ᵐ (a : E) ∂μ, ‖t⁻¹ • (f (a + t • v) - f a) * g a‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) a
have h : ∀ (x : E), ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
⊢ ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x
have pos : ∀ (hx : x ∈ K), ‖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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
⊢ ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x
have neg : ∀ (hx : x ∉ K), ‖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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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⁻¹ * ((↑C : ℝ) * ‖x + t • v - x‖) * ‖g x‖
have hbc : ‖f (x + t • v) - f x‖ ≤ (↑C : ℝ) * ‖x + t • v - x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
⊢ (↑C : ℝ) * ‖v‖ * ‖g x‖ = K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x
have rw : (↑C : ℝ) * ‖v‖ * ‖g x‖ = (↑C : ℝ) * ‖v‖ * ‖g x‖
Tactic: rw [indicator_of_mem hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x
have calc : ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ = t⁻¹ * ‖f (x + t • v) - f x‖ * ‖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, 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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‖
⊢ ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x
have calc₁ : t⁻¹ * ‖f (x + t • v) - f x‖ * ‖g x‖ ≤ t⁻¹ * ((↑C : ℝ) * ‖x + t • v - x‖) * ‖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, 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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‖
⊢ ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x
have calc₂ : t⁻¹ * ((↑C : ℝ) * ‖x + t • v - 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, 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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‖
⊢ ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x
have calc₃ : (↑C : ℝ) * ‖v‖ * ‖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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
have rw : x ∉ Function.support f
Tactic: rw [← Function.notMem_support]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
⊢ x ∉ Function.support f
have contrapose : ∀ (hx : x ∈ Function.support f), x ∈ K
Tactic: contrapose hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (hypothesis)
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‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x
have A : f x = 0
Tactic: have A : f x = 0 := by
        rw [← Function.notMem_support]
        contrapose hx
        exact self_subset_cthickening _ (subset_tsupport _ hx)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
A : f x = 0
⊢ f (x + t • v) = 0
have rw : x + t • v ∉ Function.support f
Tactic: rw [← Function.notMem_support]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
A : f x = 0
⊢ x + t • v ∉ Function.support f
have contrapose : ∀ (hx : x + t • v ∈ Function.support f), x ∈ K
Tactic: contrapose hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
A : f x = 0
hx : x + t • v ∈ Function.support f
⊢ x ∈ K
have apply : dist x (x + t • v) ≤ ‖v‖
Tactic: apply mem_cthickening_of_dist_le _ _ (‖v‖) (tsupport f) (subset_tsupport _ hx)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
A : f x = 0
hx : x + t • v ∈ Function.support f
⊢ dist x (x + t • v) ≤ ‖v‖
have simp : t * ‖v‖ ≤ ‖v‖
Tactic: simp only [dist_eq_norm, sub_add_cancel_left, norm_neg, norm_smul, Real.norm_eq_abs,
          abs_of_nonneg t_pos.le]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (hypothesis)
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
A : f x = 0
⊢ ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x
have B : f (x + t • v) = 0
Tactic: have B : f (x + t • v) = 0 := by
        rw [← Function.notMem_support]
        contrapose hx
        apply mem_cthickening_of_dist_le _ _ (‖v‖) (tsupport f) (subset_tsupport _ hx)
        simp only [dist_eq_norm, sub_add_cancel_left, norm_neg, norm_smul, Real.norm_eq_abs,
          abs_of_nonneg t_pos.le]
        exact mul_le_of_le_one_left (norm_nonneg v) ht.2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
A : f x = 0
B : f (x + t • v) = 0
⊢ ‖t⁻¹ • (f (x + t • v) - f x) * g x‖ ≤ K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x
have neg : LE.le (α := ℝ) 0 (K.indicator (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) x)
Tactic: simp only [B, A, _root_.sub_self, smul_eq_mul, mul_zero, zero_mul, norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
⊢ Integrable (ε := ℝ) (K.indicator fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) μ
have bound_integrable : IntegrableOn (ε := ℝ) (fun (x : E) ↦ (↑C : ℝ) * ‖v‖ * ‖g x‖) K μ
Tactic: rw [integrable_indicator_iff K_compact.measurableSet]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
⊢ ∀ᵐ (a : E) ∂μ, Tendsto (fun (n : ℝ) ↦ n⁻¹ • (f (a + n • v) - f a) * g a) (𝓝[>] 0) (𝓝 (lineDeriv ℝ f a v * g a))
have 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))
Tactic: filter_upwards [hf.ae_lineDifferentiableAt v] with x hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
⊢ Eq (α := ℝ) (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ) (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ)
have 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: have A : Tendsto (fun (t : ℝ) ↦ ∫ x, (t⁻¹ • (f (x + t • v) - f x)) * g x ∂μ) (𝓝[>] 0)
              (𝓝 (∫ x, lineDeriv ℝ f x v * g x ∂μ)) :=
    integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul
      hf (hg.continuous.integrable_of_hasCompactSupport h'g) v
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
⊢ Eq (α := ℝ) (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ) (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ)
have B : Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
  (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
Tactic: have B : Tendsto (fun (t : ℝ) ↦ ∫ x, (t⁻¹ • (g (x + t • (-v)) - g x)) * f x ∂μ) (𝓝[>] 0)
              (𝓝 (∫ x, lineDeriv ℝ g x (-v) * f x ∂μ)) :=
    integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul' hg h'g hf.continuous (-v)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
S1 :
  ∀ (t : ℝ),
    Eq (α := ℝ) (∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ) (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ)
have A₁ : Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
  (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
Tactic: simp only [S1] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
⊢ Eq (α := ℝ) (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ) (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ)
have suffices : ∀ (t : ℝ),
  Eq (α := ℝ) (∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ)
Tactic: suffices S1 : ∀ (t : ℝ), ∫ x, (t⁻¹ • (f (x + t • v) - f x)) * g x ∂μ =
                            ∫ x, (t⁻¹ • (g (x + t • (-v)) - g x)) * f x ∂μ by
    simp only [S1] at A; exact tendsto_nhds_unique A B