OAI/NumberTheory/PiExponent/Approximation/DeterminantContradiction.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.DeterminantContradiction.collisionConstant line 15
  2. theorem OAI.PiExponent.DeterminantContradiction.collisionConstant_pos line 17
  3. abbrev OAI.PiExponent.DeterminantContradiction.FixedData line 21
  4. def OAI.PiExponent.DeterminantContradiction.finiteNumerators line 23
  5. def OAI.PiExponent.DeterminantContradiction.finiteDenominators line 26
  6. theorem OAI.PiExponent.DeterminantContradiction.finiteDenominators_two_le line 29
  7. theorem OAI.PiExponent.DeterminantContradiction.logWeights_eq line 32
  8. abbrev OAI.PiExponent.DeterminantContradiction.Row line 36
  9. abbrev OAI.PiExponent.DeterminantContradiction.Column line 40
  10. def OAI.PiExponent.DeterminantContradiction.actualMatrix line 43
  11. def OAI.PiExponent.DeterminantContradiction.actualMinor line 50
  12. def OAI.PiExponent.DeterminantContradiction.actualMean line 55
  13. def OAI.PiExponent.DeterminantContradiction.actualRowCount line 58
  14. def OAI.PiExponent.DeterminantContradiction.lowIndexCount line 61
  15. def OAI.PiExponent.DeterminantContradiction.collisionRate line 65
  16. def OAI.PiExponent.DeterminantContradiction.collisionLimit line 69
  17. theorem OAI.PiExponent.DeterminantContradiction.actual_minor_arithmetic_lower_bound line 74
  18. theorem OAI.PiExponent.DeterminantContradiction.actualMean_bounds line 87
  19. def OAI.PiExponent.DeterminantContradiction.GlobalInterpolationStatement line 94
  20. def OAI.PiExponent.DeterminantContradiction.AnalyticAggregateStatement line 98
  21. theorem OAI.PiExponent.DeterminantContradiction.tendsto_collisionRate line 108
  22. theorem OAI.PiExponent.DeterminantContradiction.no_fixed_data_of_interpolation_and_analytic_aggregate line 125
  23. theorem OAI.PiExponent.DeterminantContradiction.piEventualLowerBound_of_interpolation_and_analytic_aggregate line 167