OAI/NumberTheory/Ostmann/Preliminaries/WeightedNormTriangle.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A finite weighted square norm under divisor summation

  1. theorem OAI.Ostmann.weighted_correlation_le_sqrt_energy line 11
  2. theorem OAI.Ostmann.sqrt_weighted_sum_energy_le line 36