OAI/Combinatorics/SquareDifference/PowerParameters.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareDifference.sourceBeta line 13
  2. def OAI.SquareDifference.sourceGamma line 15
  3. def OAI.SquareDifference.sourceTau line 17
  4. def OAI.SquareDifference.sourceSigma line 19
  5. def OAI.SquareDifference.sourceLoss line 21
  6. def OAI.SquareDifference.powerCutoff line 23
  7. def OAI.SquareDifference.childLength line 25
  8. lemma OAI.SquareDifference.sourceBeta_pos line 27
  9. lemma OAI.SquareDifference.sourceBeta_le line 29
  10. lemma OAI.SquareDifference.sourceGamma_pos line 31
  11. lemma OAI.SquareDifference.sourceTau_pos line 33
  12. lemma OAI.SquareDifference.sourceTau_le line 37
  13. lemma OAI.SquareDifference.sourceTau_lt_quarter line 42
  14. lemma OAI.SquareDifference.sourceSigma_pos line 45
  15. lemma OAI.SquareDifference.sourceLoss_pos line 48
  16. lemma OAI.SquareDifference.source_exponent_gap line 51
  17. lemma OAI.SquareDifference.eventually_rpow_dominate line 71
  18. lemma OAI.SquareDifference.powerCutoff_le line 80
  19. lemma OAI.SquareDifference.powerCutoff_mono line 83
  20. lemma OAI.SquareDifference.powerCutoff_pos line 86
  21. lemma OAI.SquareDifference.powerCutoff_le_self line 89
  22. lemma OAI.SquareDifference.powerCutoff_lower line 94
  23. lemma OAI.SquareDifference.childLength_pos line 100
  24. lemma OAI.SquareDifference.childLength_lower line 104
  25. lemma OAI.SquareDifference.childLength_cover line 106
  26. lemma OAI.SquareDifference.childLength_lt line 111
  27. lemma OAI.SquareDifference.childLength_factor line 122