/-- **Cohn-Kumar-Miller-Radchenko-Viazovska Fourier interpolation theorem.**
In dimension 8 sampling starts at `sqrt 2`, while in dimension 24 it starts
at radius `2`. In both cases the four sample sequences give a bijection
between radial Schwartz functions and rapidly decreasing data. -/
theorem ckmrv_fourier_interpolation :
    CKMRV 8 1 ∧ CKMRV 24 2 := by
  sorry

/--
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 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 := by
  sorry

/--
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 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) := by
  sorry

/--
Theorem A and C in arXiv:2408.15403.
-/
theorem cdt_linearIndependent :
    letI χ : ZMod 3 → ℂ := ![0, 1, -1]
    LinearIndependent ℚ ![1, riemannZeta 2, ZMod.LFunction χ 2] ∧
    ∀ m n : ℤ, m ≠ -1 → m ≠ 0 → n ≠ -1 → n ≠ 0 → 10 ^ 6 * |m - n| < |n| →
      letI lm := Real.log (1 + 1 / m)
      letI ln := Real.log (1 + 1 / n)
      Irrational (lm * ln) ∧
      (m ≠ n → LinearIndependent ℚ ![1, lm, ln, lm * ln]) := by
  sorry

/-- The genus of a smooth proper curve. -/
def genus (C : Over (Spec (.of k))) [IsProper C.hom] [SmoothOfRelativeDimension 1 C.hom]
    [GeometricallyIrreducible C.hom] : ℕ :=
  sorry

/-- The Jacobian of a smooth, proper curve over a field `k`. -/
def Jacobian (C : Over (Spec (.of k))) [IsProper C.hom] [SmoothOfRelativeDimension 1 C.hom]
    [GeometricallyIrreducible C.hom] : Over (Spec (.of k)) :=
  sorry

/-- The group scheme structure on the Jacobian of the curve `C`. -/
instance instGrpObj : GrpObj (Jacobian C) :=
  sorry

/-- The Jacobian of `C` is smooth of relative dimension `g` over `k`, where `g` is the
genus of `C`. -/
instance smoothOfRelativeDimension_genus :
    SmoothOfRelativeDimension (genus C) (Jacobian C).hom :=
  sorry

/-- The Jacobian of `C` is proper over `k`. -/
instance instIsProper : IsProper (Jacobian C).hom :=
  sorry

/-- The Jacobian of `C` is geometrically irreducible over `k`. -/
instance instGeometricallyIrreducible : GeometricallyIrreducible (Jacobian C).hom :=
  sorry

/-- The Abel-Jacobi map from a smooth, proper curve to its Jacobian associated
to a `k`-rational point of `C`. -/
def ofCurve (P : 𝟙_ (Over (Spec (.of k))) ⟶ C) : C ⟶ Jacobian C :=
  sorry

/-- The Abel-Jacobi map sends the `k`-rational point `P` to `0`, where `0` (denoted by `η` below) is
the neutral element of the group scheme `Jacobian C`. -/
theorem comp_ofCurve (C : Over (Spec (.of k))) [IsProper C.hom]
    [SmoothOfRelativeDimension 1 C.hom] [GeometricallyIrreducible C.hom]
    (P : 𝟙_ (Over (Spec (.of k))) ⟶ C) :
    P ≫ ofCurve P = η[Jacobian C] :=
  sorry

/--
The universal property of the Jacobian variety: For any abelian variety `A`,
any morphism `f : C ⟶ A` such that `f(P) = 0` factors uniquely through the
Jacobian of `C`.
In other words, `Jacobian C` is the Albanese variety of `C`.
-/
theorem exists_unique_ofCurve_comp (C : Over (Spec (.of k))) [IsProper C.hom]
    [SmoothOfRelativeDimension 1 C.hom] [GeometricallyIrreducible C.hom]
    (P : 𝟙_ (Over (Spec (.of k))) ⟶ C)
    {A : Over (Spec (.of k))} [Smooth A.hom] [IsProper A.hom] [GrpObj A]
    [GeometricallyIrreducible A.hom] (f : C ⟶ A) (hf : P ≫ f = η[A]) :
    ∃! (g : Jacobian C ⟶ A), f = ofCurve P ≫ g :=
  sorry

/-- **Existence of an aspherical integer homology 4-sphere** (Tschantz, answering
`[Kir97, Problem 4.17]`). There is a closed topological 4-manifold that is both
aspherical and an integer homology 4-sphere. -/
theorem aspherical_integer_homology_four_sphere :
    ∃ M : Closed4Manifold, M.IsAspherical ∧ M.IsIntegerHomologySphere := by
  sorry

/-- **π₆ of the 3-sphere.** Toda's tables give `π₆(𝕊³) ≅ ℤ/12`. -/
theorem pi6_sphere_three_mulEquiv_zmod_twelve
    (x : Metric.sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) :
    Nonempty
      (HomotopyGroup.Pi 6 (Metric.sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) x ≃*
        Multiplicative (ZMod 12)) := by
  sorry

/-- **Avila-Jitomirskaya Ten Martini theorem.** For irrational frequency
and nonzero coupling, the spectrum of the almost Mathieu operator is a
Cantor set. Here this means nonempty, compact, perfect, and totally
disconnected. -/
theorem ten_martini_problem (α coupling θ : ℝ)
    (hα : Irrational α) (hcoupling : coupling ≠ 0) :
    ∃ H : EllTwo →L[ℂ] EllTwo,
      IsAlmostMathieuOperator α coupling θ H ∧
        (spectrum ℂ H).Nonempty ∧
        IsCompact (spectrum ℂ H) ∧
        Perfect (spectrum ℂ H) ∧
        IsTotallyDisconnected (spectrum ℂ H) := by
  sorry

/-- **Adams' Hopf-invariant-one theorem** (H-space form). The sphere `𝕊ⁿ`
admits an H-space structure if and only if `n = 0`, `1`, `3`, or `7`. -/
theorem hSpace_sphere_iff (n : ℕ) :
    Nonempty (HSpace (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1)) ↔
      n = 0 ∨ n = 1 ∨ n = 3 ∨ n = 7 := by
  sorry

theorem einsiedler_katok_lindenstrauss :
    dimH {(α, β) : ℝ × ℝ | Filter.atTop.liminf
      (fun n : ℕ ↦ n * distToNearestInt (n * α) * distToNearestInt (n * β)) > 0} = 0 := by
  sorry

/-- **The Newlander–Nirenberg theorem.** An almost complex structure with
vanishing Nijenhuis tensor is integrable. Formally: for every `x` in an open
set `U ⊆ ℝ^{2n}` carrying such a structure `J` there is a smooth local
diffeomorphism `φ` (an `OpenPartialHomeomorph`, smooth in both directions)
from a neighbourhood of `x` inside `U` onto an open subset of `ℂⁿ` whose
differential is complex linear:

  `dφ_y (J y v) = i · dφ_y v`.

Such charts are holomorphic coordinates for `J`. -/
theorem newlander_nirenberg {n : ℕ} {U : Set (E n)} (_hU : IsOpen U)
    (J : E n → E n →L[ℝ] E n) (_hJ : IsAlmostComplexOn J U)
    (_hN : NijenhuisVanishesOn J U) {x : E n} (_hx : x ∈ U) :
    ∃ φ : OpenPartialHomeomorph (E n) (EuclideanSpace ℂ (Fin n)),
      x ∈ φ.source ∧ φ.source ⊆ U ∧
      ContDiffOn ℝ ∞ (φ : E n → EuclideanSpace ℂ (Fin n)) φ.source ∧
      ContDiffOn ℝ ∞ (φ.symm : EuclideanSpace ℂ (Fin n) → E n) φ.target ∧
      ∀ y ∈ φ.source, ∀ v : E n,
        fderiv ℝ (φ : E n → EuclideanSpace ℂ (Fin n)) y (J y v)
          = Complex.I • fderiv ℝ (φ : E n → EuclideanSpace ℂ (Fin n)) y v := by
  sorry

theorem mostow_rigidity (n : ℕ) (hn : 3 ≤ n) (Γ Λ : Subgroup (PO n 1))
    (disc_Γ : IsDiscrete (SetLike.coe Γ)) (disc_Λ : IsDiscrete (SetLike.coe Λ))
    [HasFundamentalDomain Γ (PO n 1)] [HasFundamentalDomain Λ (PO n 1)]
    (covol_Γ : covolume Γ (PO n 1) ≠ ⊤) (covol_Λ : covolume Λ (PO n 1) ≠ ⊤)
    (f : Γ ≃* Λ) : ∃ g : PO n 1, ∀ γ : Γ, f γ = g * γ * g⁻¹ := by
  sorry

/--
Statement of Theorem 1.2:

There exist explicit good locally testable codes (for every rate `ρ < 1`).
-/
theorem theorem_1_2 (ρ : ℝ≥0) (hρ : ρ < 1) :
    ∃ q, ∃ κ ≠ 0, ∃ (n : ℕ → ℕ), ∃ (𝒞 : (i : ℕ) → BinaryCode (n i)), IsGood 𝒞 ∧
      ∀ i, Nonempty (LTC q κ (𝒞 i)) ∧ rate (𝒞 i) ≥ ρ := by
  sorry