OAI/NumberTheory/DirichletL/Energy/AllocatedChildren.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.CenteredMomentEnergyAllocatedChildren.natural_product_eq_positive line 25
  2. lemma OAI.SevenEighths.CenteredMomentEnergyAllocatedChildren.natural_radial_eq_energy line 48
  3. lemma OAI.SevenEighths.CenteredMomentEnergyAllocatedChildren.natural_subset_radial_eq_energy line 67
  4. def OAI.SevenEighths.CenteredMomentEnergyAllocatedChildren.allocatedEnergy line 89
  5. lemma OAI.SevenEighths.CenteredMomentEnergyAllocatedChildren.child_radial_eq_energy line 103
  6. def OAI.SevenEighths.CenteredMomentEnergyAllocatedChildren.commonAllocatedEnergy line 124
  7. lemma OAI.SevenEighths.CenteredMomentEnergyAllocatedChildren.commonChild_energy line 135