diff --git a/blueprint/src/python/derived.py b/blueprint/src/python/derived.py index 818ef1b..e16d677 100644 --- a/blueprint/src/python/derived.py +++ b/blueprint/src/python/derived.py @@ -979,33 +979,12 @@ def prove_heath_brown_energy_estimate(): hypotheses.add_hypothesis(literature.find_hypothesis(keywords="Heath-Brown large value energy region 2b")) hypotheses.add_hypotheses(ad.lv_to_lver(hypotheses, zeta=False)) - # tau_0 as an affine function + # tau_0 as an affine function. lver_to_energy_bound builds the + # tau0 <= tau <= 2 tau0 and 2 <= tau <= tau0 domains itself. tau0 = Affine(0, 2, Interval(frac(1,2), frac(3,4))) - LVER_domain = Region.from_polytope( - Polytope([ - [-tau0.domain.x0, 1, 0], # sigma >= sigma_interval.x0 - [tau0.domain.x1, -1, 0], # sigma <= sigma_interval.x1 - [-tau0.c, -tau0.m, 1], # tau >= tau0 = m sigma + c - [2 * tau0.c, 2 * tau0.m, -1] # tau <= 2 tau0 = 2 m sigma + 2 c - ]) - ) - - # Compute the feasible region for LV*(s, t) as a 3-dimensional polytope - LV_star_hyp = ad.compute_LV_star(hypotheses, LVER_domain, zeta=False, debug=False) - - # domain representing 2 <= tau <= tau0 - LVER_zeta_domain = Region.from_polytope( - Polytope([ - [-tau0.domain.x0, 1, 0], # sigma >= sigma_interval.x0 - [tau0.domain.x1, -1, 0], # sigma <= sigma_interval.x1 - [-2, 0, 1], # tau0 >= 2 - [tau0.c, tau0.m, -1], # tau <= tau0 = m sigma + c - ]) - ) - # Compute the feasible region for LV_{\zeta}*(s, t) as a 3-dimensional polytope - LVZ_star_hyp = ad.compute_LV_star(hypotheses, LVER_zeta_domain, zeta=True, debug=False) - ze.lver_to_energy_bound(LV_star_hyp, LVZ_star_hyp, tau0.domain) - + hs = ze.lver_to_energy_bound(hypotheses, tau0, debug=False) + for h in hs: + print(h.data) # Part 2: \sigma \in [3/4, 25/28] ---------------------------------------------------------- @@ -1025,39 +1004,15 @@ def prove_heath_brown_energy_estimate(): # tau_0 as an affine function tau0 = Affine(4, -1, Interval(frac(3,4), frac(25,28))) - - LVER_domain = Region.from_polytope( - Polytope([ - [-tau0.domain.x0, 1, 0], # sigma >= sigma_interval.x0 - [tau0.domain.x1, -1, 0], # sigma <= sigma_interval.x1 - [-tau0.c, -tau0.m, 1], # tau >= tau0 = m sigma + c - [2 * tau0.c, 2 * tau0.m, -1] # tau <= 2 tau0 = 2 m sigma + 2 c - ]) - ) - - # Compute the feasible region for LV*(s, t) as a 3-dimensional - # polytope for a range of sigma - LV_star_hyp = ad.compute_LV_star(hypotheses, LVER_domain, zeta=False, debug=False) - - # domain representing 2 <= tau <= tau0 - LVER_zeta_domain = Region.from_polytope( - Polytope([ - [-tau0.domain.x0, 1, 0], # sigma >= sigma_interval.x0 - [tau0.domain.x1, -1, 0], # sigma <= sigma_interval.x1 - [-2, 0, 1], # tau0 >= 2 - [tau0.c, tau0.m, -1], # tau <= tau0 = m sigma + c - ]) - ) - # Compute the feasible region for LV_{\zeta}*(s, t) as a 3-dimensional polytope - LVZ_star_hyp = ad.compute_LV_star(hypotheses, LVER_zeta_domain, zeta=True, debug=False) - ze.lver_to_energy_bound(LV_star_hyp, LVZ_star_hyp, tau0.domain) + hs = ze.lver_to_energy_bound(hypotheses, tau0, debug=False) + for h in hs: + print(h.data) + return hs def prove_improved_heath_brown_energy_estimate(): - # tau_0 as a piecewise affine function - tau0s = [ - Affine(8, -4, Interval(frac(3,4), frac(4,5))) - ] + # tau_0 as an affine function + tau0 = Affine(8, -4, Interval(frac(3,4), frac(4,5))) hypotheses = Hypothesis_Set() @@ -1065,35 +1020,6 @@ def prove_improved_heath_brown_energy_estimate(): hypotheses.add_hypothesis(ad.get_raise_to_power_hypothesis(k)) # Add classical and literature Large value estimates - hypotheses.add_hypothesis(literature.find_hypothesis(keywords="Huxley large value estimate")) - hypotheses.add_hypothesis(literature.find_hypothesis(keywords="Heath-Brown large value energy region 2a")) - - # Convert all large value estimates -> large value energy region - hypotheses.add_hypotheses(ad.lv_to_lver(hypotheses, zeta=False)) - - # Convert tau_0 into a Region of (sigma, tau) - # domain representing tau0 <= tau <= 2tau0 - LVER_domain = Region.disjoint_union([ - Region.from_polytope( - Polytope([ - [-tau0.domain.x0, 1, 0], # sigma >= sigma_interval.x0 - [tau0.domain.x1, -1, 0], # sigma <= sigma_interval.x1 - [-tau0.c, -tau0.m, 1], # tau >= tau0 = m sigma + c - [2 * tau0.c, 2 * tau0.m, -1] # tau <= 2 tau0 = 2 m sigma + 2 c - ]) - ) - for tau0 in tau0s - ]) - # Compute the feasible region for LV*(s, t) as a 3-dimensional - # polytope for a range of sigma - LV_star_hyp = ad.compute_LV_star(hypotheses, LVER_domain, zeta=False) - - # New set of hypothesis for the zeta LVER computation - hypotheses = Hypothesis_Set() - - for k in range(2, 3): - hypotheses.add_hypothesis(ad.get_raise_to_power_hypothesis(k)) - hypotheses.add_hypothesis(literature.find_hypothesis(keywords="Huxley large value estimate")) hypotheses.add_hypothesis(literature.find_hypothesis(hypothesis_type="Zeta large value estimate")) hypotheses.add_hypothesis(literature.find_hypothesis(keywords="Heath-Brown large value energy region 2a")) @@ -1103,21 +1029,10 @@ def prove_improved_heath_brown_energy_estimate(): # Convert all zeta large value estimates -> zeta large value energy region hypotheses.add_hypotheses(ad.lv_to_lver(hypotheses, zeta=True)) - # domain representing 2 <= tau <= tau0 - LVER_zeta_domain = Region.disjoint_union([ - Region.from_polytope( - Polytope([ - [-tau0.domain.x0, 1, 0], # sigma >= sigma_interval.x0 - [tau0.domain.x1, -1, 0], # sigma <= sigma_interval.x1 - [-2, 0, 1], # tau0 >= 2 - [tau0.c, tau0.m, -1], # tau <= tau0 = m sigma + c - ]) - ) - for tau0 in tau0s - ]) - # Compute the feasible region for LV_{\zeta}*(s, t) as a 3-dimensional polytope - 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)) + hs = ze.lver_to_energy_bound(hypotheses, tau0) + for h in hs: + print(h.data) + return hs def prove_zero_density_energy_2(): hypotheses = Hypothesis_Set() diff --git a/blueprint/src/python/examples.py b/blueprint/src/python/examples.py index 8ed07ee..204cae3 100644 --- a/blueprint/src/python/examples.py +++ b/blueprint/src/python/examples.py @@ -498,37 +498,13 @@ def zero_density_energy_examples(): # Convert all zeta large value estimates -> zeta large value energy region hypotheses.add_hypotheses(ad.lv_to_lver(hypotheses, zeta=True)) - # tau_0 as a piecewise affine function + # tau_0 as an affine function. lver_to_energy_bound computes the + # LV* and LV_zeta* regions over the tau0 <= tau <= 2 tau0 and + # 2 <= tau <= tau0 domains itself. tau0 = Affine(0, 5, Interval(frac(3,4), 1)) - sigma_interval = tau0.domain - - # domain representing tau0 <= tau <= 2 tau0 - LVER_domain = Region.from_polytope( - Polytope([ - [-tau0.domain.x0, 1, 0], # sigma >= sigma_interval.x0 - [tau0.domain.x1, -1, 0], # sigma <= sigma_interval.x1 - [-tau0.c, -tau0.m, 1], # tau >= tau0 = m sigma + c - [2 * tau0.c, 2 * tau0.m, -1] # tau <= 2 tau0 = 2 m sigma + 2 c - ]) - ) - - # Compute the feasible region for LV*(s, t) as a 3-dimensional - # polytope for a range of sigma - LV_star_hyp = ad.compute_LV_star(hypotheses, LVER_domain, zeta=False) - - # domain representing 2 <= tau <= tau0 - LVER_zeta_domain = Region.from_polytope( - Polytope([ - [-tau0.domain.x0, 1, 0], # sigma >= sigma_interval.x0 - [tau0.domain.x1, -1, 0], # sigma <= sigma_interval.x1 - [-2, 0, 1], # tau0 >= 2 - [tau0.c, tau0.m, -1], # tau <= tau0 = m sigma + c - ]) - ) - - # Compute the feasible region for LV_{\zeta}*(s, t) as a 3-dimensional polytope - 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, sigma_interval) + bounds = ze.lver_to_energy_bound(hypotheses, tau0) + for b in bounds: + print(b.data) # example using Lemma 6.7 def beta_to_mu_example():