OAI/NumberTheory/DirichletL/Energy/DeletedChildCapacity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.CenteredMomentEnergyDeletedChildCapacity.deletion_norm line 18
  2. lemma OAI.SevenEighths.CenteredMomentEnergyDeletedChildCapacity.prime_deletion_norm line 23
  3. def OAI.SevenEighths.CenteredMomentEnergyDeletedChildCapacity.postmaskLength line 27
  4. lemma OAI.SevenEighths.CenteredMomentEnergyDeletedChildCapacity.postmaskLength_eq line 30
  5. lemma OAI.SevenEighths.CenteredMomentEnergyDeletedChildCapacity.postmaskLength_le line 36
  6. lemma OAI.SevenEighths.CenteredMomentEnergyDeletedChildCapacity.postmaskLength_nonneg line 41
  7. theorem OAI.SevenEighths.CenteredMomentEnergyDeletedChildCapacity.child_survives line 44
  8. def OAI.SevenEighths.CenteredMomentEnergyDeletedChildCapacity.deletedExcess line 57
  9. lemma OAI.SevenEighths.CenteredMomentEnergyDeletedChildCapacity.deletedExcess_le line 64
  10. theorem OAI.SevenEighths.CenteredMomentEnergyDeletedChildCapacity.child_excess_from_parent line 80
  11. theorem OAI.SevenEighths.CenteredMomentEnergyDeletedChildCapacity.child_paid_width line 101
  12. lemma OAI.SevenEighths.CenteredMomentEnergyDeletedChildCapacity.eventually_endpoint_cost line 123
  13. theorem OAI.SevenEighths.CenteredMomentEnergyDeletedChildCapacity.paired_child_excess line 127
  14. theorem OAI.SevenEighths.CenteredMomentEnergyDeletedChildCapacity.source_removal_width_cost line 153
  15. lemma OAI.SevenEighths.CenteredMomentEnergyDeletedChildCapacity.postmask_scale_pos line 194
  16. theorem OAI.SevenEighths.CenteredMomentEnergyDeletedChildCapacity.input_parent_child_excess line 199