ThreePrimeContinuousMinorArc.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.ThreePrimeContinuousMinorArc.primeExponentialSum line 12
Source documentation
The actual prime logarithmic exponential sum, with positive phase.
```
def primeExponentialSum (u : ℕ) (x : ℝ) : ℂ :=
…
```
lemma OAI.Problem337.ThreePrimeContinuousMinorArc.primeExponentialSum_eq line 16
lemma OAI.Problem337.ThreePrimeContinuousMinorArc.phase_norm line 25
Source documentation
Every real frequency gives a unit-modulus phase.
```
lemma phase_norm (t x : ℝ) :
    ‖Complex.exp (2 * Real.pi * Complex.I * (t : ℂ) * (x : ℂ))‖ = 1 := by
…
```
theorem OAI.Problem337.ThreePrimeContinuousMinorArc.primeExponentialSum_norm_le line 31
Source documentation
The unconditional amplitude estimate needed in major-arc error budgets.
```
theorem primeExponentialSum_norm_le (u : ℕ) (x : ℝ) :
    ‖primeExponentialSum u x‖ ≤ Real.log 4 * (u : ℝ) := by
…
```
Mentions: OAI.Problem337.ThreePrimeContinuousMinorArc.primeExponentialSum
theorem OAI.Problem337.ThreePrimeContinuousMinorArc.primeExponentialSum_parseval line 38
Source documentation
Exact energy of the prime exponential sum on one unit interval.
```
theorem primeExponentialSum_parseval (u : ℕ) :
    (∫ x : ℝ in 0..1, ‖primeExponentialSum u x‖ ^ 2) =
      ∑ p ∈ Nat.primesLE u, Real.log (p : ℝ) ^ 2 := by
…
```
Mentions: OAI.Problem337.ThreePrimeContinuousMinorArc.primeExponentialSum

theorem OAI.Problem337.ThreePrimeContinuousMinorArc.prime_minor_cubic_bound line 47

Source documentation

Continuous prime minor arcs with an arbitrary norm-bounded twist. The prime supremum estimate remains an explicit analytic hypothesis.

theorem prime_minor_cubic_bound (u : ℕ) (hu : 2 ≤ u)
    (phase : ℝ → ℂ) (minor : Set ℝ) (hmeas : MeasurableSet minor)
    (hsubset : minor ⊆ Set.Icc 0 1) (ε : ℝ) (hε : 0 ≤ ε)
    (hminor : ∀ x ∈ minor, ‖primeExponentialSum u x‖ ≤
      ε * (u : ℝ) / Real.log (u : ℝ))
    (hphase : ∀ x ∈ minor, ‖phase x‖ ≤ 1) :
    ‖∫ x in minor, primeExponentialSum u x ^ 3 * phase x‖ ≤
      ε * Real.log 4 * (u : ℝ) ^ 2 := by
…

Mentions: OAI.Problem337.ThreePrimeContinuousMinorArc.primeExponentialSum

theorem OAI.Problem337.ThreePrimeContinuousMinorArc.prime_minor_extraction_bound line 73

Source documentation

Conventional negative extraction frequency for the cubic prime count.

theorem prime_minor_extraction_bound (u : ℕ) (hu : 2 ≤ u)
    (minor : Set ℝ) (hmeas : MeasurableSet minor)
    (hsubset : minor ⊆ Set.Icc 0 1) (ε : ℝ) (hε : 0 ≤ ε)
    (hminor : ∀ x ∈ minor, ‖primeExponentialSum u x‖ ≤
      ε * (u : ℝ) / Real.log (u : ℝ)) :
    ‖∫ x in minor, primeExponentialSum u x ^ 3 *
      Complex.exp (2 * Real.pi * Complex.I * (-(u : ℂ)) * (x : ℂ))‖ ≤
      ε * Real.log 4 * (u : ℝ) ^ 2 := by
…

Mentions: OAI.Problem337.ThreePrimeContinuousMinorArc.primeExponentialSum