OAI/NumberTheory/JointDickman/Amplification/TwistedBinInterpolants.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual nonprincipal multiplicative interpolants

  1. def OAI.JointDickman.twistedWeightedBinInterpolant line 11
  2. theorem OAI.JointDickman.twistedWeightedBinInterpolant_multiplicative line 16
  3. theorem OAI.JointDickman.twistedWeightedBinInterpolant_norm_le line 30
  4. theorem OAI.JointDickman.small_prime_binLabel_eq_one line 39
  5. theorem OAI.JointDickman.finitePrimeWeight_prime_eq_one line 57
  6. theorem OAI.JointDickman.twistedWeightedBinInterpolant_small_prime line 67