internlm/Lean-Github huggingface dataset:
Theorem: W21_approximation
Proof state before:
case hp.refine_2.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : W21
g : trunc
f' : W1 1 ℂ := W1.deriv f
f'' : W1 0 ℂ := f'.deriv
g' : CS 1 ℝ := g.deriv
g'' : CS 0 ℝ := g'.deriv
h : ℝ → ℝ → ℝ := fun R v => 1 - (g.scale R).toFun v
h' : ℝ → CS 1 ℝ := fun R => -(g.scale R).deriv
h'' : ℝ → CS 0 ℝ := fun R => -(g.scale R).deriv.deriv
ch : ∀ {R : ℝ}, Continuous fun v => ↑(h R v)
ch' : ∀ {R : ℝ}, Continuous fun v => ↑((h' R).toFun v)
ch'' : ∀ {R : ℝ}, Continuous fun v => ↑((h'' R).toFun v)
dh : ∀ (R v : ℝ), HasDerivAt (h R) ((h' R).toFun v) v
dh' : ∀ (R v : ℝ), HasDerivAt (h' R).toFun ((h'' R).toFun v) v
hh1 : ∀ (R v : ℝ), |h R v| ≤ 1
vR : ∀ (v : ℝ), Tendsto (fun R => v * R⁻¹) atTop (𝓝 0)
F : ℝ → ℝ → ℝ :=
  fun R v => ‖↑((h'' R).toFun v) * f.toFun v + 2 * ↑((h' R).toFun v) * f'.toFun v + ↑(h R v) * f''.toFun v‖
c1 : ℝ
mg' : ∀ (v : ℝ), ‖g'.toFun v‖ ≤ c1
c2 : ℝ
mg'' : ∀ (v : ℝ), ‖g''.toFun v‖ ≤ c2
bound : ℝ → ℝ := fun v => c2 * ‖f.toFun v‖ + 2 * c1 * ‖f'.toFun v‖ + ‖f''.toFun v‖
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (R : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a
e3 : Integrable bound volume
v : ℝ
evg' : g'.toFun =ᶠ[𝓝 0] 0
evg'' : g''.toFun =ᶠ[𝓝 0] 0
eh' : ∀ (v : ℝ), ∀ᶠ (R : ℝ) in atTop, (h' R).toFun v = 0
⊢ ∀ᶠ (x' : ℝ) in atTop, 2 * ↑((h' x').toFun v) * f'.toFun v = 0
Tactic:
filter_upwards [eh' v] with R hR
Proof state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : W21
g : trunc
f' : W1 1 ℂ := W1.deriv f
f'' : W1 0 ℂ := f'.deriv
g' : CS 1 ℝ := g.deriv
g'' : CS 0 ℝ := g'.deriv
h : ℝ → ℝ → ℝ := fun R v => 1 - (g.scale R).toFun v
h' : ℝ → CS 1 ℝ := fun R => -(g.scale R).deriv
h'' : ℝ → CS 0 ℝ := fun R => -(g.scale R).deriv.deriv
ch : ∀ {R : ℝ}, Continuous fun v => ↑(h R v)
ch' : ∀ {R : ℝ}, Continuous fun v => ↑((h' R).toFun v)
ch'' : ∀ {R : ℝ}, Continuous fun v => ↑((h'' R).toFun v)
dh : ∀ (R v : ℝ), HasDerivAt (h R) ((h' R).toFun v) v
dh' : ∀ (R v : ℝ), HasDerivAt (h' R).toFun ((h'' R).toFun v) v
hh1 : ∀ (R v : ℝ), |h R v| ≤ 1
vR : ∀ (v : ℝ), Tendsto (fun R => v * R⁻¹) atTop (𝓝 0)
F : ℝ → ℝ → ℝ :=
  fun R v => ‖↑((h'' R).toFun v) * f.toFun v + 2 * ↑((h' R).toFun v) * f'.toFun v + ↑(h R v) * f''.toFun v‖
c1 : ℝ
mg' : ∀ (v : ℝ), ‖g'.toFun v‖ ≤ c1
c2 : ℝ
mg'' : ∀ (v : ℝ), ‖g''.toFun v‖ ≤ c2
bound : ℝ → ℝ := fun v => c2 * ‖f.toFun v‖ + 2 * c1 * ‖f'.toFun v‖ + ‖f''.toFun v‖
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (R : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a
e3 : Integrable bound volume
v : ℝ
evg' : g'.toFun =ᶠ[𝓝 0] 0
evg'' : g''.toFun =ᶠ[𝓝 0] 0
eh' : ∀ (v : ℝ), ∀ᶠ (R : ℝ) in atTop, (h' R).toFun v = 0
R : ℝ
hR : (h' R).toFun v = 0
⊢ 2 * ↑((h' R).toFun v) * f'.toFun v = 0
Theorem: W21_approximation
Proof state before:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : W21
g : trunc
f' : W1 1 ℂ := W1.deriv f
f'' : W1 0 ℂ := f'.deriv
g' : CS 1 ℝ := g.deriv
g'' : CS 0 ℝ := g'.deriv
h : ℝ → ℝ → ℝ := fun R v => 1 - (g.scale R).toFun v
h' : ℝ → CS 1 ℝ := fun R => -(g.scale R).deriv
h'' : ℝ → CS 0 ℝ := fun R => -(g.scale R).deriv.deriv
ch : ∀ {R : ℝ}, Continuous fun v => ↑(h R v)
ch' : ∀ {R : ℝ}, Continuous fun v => ↑((h' R).toFun v)
ch'' : ∀ {R : ℝ}, Continuous fun v => ↑((h'' R).toFun v)
dh : ∀ (R v : ℝ), HasDerivAt (h R) ((h' R).toFun v) v
dh' : ∀ (R v : ℝ), HasDerivAt (h' R).toFun ((h'' R).toFun v) v
hh1 : ∀ (R v : ℝ), |h R v| ≤ 1
vR : ∀ (v : ℝ), Tendsto (fun R => v * R⁻¹) atTop (𝓝 0)
F : ℝ → ℝ → ℝ :=
  fun R v => ‖↑((h'' R).toFun v) * f.toFun v + 2 * ↑((h' R).toFun v) * f'.toFun v + ↑(h R v) * f''.toFun v‖
c1 : ℝ
mg' : ∀ (v : ℝ), ‖g'.toFun v‖ ≤ c1
c2 : ℝ
mg'' : ∀ (v : ℝ), ‖g''.toFun v‖ ≤ c2
bound : ℝ → ℝ := fun v => c2 * ‖f.toFun v‖ + 2 * c1 * ‖f'.toFun v‖ + ‖f''.toFun v‖
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (R : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a
e3 : Integrable bound volume
v : ℝ
evg' : g'.toFun =ᶠ[𝓝 0] 0
evg'' : g''.toFun =ᶠ[𝓝 0] 0
eh' : ∀ (v : ℝ), ∀ᶠ (R : ℝ) in atTop, (h' R).toFun v = 0
R : ℝ
hR : (h' R).toFun v = 0
⊢ 2 * ↑((h' R).toFun v) * f'.toFun v = 0
Tactic:
simp [hR]
Proof state after:
no goals
Theorem: W21_approximation
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : W21
g : trunc
f' : W1 1 ℂ := W1.deriv f
f'' : W1 0 ℂ := f'.deriv
g' : CS 1 ℝ := g.deriv
g'' : CS 0 ℝ := g'.deriv
h : ℝ → ℝ → ℝ := fun R v => 1 - (g.scale R).toFun v
h' : ℝ → CS 1 ℝ := fun R => -(g.scale R).deriv
h'' : ℝ → CS 0 ℝ := fun R => -(g.scale R).deriv.deriv
ch : ∀ {R : ℝ}, Continuous fun v => ↑(h R v)
ch' : ∀ {R : ℝ}, Continuous fun v => ↑((h' R).toFun v)
ch'' : ∀ {R : ℝ}, Continuous fun v => ↑((h'' R).toFun v)
dh : ∀ (R v : ℝ), HasDerivAt (h R) ((h' R).toFun v) v
dh' : ∀ (R v : ℝ), HasDerivAt (h' R).toFun ((h'' R).toFun v) v
hh1 : ∀ (R v : ℝ), |h R v| ≤ 1
vR : ∀ (v : ℝ), Tendsto (fun R => v * R⁻¹) atTop (𝓝 0)
F : ℝ → ℝ → ℝ :=
  fun R v => ‖↑((h'' R).toFun v) * f.toFun v + 2 * ↑((h' R).toFun v) * f'.toFun v + ↑(h R v) * f''.toFun v‖
c1 : ℝ
mg' : ∀ (v : ℝ), ‖g'.toFun v‖ ≤ c1
c2 : ℝ
mg'' : ∀ (v : ℝ), ‖g''.toFun v‖ ≤ c2
bound : ℝ → ℝ := fun v => c2 * ‖f.toFun v‖ + 2 * c1 * ‖f'.toFun v‖ + ‖f''.toFun v‖
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (R : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a
e3 : Integrable bound volume
v✝ : ℝ
evg' : g'.toFun =ᶠ[𝓝 0] 0
evg'' : g''.toFun =ᶠ[𝓝 0] 0
v : ℝ
⊢ ∀ᶠ (R : ℝ) in atTop, (h' R).toFun v = 0
Tactic:
filter_upwards [(vR v).eventually evg'] with R hR
Proof state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : W21
g : trunc
f' : W1 1 ℂ := W1.deriv f
f'' : W1 0 ℂ := f'.deriv
g' : CS 1 ℝ := g.deriv
g'' : CS 0 ℝ := g'.deriv
h : ℝ → ℝ → ℝ := fun R v => 1 - (g.scale R).toFun v
h' : ℝ → CS 1 ℝ := fun R => -(g.scale R).deriv
h'' : ℝ → CS 0 ℝ := fun R => -(g.scale R).deriv.deriv
ch : ∀ {R : ℝ}, Continuous fun v => ↑(h R v)
ch' : ∀ {R : ℝ}, Continuous fun v => ↑((h' R).toFun v)
ch'' : ∀ {R : ℝ}, Continuous fun v => ↑((h'' R).toFun v)
dh : ∀ (R v : ℝ), HasDerivAt (h R) ((h' R).toFun v) v
dh' : ∀ (R v : ℝ), HasDerivAt (h' R).toFun ((h'' R).toFun v) v
hh1 : ∀ (R v : ℝ), |h R v| ≤ 1
vR : ∀ (v : ℝ), Tendsto (fun R => v * R⁻¹) atTop (𝓝 0)
F : ℝ → ℝ → ℝ :=
  fun R v => ‖↑((h'' R).toFun v) * f.toFun v + 2 * ↑((h' R).toFun v) * f'.toFun v + ↑(h R v) * f''.toFun v‖
c1 : ℝ
mg' : ∀ (v : ℝ), ‖g'.toFun v‖ ≤ c1
c2 : ℝ
mg'' : ∀ (v : ℝ), ‖g''.toFun v‖ ≤ c2
bound : ℝ → ℝ := fun v => c2 * ‖f.toFun v‖ + 2 * c1 * ‖f'.toFun v‖ + ‖f''.toFun v‖
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (R : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a
e3 : Integrable bound volume
v✝ : ℝ
evg' : g'.toFun =ᶠ[𝓝 0] 0
evg'' : g''.toFun =ᶠ[𝓝 0] 0
v R : ℝ
hR : g'.toFun (v * R⁻¹) = OfNat.ofNat 0 (v * R⁻¹)
⊢ (h' R).toFun v = 0
Theorem: W21_approximation
Proof state before:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : W21
g : trunc
f' : W1 1 ℂ := W1.deriv f
f'' : W1 0 ℂ := f'.deriv
g' : CS 1 ℝ := g.deriv
g'' : CS 0 ℝ := g'.deriv
h : ℝ → ℝ → ℝ := fun R v => 1 - (g.scale R).toFun v
h' : ℝ → CS 1 ℝ := fun R => -(g.scale R).deriv
h'' : ℝ → CS 0 ℝ := fun R => -(g.scale R).deriv.deriv
ch : ∀ {R : ℝ}, Continuous fun v => ↑(h R v)
ch' : ∀ {R : ℝ}, Continuous fun v => ↑((h' R).toFun v)
ch'' : ∀ {R : ℝ}, Continuous fun v => ↑((h'' R).toFun v)
dh : ∀ (R v : ℝ), HasDerivAt (h R) ((h' R).toFun v) v
dh' : ∀ (R v : ℝ), HasDerivAt (h' R).toFun ((h'' R).toFun v) v
hh1 : ∀ (R v : ℝ), |h R v| ≤ 1
vR : ∀ (v : ℝ), Tendsto (fun R => v * R⁻¹) atTop (𝓝 0)
F : ℝ → ℝ → ℝ :=
  fun R v => ‖↑((h'' R).toFun v) * f.toFun v + 2 * ↑((h' R).toFun v) * f'.toFun v + ↑(h R v) * f''.toFun v‖
c1 : ℝ
mg' : ∀ (v : ℝ), ‖g'.toFun v‖ ≤ c1
c2 : ℝ
mg'' : ∀ (v : ℝ), ‖g''.toFun v‖ ≤ c2
bound : ℝ → ℝ := fun v => c2 * ‖f.toFun v‖ + 2 * c1 * ‖f'.toFun v‖ + ‖f''.toFun v‖
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (R : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a
e3 : Integrable bound volume
v✝ : ℝ
evg' : g'.toFun =ᶠ[𝓝 0] 0
evg'' : g''.toFun =ᶠ[𝓝 0] 0
v R : ℝ
hR : g'.toFun (v * R⁻¹) = OfNat.ofNat 0 (v * R⁻¹)
⊢ (h' R).toFun v = 0
Tactic:
simp [g'] at hR
Proof state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : W21
g : trunc
f' : W1 1 ℂ := W1.deriv f
f'' : W1 0 ℂ := f'.deriv
g' : CS 1 ℝ := g.deriv
g'' : CS 0 ℝ := g'.deriv
h : ℝ → ℝ → ℝ := fun R v => 1 - (g.scale R).toFun v
h' : ℝ → CS 1 ℝ := fun R => -(g.scale R).deriv
h'' : ℝ → CS 0 ℝ := fun R => -(g.scale R).deriv.deriv
ch : ∀ {R : ℝ}, Continuous fun v => ↑(h R v)
ch' : ∀ {R : ℝ}, Continuous fun v => ↑((h' R).toFun v)
ch'' : ∀ {R : ℝ}, Continuous fun v => ↑((h'' R).toFun v)
dh : ∀ (R v : ℝ), HasDerivAt (h R) ((h' R).toFun v) v
dh' : ∀ (R v : ℝ), HasDerivAt (h' R).toFun ((h'' R).toFun v) v
hh1 : ∀ (R v : ℝ), |h R v| ≤ 1
vR : ∀ (v : ℝ), Tendsto (fun R => v * R⁻¹) atTop (𝓝 0)
F : ℝ → ℝ → ℝ :=
  fun R v => ‖↑((h'' R).toFun v) * f.toFun v + 2 * ↑((h' R).toFun v) * f'.toFun v + ↑(h R v) * f''.toFun v‖
c1 : ℝ
mg' : ∀ (v : ℝ), ‖g'.toFun v‖ ≤ c1
c2 : ℝ
mg'' : ∀ (v : ℝ), ‖g''.toFun v‖ ≤ c2
bound : ℝ → ℝ := fun v => c2 * ‖f.toFun v‖ + 2 * c1 * ‖f'.toFun v‖ + ‖f''.toFun v‖
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (R : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a
e3 : Integrable bound volume
v✝ : ℝ
evg' : g'.toFun =ᶠ[𝓝 0] 0
evg'' : g''.toFun =ᶠ[𝓝 0] 0
v R : ℝ
hR : g.deriv.toFun (v * R⁻¹) = 0
⊢ (h' R).toFun v = 0
Theorem: W21_approximation
Proof state before:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : W21
g : trunc
f' : W1 1 ℂ := W1.deriv f
f'' : W1 0 ℂ := f'.deriv
g' : CS 1 ℝ := g.deriv
g'' : CS 0 ℝ := g'.deriv
h : ℝ → ℝ → ℝ := fun R v => 1 - (g.scale R).toFun v
h' : ℝ → CS 1 ℝ := fun R => -(g.scale R).deriv
h'' : ℝ → CS 0 ℝ := fun R => -(g.scale R).deriv.deriv
ch : ∀ {R : ℝ}, Continuous fun v => ↑(h R v)
ch' : ∀ {R : ℝ}, Continuous fun v => ↑((h' R).toFun v)
ch'' : ∀ {R : ℝ}, Continuous fun v => ↑((h'' R).toFun v)
dh : ∀ (R v : ℝ), HasDerivAt (h R) ((h' R).toFun v) v
dh' : ∀ (R v : ℝ), HasDerivAt (h' R).toFun ((h'' R).toFun v) v
hh1 : ∀ (R v : ℝ), |h R v| ≤ 1
vR : ∀ (v : ℝ), Tendsto (fun R => v * R⁻¹) atTop (𝓝 0)
F : ℝ → ℝ → ℝ :=
  fun R v => ‖↑((h'' R).toFun v) * f.toFun v + 2 * ↑((h' R).toFun v) * f'.toFun v + ↑(h R v) * f''.toFun v‖
c1 : ℝ
mg' : ∀ (v : ℝ), ‖g'.toFun v‖ ≤ c1
c2 : ℝ
mg'' : ∀ (v : ℝ), ‖g''.toFun v‖ ≤ c2
bound : ℝ → ℝ := fun v => c2 * ‖f.toFun v‖ + 2 * c1 * ‖f'.toFun v‖ + ‖f''.toFun v‖
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (R : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a
e3 : Integrable bound volume
v✝ : ℝ
evg' : g'.toFun =ᶠ[𝓝 0] 0
evg'' : g''.toFun =ᶠ[𝓝 0] 0
v R : ℝ
hR : g.deriv.toFun (v * R⁻¹) = 0
⊢ (h' R).toFun v = 0
Tactic:
simp [h', CS.deriv_scale', mul_comm R⁻¹, hR]
Proof state after:
no goals
Theorem: W21_approximation
Proof state before:
case hp.refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : W21
g : trunc
f' : W1 1 ℂ := W1.deriv f
f'' : W1 0 ℂ := f'.deriv
g' : CS 1 ℝ := g.deriv
g'' : CS 0 ℝ := g'.deriv
h : ℝ → ℝ → ℝ := fun R v => 1 - (g.scale R).toFun v
h' : ℝ → CS 1 ℝ := fun R => -(g.scale R).deriv
h'' : ℝ → CS 0 ℝ := fun R => -(g.scale R).deriv.deriv
ch : ∀ {R : ℝ}, Continuous fun v => ↑(h R v)
ch' : ∀ {R : ℝ}, Continuous fun v => ↑((h' R).toFun v)
ch'' : ∀ {R : ℝ}, Continuous fun v => ↑((h'' R).toFun v)
dh : ∀ (R v : ℝ), HasDerivAt (h R) ((h' R).toFun v) v
dh' : ∀ (R v : ℝ), HasDerivAt (h' R).toFun ((h'' R).toFun v) v
hh1 : ∀ (R v : ℝ), |h R v| ≤ 1
vR : ∀ (v : ℝ), Tendsto (fun R => v * R⁻¹) atTop (𝓝 0)
F : ℝ → ℝ → ℝ :=
  fun R v => ‖↑((h'' R).toFun v) * f.toFun v + 2 * ↑((h' R).toFun v) * f'.toFun v + ↑(h R v) * f''.toFun v‖
c1 : ℝ
mg' : ∀ (v : ℝ), ‖g'.toFun v‖ ≤ c1
c2 : ℝ
mg'' : ∀ (v : ℝ), ‖g''.toFun v‖ ≤ c2
bound : ℝ → ℝ := fun v => c2 * ‖f.toFun v‖ + 2 * c1 * ‖f'.toFun v‖ + ‖f''.toFun v‖
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (R : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a
e3 : Integrable bound volume
v : ℝ
evg' : g'.toFun =ᶠ[𝓝 0] 0
evg'' : g''.toFun =ᶠ[𝓝 0] 0
⊢ atTop.ZeroAtFilter fun n => ↑(h n v) * f''.toFun v
Tactic:
simpa [h] using ((g.tendsto_scale v).const_sub 1).ofReal.mul tendsto_const_nhds
Proof state after:
no goals
Theorem: Mathlib.Tactic.RPowRing.atom_pf
Proof state before:
a : ℝ
⊢ a = a * 1
Tactic:
simp
Proof state after:
no goals
Theorem: Mathlib.Tactic.RPowRing.atom_pf'
Proof state before:
a a' : ℝ
p : a = a'
⊢ a = a * 1
Tactic:
simp [*]
Proof state after:
no goals
Theorem: Mathlib.Tactic.RPowRing.atom_pow_pf
Proof state before:
a : ℝ
⊢ a = a ^ 1 * 1
Tactic:
simp
Proof state after:
no goals
Theorem: Mathlib.Tactic.RPowRing.atom_pow_pf'
Proof state before:
a a' : ℝ
p : a = a'
⊢ a = a ^ 1 * 1
Tactic:
simp [*]
Proof state after:
no goals
Theorem: Mathlib.Tactic.RPowRing.mul_pf_left
Proof state before:
a₂ b c a₁ : ℝ
x✝ : a₂ * b = c
⊢ a₁ * a₂ * b = a₁ * c
Tactic:
subst_vars
Proof state after:
a₂ b a₁ : ℝ
⊢ a₁ * a₂ * b = a₁ * (a₂ * b)
Theorem: Mathlib.Tactic.RPowRing.mul_pf_left
Proof state before:
a₂ b a₁ : ℝ
⊢ a₁ * a₂ * b = a₁ * (a₂ * b)
Tactic:
rw [mul_assoc]
Proof state after:
no goals
Theorem: Mathlib.Tactic.RPowRing.mul_pf_right
Proof state before:
a b₂ c b₁ : ℝ
x✝ : a * b₂ = c
⊢ a * (b₁ * b₂) = b₁ * c
Tactic:
subst_vars
Proof state after:
a b₂ b₁ : ℝ
⊢ a * (b₁ * b₂) = b₁ * (a * b₂)
Theorem: Mathlib.Tactic.RPowRing.mul_pf_right
Proof state before:
a b₂ b₁ : ℝ
⊢ a * (b₁ * b₂) = b₁ * (a * b₂)
Tactic:
rw [mul_left_comm]
Proof state after:
no goals
Theorem: Mathlib.Tactic.RPowRing.mul_pp_pf_overlap
Proof state before:
x a₂ b₂ c ea eb : ℝ
h : 0 < x
x✝ : a₂ * b₂ = c
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * c
Tactic:
subst_vars
Proof state after:
x a₂ b₂ ea eb : ℝ
h : 0 < x
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)
Theorem: Mathlib.Tactic.RPowRing.mul_pp_pf_overlap
Proof state before:
x a₂ b₂ ea eb : ℝ
h : 0 < x
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)
Tactic:
rw [rpow_add h, mul_mul_mul_comm]
Proof state after:
no goals
Theorem: Mathlib.Tactic.RPowRing.pow_pf
Proof state before:
a b b' : ℝ
ha : 0 < a
hb : 0 < b
e₁ e₂ : ℝ
x✝ : b ^ e₂ = b'
⊢ (a ^ e₁ * b) ^ e₂ = a ^ (e₁ * e₂) * b'
Tactic:
subst_vars
Proof state after:
a b : ℝ
ha : 0 < a
hb : 0 < b
e₁ e₂ : ℝ
⊢ (a ^ e₁ * b) ^ e₂ = a ^ (e₁ * e₂) * b ^ e₂
Theorem: Mathlib.Tactic.RPowRing.pow_pf
Proof state before:
a b : ℝ
ha : 0 < a
hb : 0 < b
e₁ e₂ : ℝ
⊢ (a ^ e₁ * b) ^ e₂ = a ^ (e₁ * e₂) * b ^ e₂
Tactic:
rw [mul_rpow (rpow_pos_of_pos ha e₁).le hb.le, rpow_mul ha.le]
Proof state after:
no goals
Theorem: Mathlib.Tactic.RPowRing.pow_congr
Proof state before:
a a' c b : ℝ
x✝¹ : a = a'
x✝ : a' ^ b = c
⊢ a ^ b = c
Tactic:
subst_vars
Proof state after:
a' b : ℝ
⊢ a' ^ b = a' ^ b
Theorem: Mathlib.Tactic.RPowRing.pow_congr
Proof state before:
a' b : ℝ
⊢ a' ^ b = a' ^ b
Tactic:
rfl
Proof state after:
no goals
Theorem: Mathlib.Tactic.RPowRing.inv_congr
Proof state before:
a a' b : ℝ
x✝¹ : a = a'
x✝ : a' ^ (-1) = b
⊢ a⁻¹ = b
Tactic:
subst_vars
Proof state after:
a' : ℝ
⊢ a'⁻¹ = a' ^ (-1)
Theorem: Mathlib.Tactic.RPowRing.inv_congr
Proof state before:
a' : ℝ
⊢ a'⁻¹ = a' ^ (-1)
Tactic:
simp [rpow_neg_one]
Proof state after:
no goals
Theorem: Mathlib.Tactic.RPowRing.npow_congr
Proof state before:
a a' : ℝ
b : ℕ
c : ℝ
x✝¹ : a = a'
x✝ : a' ^ ↑b = c
⊢ Monoid.npow b a = c
Tactic:
subst_vars
Proof state after:
a' : ℝ
b : ℕ
⊢ Monoid.npow b a' = a' ^ ↑b
Theorem: Real.pow_neg
Proof state before:
a b : ℝ
h : 0 ≤ a
⊢ a ^ (-b) = a⁻¹ ^ b
Tactic:
simp [← rpow_neg_one, ← rpow_mul h]
Proof state after:
no goals
Theorem: Real.inv_rpow'
Proof state before:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x⁻¹ ^ y = x ^ (-y)
Tactic:
simp only [← rpow_neg_one, ← rpow_mul hx, neg_mul, one_mul]
Proof state after:
no goals
Theorem: Real.rpow_inv
Proof state before:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (x ^ y)⁻¹ = x ^ (-y)
Tactic:
simp [← inv_rpow' hx, inv_rpow hx]
Proof state after:
no goals
Theorem: Mathlib.Tactic.RPowRing.fix_cast₃
Proof state before:
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑n = OfNat.ofNat n
Tactic:
rfl
Proof state after:
no goals
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ d ∈ range (N + 1), (f * ↑ζ) d = ∑ d ∈ filter (fun d => d.2 ∈ d.1.divisors) (range (N + 1) ×ˢ range (N + 1)), f d.2
Tactic:
simp_rw [sum_filter, sum_product]
Proof state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ d ∈ range (N + 1), (f * ↑ζ) d = ∑ x ∈ range (N + 1), ∑ x_1 ∈ range (N + 1), if x_1 ∈ x.divisors then f x_1 else 0
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ d ∈ range (N + 1), (f * ↑ζ) d = ∑ x ∈ range (N + 1), ∑ x_1 ∈ range (N + 1), if x_1 ∈ x.divisors then f x_1 else 0
Tactic:
apply sum_congr rfl (fun x hx ↦ ?_)
Proof state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
⊢ (f * ↑ζ) x = ∑ x_1 ∈ range (N + 1), if x_1 ∈ x.divisors then f x_1 else 0
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
⊢ (f * ↑ζ) x = ∑ x_1 ∈ range (N + 1), if x_1 ∈ x.divisors then f x_1 else 0
Tactic:
rw [← sum_filter, sum_congr (s₂ := divisors x) ?_ fun _ _ ↦ rfl, coe_mul_zeta_apply]
Proof state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
⊢ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1)) = x.divisors
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
⊢ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1)) = x.divisors
Tactic:
refine Subset.antisymm ?_ ?_ <;> intro d hd
Proof state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1))
⊢ d ∈ x.divisors

case refine_2
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ x.divisors
⊢ d ∈ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1))
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1))
⊢ d ∈ x.divisors
Tactic:
exact (mem_filter.mp hd).right
Proof state after:
no goals
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ x.divisors
⊢ d ∈ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1))
Tactic:
have h : d ≤ x := by
  rw [divisors, mem_filter] at hd
  exact lt_succ.mp (mem_Ico.mp hd.left).right
Proof state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ x.divisors
h : d ≤ x
⊢ d ∈ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1))
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ x.divisors
h : d ≤ x
⊢ d ∈ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1))
Tactic:
exact mem_filter.mpr ⟨mem_range.mpr (lt_of_le_of_lt h $ mem_range.mp hx), hd⟩
Proof state after:
no goals
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ x.divisors
⊢ d ≤ x
Tactic:
rw [divisors, mem_filter] at hd
Proof state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ Ico 1 (x + 1) ∧ d ∣ x
⊢ d ≤ x
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ Ico 1 (x + 1) ∧ d ∣ x
⊢ d ≤ x
Tactic:
exact lt_succ.mp (mem_Ico.mp hd.left).right
Proof state after:
no goals
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ d ∈ filter (fun d => d.2 ∈ d.1.divisors) (range (N + 1) ×ˢ range (N + 1)), f d.2 =
    ∑ d ∈ range (N + 1), ∑ _m ∈ filter (fun x => d ∈ x.divisors) (range (N + 1)), f d
Tactic:
rw [sum_filter, sum_product_right]
Proof state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ (∑ y ∈ range (N + 1), ∑ x ∈ range (N + 1), if (x, y).2 ∈ (x, y).1.divisors then f (x, y).2 else 0) =
    ∑ d ∈ range (N + 1), ∑ _m ∈ filter (fun x => d ∈ x.divisors) (range (N + 1)), f d
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ (∑ y ∈ range (N + 1), ∑ x ∈ range (N + 1), if (x, y).2 ∈ (x, y).1.divisors then f (x, y).2 else 0) =
    ∑ d ∈ range (N + 1), ∑ _m ∈ filter (fun x => d ∈ x.divisors) (range (N + 1)), f d
Tactic:
refine sum_congr rfl (fun y _ ↦ by simp only [← sum_filter])
Proof state after:
no goals
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ (∑ x ∈ range (N + 1), if (x, y).2 ∈ (x, y).1.divisors then f (x, y).2 else 0) =
    ∑ _m ∈ filter (fun x => y ∈ x.divisors) (range (N + 1)), f y
Tactic:
simp only [← sum_filter]
Proof state after:
no goals
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ d ∈ range (N + 1), ∑ _m ∈ filter (fun x => d ∈ x.divisors) (range (N + 1)), f d = ∑ d ∈ range (N + 1), (N / d) • f d
Tactic:
rw [sum_congr rfl fun y _ ↦ ?_]
Proof state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ ∑ _m ∈ filter (fun x => y ∈ x.divisors) (range (N + 1)), f y = (N / y) • f y
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ ∑ _m ∈ filter (fun x => y ∈ x.divisors) (range (N + 1)), f y = (N / y) • f y
Tactic:
rw [sum_const]
Proof state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ (filter (fun x => y ∈ x.divisors) (range (N + 1))).card • f y = (N / y) • f y
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ (filter (fun x => y ∈ x.divisors) (range (N + 1))).card • f y = (N / y) • f y
Tactic:
congr
Proof state after:
case e_a
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ (filter (fun x => y ∈ x.divisors) (range (N + 1))).card = N / y
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
case e_a
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ (filter (fun x => y ∈ x.divisors) (range (N + 1))).card = N / y
Tactic:
simp_rw [mem_divisors, and_comm (b := _ ≠ 0), ← filter_filter]
Proof state after:
case e_a
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ (filter (fun a => y ∣ a) (filter (fun a => a ≠ 0) (range (N + 1)))).card = N / y
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
case e_a
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
this : filter (fun x => x ≠ 0) (range (N + 1)) = Ioc 0 N
⊢ (filter (fun a => y ∣ a) (filter (fun a => a ≠ 0) (range (N + 1)))).card = N / y
Tactic:
rw [this, Nat.Ioc_filter_dvd_card_eq_div]
Proof state after:
no goals
Theorem: ArithmeticFunction.sum_range_mul_zeta
Proof state before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ filter (fun x => x ≠ 0) (range (N + 1)) = Ioc 0 N
Tactic:
ext a
Proof state after:
case a
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
a : ℕ
⊢ a ∈ filter (fun x => x ≠ 0) (range (N + 1)) ↔ a ∈ Ioc 0 N