internlm/Lean-Github huggingface dataset:
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 v) * f.toFun v‖
eh : ∀ (v : ℝ), ∀ᶠ (R : ℝ) in atTop, h R v = 0
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
R v : ℝ
⊢ 0 ≤ Complex.abs (f.toFun v)
Tactic:
simp
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 v) * f.toFun v‖
eh : ∀ (v : ℝ), ∀ᶠ (R : ℝ) in atTop, h R v = 0
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F n a‖ ≤ ‖f.toFun a‖
⊢ ∀ᵐ (a : ℝ), Tendsto (fun n => F n a) atTop (𝓝 0)
Tactic:
apply eventually_of_forall
Proof state after:
case hp
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 v) * f.toFun v‖
eh : ∀ (v : ℝ), ∀ᶠ (R : ℝ) in atTop, h R v = 0
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F n a‖ ≤ ‖f.toFun a‖
⊢ ∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 0)
Theorem: W21_approximation
Proof state before:
case hp
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 v) * f.toFun v‖
eh : ∀ (v : ℝ), ∀ᶠ (R : ℝ) in atTop, h R v = 0
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F n a‖ ≤ ‖f.toFun a‖
⊢ ∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 0)
Tactic:
intro v
Proof state after:
case hp
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 v) * f.toFun v‖
eh : ∀ (v : ℝ), ∀ᶠ (R : ℝ) in atTop, h R v = 0
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F n a‖ ≤ ‖f.toFun a‖
v : ℝ
⊢ Tendsto (fun n => F n v) atTop (𝓝 0)
Theorem: W21_approximation
Proof state before:
case hp
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 v) * f.toFun v‖
eh : ∀ (v : ℝ), ∀ᶠ (R : ℝ) in atTop, h R v = 0
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F n a‖ ≤ ‖f.toFun a‖
v : ℝ
⊢ Tendsto (fun n => F n v) atTop (𝓝 0)
Tactic:
apply tendsto_nhds_of_eventually_eq
Proof state after:
case hp.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 v) * f.toFun v‖
eh : ∀ (v : ℝ), ∀ᶠ (R : ℝ) in atTop, h R v = 0
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F n a‖ ≤ ‖f.toFun a‖
v : ℝ
⊢ ∀ᶠ (x' : ℝ) in atTop, F x' v = 0
Theorem: W21_approximation
Proof state before:
case hp.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 v) * f.toFun v‖
eh : ∀ (v : ℝ), ∀ᶠ (R : ℝ) in atTop, h R v = 0
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F n a‖ ≤ ‖f.toFun a‖
v : ℝ
⊢ ∀ᶠ (x' : ℝ) in atTop, F x' 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 v) * f.toFun v‖
eh : ∀ (v : ℝ), ∀ᶠ (R : ℝ) in atTop, h R v = 0
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F n a‖ ≤ ‖f.toFun a‖
v R : ℝ
hR : h R v = 0
⊢ F R 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 v) * f.toFun v‖
eh : ∀ (v : ℝ), ∀ᶠ (R : ℝ) in atTop, h R v = 0
e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
e2 : ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F n a‖ ≤ ‖f.toFun a‖
v R : ℝ
hR : h R v = 0
⊢ F R v = 0
Tactic:
simp [F, hR]
Proof state after:
no goals
Theorem: W21_approximation
Proof state before:
case refine_2
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)
⊢ Tendsto (fun k => ∫ (v : ℝ), ‖deriv (deriv fun v => ↑(h k v) * f.toFun v) v‖) atTop (𝓝 0)
Tactic:
let F R v := ‖h'' R v * f v + 2 * h' R v * f' v + h R v * f'' v‖
Proof state after:
case refine_2
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‖
⊢ Tendsto (fun k => ∫ (v : ℝ), ‖deriv (deriv fun v => ↑(h k v) * f.toFun v) v‖) atTop (𝓝 0)
Theorem: W21_approximation
Proof state before:
case refine_2
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‖
⊢ Tendsto (fun k => ∫ (v : ℝ), ‖deriv (deriv fun v => ↑(h k v) * f.toFun v) v‖) atTop (𝓝 0)
Tactic:
convert_to Tendsto (fun R ↦ ∫ (v : ℝ), F R v) atTop (𝓝 0)
Proof state after:
case h.e'_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‖
⊢ (fun k => ∫ (v : ℝ), ‖deriv (deriv fun v => ↑(h k v) * f.toFun v) v‖) = fun R => ∫ (v : ℝ), F R v

case refine_2
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‖
⊢ Tendsto (fun R => ∫ (v : ℝ), F R v) atTop (𝓝 0)
Theorem: W21_approximation
Proof state before:
case refine_2
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‖
⊢ Tendsto (fun R => ∫ (v : ℝ), F R v) atTop (𝓝 0)
Tactic:
obtain ⟨c1, mg'⟩ := g'.bounded
Proof state after:
case refine_2.intro
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
⊢ Tendsto (fun R => ∫ (v : ℝ), F R v) atTop (𝓝 0)
Theorem: W21_approximation
Proof state before:
case refine_2.intro
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
⊢ Tendsto (fun R => ∫ (v : ℝ), F R v) atTop (𝓝 0)
Tactic:
obtain ⟨c2, mg''⟩ := g''.bounded
Proof state after:
case refine_2.intro.intro
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
⊢ Tendsto (fun R => ∫ (v : ℝ), F R v) atTop (𝓝 0)
Theorem: W21_approximation
Proof state before:
case refine_2.intro.intro
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
⊢ Tendsto (fun R => ∫ (v : ℝ), F R v) atTop (𝓝 0)
Tactic:
let bound v := c2 * ‖f v‖ + 2 * c1 * ‖f' v‖ + ‖f'' v‖
Proof state after:
case refine_2.intro.intro
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‖
⊢ Tendsto (fun R => ∫ (v : ℝ), F R v) atTop (𝓝 0)
Theorem: W21_approximation
Proof state before:
case refine_2.intro.intro
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‖
⊢ Tendsto (fun R => ∫ (v : ℝ), F R v) atTop (𝓝 0)
Tactic:
have e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume := by
  apply eventually_of_forall ; intro R ; apply (Continuous.norm ?_).aestronglyMeasurable
  exact ((ch''.mul f.continuous).add ((continuous_const.mul ch').mul f.deriv.continuous)).add
    (ch.mul f.deriv.deriv.continuous)
Proof state after:
case refine_2.intro.intro
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
⊢ Tendsto (fun R => ∫ (v : ℝ), F R v) atTop (𝓝 0)