OAI/NumberTheory/Jacobsthal/Estimates/EvenInverseBands.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.Erdos970Dependency.StateMarginalBridge.evenReal_map_lift line 19
  2. theorem OAI.Erdos970.Erdos970Dependency.StateMarginalBridge.oddReal_map_lift line 25
  3. theorem OAI.Erdos970.Erdos970Dependency.StateMarginalBridge.propagate_even line 31
  4. theorem OAI.Erdos970.Erdos970Dependency.StateMarginalBridge.propagate_odd line 39
  5. theorem OAI.Erdos970.Erdos970Dependency.StateMarginalBridge.state_even_first line 47
  6. theorem OAI.Erdos970.Erdos970Dependency.StateMarginalBridge.state_odd_first line 52
  7. theorem OAI.Erdos970.Erdos970Dependency.StateMarginalBridge.state_even_two line 57
  8. theorem OAI.Erdos970.Erdos970Dependency.StateMarginalBridge.state_odd_two line 64
  9. theorem OAI.Erdos970.Erdos970Dependency.StateMarginalBridge.state_reg_three line 71
  10. theorem OAI.Erdos970.Erdos970Dependency.InitialStateDomination.initial_state_measure_le line 90
  11. theorem OAI.Erdos970.Erdos970Dependency.InitialStateDomination.initial_two_step_domination line 106
  12. def OAI.Erdos970.NumberTheoryLean.InvariantInverseWeights.stateWeight line 125
  13. theorem OAI.Erdos970.NumberTheoryLean.InvariantInverseWeights.stateWeight_pos line 128
  14. theorem OAI.Erdos970.NumberTheoryLean.InvariantInverseWeights.stateWeight_measurable line 133
  15. def OAI.Erdos970.NumberTheoryLean.InvariantInverseWeights.inverseWeightCutoff line 137
  16. theorem OAI.Erdos970.NumberTheoryLean.InvariantInverseWeights.inverseWeightCutoff_measurable line 140
  17. theorem OAI.Erdos970.NumberTheoryLean.InvariantInverseWeights.even_inverse_density_le line 144
  18. theorem OAI.Erdos970.NumberTheoryLean.InvariantInverseWeights.odd_inverse_density_le line 162
  19. theorem OAI.Erdos970.NumberTheoryLean.InvariantInverseWeights.inverseWeightCutoff_mass_le line 182
  20. def OAI.Erdos970.NumberTheoryLean.FirstStepInverseWeight.firstDensityConstant line 225
  21. theorem OAI.Erdos970.NumberTheoryLean.FirstStepInverseWeight.firstDensityConstant_pos line 227
  22. theorem OAI.Erdos970.NumberTheoryLean.FirstStepInverseWeight.W_le_three line 229
  23. theorem OAI.Erdos970.NumberTheoryLean.FirstStepInverseWeight.first_odd_density_bound line 235
  24. theorem OAI.Erdos970.NumberTheoryLean.FirstStepInverseWeight.first_odd_inverse_mass line 259
  25. def OAI.Erdos970.NumberTheoryLean.RegeneratingInverseBands.gapValue line 314
  26. def OAI.Erdos970.NumberTheoryLean.RegeneratingInverseBands.inverseArrivalBand line 316
  27. theorem OAI.Erdos970.NumberTheoryLean.RegeneratingInverseBands.inverseArrivalBand_measurable line 321
  28. theorem OAI.Erdos970.NumberTheoryLean.RegeneratingInverseBands.stateBandReward_le line 328
  29. theorem OAI.Erdos970.NumberTheoryLean.RegeneratingInverseBands.inverseArrivalBand_le_costBand line 337
  30. theorem OAI.Erdos970.NumberTheoryLean.RegeneratingInverseBands.regeneration_inverse_cutoff_band line 362
  31. theorem OAI.Erdos970.NumberTheoryLean.RegeneratingInverseBands.regeneration_inverse_arrival_band line 375
  32. theorem OAI.Erdos970.NumberTheoryLean.RegeneratingInverseBands.first_odd_inverse_arrival_band line 387
  33. theorem OAI.Erdos970.NumberTheoryLean.EvenBandBounds.even_uniform_band line 416
  34. theorem OAI.Erdos970.NumberTheoryLean.EvenBandBounds.prefixOccupation_two line 437
  35. theorem OAI.Erdos970.NumberTheoryLean.EvenBandBounds.fullOccupation_first_and_later line 442
  36. def OAI.Erdos970.NumberTheoryLean.WeightedGapTail.tailSeries line 459
  37. theorem OAI.Erdos970.NumberTheoryLean.WeightedGapTail.tailSeries_nonneg line 462
  38. theorem OAI.Erdos970.NumberTheoryLean.WeightedGapTail.tailSeries_summable line 464
  39. def OAI.Erdos970.NumberTheoryLean.WeightedGapTail.tailBudget line 474
  40. theorem OAI.Erdos970.NumberTheoryLean.WeightedGapTail.tailBudget_tendsto_zero line 477
  41. def OAI.Erdos970.NumberTheoryLean.WeightedGapTail.tailReward line 484
  42. theorem OAI.Erdos970.NumberTheoryLean.WeightedGapTail.tailReward_measurable line 489
  43. def OAI.Erdos970.NumberTheoryLean.WeightedGapTail.binCoefficient line 496
  44. theorem OAI.Erdos970.NumberTheoryLean.WeightedGapTail.tailReward_le_band_sum line 499
  45. theorem OAI.Erdos970.NumberTheoryLean.WeightedGapTail.weighted_tail_of_inverse_bands line 541
  46. theorem OAI.Erdos970.NumberTheoryLean.WeightedGapTail.regeneration_weighted_tail line 569
  47. def OAI.Erdos970.ErdosHighRatioBandTail.highStates line 594
  48. def OAI.Erdos970.ErdosHighRatioBandTail.highReward line 596
  49. def OAI.Erdos970.ErdosHighRatioBandTail.highBand line 599
  50. theorem OAI.Erdos970.ErdosHighRatioBandTail.highStates_measurable line 602
  51. theorem OAI.Erdos970.ErdosHighRatioBandTail.highReward_measurable line 605
  52. theorem OAI.Erdos970.ErdosHighRatioBandTail.highBand_measurable line 608
  53. theorem OAI.Erdos970.ErdosHighRatioBandTail.highReward_integral line 612
  54. theorem OAI.Erdos970.ErdosHighRatioBandTail.highBand_integral line 617
  55. theorem OAI.Erdos970.ErdosHighRatioBandTail.stateMeasure_tail_tendsto line 627
  56. theorem OAI.Erdos970.ErdosHighRatioBandTail.later_band_tail_bound line 643
  57. theorem OAI.Erdos970.NumberTheoryLean.EvenInverseBands.even_inverse_arrival_from_two line 666
  58. theorem OAI.Erdos970.NumberTheoryLean.EvenInverseBands.even_future_inverse_arrival_band line 685
  59. theorem OAI.Erdos970.NumberTheoryLean.EvenInverseBands.inverseArrivalBand_le_weight line 699
  60. theorem OAI.Erdos970.NumberTheoryLean.EvenInverseBands.starting_inverse_weight_le line 708
  61. theorem OAI.Erdos970.NumberTheoryLean.EvenInverseBands.source_inverse_phi_band line 714
  62. theorem OAI.Erdos970.NumberTheoryLean.EvenInverseBands.source_exponential_reward_tail line 735