Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
115 changes: 15 additions & 100 deletions blueprint/src/python/derived.py
Original file line number Diff line number Diff line change
Expand Up @@ -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] ----------------------------------------------------------

Expand All @@ -1025,75 +1004,22 @@ 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()

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(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"))
Expand All @@ -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()
Expand Down
36 changes: 6 additions & 30 deletions blueprint/src/python/examples.py
Original file line number Diff line number Diff line change
Expand Up @@ -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():
Expand Down