OAI/NumberTheory/Ostmann/Characters/SparseTruncationRate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A concrete linear truncation cutoff for the sparse weight

  1. theorem OAI.Ostmann.sparse_grid_ratio_le_exp line 9
  2. theorem OAI.Ostmann.sparse_truncation_constant_le_exp line 13
  3. theorem OAI.Ostmann.sparse_truncation_error_rate line 23

    Source documentation

    The fixed choice K >= 1000 L controls both the scalar and operator tails. Only the harmonic-mass bound H <= L remains to be supplied by the prime band.

    theorem sparse_truncation_error_rate (L H : ℝ) (K : ℕ)
    (hL : 1 ≤ L) (hH : H ≤ L) (hK : 1000 * L ≤ K) :
    2 * Real.exp (6 * H) * (100 / 103 : ℝ) ^ (K + 1) / (1 - 100 / 103) ^ 2 ≤
      Real.exp (-5 * L) := by
…