noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.B10PanGeometryUpperWindow (N : ℕ) (γ : ℝ) : ℕ

The common upper Pan window used to consume the actual C10 support at both x = N and x = ⌊εN⌋.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.B10PanGeometryUpperWindow N γ = ⌊↑N ^ ((1 + γ) / 2)⌋₊

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.B10PanGeometry_support_le_upperWindow {N : ℕ} {β γ : ℝ} {m : ℕ} (hN : 2 ≤ N) (hγ : γ < 1 / 3) (hm : m ∈ goldbachC10ProductSupport N (↑N ^ β) (↑N ^ γ)) : m ≤ B10PanGeometryUpperWindow N γ

Every actual support point lies below the common upper window.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.B10PanGeometry_upperWindow_le_rpow_two_thirds {N : ℕ} (hN : 1 ≤ N) {γ : ℝ} (hγ : γ < 1 / 3) : ↑(B10PanGeometryUpperWindow N γ) ≤ ↑N ^ (2 / 3)

The common upper window is admissible for the original x = N scale.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.B10PanGeometry_upperWindow_le_scaled_floor_rpow_eventually (ε γ : ℝ) (hε : 0 < ε) (hγ : γ < 1 / 3) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ↑(B10PanGeometryUpperWindow N γ) ≤ ↑⌊ε * ↑N⌋₊ ^ (2 / 3)

The common upper window is eventually admissible for the smaller endpoint x = ⌊εN⌋.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.B10PanGeometry_support_mem_commonWindow_eventually (ε γ B : ℝ) (hε : 0 < ε) (hεlt : ε < 1) (hγ : γ < 1 / 3) (hB : 0 ≤ B) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → have A₁ := LiuWeight.liuPanSourceIntervalLower N B; have A₂ := B10PanGeometryUpperWindow N γ; Real.log ↑N ^ (2 * B) ≤ ↑A₁ ∧ Real.log ↑⌊ε * ↑N⌋₊ ^ (2 * B) ≤ ↑A₁ ∧ ↑A₂ ≤ ↑⌊ε * ↑N⌋₊ ^ (2 / 3) ∧ ↑A₂ ≤ ↑N ^ (2 / 3) ∧ ∀ (β : ℝ), 1 / 18 < β → ∀ m ∈ goldbachC10ProductSupport N (↑N ^ β) (↑N ^ γ), m ∈ Finset.Ioc A₁ A₂

The original lower Pan window also covers the smaller endpoint x = ⌊εN⌋, and together with the common upper window it contains every actual support point.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.B10PanGeometry_panModulusCutoff_comparison_eventually (ε B : ℝ) (hε : 0 < ε) (hεlt : ε < 1) (hB : 0 ≤ B) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → LiuWeight.panModulusCutoff N (B + 1) ≤ LiuWeight.panModulusCutoff ⌊ε * ↑N⌋₊ B ∧ LiuWeight.panModulusCutoff N (B + 1) ≤ LiuWeight.panModulusCutoff N B

The smaller-endpoint modulus cutoff with exponent B eventually dominates the original-scale cutoff with exponent B + 1; the latter is also bounded by the original cutoff with exponent B.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.B10PanGeometry_scaled_div_log_rpow_le_eventually (ε U : ℝ) (hε : 0 < ε) (hεlt : ε < 1) (hU : 0 ≤ U) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ↑⌊ε * ↑N⌋₊ / Real.log ↑⌊ε * ↑N⌋₊ ^ U ≤ 2 ^ U * ↑N / Real.log ↑N ^ U

The smaller endpoint carries at most the original N / log(N)^U scale up to the explicit factor 2^U.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.B10PanGeometry_consumer_threshold (ε γ B U : ℝ) (K : ℕ) (hε : 0 < ε) (hεlt : ε < 1) (hγ : γ < 1 / 3) (hB : 0 ≤ B) (hU : 0 ≤ U) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → K ≤ N ∧ K ≤ ⌊ε * ↑N⌋₊ ∧ 2 ≤ ⌊ε * ↑N⌋₊ ∧ have A₁ := LiuWeight.liuPanSourceIntervalLower N B; have A₂ := B10PanGeometryUpperWindow N γ; Real.log ↑N ^ (2 * B) ≤ ↑A₁ ∧ Real.log ↑⌊ε * ↑N⌋₊ ^ (2 * B) ≤ ↑A₁ ∧ ↑A₂ ≤ ↑⌊ε * ↑N⌋₊ ^ (2 / 3) ∧ ↑A₂ ≤ ↑N ^ (2 / 3) ∧ LiuWeight.panModulusCutoff N (B + 1) ≤ LiuWeight.panModulusCutoff ⌊ε * ↑N⌋₊ B ∧ LiuWeight.panModulusCutoff N (B + 1) ≤ LiuWeight.panModulusCutoff N B ∧ ↑⌊ε * ↑N⌋₊ / Real.log ↑⌊ε * ↑N⌋₊ ^ U ≤ 2 ^ U * ↑N / Real.log ↑N ^ U ∧ ∀ (β : ℝ), 1 / 18 < β → ∀ m ∈ goldbachC10ProductSupport N (↑N ^ β) (↑N ^ γ), m ∈ Finset.Ioc A₁ A₂

Threshold form of the combined B10 Pan-geometry packet.