noncomputable def G12RectangleWF.omegaDensity : ArithmeticFunction ℝ

Pointwise conversion to the producer's omega convention.

Equations

• G12RectangleWF.omegaDensity = { toFun := fun (d : ℕ) => ↑d * AnalyticNumberTheory.Sieve.goldbachNu d, map_zero' := G12RectangleWF.omegaDensity._proof_1 }

theorem G12RectangleWF.omegaDensity_mult : omegaDensity.IsMultiplicative

theorem G12RectangleWF.density_eq : MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.primeDensity omegaDensity = AnalyticNumberTheory.Sieve.goldbachNu

theorem G12RectangleWF.local_density_bounds (N : ℕ) (hEven : Even N) (Z : ℝ) (p : ℕ) : p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z → 0 ≤ omegaDensity p / ↑p ∧ omegaDensity p / ↑p < 1

theorem G12RectangleWF.exists_local_dimension : ∃ (K : ℝ), 1 < K ∧ ∀ (N : ℕ), Even N → ∀ (Z : ℝ), MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.DimensionOneProductBound (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (⇑(MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.primeDensity omegaDensity)) K

One inherited B10 constant, uniform before every rectangle parameter.

noncomputable def G12RectangleWF.smallOutput (N : ℕ) (ε Z : ℝ) (M T : ℕ) : ℝ

Equations

• G12RectangleWF.smallOutput N ε Z M T = ∑ a ∈ G12RectangleWF.labels N ε M T, if G12RectangleWF.output N a < ⌈Z⌉₊ then 1 else 0

noncomputable def G12RectangleWF.primeCount (N : ℕ) (ε : ℝ) (M T : ℕ) : ℝ

Equations

• G12RectangleWF.primeCount N ε M T = ∑ a ∈ G12RectangleWF.labels N ε M T, if Nat.Prime (G12RectangleWF.output N a) then 1 else 0

theorem G12RectangleWF.primeCount_eq_original (N : ℕ) (ε : ℝ) (M T : ℕ) : primeCount N ε M T = 400 * ∑ p ∈ G12LowRectangle.rectangle N ε M T, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0

theorem G12RectangleWF.prime_le_sifted_small (N : ℕ) (ε Z : ℝ) (M T : ℕ) : primeCount N ε M T ≤ MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceSifted (labels N ε M T) (output N) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) + smallOutput N ε Z M T

theorem G12RectangleWF.exists_rectangle_sieve : ∃ (K : ℝ) (C : ℝ), 1 < K ∧ 0 < C ∧ ∀ (η : ℝ), 0 < η → η < 1 / 8 → ∃ (Q₀ : ℝ), 4 ≤ Q₀ ∧ ∀ (Q : ℝ), Q₀ ≤ Q → ∀ (N : ℕ), Even N → ∀ (ε Z : ℝ) (M T : ℕ), 2 ≤ Z → Z ≤ √Q → have P := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z; have D := MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η; have V := ∏ p ∈ P, (1 - AnalyticNumberTheory.Sieve.goldbachNu p); have E := C * (η + (η ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log Q ^ (-(1 / 3))); (∀ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true P D η Z, MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable (MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true P D η Z t) Q) ∧ primeCount N ε M T ≤ 400 * mass N ε M T * V * (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log Q / Real.log Z) + E) + MathlibNt.SieveTheory.LiLiuPrereqWF.externalRemainder true P D η Z (labels N ε M T) (output N) (400 * mass N ε M T) AnalyticNumberTheory.Sieve.goldbachNu + smallOutput N ε Z M T

The genuine producer is called on the actual repeated rectangle labels. The remainder is the signed sum of exactly the displayed family members.