Theorem: Sieve.prod_factors_one_div_compMult_ge (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean)

State before:
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
⊢ f d * ∏ p ∈ d.primeFactors, 1 / (1 - f p) = ∏ p ∈ d.primeFactors, f p / (1 - f p)
Tactic:
conv => { lhs; congr; rw [←Nat.prod_primeFactors_of_squarefree hd] }
State after:
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
⊢ f (∏ p ∈ d.primeFactors, p) * ∏ p ∈ d.primeFactors, 1 / (1 - f p) = ∏ p ∈ d.primeFactors, f p / (1 - f p)

State before:
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
⊢ f (∏ p ∈ d.primeFactors, p) * ∏ p ∈ d.primeFactors, 1 / (1 - f p) = ∏ p ∈ d.primeFactors, f p / (1 - f p)
Tactic:
rw [hf.isMultiplicative.map_prod_of_subset_primeFactors _ _ subset_rfl,
  ←Finset.prod_mul_distrib]
State after:
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
⊢ ∏ x ∈ d.primeFactors, f x * (1 / (1 - f x)) = ∏ p ∈ d.primeFactors, f p / (1 - f p)

State before:
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
⊢ ∏ x ∈ d.primeFactors, f x * (1 / (1 - f x)) = ∏ p ∈ d.primeFactors, f p / (1 - f p)
Tactic:
simp_rw[one_div, div_eq_mul_inv]
State after:
no goals

State before:
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
⊢ ∏ p ∈ d.primeFactors, f p / (1 - f p) ≥ ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, f p ^ n
Tactic:
gcongr with p hp
State after:
case h0
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
⊢ ∀ i ∈ d.primeFactors, 0 ≤ ∑ n ∈ Finset.Icc 1 M, f i ^ n

case h1
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p ∈ d.primeFactors
⊢ ∑ n ∈ Finset.Icc 1 M, f p ^ n ≤ f p / (1 - f p)

State before:
case h1
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p ∈ d.primeFactors
⊢ ∑ n ∈ Finset.Icc 1 M, f p ^ n ≤ f p / (1 - f p)
Tactic:
rw [Nat.mem_primeFactors_of_ne_zero hd.ne_zero] at hp
State after:
case h1
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ ∑ n ∈ Finset.Icc 1 M, f p ^ n ≤ f p / (1 - f p)

State before:
case h1
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ ∑ n ∈ Finset.Icc 1 M, f p ^ n ≤ f p / (1 - f p)
Tactic:
rw [←Nat.Ico_succ_right, geom_sum_Ico, ←mul_div_mul_left (c:= (-1:ℝ)) (f p ^ Nat.succ M - f p ^ 1)]
State after:
case h1
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ -1 * (f p ^ M.succ - f p ^ 1) / (-1 * (f p - 1)) ≤ f p / (1 - f p)

case h1.hc
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ -1 ≠ 0

case h1.hx
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ f p ≠ 1

case h1.hmn
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ 1 ≤ M.succ

State before:
case h1
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ -1 * (f p ^ M.succ - f p ^ 1) / (-1 * (f p - 1)) ≤ f p / (1 - f p)

case h1.hc
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ -1 ≠ 0

case h1.hx
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ f p ≠ 1

case h1.hmn
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ 1 ≤ M.succ
Tactic:
gcongr
State after:
case h1.hc
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ 0 ≤ f p

case h1.hd
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ 0 < 1 - f p

case h1.hac
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ -1 * (f p ^ M.succ - f p ^ 1) ≤ f p

case h1.hbd
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ 1 - f p ≤ -1 * (f p - 1)

case h1.hc
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ -1 ≠ 0

case h1.hx
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ f p ≠ 1

case h1.hmn
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ 1 ≤ M.succ

State before:
case h0
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
⊢ ∀ i ∈ d.primeFactors, 0 ≤ ∑ n ∈ Finset.Icc 1 M, f i ^ n
Tactic:
exact fun p _ => Finset.sum_nonneg fun n _ => pow_nonneg (hf_nonneg p) n
State after:
no goals

State before:
case h1.hc
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ 0 ≤ f p
Tactic:
apply hf_nonneg
State after:
no goals

State before:
case h1.hd
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ 0 < 1 - f p
Tactic:
linarith [hf_size p hp.1 hp.2]
State after:
no goals

State before:
case h1.hac
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ -1 * (f p ^ M.succ - f p ^ 1) ≤ f p
Tactic:
rw [pow_one]
State after:
case h1.hac
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ -1 * (f p ^ M.succ - f p) ≤ f p

State before:
case h1.hac
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ -1 * (f p ^ M.succ - f p) ≤ f p
Tactic:
have : 0 ≤ f p ^ (M.succ) := by
  apply pow_nonneg
  apply hf_nonneg
State after:
case h1.hac
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
this : 0 ≤ f p ^ M.succ
⊢ -1 * (f p ^ M.succ - f p) ≤ f p

State before:
case h1.hac
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
this : 0 ≤ f p ^ M.succ
⊢ -1 * (f p ^ M.succ - f p) ≤ f p
Tactic:
linarith only [this]
State after:
no goals

State before:
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ 0 ≤ f p ^ M.succ
Tactic:
apply pow_nonneg
State after:
case H
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ 0 ≤ f p

State before:
case H
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ 0 ≤ f p
Tactic:
apply hf_nonneg
State after:
no goals

State before:
case h1.hbd
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ 1 - f p ≤ -1 * (f p - 1)
Tactic:
linarith only
State after:
no goals

State before:
case h1.hc
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ -1 ≠ 0
Tactic:
norm_num
State after:
no goals

State before:
case h1.hx
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ f p ≠ 1
Tactic:
apply ne_of_lt $ hf_size p hp.1 hp.2
State after:
no goals

State before:
case h1.hmn
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
⊢ 1 ≤ M.succ
Tactic:
apply Nat.succ_le_iff.mpr (Nat.succ_pos _)
State after:
no goals

State before:
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
⊢ ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, f p ^ n = ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, f (p ^ n)
Tactic:
simp_rw [hf.apply_pow]
State after:
no goals