Issue 198 energy improvement

blueprint/src/chapter/zero_density_energy.tex

@@ -404,6 +404,45 @@ \section{Known additive energy bounds}
 for $4\sigma - 2 \le \tau' \le 3\sigma - 1$. The treatment is analogous to before, so we omit the proof.
 \end{proof}
 
+Combining the Heath--Brown relations with the third Guth--Maynard relation (Lemma \ref{gm-3}) improves Theorem \ref{hb-energy-bound} in the range $2/3 \le \sigma \le 3/4$.
+
+\begin{theorem}\label{imp-energy-bound1}
+For $2/3 \le \sigma \le 3/4$, one has
+\begin{align*}
+\A^*(\sigma) &\le \frac{10 - 11\sigma}{(2 - \sigma)(1 - \sigma)}, && \frac{2}{3} \le \sigma \le \frac{5}{7},\\
+\A^*(\sigma) &\le \frac{3(25 - 27\sigma)}{8(2 - \sigma)(1 - \sigma)}, && \frac{5}{7} \le \sigma \le \frac{315}{433},\\
+\A^*(\sigma) &\le \frac{2(45 - 44\sigma)}{(2\sigma + 15)(1 - \sigma)}, && \frac{315}{433} \le \sigma \le \frac{3}{4}.
+\end{align*}
+\end{theorem}
+
+\derived
+\code{prove_heath_brown_guth_maynard_energy_estimate()}
+
+\begin{proof}\uses{zeroe-large-cor-0, l2-mvt, hbt, hb-energy-simp, gm-3, power-energy}
+Take $\tau_0=2$ in Corollary \ref{zeroe-large-cor-0}. The $\LV^*_{\zeta}$ supremum is now trivial, so it remains to bound $\rho^*/\tau$ for $(\sigma,\tau,\rho,\rho^*,s)\in\Energy$ with $2\leq\tau\leq4$. The relevant large-value-energy region is obtained by intersecting the $L^2$ large-value consequence from \Cref{l2-mvt}, the Heath--Brown regions \Cref{hbt,hb-energy-simp}, the third Guth--Maynard energy relation \Cref{gm-3}, and their $k=2,3,4$ power transforms from \Cref{power-energy}. Starting from the $L^2$ estimate and Heath--Brown region 2b, adding either \Cref{hbt} or \Cref{gm-3} alone is insufficient; the claimed bounds arise when both are included in the full intersection.
+
+Exact polyhedral elimination of this intersection, as implemented by \code{prove_heath_brown_guth_maynard_energy_estimate()}, gives the three bounds in the statement. The first two transition profiles can be seen explicitly. They share
+\[
+\tau=2(2-\sigma), \qquad \rho=6(1-\sigma),
+\]
+while the two $k=2$ branches of the third Guth--Maynard energy relation give respectively
+\[
+\rho^*=2(10-11\sigma), \qquad \rho^*=\frac{3(25-27\sigma)}{4}.
+\]
+Their difference is $(7\sigma-5)/4$, so they cross exactly at $\sigma=5/7$. Consequently the corresponding values of $\rho^*/\tau$ are
+\[
+\frac{10-11\sigma}{2-\sigma}
+\qquad\text{and}\qquad
+\frac{3(25-27\sigma)}{8(2-\sigma)}.
+\]
+The second and third pieces meet because
+\[
+\frac{3(25-27\sigma)}{8(2-\sigma)}
+=\frac{2(45-44\sigma)}{2\sigma+15}
+\]
+at $\sigma=315/433$. These extremal profiles explain the two transition points; the upper bounds themselves follow from the exact calculation using the full intersection described above.
+\end{proof}
+
 Using Theorem \ref{guth-maynard-lvt}, it is possible to obtain improved energy estimates near $\sigma = 3/4$, which are given by the next two theorems.
 
 \begin{theorem}\label{imp-energy-bound2}
@@ -1127,9 +1166,11 @@ \section{Known additive energy bounds}
     \hline
     $\dfrac{10 - 11\sigma}{(2 - \sigma)(1 - \sigma)}$ & $\dfrac{1}{2} \leq \sigma \le \dfrac{2}{3} = 0.6666\ldots$ & Theorem \ref{hb-energy-bound}\\
     \hline
-    $\dfrac{18 - 19\sigma}{(4 - 2\sigma)(1 - \sigma)}$ & $\dfrac{2}{3} \leq \sigma \le \dfrac{7}{10} = 0.7$ & Theorem \ref{hb-energy-bound}\\
+    $\dfrac{10 - 11\sigma}{(2 - \sigma)(1 - \sigma)}$ & $\dfrac{2}{3} \leq \sigma \le \dfrac{5}{7} = 0.7142\ldots$ & Theorem \ref{imp-energy-bound1}\\
+    \hline
+    $\dfrac{3(25 - 27\sigma)}{8(2 - \sigma)(1 - \sigma)}$ & $\dfrac{5}{7} \leq \sigma \le \dfrac{626 - \sqrt{3301}}{785} = 0.7242\ldots$ & Theorem \ref{imp-energy-bound1}\\
     \hline
-    $\dfrac{5(18 - 19\sigma)}{2(5\sigma + 3)(1 - \sigma)}$ & $\dfrac{7}{10} \leq \sigma \le \dfrac{539 - \sqrt{42121}}{460} = 0.7255\ldots$ & Theorem \ref{imp-energy-bound2}\\
+    $\dfrac{5(18 - 19\sigma)}{2(5\sigma + 3)(1 - \sigma)}$ & $\dfrac{626 - \sqrt{3301}}{785} \leq \sigma \le \dfrac{539 - \sqrt{42121}}{460} = 0.7255\ldots$ & Theorem \ref{imp-energy-bound2}\\
     \hline
     $\dfrac{2(45 - 44\sigma)}{(2\sigma + 15)(1 - \sigma)}$ & $\dfrac{539 - \sqrt{42121}}{460} \leq \sigma \le \dfrac{165}{226} = 0.7300\ldots$ & Theorem \ref{imp-energy-bound2}\\
     \hline

blueprint/src/python/derived.py

@@ -1119,6 +1119,27 @@ def prove_improved_heath_brown_energy_estimate():
     LVZ_star_hyp = ad.compute_LV_star(hypotheses, LVER_zeta_domain, zeta=True)
     bounds = ze.lver_to_energy_bound(LV_star_hyp, LVZ_star_hyp, Interval(frac(1,2), 1))
 
+def prove_heath_brown_guth_maynard_energy_estimate():
+    hypotheses = Hypothesis_Set()
+
+    for k in range(2, 5):
+        hypotheses.add_hypothesis(ad.get_raise_to_power_hypothesis(k))
+
+    # Add classical and literature Large value estimates
+    hypotheses.add_hypothesis(lv.large_value_estimate_L2)
+    hypotheses.add_hypothesis(literature.find_hypothesis(name="Heath-Brown large value energy region 2a"))
+    hypotheses.add_hypothesis(literature.find_hypothesis(name="Heath-Brown large value energy region 2b"))
+    hypotheses.add_hypothesis(literature.find_hypothesis(name="Guth--Maynard large value energy region 3"))
+
+    # Convert all large value estimates -> large value energy region
+    hypotheses.add_hypotheses(ad.lv_to_lver(hypotheses, zeta=False))
+
+    tau0 = Affine(0, 2, Interval(frac(2,3), frac(3,4)))
+    hs = ze.lver_to_energy_bound(hypotheses, tau0, debug=False)
+    for h in hs:
+        print(h.data)
+    return hs
+
 def prove_zero_density_energy_2():
     hypotheses = Hypothesis_Set()
 
@@ -1398,6 +1419,7 @@ def prove_zero_density_energy_13():
 def prove_all_zero_density_energy_estimates():
     prove_heath_brown_energy_estimate()
     prove_improved_heath_brown_energy_estimate()
+    prove_heath_brown_guth_maynard_energy_estimate()
     prove_zero_density_energy_2()
     prove_zero_density_energy_3()
     prove_zero_density_energy_4()

blueprint/src/python/visualizations.py

@@ -257,9 +257,12 @@ def zero_density_energy_plot():
     ze.add_trivial_zero_density_energy_estimates(hypotheses)
 
     # List of new derived estimates so far. TODO: replace with actual derivations
+    crossover = (626 - math.sqrt(3301)) / 785
     energy_estimates = [
             (RF.parse("1000000"), Interval(frac(1,2), 1)), # default
-            (RF.parse("5 * (18 - 19 * x) / (2 * (5 * x + 3) * (1 - x))"), Interval(frac(7,10), 0.7255)),
+            (RF.parse("(10 - 11 * x) / ((2 - x) * (1 - x))"), Interval(frac(2,3), frac(5,7))),
+            (RF.parse("3 * (25 - 27 * x) / (8 * (2 - x) * (1 - x))"), Interval(frac(5,7), crossover)),
+            (RF.parse("5 * (18 - 19 * x) / (2 * (5 * x + 3) * (1 - x))"), Interval(crossover, 0.7255)),
             (RF.parse("2 * (45 - 44 * x) / ((2 * x + 15) * (1 - x))"), Interval(0.7255, 0.73)),
             (RF.parse("(457 - 546 * x) / (2 * (61 - 58 * x) * (1 - x))"), Interval(0.73, 0.7373)),
             (RF.parse("5 * (18 - 19 * x) / (2 * (5 * x + 3) * (1 - x))"), Interval(0.7373, frac(42,55))),

blueprint/src/python/zero_density_energy_estimate.py

@@ -323,7 +323,11 @@ def lver_to_energy_bound(
 
     # Take maximum
     bounds = [(f[0], f[1]) for f in fns]
-    sup = RF.max(bounds, sigma_interval)
+    sup = RF.max(
+        bounds,
+        sigma_interval,
+        track_dependencies=False
+    )
     return [
         derived_zero_density_energy_estimate(
             # Remember to divide by (1 - \\sigma)