OAI/NumberTheory/DirichletL/Energy/ReferenceState.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentEnergyReferenceState.effectiveRadial line 16
  2. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceState.radialEnergy_effective line 19
  3. def OAI.SevenEighths.CenteredMomentEnergyReferenceState.effectiveState line 28
  4. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceState.effective_row_norm line 33
  5. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceState.effective_character_nonprincipal line 39
  6. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceState.effective_character_cap line 47
  7. def OAI.SevenEighths.CenteredMomentEnergyReferenceState.comparisonFirst line 57
  8. def OAI.SevenEighths.CenteredMomentEnergyReferenceState.comparisonSecond line 58
  9. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceState.comparison_positive line 60
  10. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceState.comparison_same_product line 64
  11. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceState.comparison_second_power line 69
  12. theorem OAI.SevenEighths.CenteredMomentEnergyReferenceState.balanced_reference_geometry line 75
  13. theorem OAI.SevenEighths.CenteredMomentEnergyReferenceState.balanced_reflection_margins line 96