Helfgott's Proposition 6.2 on the ternary Goldbach minor arcs
Source: github.com/sthubbar/goldbach-lean/tree/d0d978d2cf565be71d69…
A Lean 4 proof of Lemma 6.1 and Proposition 6.2 of H. A. Helfgott, The ternary Goldbach conjecture is true, arXiv 1312.7748v2, Section 6.1, pages 46 to 48. Lemma 6.1 is a summation by parts bound. Proposition 6.2 turns l2 bounds on S1 over the major arcs and l-infinity bounds on S2 off them into a bound for the integral of |S1|^2 |S2| over the minor arcs, without the factor log x that a plain product of norms would lose. Lemma 6.1 is stated as in the paper. Proposition 6.2 is given in three forms: an abstract measure form with a natural upper endpoint; the arcs of display 3.5 for a finite…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-03-000029
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-03-000029/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-03-000029/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'