OAI/NumberTheory/DirichletL/Moments/AllocatedChildCapacity.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.clippingLoss line 18
  2. lemma OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.clipped_log line 21
  3. lemma OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.clipped_pair_log line 31
  4. lemma OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.clipping_loss_bound line 38
  5. lemma OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.profile_polynomial_survives line 58
  6. def OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.plainLogs line 67
  7. def OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.remainingLogs line 72
  8. def OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.preVolume line 75
  9. lemma OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.preVolume_pos line 78
  10. lemma OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.selectedNorm_ge_one line 81
  11. lemma OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.formalReduction_ge_one line 88
  12. lemma OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.remainingLogs_le line 93
  13. lemma OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.raw_volume line 99
  14. lemma OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.raw_log_volume line 109
  15. theorem OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.affine_exact line 123
  16. theorem OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.excess_le line 134
  17. theorem OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.allocated_survives line 148
  18. theorem OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.paired_capacity line 164
  19. theorem OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.common_preVolume line 185
  20. lemma OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.common_reduction_ge_one line 196
  21. lemma OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.common_slot_logs_le line 211
  22. theorem OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.common_allocated_raw_volume line 220
  23. theorem OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.common_paired_capacity line 241
  24. theorem OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.excess_le_remaining line 283
  25. theorem OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.allocated_clipping line 296
  26. lemma OAI.SevenEighths.CenteredMomentAllocatedChildCapacity.native_excess line 309