OAI/NumberTheory/JointDickman/Arithmetic/RoughPhaseScales.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic cutoff for the remaining middle-frequency range

  1. lemma OAI.JointDickman.rough_logarithmic_cutoff line 11
  2. lemma OAI.JointDickman.rough_cutoff_phase_loss line 30
  3. lemma OAI.JointDickman.rough_prime_mass_bounded line 42
  4. lemma OAI.JointDickman.rough_phase_budget_tendsto line 56