internlm/Lean-Github huggingface dataset:
Theorem: Sieve.CompletelyMultiplicative.zeta
Proof state before:
case neg.hnc
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ ¬(a = 0 ∨ b = 0)
Tactic:
push_neg
Proof state after:
case neg.hnc
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ a ≠ 0 ∧ b ≠ 0
Theorem: Sieve.CompletelyMultiplicative.zeta
Proof state before:
case neg.hnc
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ a ≠ 0 ∧ b ≠ 0
Tactic:
exact ⟨ha, hb⟩
Proof state after:
no goals
Theorem: Sieve.CompletelyMultiplicative.zeta
Proof state before:
case pos
a b : ℕ
ha : a = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
Tactic:
simp [ha]
Proof state after:
no goals
Theorem: Sieve.CompletelyMultiplicative.zeta
Proof state before:
case pos
a b : ℕ
ha : ¬a = 0
hb : b = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
Tactic:
simp [hb]
Proof state after:
no goals
Theorem: Sieve.CompletelyMultiplicative.id
Proof state before:
⊢ CompletelyMultiplicative ↑ArithmeticFunction.id
Tactic:
constructor <;> simp
Proof state after:
no goals
Theorem: Sieve.CompletelyMultiplicative.pmul
Proof state before:
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ CompletelyMultiplicative (f.pmul g)
Tactic:
constructor
Proof state after:
case left
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ (f.pmul g) 1 = 1

case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ ∀ (a b : ℕ), (f.pmul g) (a * b) = (f.pmul g) a * (f.pmul g) b
Theorem: Sieve.CompletelyMultiplicative.pmul
Proof state before:
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ ∀ (a b : ℕ), (f.pmul g) (a * b) = (f.pmul g) a * (f.pmul g) b
Tactic:
intro a b
Proof state after:
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ (f.pmul g) (a * b) = (f.pmul g) a * (f.pmul g) b
Theorem: Sieve.CompletelyMultiplicative.pmul
Proof state before:
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ (f.pmul g) (a * b) = (f.pmul g) a * (f.pmul g) b
Tactic:
simp_rw [pmul_apply, hf.2, hg.2]
Proof state after:
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ f a * f b * (g a * g b) = f a * g a * (f b * g b)
Theorem: Sieve.CompletelyMultiplicative.pmul
Proof state before:
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ f a * f b * (g a * g b) = f a * g a * (f b * g b)
Tactic:
ring
Proof state after:
no goals
Theorem: Sieve.CompletelyMultiplicative.pmul
Proof state before:
case left
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ (f.pmul g) 1 = 1
Tactic:
rw [pmul_apply, hf.1, hg.1, mul_one]
Proof state after:
no goals
Theorem: Sieve.CompletelyMultiplicative.pdiv
Proof state before:
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ CompletelyMultiplicative (f.pdiv g)
Tactic:
constructor
Proof state after:
case left
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ (f.pdiv g) 1 = 1

case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ ∀ (a b : ℕ), (f.pdiv g) (a * b) = (f.pdiv g) a * (f.pdiv g) b
Theorem: Sieve.CompletelyMultiplicative.pdiv
Proof state before:
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ ∀ (a b : ℕ), (f.pdiv g) (a * b) = (f.pdiv g) a * (f.pdiv g) b
Tactic:
intro a b
Proof state after:
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ (f.pdiv g) (a * b) = (f.pdiv g) a * (f.pdiv g) b
Theorem: Sieve.CompletelyMultiplicative.pdiv
Proof state before:
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ (f.pdiv g) (a * b) = (f.pdiv g) a * (f.pdiv g) b
Tactic:
simp_rw [pdiv_apply, hf.2, hg.2]
Proof state after:
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ f a * f b / (g a * g b) = f a / g a * (f b / g b)
Theorem: Sieve.CompletelyMultiplicative.pdiv
Proof state before:
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ f a * f b / (g a * g b) = f a / g a * (f b / g b)
Tactic:
ring
Proof state after:
no goals
Theorem: Sieve.CompletelyMultiplicative.pdiv
Proof state before:
case left
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ (f.pdiv g) 1 = 1
Tactic:
rw [pdiv_apply, hf.1, hg.1, div_one]
Proof state after:
no goals
Theorem: Sieve.CompletelyMultiplicative.apply_pow
Proof state before:
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
a n : ℕ
⊢ f (a ^ n) = f a ^ n
Tactic:
induction n with
| zero => simp_rw [pow_zero, hf.1]
| succ n' ih => simp_rw [pow_succ, hf.2, ih]
Proof state after:
no goals
Theorem: Sieve.CompletelyMultiplicative.apply_pow
Proof state before:
case zero
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
a : ℕ
⊢ f (a ^ 0) = f a ^ 0
Tactic:
simp_rw [pow_zero, hf.1]
Proof state after:
no goals
Theorem: Sieve.CompletelyMultiplicative.apply_pow
Proof state before:
case succ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
a n' : ℕ
ih : f (a ^ n') = f a ^ n'
⊢ f (a ^ (n' + 1)) = f a ^ (n' + 1)
Tactic:
simp_rw [pow_succ, hf.2, ih]
Proof state after:
no goals
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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] }
Proof 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)
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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]
Proof 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)
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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]
Proof state after:
no goals
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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
Proof 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)
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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
Proof 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)
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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)]
Proof 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
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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
Proof 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
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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
Proof state after:
no goals
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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
Proof state after:
no goals
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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]
Proof state after:
no goals
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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]
Proof 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
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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
Proof 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
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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]
Proof state after:
no goals
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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
Proof 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
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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
Proof state after:
no goals
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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
Proof state after:
no goals
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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
Proof state after:
no goals
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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
Proof state after:
no goals
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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 _)
Proof state after:
no goals
Theorem: Sieve.prod_factors_one_div_compMult_ge
Proof 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]
Proof state after:
no goals
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
⊢ ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, f (p ^ n) = ∑ m ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors, f m
Tactic:
rw [Finset.prod_sum]
Proof state after:
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
⊢ ∑ p ∈ d.primeFactors.pi fun p => Finset.Icc 1 M, ∏ x ∈ d.primeFactors.attach, f (↑x ^ p ↑x ⋯) =
    ∑ m ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors, f m
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
⊢ ∑ p ∈ d.primeFactors.pi fun p => Finset.Icc 1 M, ∏ x ∈ d.primeFactors.attach, f (↑x ^ p ↑x ⋯) =
    ∑ m ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors, f m
Tactic:
let i : (a:_) → (ha : a ∈ Finset.pi d.primeFactors fun p => Finset.Icc 1 M) → ℕ :=
  fun a _ => ∏ p in d.primeFactors.attach, p.1 ^ (a p p.2)
Proof state after:
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
⊢ ∑ p ∈ d.primeFactors.pi fun p => Finset.Icc 1 M, ∏ x ∈ d.primeFactors.attach, f (↑x ^ p ↑x ⋯) =
    ∑ m ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors, f m
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
⊢ ∑ p ∈ d.primeFactors.pi fun p => Finset.Icc 1 M, ∏ x ∈ d.primeFactors.attach, f (↑x ^ p ↑x ⋯) =
    ∑ m ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors, f m
Tactic:
have hi_ne_zero : ∀ (a : _) (ha : a ∈ Finset.pi d.primeFactors fun _p => Finset.Icc 1 M),
    i a ha ≠ 0 := by
  intro a ha
  erw [Finset.prod_ne_zero_iff]
  exact fun p _ => pow_ne_zero _ (ne_of_gt (Nat.pos_of_mem_factors (List.mem_toFinset.mp p.property)))
Proof state after:
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
⊢ ∑ p ∈ d.primeFactors.pi fun p => Finset.Icc 1 M, ∏ x ∈ d.primeFactors.attach, f (↑x ^ p ↑x ⋯) =
    ∑ m ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors, f m
Theorem: Sieve.prod_factors_sum_pow_compMult
Proof state before:
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
⊢ ∑ p ∈ d.primeFactors.pi fun p => Finset.Icc 1 M, ∏ x ∈ d.primeFactors.attach, f (↑x ^ p ↑x ⋯) =
    ∑ m ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors, f m
Tactic:
have h : ∀ (a : _) (ha : a ∈ Finset.pi d.primeFactors fun _p => Finset.Icc 1 M),
    ∏ p in d.primeFactors.attach, f (p.1 ^ (a p p.2)) = f (i a ha) := by
  intro a ha
  apply symm
  apply hf.isMultiplicative.map_prod
  intro x _ y _ hxy
  simp_rw [Finset.mem_pi, Finset.mem_Icc, Nat.succ_le] at ha
  apply (Nat.coprime_pow_left_iff (ha x x.2).1 ..).mpr
  apply (Nat.coprime_pow_right_iff (ha y y.2).1 ..).mpr
  have hxp := Nat.prime_of_mem_factors (List.mem_toFinset.mp x.2)
  rw [Nat.Prime.coprime_iff_not_dvd hxp]
  rw [Nat.prime_dvd_prime_iff_eq hxp $ Nat.prime_of_mem_factors (List.mem_toFinset.mp y.2)]
  exact fun hc => hxy (Subtype.eq hc)
Proof state after:
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
h :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    ∏ p ∈ d.primeFactors.attach, f (↑p ^ a ↑p ⋯) = f (i a ha)
⊢ ∑ p ∈ d.primeFactors.pi fun p => Finset.Icc 1 M, ∏ x ∈ d.primeFactors.attach, f (↑x ^ p ↑x ⋯) =
    ∑ m ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors, f m