The Weyl bound for Dirichlet L-functions of cube-free conductor

Problem statement

Notes: The proof binders `hq` and `hχ` are named `_hq` and `_hχ` here. This is alpha-equivalent and suppresses unused-variable warnings in the generated `Solution.lean` delegation.

Source: I. Petrow and M. P. Young, `The Weyl bound for Dirichlet L-functions of cube-free conductor`, Annals of Math, 192 (2) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2020-192-2-DirichletWeylBound.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`corollary_1_3 (ε : ℝ) (hε : 0 < ε) : ∃ C : ℝ,
    ∀ q (_hq : q.IsCubeFree) [NeZero q] (χ : DirichletCharacter ℂ q) (_hχ : χ.IsPrimitive) (t : ℝ),
      ‖χ.LFunction (1 / 2 + I * t)‖ ≤ C * q ^ (1 / 6 + ε) * (1 + |t|) ^ (1 / 6 + ε) := byε:ℝhε:0 < ε⊢ ∃ C,
  ∀ (q : ℕ),
    q.IsCubeFree →
      ∀ [inst : NeZero q] (χ : DirichletCharacter ℂ q),
        χ.IsPrimitive →
          ∀ (t : ℝ), ‖DirichletCharacter.LFunction χ (1 / 2 + I * ↑t)‖ ≤ C * ↑q ^ (1 / 6 + ε) * (1 + |t|) ^ (1 / 6 + ε)
  sorryAll goals completed! 🐙