internlm/Lean-Github huggingface dataset:
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case h.right
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ ↑d ≤ x

case h.right
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 ≤ x
Tactic:
exact hd.2
Proof state after:
case h.right
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 ≤ x
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case h.right
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 ≤ x
Tactic:
apply le_of_lt
Proof state after:
case h.right.a
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 < x
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case h.right.a
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 < x
Tactic:
exact hx_pos
Proof state after:
no goals
Theorem: Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow
Proof state before:
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ (∑ d ∈ P.divisors, if ↑d ≤ x then ↑h ^ ω d else 0) ≤ x * (1 + x.log) ^ h
Tactic:
trans (∑ d in P.divisors, x * if ↑d ≤ x then (h : ℝ) ^ ω d / d else (0 : ℝ))
Proof state after:
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ (∑ d ∈ P.divisors, if ↑d ≤ x then ↑h ^ ω d else 0) ≤ ∑ d ∈ P.divisors, x * if ↑d ≤ x then ↑h ^ ω d / ↑d else 0

P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ (∑ d ∈ P.divisors, x * if ↑d ≤ x then ↑h ^ ω d / ↑d else 0) ≤ x * (1 + x.log) ^ h
Theorem: Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow
Proof state before:
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ (∑ d ∈ P.divisors, x * if ↑d ≤ x then ↑h ^ ω d / ↑d else 0) ≤ x * (1 + x.log) ^ h
Tactic:
rw [←mul_sum]
Proof state after:
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ (x * ∑ i ∈ P.divisors, if ↑i ≤ x then ↑h ^ ω i / ↑i else 0) ≤ x * (1 + x.log) ^ h
Theorem: Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow
Proof state before:
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ (x * ∑ i ∈ P.divisors, if ↑i ≤ x then ↑h ^ ω i / ↑i else 0) ≤ x * (1 + x.log) ^ h
Tactic:
gcongr
Proof state after:
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ (∑ i ∈ P.divisors, if ↑i ≤ x then ↑h ^ ω i / ↑i else 0) ≤ (1 + x.log) ^ h
Theorem: Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow
Proof state before:
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ (∑ i ∈ P.divisors, if ↑i ≤ x then ↑h ^ ω i / ↑i else 0) ≤ (1 + x.log) ^ h
Tactic:
apply sum_pow_cardDistinctFactors_div_self_le_log_pow x hx hP
Proof state after:
no goals
Theorem: Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow
Proof state before:
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ (∑ d ∈ P.divisors, if ↑d ≤ x then ↑h ^ ω d else 0) ≤ ∑ d ∈ P.divisors, x * if ↑d ≤ x then ↑h ^ ω d / ↑d else 0
Tactic:
simp_rw [mul_ite, mul_zero, ←sum_filter]
Proof state after:
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ ∑ a ∈ filter (fun a => ↑a ≤ x) P.divisors, ↑h ^ ω a ≤ ∑ a ∈ filter (fun a => ↑a ≤ x) P.divisors, x * (↑h ^ ω a / ↑a)
Theorem: Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow
Proof state before:
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ ∑ a ∈ filter (fun a => ↑a ≤ x) P.divisors, ↑h ^ ω a ≤ ∑ a ∈ filter (fun a => ↑a ≤ x) P.divisors, x * (↑h ^ ω a / ↑a)
Tactic:
gcongr with i hi
Proof state after:
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ filter (fun a => ↑a ≤ x) P.divisors
⊢ ↑h ^ ω i ≤ x * (↑h ^ ω i / ↑i)
Theorem: Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow
Proof state before:
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ filter (fun a => ↑a ≤ x) P.divisors
⊢ ↑h ^ ω i ≤ x * (↑h ^ ω i / ↑i)
Tactic:
rw [div_eq_mul_inv, mul_comm _ (i:ℝ)⁻¹, ←mul_assoc]
Proof state after:
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ filter (fun a => ↑a ≤ x) P.divisors
⊢ ↑h ^ ω i ≤ x * (↑i)⁻¹ * ↑h ^ ω i
Theorem: Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow
Proof state before:
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ filter (fun a => ↑a ≤ x) P.divisors
⊢ ↑h ^ ω i ≤ x * (↑i)⁻¹ * ↑h ^ ω i
Tactic:
trans (1*(h:ℝ)^ω i)
Proof state after:
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ filter (fun a => ↑a ≤ x) P.divisors
⊢ ↑h ^ ω i ≤ 1 * ↑h ^ ω i

P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ filter (fun a => ↑a ≤ x) P.divisors
⊢ 1 * ↑h ^ ω i ≤ x * (↑i)⁻¹ * ↑h ^ ω i
Theorem: Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow
Proof state before:
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ filter (fun a => ↑a ≤ x) P.divisors
⊢ 1 * ↑h ^ ω i ≤ x * (↑i)⁻¹ * ↑h ^ ω i
Tactic:
gcongr
Proof state after:
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ filter (fun a => ↑a ≤ x) P.divisors
⊢ 1 ≤ x * (↑i)⁻¹
Theorem: Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow
Proof state before:
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ filter (fun a => ↑a ≤ x) P.divisors
⊢ 1 ≤ x * (↑i)⁻¹
Tactic:
rw [mem_filter] at hi
Proof state after:
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ P.divisors ∧ ↑i ≤ x
⊢ 1 ≤ x * (↑i)⁻¹
Theorem: Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow
Proof state before:
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ P.divisors ∧ ↑i ≤ x
⊢ 1 ≤ x * (↑i)⁻¹
Tactic:
rw [←div_eq_mul_inv]
Proof state after:
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ P.divisors ∧ ↑i ≤ x
⊢ 1 ≤ x / ↑i
Theorem: Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow
Proof state before:
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ P.divisors ∧ ↑i ≤ x
⊢ 1 ≤ x / ↑i
Tactic:
apply one_le_div (by norm_cast; apply Nat.pos_of_mem_divisors hi.1) |>.mpr hi.2
Proof state after:
no goals
Theorem: Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow
Proof state before:
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ filter (fun a => ↑a ≤ x) P.divisors
⊢ ↑h ^ ω i ≤ 1 * ↑h ^ ω i
Tactic:
rw [one_mul]
Proof state after:
no goals
Theorem: Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow
Proof state before:
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ P.divisors ∧ ↑i ≤ x
⊢ 0 < ↑i
Tactic:
norm_cast
Proof state after:
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ P.divisors ∧ ↑i ≤ x
⊢ 0 < i
Theorem: Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow
Proof state before:
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ P.divisors ∧ ↑i ≤ x
⊢ 0 < i
Tactic:
apply Nat.pos_of_mem_divisors hi.1
Proof state after:
no goals
Theorem: contDiff_ofReal
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
⊢ ContDiff ℝ ⊤ ofReal'
Tactic:
have key x : HasDerivAt ofReal' 1 x := hasDerivAt_id x |>.ofReal_comp
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
⊢ ContDiff ℝ ⊤ ofReal'
Theorem: contDiff_ofReal
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
⊢ ContDiff ℝ ⊤ ofReal'
Tactic:
have key' : deriv ofReal' = fun _ => 1 := by ext x ; exact (key x).deriv
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
key' : deriv ofReal' = fun x => 1
⊢ ContDiff ℝ ⊤ ofReal'
Theorem: contDiff_ofReal
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
key' : deriv ofReal' = fun x => 1
⊢ ContDiff ℝ ⊤ ofReal'
Tactic:
refine contDiff_top_iff_deriv.mpr ⟨fun x => (key x).differentiableAt, ?_⟩
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
key' : deriv ofReal' = fun x => 1
⊢ ContDiff ℝ ⊤ (deriv ofReal')
Theorem: contDiff_ofReal
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
key' : deriv ofReal' = fun x => 1
⊢ ContDiff ℝ ⊤ (deriv ofReal')
Tactic:
simpa [key'] using contDiff_const
Proof state after:
no goals
Theorem: contDiff_ofReal
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
⊢ deriv ofReal' = fun x => 1
Tactic:
ext x
Proof state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
x : ℝ
⊢ deriv ofReal' x = 1
Theorem: contDiff_ofReal
Proof state before:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
key : ∀ (x : ℝ), HasDerivAt ofReal' 1 x
x : ℝ
⊢ deriv ofReal' x = 1
Tactic:
exact (key x).deriv
Proof state after:
no goals
Theorem: tendsto_funscale
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : ℝ → E
hf : ContinuousAt f 0
x : ℝ
⊢ Tendsto (fun R => R⁻¹ • x) atTop (𝓝 0)
Tactic:
simpa using tendsto_inv_atTop_zero.mul_const x
Proof state after:
no goals
Theorem: CS.hasDerivAt
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x✝ v : ℝ
f : CS (n + 1) E
x : ℝ
⊢ 1 ≤ ↑(n + 1)
Tactic:
simp
Proof state after:
no goals
Theorem: CS.deriv_smul
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v : ℝ
f : CS (n + 1) E
⊢ (R • f).deriv = R • f.deriv
Tactic:
ext x
Proof state after:
case toFun.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x✝ v : ℝ
f : CS (n + 1) E
x : ℝ
⊢ (R • f).deriv.toFun x = (R • f.deriv).toFun x
Theorem: CS.deriv_smul
Proof state before:
case toFun.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x✝ v : ℝ
f : CS (n + 1) E
x : ℝ
⊢ (R • f).deriv.toFun x = (R • f.deriv).toFun x
Tactic:
exact (f.hasDerivAt x |>.const_smul R).deriv
Proof state after:
no goals
Theorem: CS.deriv_scale
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v : ℝ
f : CS (n + 1) E
⊢ (f.scale R).deriv = R⁻¹ • f.deriv.scale R
Tactic:
ext v
Proof state after:
case toFun.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
⊢ (f.scale R).deriv.toFun v = (R⁻¹ • f.deriv.scale R).toFun v
Theorem: CS.deriv_scale
Proof state before:
case toFun.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
⊢ (f.scale R).deriv.toFun v = (R⁻¹ • f.deriv.scale R).toFun v
Tactic:
by_cases hR : R = 0 <;> simp [hR, scale]
Proof state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : R = 0
⊢ { toFun := 0, h1 := ⋯, h2 := ⋯ }.deriv.toFun v = 0

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : ¬R = 0
⊢ { toFun := fun x => funscale f.toFun R x, h1 := ⋯, h2 := ⋯ }.deriv.toFun v = R⁻¹ • funscale f.deriv.toFun R v
Theorem: CS.deriv_scale
Proof state before:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : R = 0
⊢ { toFun := 0, h1 := ⋯, h2 := ⋯ }.deriv.toFun v = 0
Tactic:
simp [deriv, smul]
Proof state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : R = 0
⊢ _root_.deriv 0 v = 0
Theorem: CS.deriv_scale
Proof state before:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : R = 0
⊢ _root_.deriv 0 v = 0
Tactic:
exact deriv_const _ _
Proof state after:
no goals
Theorem: CS.deriv_scale
Proof state before:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : ¬R = 0
⊢ { toFun := fun x => funscale f.toFun R x, h1 := ⋯, h2 := ⋯ }.deriv.toFun v = R⁻¹ • funscale f.deriv.toFun R v
Tactic:
exact ((f.hasDerivAt (R⁻¹ • v)).scomp v (by simpa using (hasDerivAt_id v).const_smul R⁻¹)).deriv
Proof state after:
no goals
Theorem: CS.deriv_scale
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : ¬R = 0
⊢ HasDerivAt (HSMul.hSMul R⁻¹) R⁻¹ v
Tactic:
simpa using (hasDerivAt_id v).const_smul R⁻¹
Proof state after:
no goals
Theorem: CS.deriv_scale'
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v : ℝ
f : CS (n + 1) E
⊢ (f.scale R).deriv.toFun v = R⁻¹ • f.deriv.toFun (R⁻¹ • v)
Tactic:
rw [deriv_scale, smul_apply]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v : ℝ
f : CS (n + 1) E
⊢ R⁻¹ • (f.deriv.scale R).toFun v = R⁻¹ • f.deriv.toFun (R⁻¹ • v)
Theorem: CS.deriv_scale'
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v : ℝ
f : CS (n + 1) E
⊢ R⁻¹ • (f.deriv.scale R).toFun v = R⁻¹ • f.deriv.toFun (R⁻¹ • v)
Tactic:
by_cases hR : R = 0 <;> simp [hR, scale, funscale]
Proof state after:
no goals
Theorem: CS.hasDerivAt_scale
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R✝ x✝ v : ℝ
f : CS (n + 1) E
R x : ℝ
⊢ HasDerivAt (f.scale R).toFun (R⁻¹ • _root_.deriv f.toFun (R⁻¹ • x)) x
Tactic:
convert hasDerivAt (f.scale R) x
Proof state after:
case h.e'_7
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R✝ x✝ v : ℝ
f : CS (n + 1) E
R x : ℝ
⊢ R⁻¹ • _root_.deriv f.toFun (R⁻¹ • x) = (f.scale R).deriv.toFun x
Theorem: CS.hasDerivAt_scale
Proof state before:
case h.e'_7
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R✝ x✝ v : ℝ
f : CS (n + 1) E
R x : ℝ
⊢ R⁻¹ • _root_.deriv f.toFun (R⁻¹ • x) = (f.scale R).deriv.toFun x
Tactic:
rw [deriv_scale']
Proof state after:
case h.e'_7
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R✝ x✝ v : ℝ
f : CS (n + 1) E
R x : ℝ
⊢ R⁻¹ • _root_.deriv f.toFun (R⁻¹ • x) = R⁻¹ • f.deriv.toFun (R⁻¹ • x)
Theorem: CS.hasDerivAt_scale
Proof state before:
case h.e'_7
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R✝ x✝ v : ℝ
f : CS (n + 1) E
R x : ℝ
⊢ R⁻¹ • _root_.deriv f.toFun (R⁻¹ • x) = R⁻¹ • f.deriv.toFun (R⁻¹ • x)
Tactic:
rfl
Proof state after:
no goals
Theorem: CS.tendsto_scale
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x✝ v : ℝ
f : CS n E
x : ℝ
⊢ Tendsto (fun R => (f.scale R).toFun x) atTop (𝓝 (f.toFun 0))
Tactic:
apply (tendsto_funscale f.continuous.continuousAt x).congr'
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x✝ v : ℝ
f : CS n E
x : ℝ
⊢ (fun R => funscale f.toFun R x) =ᶠ[atTop] fun R => (f.scale R).toFun x
Theorem: CS.tendsto_scale
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x✝ v : ℝ
f : CS n E
x : ℝ
⊢ (fun R => funscale f.toFun R x) =ᶠ[atTop] fun R => (f.scale R).toFun x
Tactic:
filter_upwards [eventually_ne_atTop 0] with R hR
Proof state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R✝ x✝ v : ℝ
f : CS n E
x R : ℝ
hR : R ≠ 0
⊢ funscale f.toFun R x = (f.scale R).toFun x
Theorem: CS.tendsto_scale
Proof state before:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R✝ x✝ v : ℝ
f : CS n E
x R : ℝ
hR : R ≠ 0
⊢ funscale f.toFun R x = (f.scale R).toFun x
Tactic:
simp [scale, hR]
Proof state after:
no goals
Theorem: CS.bounded
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : CS n E
R x v : ℝ
⊢ ∃ C, ∀ (v : ℝ), ‖f.toFun v‖ ≤ C
Tactic:
obtain ⟨x, hx⟩ := (continuous_norm.comp f.continuous).exists_forall_ge_of_hasCompactSupport f.h2.norm
Proof state after:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : CS n E
R x✝ v x : ℝ
hx : ∀ (y : ℝ), ((fun a => ‖a‖) ∘ f.toFun) y ≤ ((fun a => ‖a‖) ∘ f.toFun) x
⊢ ∃ C, ∀ (v : ℝ), ‖f.toFun v‖ ≤ C
Theorem: CS.bounded
Proof state before:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : CS n E
R x✝ v x : ℝ
hx : ∀ (y : ℝ), ((fun a => ‖a‖) ∘ f.toFun) y ≤ ((fun a => ‖a‖) ∘ f.toFun) x
⊢ ∃ C, ∀ (v : ℝ), ‖f.toFun v‖ ≤ C
Tactic:
exact ⟨_, hx⟩
Proof state after:
no goals
Theorem: trunc.nonneg
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
g : trunc
x : ℝ
⊢ ∀ a ∈ Set.Icc (-1) 1, 0 ≤ 1 a
Tactic:
simp
Proof state after:
no goals
Theorem: trunc.le_one
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
g : trunc
x : ℝ
⊢ ∀ x ∉ Set.Ioo (-2) 2, 0 ≤ 1 x
Tactic:
simp
Proof state after:
no goals
Theorem: trunc.zero
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
g : trunc
⊢ g.toFun =ᶠ[𝓝 0] 1
Tactic:
have : Set.Icc (-1) 1 ∈ 𝓝 (0 : ℝ) := by apply Icc_mem_nhds <;> linarith
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
g : trunc
this : Set.Icc (-1) 1 ∈ 𝓝 0
⊢ g.toFun =ᶠ[𝓝 0] 1
Theorem: trunc.zero
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
g : trunc
this : Set.Icc (-1) 1 ∈ 𝓝 0
⊢ g.toFun =ᶠ[𝓝 0] 1
Tactic:
exact eventually_of_mem this (fun x hx => le_antisymm (g.le_one x) (by simpa [hx] using g.h3 x))
Proof state after:
no goals
Theorem: trunc.zero
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
g : trunc
⊢ Set.Icc (-1) 1 ∈ 𝓝 0
Tactic:
apply Icc_mem_nhds <;> linarith
Proof state after:
no goals
Theorem: trunc.zero
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
g : trunc
this : Set.Icc (-1) 1 ∈ 𝓝 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ 1 x ≤ g.toFun x
Tactic:
simpa [hx] using g.h3 x
Proof state after:
no goals
Theorem: W1.differentiable
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : W1 (n + 1) E
⊢ 1 ≤ ↑(n + 1)
Tactic:
simp
Proof state after:
no goals
Theorem: W1.iteratedDeriv_sub
Proof state before:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f g : ℝ → E
hf : ContDiff ℝ (↑0) f
hg : ContDiff ℝ (↑0) g
⊢ iteratedDeriv 0 (f - g) = iteratedDeriv 0 f - iteratedDeriv 0 g
Tactic:
rfl
Proof state after:
no goals
Theorem: W1.iteratedDeriv_sub
Proof state before:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
⊢ iteratedDeriv (n + 1) (f - g) = iteratedDeriv (n + 1) f - iteratedDeriv (n + 1) g
Tactic:
have hf' : ContDiff ℝ n (deriv f) := hf.iterate_deriv' n 1
Proof state after:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
⊢ iteratedDeriv (n + 1) (f - g) = iteratedDeriv (n + 1) f - iteratedDeriv (n + 1) g
Theorem: W1.iteratedDeriv_sub
Proof state before:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
⊢ iteratedDeriv (n + 1) (f - g) = iteratedDeriv (n + 1) f - iteratedDeriv (n + 1) g
Tactic:
have hg' : ContDiff ℝ n (deriv g) := hg.iterate_deriv' n 1
Proof state after:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
⊢ iteratedDeriv (n + 1) (f - g) = iteratedDeriv (n + 1) f - iteratedDeriv (n + 1) g
Theorem: W1.iteratedDeriv_sub
Proof state before:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
hfg : deriv (f - g) = deriv f - deriv g
⊢ iteratedDeriv (n + 1) (f - g) = iteratedDeriv (n + 1) f - iteratedDeriv (n + 1) g
Tactic:
simp_rw [iteratedDeriv_succ', ← ih hf' hg', hfg]
Proof state after:
no goals
Theorem: W1.iteratedDeriv_sub
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
⊢ deriv (f - g) = deriv f - deriv g
Tactic:
ext x
Proof state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
x : ℝ
⊢ deriv (f - g) x = (deriv f - deriv g) x
Theorem: W1.iteratedDeriv_sub
Proof state before:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
x : ℝ
⊢ deriv (f - g) x = (deriv f - deriv g) x
Tactic:
apply deriv_sub
Proof state after:
case h.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
x : ℝ
⊢ DifferentiableAt ℝ (fun y => f y) x

case h.hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
x : ℝ
⊢ DifferentiableAt ℝ (fun y => g y) x
Theorem: W1.iteratedDeriv_sub
Proof state before:
case h.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
x : ℝ
⊢ DifferentiableAt ℝ (fun y => f y) x
Tactic:
exact (hf.differentiable (by simp)).differentiableAt
Proof state after:
no goals