Linear independence results of Calegari–Dimitrov–Tang

Problem statement

Notes: Unavailable.

Source: https://arxiv.org/abs/2408.15403

Informal solution: See Figure 1.3.0. 'Leitfaden: paths to Theorems A and C' for a dependency graph of the results. The dotted lines indicates that there are two alternate paths to Theorems A and C, either through § 6 (by multivariable methods, based on measure concentration) or § 7 (by single variable methods, based on some Arakelov theory and Bost’s inequality on evaluation heights). Arithmetic holonomy bounds are ultimately the main concern of this paper.

theorem declaration uses `sorry`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⊢ LinearIndependent ℚ ![1, riemannZeta 2, ZMod.LFunction ![0, 1, -1] 2] ∧
  ∀ (m n : ℤ),
    m ≠ -1 →
      m ≠ 0 →
        n ≠ -1 →
          n ≠ 0 →
            10 ^ 6 * |m - n| < |n| →
              Irrational (Real.log (1 + 1 / ↑m) * Real.log (1 + 1 / ↑n)) ∧
                (m ≠ n →
                  LinearIndependent ℚ
                    ![1, Real.log (1 + 1 / ↑m), Real.log (1 + 1 / ↑n), Real.log (1 + 1 / ↑m) * Real.log (1 + 1 / ↑n)])
  sorryAll goals completed! 🐙