Theorem: BrunTitchmarsh.multSum_eq (PrimeNumberTheoremAnd/BrunTitchmarsh.lean)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (primeInterSieve x y z hz).multSum d = ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d)
Tactic:
unfold Sieve.multSum
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (∑ n ∈ (primeInterSieve x y z hz).support, if d ∣ n then (primeInterSieve x y z hz).weights n else 0) =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (∑ n ∈ (primeInterSieve x y z hz).support, if d ∣ n then (primeInterSieve x y z hz).weights n else 0) =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d)
Tactic:
rw[primeInterSieve]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (∑
      n ∈
        { support := Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊, prodPrimes := primorial ⌊z⌋₊, prodPrimes_squarefree := ⋯,
            weights := fun x => 1, weights_nonneg := primeInterSieve.proof_2, totalMass := y,
            nu := (↑ζ).pdiv ↑ArithmeticFunction.id, nu_mult := primeInterSieve.proof_3, nu_pos_of_prime := ⋯,
            nu_lt_one_of_prime := ⋯, level := z, one_le_level := hz }.support,
      if d ∣ n then
        { support := Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊, prodPrimes := primorial ⌊z⌋₊, prodPrimes_squarefree := ⋯,
              weights := fun x => 1, weights_nonneg := primeInterSieve.proof_2, totalMass := y,
              nu := (↑ζ).pdiv ↑ArithmeticFunction.id, nu_mult := primeInterSieve.proof_3, nu_pos_of_prime := ⋯,
              nu_lt_one_of_prime := ⋯, level := z, one_le_level := hz }.weights
          n
      else 0) =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (∑
      n ∈
        { support := Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊, prodPrimes := primorial ⌊z⌋₊, prodPrimes_squarefree := ⋯,
            weights := fun x => 1, weights_nonneg := primeInterSieve.proof_2, totalMass := y,
            nu := (↑ζ).pdiv ↑ArithmeticFunction.id, nu_mult := primeInterSieve.proof_3, nu_pos_of_prime := ⋯,
            nu_lt_one_of_prime := ⋯, level := z, one_le_level := hz }.support,
      if d ∣ n then
        { support := Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊, prodPrimes := primorial ⌊z⌋₊, prodPrimes_squarefree := ⋯,
              weights := fun x => 1, weights_nonneg := primeInterSieve.proof_2, totalMass := y,
              nu := (↑ζ).pdiv ↑ArithmeticFunction.id, nu_mult := primeInterSieve.proof_3, nu_pos_of_prime := ⋯,
              nu_lt_one_of_prime := ⋯, level := z, one_le_level := hz }.weights
          n
      else 0) =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d)
Tactic:
simp only [Finset.sum_boole, Nat.cast_inj]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (Finset.filter (fun x => d ∣ x) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card = ⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (Finset.filter (fun x => d ∣ x) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card =
    (Finset.filter (fun x => d ∣ x) (Finset.Ioc (⌈x⌉₊ - 1) ⌊x + y⌋₊)).card
Tactic:
rw [←Nat.Icc_succ_left]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (Finset.filter (fun x => d ∣ x) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card =
    (Finset.filter (fun x => d ∣ x) (Finset.Icc (⌈x⌉₊ - 1).succ ⌊x + y⌋₊)).card

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (Finset.filter (fun x => d ∣ x) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card =
    (Finset.filter (fun x => d ∣ x) (Finset.Icc (⌈x⌉₊ - 1).succ ⌊x + y⌋₊)).card
Tactic:
congr
State after:
case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ⌈x⌉₊ = (⌈x⌉₊ - 1).succ

State before:
case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ⌈x⌉₊ = (⌈x⌉₊ - 1).succ
Tactic:
rw [←Nat.succ_sub]
State after:
case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ⌈x⌉₊ = ⌈x⌉₊.succ - 1

case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 1 ≤ ⌈x⌉₊

State before:
case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ⌈x⌉₊ = ⌈x⌉₊.succ - 1

case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 1 ≤ ⌈x⌉₊
Tactic:
rfl
State after:
case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 1 ≤ ⌈x⌉₊

State before:
case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 1 ≤ ⌈x⌉₊
Tactic:
simp [hx]
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (Finset.filter (fun x => d ∣ x) (Finset.Ioc (⌈x⌉₊ - 1) ⌊x + y⌋₊)).card = ⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d
Tactic:
rw[BrunTitchmarsh.card_Ioc_filter_dvd _ _ _ hd]
State after:
no goals