Theorem: Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean)

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 : ℝ))
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

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]
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

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
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

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
State after:
no goals

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]
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)

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
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)

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]
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

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)
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

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
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)⁻¹

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
State after:
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ P.divisors ∧ ↑i ≤ x
⊢ 1 ≤ x * (↑i)⁻¹

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]
State after:
case h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ P.divisors ∧ ↑i ≤ x
⊢ 1 ≤ x / ↑i

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
State after:
no goals

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]
State after:
no goals

State before:
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ P.divisors ∧ ↑i ≤ x
⊢ 0 < ↑i
Tactic:
norm_cast
State after:
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
i : ℕ
hi : i ∈ P.divisors ∧ ↑i ≤ x
⊢ 0 < i

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
State after:
no goals