OAI/NumberTheory/CubicMoment/Estimates/MeanValueGaussianRows.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform row sums for the Gaussian matrix on logarithmic frequencies.

  1. lemma OAI.CubicFirstMoment.nat_dist_cast_eq_abs line 12
  2. lemma OAI.CubicFirstMoment.geometric_nat_distance_sum line 19
  3. lemma OAI.CubicFirstMoment.gaussian_log_frequency_decay line 82
  4. lemma OAI.CubicFirstMoment.gaussian_log_frequency_row_bound line 107