ThreePrimeMangoldt.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.supplyIntegerTriples line 12
Source documentation
All positive ordered triples of fixed sum, without primality restrictions.
```
def supplyIntegerTriples (u : ℕ) : Finset (ℕ × ℕ × ℕ) :=
…
```
def OAI.Problem337.primeLogWeight line 17
Source documentation
Logarithmic weight supported only on primes, unlike the von Mangoldt weight.
```
def primeLogWeight (n : ℕ) : ℝ := if n.Prime then Real.log n else 0
```
def OAI.Problem337.mangoldtTripleSum line 20
Source documentation
The weighted ternary convolution used in the analytic three-prime theorem.
```
def mangoldtTripleSum (u : ℕ) : ℝ :=
…
```
def OAI.Problem337.primeTripleLogSum line 26
Source documentation
The corresponding weighted sum over genuine prime triples.
```
def primeTripleLogSum (u : ℕ) : ℝ :=
…
```
lemma OAI.Problem337.primeLogWeight_nonneg line 30
lemma OAI.Problem337.primeLogWeight_le_vonMangoldt line 36
lemma OAI.Problem337.primeTripleLogSum_eq line 43

lemma OAI.Problem337.fixed_sum_coordinate_sum_le line 60

Source documentation

A weighted version of the fixed-coordinate counting bound.

lemma fixed_sum_coordinate_sum_le
    {α : Type*} [DecidableEq α] (T : Finset α) (U : Finset ℕ)
    (x y z : α → ℕ) (u : ℕ) (f : ℕ → ℝ)
    (hf : ∀ n ∈ U, 0 ≤ f n)
    (hsum : ∀ t ∈ T, x t + y t + z t = u)
    (hU : ∀ t ∈ T, x t ∈ U ∧ y t ∈ U)
    (hinj : Function.Injective (fun t => (x t, y t, z t))) :
    (∑ t ∈ T, f (x t)) ≤ (U.card : ℝ) * ∑ n ∈ U, f n := by
…

lemma OAI.Problem337.sum_primePowerLogWeight line 96
Source documentation
Prime powers of exponent at least two carry exactly the difference of the Chebyshev functions.
```
lemma sum_primePowerLogWeight (u : ℕ) :
    (∑ n ∈ Finset.Icc 1 u,
      (ArithmeticFunction.vonMangoldt n - primeLogWeight n)) =
        Chebyshev.psi u - Chebyshev.theta u := by
…
```
Mentions: OAI.Problem337.primeLogWeight
lemma OAI.Problem337.triple_product_difference_le line 108
lemma OAI.Problem337.mangoldtTripleSum_le_primeTripleLogSum line 125
theorem OAI.Problem337.mangoldt_triple_error_isLittleO line 199
Source documentation
The contribution from genuine higher prime powers is lower order than the quadratic main term. This uses Mathlib's elementary ψ - θ = O(sqrt x) bound.
```
theorem mangoldt_triple_error_isLittleO :
    (fun x : ℝ => 3 * x * Real.log x ^ 2 *
      (Chebyshev.psi x - Chebyshev.theta x)) =o[atTop] (fun x : ℝ => x ^ 2) := by
…
```

theorem OAI.Problem337.eventually_mangoldt_triple_error_lt line 220

Source documentation

Explicit error absorption along the natural-number parameter.

theorem eventually_mangoldt_triple_error_lt (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ u : ℕ in atTop,
      3 * (u : ℝ) * Real.log (u : ℝ) ^ 2 *
        (Chebyshev.psi u - Chebyshev.theta u) < ε * (u : ℝ) ^ 2 := by
…

theorem OAI.Problem337.weighted_prime_lower_bound_of_mangoldt line 233
Source documentation
An analytic quadratic lower bound for the von Mangoldt convolution implies one for the prime-only weighted sum. No analytic lower bound is asserted here.
```
theorem weighted_prime_lower_bound_of_mangoldt
    (c : ℝ) (hc : 0 < c)
    (hmain : ∀ᶠ u : ℕ in atTop, Odd u → c * (u : ℝ) ^ 2 ≤ mangoldtTripleSum u) :
    ∀ᶠ u : ℕ in atTop, Odd u →
      (c / 2) * (u : ℝ) ^ 2 ≤ primeTripleLogSum u := by
…
```
Mentions: OAI.Problem337.mangoldtTripleSum, OAI.Problem337.primeTripleLogSum