OAI/NumberTheory/DirichletL/CubicSieve/PooledRows.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecondPassArithmetic.GlobalFirstAdmissible line 83
  2. def OAI.SecondPassArithmetic.globalFirstIndex line 88
  3. def OAI.SecondPassArithmetic.globalFirstPooledRow line 91
  4. def OAI.SecondPassArithmetic.globalFirstCoefficient line 94
  5. theorem OAI.SecondPassArithmetic.globalPooledRowScale_first line 98
  6. theorem OAI.SecondPassArithmetic.globalBinFirstCoefficient_first line 109
  7. def OAI.SecondPassArithmetic.globalFirstConcreteCutoff line 119
  8. def OAI.SecondPassArithmetic.globalFirstSupportedPool line 124
  9. theorem OAI.SecondPassArithmetic.globalFirstSupportedPool_admissible line 131
  10. theorem OAI.SecondPassArithmetic.globalFirstSupportedPool_frequency_ne_zero line 142
  11. theorem OAI.SecondPassArithmetic.globalFirstSupportedPool_index_mem_box line 152
  12. theorem OAI.SecondPassArithmetic.globalSecondLiteralTerm_zero_of_not_support line 183
  13. theorem OAI.SecondPassArithmetic.globalFirstTruncatedSource_eq_supported line 201
  14. theorem OAI.SecondPassArithmetic.globalFirstTruncatedSource_eq_bins line 225
  15. def OAI.SecondPassArithmetic.globalChildBudget line 290
  16. theorem OAI.SecondPassArithmetic.globalFirstTruncatedSource_actual_transfer line 303
  17. theorem OAI.SecondPassArithmetic.globalFirstCoreRows_actual_transfer line 363
  18. abbrev OAI.InitialMeanSquare.O line 446
  19. structure OAI.InitialMeanSquare.Datum line 448
  20. def OAI.InitialMeanSquare.newRow line 454
  21. def OAI.InitialMeanSquare.newLabel line 455
  22. def OAI.InitialMeanSquare.oldCommon line 456
  23. def OAI.InitialMeanSquare.observation line 457
  24. theorem OAI.InitialMeanSquare.span_newRow line 459
  25. theorem OAI.InitialMeanSquare.divisor_dvd_row line 463
  26. theorem OAI.InitialMeanSquare.divisor_dvd_label line 467
  27. theorem OAI.InitialMeanSquare.divisor_ne_zero_of_row line 469
  28. theorem OAI.InitialMeanSquare.divisor_injective_on_fiber line 474
  29. theorem OAI.InitialMeanSquare.fiber_card_le line 498
  30. theorem OAI.InitialMeanSquare.fiber_small_power line 513
  31. theorem OAI.InitialMeanSquare.weighted_energy_pushforward line 526
  32. theorem OAI.InitialMeanSquare.norm_newRow line 545
  33. theorem OAI.InitialMeanSquare.norm_newLabel line 549
  34. theorem OAI.InitialMeanSquare.norm_oldCommon line 553
  35. theorem OAI.InitialMeanSquare.label_and_mask line 559
  36. def OAI.InitialMeanSquare.columnScale line 576
  37. def OAI.InitialMeanSquare.rowScale line 577
  38. theorem OAI.InitialMeanSquare.initial_prefactor line 579
  39. theorem OAI.InitialMeanSquare.initial_column_scale line 582
  40. theorem OAI.InitialMeanSquare.initial_row_bound line 585
  41. theorem OAI.InitialMeanSquare.initial_mass line 594
  42. theorem OAI.InitialMeanSquare.initial_invariant_identity line 598
  43. theorem OAI.InitialMeanSquare.initial_invariant_bound line 604
  44. theorem OAI.InitialMeanSquare.initial_invariant_power_general line 611
  45. theorem OAI.InitialMeanSquare.initial_invariant_power line 621
  46. theorem OAI.InitialMeanSquare.initial_invariant_reserved_margin line 632
  47. theorem OAI.InitialMeanSquare.initial_budget_identity line 646