On the Chowla and twin primes conjectures over 𝔽_q[T]

Problem statement

Notes: Unavailable.

Source: W. Sawin and M. Shusterman, `On the Chowla and twin primes conjectures over 𝔽_q[T]`, Annals of Math, 196 (2) 2022. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2022-196-2-ChowlaAndTwinPrimeOverFqT.lean

Informal solution: Unavailable.

/--
Statement of Theorem 1.1:

For an odd prime number `p`, and a power `q` of `p` satisfying
`q > 685090 * p ^ 2`, the following holds. For any nonzero `h ∈ 𝔽_q[T]`, we have
`#{f ∈ 𝔽_q[T] : |f| = X, f and f + h are prime} ∼ 𝔖_q(h) X / log_q^2 (X)`
as `X → ∞` through the powers of `q`.

Moreover, we have a power saving (depending on q) in the asymptotic above.
-/
theorem declaration uses `sorry`theorem_1_1 (hp : Odd p) (hq : q > 685090 * p ^ 2) :
    ∃ ε > (0 : ℝ), -- there exists a power saving such that ...
      ∀ h ≠ 0, (fun X : powers q ↦ Set.ncard {f | ‖f‖ = X ∧ f ∈ primes 𝔽_q ∧ f + h ∈ primes 𝔽_q} -
        𝔖_q h * X / (Real.logb q X) ^ 2) =O[Filter.atTop] (fun X : powers q ↦ (X : ℝ) ^ (1 - ε)) :=
  sorry

/--
Statement of Theorem 1.3:

For an odd prime number `p`, an integer `k ≥ 1`, and a power `q` of `p` satisfying `q > p²k²e²`,
the following holds. For every fixed choice of `k` distinct polynomials `h₁,...,hₖ ∈ 𝔽_q[T]`,
we have `∑ (f ∈ 𝔽_q[T]⁺, |f| ≤ X), μ(f + h₁) μ(f + h₂) ... μ(f + hₖ) = o(X)`, `X → ∞`.
-/
theorem declaration uses `sorry`theorem_1_3 (hp : Odd p) (k : ℕ) (hk : k ≥ 1) (hq : q > p ^ 2 * k ^ 2 * e ^ 2)
    (h : Fin k → 𝔽_q[X]) (h_distinct : Function.Injective h) :
    (fun X : ℝ ↦ ∑' f : monicBounded 𝔽_q X, ∏ i, moebius (f + h i)) =o[Filter.atTop] id :=
  sorry