Higher uniformity of bounded multiplicative functions in short intervals on average

Problem statement

Notes: The proof binders `hQ`, `hC`, `hf`, `hf'`, `hX`, `hXH`, and `hHX` in `theorem_1_3` are prefixed with `_` here. This is alpha-equivalent and suppresses unused-variable warnings in the generated `Solution.lean`, whose delegation supplies the enclosing proof at once.

Source: K. Matomäki, M. Radziwiłł, T. Tao, J. Teräväinen, and T. Ziegler, `Higher uniformity of bounded multiplicative functions in short intervals on average`, Annals of Math, 197 (2) 2023. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2023-197-2-BoundedMultiplicativeFunctions.lean

Informal solution: Unavailable.

/--
Statement of Theorem 1.3 (Non-pretentious multiplicative functions do not correlate
with polynomial phases on short intervals on average):

Let `k : ℕ`, `θ : ℝ` such that `0 < θ < 1/2` and `η : ℝ` such that `η > 0`. Then there exist
constants `Q : ℕ` such that `Q > 0`, `C : ℝ` such that `C > 0`, and `B : ℝ`, such that for any
multiplicative 1-bounded arithmetic function `f : ℕ → ℂ`, any `X : ℝ` such that `X ≥ 1` and any
`H : ℝ` such that `Xᶿ ≤ H ≤ X¹⁻ᶿ`, if

`∫ x ∈ [X, 2X], ‖f‖_{uᵏ⁺¹[x, x + H]}dx ≥ ηX`

then

`M(f;CXᵏ⁺¹/Hᵏ⁺¹,Q) ≤ B`.
-/
theorem declaration uses `sorry`theorem_1_3 (k : ℕ) (θ : ℝ) (hθ₀ : 0 < θ) (hθ₁ : θ < 1 / 2) (η : ℝ) (hη : η > 0) :
    ∃ (Q : ℕ+) (_hQ : 1 ≤ Q) (C : ℝ) (_hC : 0 < C) (B : ℝ),
      ∀ (f : ArithmeticFunction ℂ) (_hf : f.IsMultiplicative) (_hf' : IsOneBounded f)
        (X : ℝ) (_hX : X ≥ 1) (H : ℝ) (_hXH : X ^ θ ≤ H) (_hHX : H ≤ X ^ (1 - θ)),
          ∫ x in X..(2 * X), weakGowersUniformityNorm k x H f.intExtension ≥ η * X →
            M f (C * X ^ (k + 1) / H ^ (k + 1)) Q ≤ B := byk:ℕθ:ℝhθ₀:0 < θhθ₁:θ < 1 / 2η:ℝhη:η > 0⊢ ∃ Q,
  ∃ (_ : 1 ≤ Q),
    ∃ C,
      ∃ (_ : 0 < C),
        ∃ B,
          ∀ (f : ArithmeticFunction ℂ),
            f.IsMultiplicative →
              IsOneBounded ⇑f →
                ∀ X ≥ 1,
                  ∀ (H : ℝ),
                    X ^ θ ≤ H →
                      H ≤ X ^ (1 - θ) →
                        ∫ (x : ℝ) in X..2 * X, weakGowersUniformityNorm k x H f.intExtension ≥ η * X →
                          M (⇑f) (C * X ^ (k + 1) / H ^ (k + 1)) Q ≤ B
  sorryAll goals completed! 🐙

/--
Statement of Corollary 1.1 (Liouville does not correlate with polynomial phases on
short intervals on average):

Let `λ` denote the liouville function. Fix `k : ℕ` and `θ : ℝ` such that `0 < θ < 1`. Then

`∫ x ∈ [X, 2X], ‖λ‖_{uᵏ⁺¹[x, x + Xᶿ]}dx = o(X)`

as `X → ∞`.
-/
theorem declaration uses `sorry`corollary_1_1 (k : ℕ) (θ : ℝ) (hθ₀ : 0 < θ) (hθ₁ : θ < 1) :
    (fun X ↦ ∫ x in X..(2 * X), weakGowersUniformityNorm k x (X ^ θ) (fun n ↦ liouville ⌊n⌋₊))
      =o[atTop] (fun X ↦ X) := byk:ℕθ:ℝhθ₀:0 < θhθ₁:θ < 1⊢ (fun X => ∫ (x : ℝ) in X..2 * X, weakGowersUniformityNorm k x (X ^ θ) fun n => ↑(liouville ⌊n⌋₊)) =o[atTop] fun X => X
  sorryAll goals completed! 🐙