OAI/NumberTheory/Catalan/Arithmetic/SmallOddPrimePartition.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.parityBoundarySum_prime_log_lower line 15
  2. theorem OAI.InternalCatalan.boundaryPlus_odd_prime_log_lower line 26
  3. theorem OAI.InternalCatalan.boundaryMinus_odd_prime_log_lower line 45
  4. theorem OAI.InternalCatalan.momentRat_odd_prime_log_lower line 60
  5. theorem OAI.InternalCatalan.int_prime_valuation_nonneg line 93
  6. theorem OAI.InternalCatalan.rational_prime_valuation_den_lower line 99
  7. theorem OAI.InternalCatalan.centralCoeffKernel_odd_prime_nonneg line 105
  8. theorem OAI.InternalCatalan.prime_add_lower line 112
  9. theorem OAI.InternalCatalan.rawEntryRat_odd_prime_log_lower line 117
  10. theorem OAI.InternalCatalan.filteredEntryRat_odd_prime_log_lower line 161
  11. theorem OAI.InternalCatalan.prime_prod_valuation_lower line 193
  12. theorem OAI.InternalCatalan.prime_det_valuation_lower line 211
  13. theorem OAI.InternalCatalan.determinantRat_odd_prime_log_lower line 229
  14. theorem OAI.InternalCatalan.nat_log_mul_log_prime_le line 247
  15. theorem OAI.InternalCatalan.nat_valuation_mul_log_prime_le line 255
  16. theorem OAI.InternalCatalan.determinantRat_odd_prime_log_weighted_lower line 265
  17. theorem OAI.InternalCatalan.determinantRat_odd_prime_above_degrees_integral line 293
  18. theorem OAI.InternalCatalan.log_abs_determinantRat_truncated_lower line 311
  19. theorem OAI.InternalCatalan.prime_ne_H line 365
  20. theorem OAI.InternalCatalan.determinantRat_above_degrees_local_integral line 376
  21. theorem OAI.InternalCatalan.determinantRat_odd_prime_loss_above_degrees line 386
  22. def OAI.InternalCatalan.smallOddPrimes line 407
  23. theorem OAI.InternalCatalan.mem_smallOddPrimes_iff line 410
  24. theorem OAI.InternalCatalan.smallOddPrimes_card_le line 420
  25. def OAI.InternalCatalan.smallOddPrimeContribution line 432
  26. def OAI.InternalCatalan.smallOddPrimeError line 436
  27. theorem OAI.InternalCatalan.smallOddPrimeError_nonneg line 440
  28. theorem OAI.InternalCatalan.smallOddPrimeContribution_lower line 451
  29. theorem OAI.InternalCatalan.prime_prod_valuation_weighted_lower line 492
  30. theorem OAI.InternalCatalan.oddPhysicalScalar_valuation_lower line 506
  31. theorem OAI.InternalCatalan.oddPhysicalVector_valuation_nonneg line 528
  32. theorem OAI.InternalCatalan.oddPhysicalVectorMinor_valuation_nonneg line 545
  33. theorem OAI.InternalCatalan.oddPhysicalMinor_valuation_lower line 560
  34. theorem OAI.InternalCatalan.log_nat_div_sqrt_tendsto_zero line 605
  35. theorem OAI.InternalCatalan.smallOddPrimeError_div_sq_eq line 620
  36. theorem OAI.InternalCatalan.smallOddPrimeError_div_sq_tendsto_zero line 638
  37. theorem OAI.InternalCatalan.smallOddPrimeContribution_eventually_lower line 649
  38. theorem OAI.InternalCatalan.smallOddPrimeCutoff_bounds line 673
  39. theorem OAI.InternalCatalan.smallOddPrimes_eq_filter_H line 684
  40. theorem OAI.InternalCatalan.oddPrimeContribution_split line 698