OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/MixedWeight.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryTwoScaleCofactor.mixedWeight line 23
  2. def OAI.OrdinaryTwoScaleCofactor.mixedCoefficient line 28
  3. def OAI.OrdinaryTwoScaleCofactor.mixedEnergy line 32
  4. lemma OAI.OrdinaryTwoScaleCofactor.mixedEnergy_nonneg line 37
  5. lemma OAI.OrdinaryTwoScaleCofactor.actual_two_scale_polynomial line 41
  6. theorem OAI.OrdinaryTwoScaleCofactor.mixed_spaced_energy line 62
  7. def OAI.OrdinaryTwoScaleCofactor.transitionFrequencies line 86
  8. def OAI.OrdinaryTwoScaleCofactor.transitionEnergy line 91
  9. lemma OAI.OrdinaryTwoScaleCofactor.transition_amplification line 96
  10. theorem OAI.OrdinaryTwoScaleCofactor.actual_transition_energy line 123