internlm/Lean-Github huggingface dataset:
Theorem: W21_approximation
Proof state before:
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‖
R v : ℝ
df : ∀ (v : ℝ), HasDerivAt f.toFun (f'.toFun v) v
df' : ∀ (v : ℝ), HasDerivAt f'.toFun (f''.toFun v) v
l3 : ∀ (v : ℝ), HasDerivAt (fun v => ↑(h R v) * f.toFun v) (↑((h' R).toFun v) * f.toFun v + ↑(h R v) * f'.toFun v) v
l5 :
  HasDerivAt (fun v => ↑((h' R).toFun v) * f.toFun v) (↑((h'' R).toFun v) * f.toFun v + ↑((h' R).toFun v) * f'.toFun v)
    v
l7 : HasDerivAt (fun v => ↑(h R v) * f'.toFun v) (↑((h' R).toFun v) * f'.toFun v + ↑(h R v) * f''.toFun v) v
d1 : (deriv fun v => ↑(h R v) * f.toFun v) = fun v => ↑((h' R).toFun v) * f.toFun v + ↑(h R v) * f'.toFun v
⊢ ↑((h'' R).toFun v) * f.toFun v + 2 * ↑((h' R).toFun v) * f'.toFun v + ↑(h R v) * f''.toFun v =
    ↑((h'' R).toFun v) * f.toFun v + ↑((h' R).toFun v) * f'.toFun v +
      (↑((h' R).toFun v) * f'.toFun v + ↑(h R v) * f''.toFun v)
Tactic:
ring
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‖
⊢ ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume
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).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‖
⊢ ∀ (x : ℝ), AEStronglyMeasurable (F x) volume
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).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‖
⊢ ∀ (x : ℝ), AEStronglyMeasurable (F x) volume
Tactic:
intro R
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).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‖
R : ℝ
⊢ AEStronglyMeasurable (F R) volume
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).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‖
R : ℝ
⊢ AEStronglyMeasurable (F R) volume
Tactic:
apply (Continuous.norm ?_).aestronglyMeasurable
Proof state after:
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‖
R : ℝ
⊢ Continuous fun x => ↑((h'' R).toFun x) * f.toFun x + 2 * ↑((h' R).toFun x) * f'.toFun x + ↑(h R x) * f''.toFun x
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‖
R : ℝ
⊢ Continuous fun x => ↑((h'' R).toFun x) * f.toFun x + 2 * ↑((h' R).toFun x) * f'.toFun x + ↑(h R x) * f''.toFun x
Tactic:
exact ((ch''.mul f.continuous).add ((continuous_const.mul ch').mul f.deriv.continuous)).add
  (ch.mul f.deriv.deriv.continuous)
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
⊢ ∀ᶠ (R : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a
Tactic:
have hc1 : ∀ᶠ R in atTop, ∀ v, |h' R v| ≤ c1 := by
  filter_upwards [eventually_ge_atTop 1] with R hR v
  have hR' : R ≠ 0 := by linarith
  have : 0 ≤ R := by linarith
  simp [h', CS.deriv_scale, abs_mul, abs_inv, abs_eq_self.mpr this] ; simp [CS.scale, funscale, hR']
  convert_to _ ≤ c1 * 1 ; simp ; rw [mul_comm]
  apply mul_le_mul (mg' _) (inv_le_of_inv_le (by linarith) (by simpa using hR)) (by positivity)
  exact (abs_nonneg _).trans (mg' 0)
Proof state after:
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
hc1 : ∀ᶠ (R : ℝ) in atTop, ∀ (v : ℝ), |(h' R).toFun v| ≤ c1
⊢ ∀ᶠ (R : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a
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
hc1 : ∀ᶠ (R : ℝ) in atTop, ∀ (v : ℝ), |(h' R).toFun v| ≤ c1
⊢ ∀ᶠ (R : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a
Tactic:
have hc2 : ∀ᶠ R in atTop, ∀ v, |h'' R v| ≤ c2 := by
  filter_upwards [eventually_ge_atTop 1] with R hR v
  have e1 : 0 ≤ R := by linarith
  have e2 : R⁻¹ ≤ 1 := inv_le_of_inv_le (by linarith) (by simpa using hR)
  have e3 : R ≠ 0 := by linarith
  simp [h'', CS.deriv_scale, CS.deriv_smul, abs_mul, abs_inv, abs_eq_self.mpr e1]
  convert_to _ ≤ 1 * (1 * c2) ; simp
  apply mul_le_mul e2 ?_ (by positivity) zero_le_one
  apply mul_le_mul e2 ?_ (by positivity) zero_le_one
  simp [CS.scale, e3, funscale] ; apply mg''
Proof state after:
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
hc1 : ∀ᶠ (R : ℝ) in atTop, ∀ (v : ℝ), |(h' R).toFun v| ≤ c1
hc2 : ∀ᶠ (R : ℝ) in atTop, ∀ (v : ℝ), |(h'' R).toFun v| ≤ c2
⊢ ∀ᶠ (R : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a
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
hc1 : ∀ᶠ (R : ℝ) in atTop, ∀ (v : ℝ), |(h' R).toFun v| ≤ c1
hc2 : ∀ᶠ (R : ℝ) in atTop, ∀ (v : ℝ), |(h'' R).toFun v| ≤ c2
⊢ ∀ᶠ (R : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a
Tactic:
filter_upwards [hc1, hc2] with R hc1 hc2
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
hc1✝ : ∀ᶠ (R : ℝ) in atTop, ∀ (v : ℝ), |(h' R).toFun v| ≤ c1
hc2✝ : ∀ᶠ (R : ℝ) in atTop, ∀ (v : ℝ), |(h'' R).toFun v| ≤ c2
R : ℝ
hc1 : ∀ (v : ℝ), |(h' R).toFun v| ≤ c1
hc2 : ∀ (v : ℝ), |(h'' R).toFun v| ≤ c2
⊢ ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a
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
hc1✝ : ∀ᶠ (R : ℝ) in atTop, ∀ (v : ℝ), |(h' R).toFun v| ≤ c1
hc2✝ : ∀ᶠ (R : ℝ) in atTop, ∀ (v : ℝ), |(h'' R).toFun v| ≤ c2
R : ℝ
hc1 : ∀ (v : ℝ), |(h' R).toFun v| ≤ c1
hc2 : ∀ (v : ℝ), |(h'' R).toFun v| ≤ c2
⊢ ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a
Tactic:
apply eventually_of_forall
Proof state after:
case h.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).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
hc1✝ : ∀ᶠ (R : ℝ) in atTop, ∀ (v : ℝ), |(h' R).toFun v| ≤ c1
hc2✝ : ∀ᶠ (R : ℝ) in atTop, ∀ (v : ℝ), |(h'' R).toFun v| ≤ c2
R : ℝ
hc1 : ∀ (v : ℝ), |(h' R).toFun v| ≤ c1
hc2 : ∀ (v : ℝ), |(h'' R).toFun v| ≤ c2
⊢ ∀ (x : ℝ), ‖F R x‖ ≤ bound x
Theorem: W21_approximation
Proof state before:
case h.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).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
hc1✝ : ∀ᶠ (R : ℝ) in atTop, ∀ (v : ℝ), |(h' R).toFun v| ≤ c1
hc2✝ : ∀ᶠ (R : ℝ) in atTop, ∀ (v : ℝ), |(h'' R).toFun v| ≤ c2
R : ℝ
hc1 : ∀ (v : ℝ), |(h' R).toFun v| ≤ c1
hc2 : ∀ (v : ℝ), |(h'' R).toFun v| ≤ c2
⊢ ∀ (x : ℝ), ‖F R x‖ ≤ bound x
Tactic:
intro v
Proof state after:
case h.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).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
hc1✝ : ∀ᶠ (R : ℝ) in atTop, ∀ (v : ℝ), |(h' R).toFun v| ≤ c1
hc2✝ : ∀ᶠ (R : ℝ) in atTop, ∀ (v : ℝ), |(h'' R).toFun v| ≤ c2
R : ℝ
hc1 : ∀ (v : ℝ), |(h' R).toFun v| ≤ c1
hc2 : ∀ (v : ℝ), |(h'' R).toFun v| ≤ c2
v : ℝ
⊢ ‖F R v‖ ≤ bound v