OAI/NumberTheory/DirichletL/Moments/EligibleEnergy.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SevenEighths.CenteredMomentEligibleEnergy.Data line 14
  2. def OAI.SevenEighths.CenteredMomentEligibleEnergy.Data.coefficient line 33
  3. def OAI.SevenEighths.CenteredMomentEligibleEnergy.Data.energy line 36
  4. def OAI.SevenEighths.CenteredMomentEligibleEnergy.Data.childEnergy line 40
  5. def OAI.SevenEighths.CenteredMomentEligibleEnergy.Data.profileFactor line 46
  6. lemma OAI.SevenEighths.CenteredMomentEligibleEnergy.Data.energy_nonneg line 49
  7. lemma OAI.SevenEighths.CenteredMomentEligibleEnergy.Data.child_nonneg line 52
  8. lemma OAI.SevenEighths.CenteredMomentEligibleEnergy.Data.profile_nonneg line 57
  9. lemma OAI.SevenEighths.CenteredMomentEligibleEnergy.Data.reduction_pos line 61
  10. theorem OAI.SevenEighths.CenteredMomentEligibleEnergy.actual_source_from_children line 65
  11. lemma OAI.SevenEighths.CenteredMomentEligibleEnergy.sqrt_sum_le line 99
  12. lemma OAI.SevenEighths.CenteredMomentEligibleEnergy.sqrt_reciprocal line 108
  13. theorem OAI.SevenEighths.CenteredMomentEligibleEnergy.actual_source_root_from_children line 111