Arithmetic on the difference-preserving main carrier

The common index remains part of the carrier. In particular its two forbidden diagonals are never reintroduced when either arithmetic mean is applied.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainRestrictedU (d n m m' : ℕ) (h : ℤ) : ℤ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainRestrictedU d n m m' h = h * ↑m' * (↑d * ↑n - ↑m)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainRestrictedMax (a : ℤ) (d N M H S : ℕ) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainRestrictedMax a d N M H S = 2 * a.natAbs * H * M * (d * N + M) * S

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainRestricted_numerator (d n m m' s s' : ℕ) (a h h' : ℤ) : iv3CorrelationNumerator d n m m' s s' a h h' = mainJointNumerator a (mainRestrictedU d n m m' h) (mainRestrictedU d n m' m h') s s'

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainRestrictedU_ne_zero {d n m m' : ℕ} {h : ℤ} (hh : h ≠ 0) (hm' : 0 < m') (hd : ↑d * ↑n - ↑m ≠ 0) : mainRestrictedU d n m m' h ≠ 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainRestrictedU_abs_le {d n m m' N M H : ℕ} {h : ℤ} (hn : n ≤ N) (hm : m ≤ M) (hm' : m' ≤ M) (hh : h.natAbs ≤ H) : (mainRestrictedU d n m m' h).natAbs ≤ H * M * (d * N + M)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainRestricted_joint_scale_le {d n m m' N M H S : ℕ} {a h h' : ℤ} (hn : n ≤ N) (hm : m ≤ M) (hm' : m' ≤ M) (hh : h.natAbs ≤ H) (hh' : h'.natAbs ≤ H) : a.natAbs * ((mainRestrictedU d n m m' h).natAbs + (mainRestrictedU d n m' m h').natAbs) * S ≤ mainRestrictedMax a d N M H S

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainRestricted_constant_le {d m m' s s' N M H S : ℕ} {a h h' : ℤ} (hm : m ≤ M) (hm' : m' ≤ M) (hs : s ≤ S) (hs' : s' ≤ S) (hh : h.natAbs ≤ H) (hh' : h'.natAbs ≤ H) : (iv3MainConstant m m' s s' a h h').natAbs ≤ mainRestrictedMax a d N M H S

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainRestrictedData (d : ℕ) (a : ℤ) (N M S : ℕ) (H : Finset ℤ) (v : WGramSecondaryBase) : Prop

The arithmetic assumptions on an arbitrary finite seven-coordinate carrier. Actual Gram membership will supply every conjunct.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainRestrictedData d a N M S H v = (v.1 ∈ Finset.Ioc 0 N ∧ v.2.1.1 ∈ Finset.Ioc 0 M ∧ v.2.2.1 ∈ Finset.Ioc 0 M ∧ v.2.1.2.1 ∈ Finset.Ioc 0 S ∧ v.2.2.2.1 ∈ Finset.Ioc 0 S ∧ v.2.1.2.2 ∈ H ∧ v.2.2.2.2 ∈ H ∧ ↑d * ↑v.1 - ↑v.2.1.1 ≠ 0 ∧ ↑d * ↑v.1 - ↑v.2.2.1 ≠ 0 ∧ v.2.2.2.2 * ↑v.2.1.2.1 ≠ v.2.1.2.2 * ↑v.2.2.2.1 ∧ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3CorrelationNumerator d v.1 v.2.1.1 v.2.2.1 v.2.1.2.1 v.2.2.2.1 a v.2.1.2.2 v.2.2.2.2 ≠ 0)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainRestricted_sum_fibers {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (G : Finset α) (π : α → β) (f : α → ℝ) : ∑ v ∈ G, f v = ∑ b ∈ Finset.image π G, ∑ v ∈ G with π v = b, f v

Summation over an image fiber keeps all ordered coordinates.