OAI/Combinatorics/GraphThreshold/CapacityIteration.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Capacities and finite inflation products

The capacity after t successful reductions is natural-number division by 2^t. All product estimates below are finite; no infinite product is used.

  1. def OAI.LeanBlast.SecondKahnKalai.reducedCapacity line 25
  2. def OAI.LeanBlast.SecondKahnKalai.successesNeeded line 27
  3. theorem OAI.LeanBlast.SecondKahnKalai.reducedCapacity_zero line 29
  4. theorem OAI.LeanBlast.SecondKahnKalai.reducedCapacity_succ line 32
  5. theorem OAI.LeanBlast.SecondKahnKalai.reducedCapacity_add line 36
  6. theorem OAI.LeanBlast.SecondKahnKalai.reducedCapacity_eq_floor line 40
  7. theorem OAI.LeanBlast.SecondKahnKalai.antitone_reducedCapacity line 45
  8. theorem OAI.LeanBlast.SecondKahnKalai.monotone_reducedCapacity_left line 51
  9. theorem OAI.LeanBlast.SecondKahnKalai.reducedCapacity_zero_prefix line 55
  10. theorem OAI.LeanBlast.SecondKahnKalai.reducedCapacity_growth line 62
  11. theorem OAI.LeanBlast.SecondKahnKalai.strictAntiOn_reducedCapacity line 71
  12. theorem OAI.LeanBlast.SecondKahnKalai.reducedCapacity_successesNeeded line 79
  13. theorem OAI.LeanBlast.SecondKahnKalai.reducedCapacity_eq_zero_of_le line 83
  14. theorem OAI.LeanBlast.SecondKahnKalai.successesNeeded_pos line 87
  15. theorem OAI.LeanBlast.SecondKahnKalai.monotone_successesNeeded line 90
  16. theorem OAI.LeanBlast.SecondKahnKalai.successesNeeded_half_lt line 95
  17. theorem OAI.LeanBlast.SecondKahnKalai.successesNeeded_eq_floor_logb line 103
  18. theorem OAI.LeanBlast.SecondKahnKalai.successesNeeded_le_logb line 108
  19. theorem OAI.LeanBlast.SecondKahnKalai.capacity_logb_nonneg line 114
  20. theorem OAI.LeanBlast.SecondKahnKalai.label_empty_after_successes line 118
  21. theorem OAI.LeanBlast.SecondKahnKalai.capacity_prefix_sum_le line 125

    Source documentation

    Geometric growth bounds every earlier prefix by one fifteenth of the current capacity. The natural form avoids premature division.

    theorem capacity_prefix_sum_le (m : ℕ → ℕ) (k : ℕ)
    (hgrowth : ∀ j, j + 1 < k → 16 * m j ≤ m (j + 1)) :
    ∀ j, j < k → 15 * (∑ h ∈ range j, m h) ≤ m j := by
…
  22. theorem OAI.LeanBlast.SecondKahnKalai.capacity_prefix_sum_real_le line 138
  23. theorem OAI.LeanBlast.SecondKahnKalai.strictMonoOn_capacities line 146
  24. theorem OAI.LeanBlast.SecondKahnKalai.monotoneOn_capacities line 164

    Source documentation

    Index monotonicity also holds before an initial zero-capacity segment is removed. No positivity assumption is needed here.

    theorem monotoneOn_capacities (m : ℕ → ℕ) (k : ℕ)
    (hgrowth : ∀ j, j + 1 < k → 16 * m j ≤ m (j + 1)) :
    MonotoneOn m (Set.Iio k) := by
…
  25. theorem OAI.LeanBlast.SecondKahnKalai.sum_positive_geometric_le line 174

    Source documentation

    A finite sum of distinct positive geometric powers.

    theorem sum_positive_geometric_le (s : Finset ℕ) {q : ℝ}
    (hq : 0 ≤ q) (hq1 : q < 1) (hpos : ∀ m ∈ s, 1 ≤ m) :
    (∑ m ∈ s, q ^ m) ≤ q / (1 - q) := by
…
  26. theorem OAI.LeanBlast.SecondKahnKalai.one_sub_sum_le_prod_one_sub line 189

    Source documentation

    Elementary finite product bound, applied below to the retention factors.

    theorem one_sub_sum_le_prod_one_sub {ι : Type*} (s : Finset ι) (f : ι → ℝ)
    (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ 1) :
    1 - (∑ i ∈ s, f i) ≤ ∏ i ∈ s, (1 - f i) := by
…
  27. theorem OAI.LeanBlast.SecondKahnKalai.exp_neg_one_le_two_fifths line 205
  28. theorem OAI.LeanBlast.SecondKahnKalai.sum_exp_neg_capacities_le_two_thirds line 214
  29. theorem OAI.LeanBlast.SecondKahnKalai.finite_retentionProduct_ge_one_third line 226
  30. theorem OAI.LeanBlast.SecondKahnKalai.finite_spreadInflation_lt_four line 237
  31. theorem OAI.LeanBlast.SecondKahnKalai.spreadInflation_lt_four line 246
  32. def OAI.LeanBlast.SecondKahnKalai.iteratedSpread line 260
  33. theorem OAI.LeanBlast.SecondKahnKalai.iteratedSpread_zero line 263
  34. theorem OAI.LeanBlast.SecondKahnKalai.iteratedSpread_succ line 266
  35. theorem OAI.LeanBlast.SecondKahnKalai.halving_spreadInflation_lt_four line 271
  36. theorem OAI.LeanBlast.SecondKahnKalai.iteratedSpread_pos line 280
  37. theorem OAI.LeanBlast.SecondKahnKalai.iteratedSpread_le_four_mul line 292
  38. theorem OAI.LeanBlast.SecondKahnKalai.exp_neg_seven_le_one_eighth line 297
  39. theorem OAI.LeanBlast.SecondKahnKalai.sum_exp_neg_seven_capacities_lt_one_quarter line 306
  40. theorem OAI.LeanBlast.SecondKahnKalai.capacity_failure_sum_lt_one_quarter line 320
  41. def OAI.LeanBlast.SecondKahnKalai.capacityReserve line 349

    Source documentation

    A history-free allowance for the spread parameter at capacity m.

    def capacityReserve (σ : ℝ) (m : ℕ) : ℝ :=
…
  42. theorem OAI.LeanBlast.SecondKahnKalai.retentionFactor_pos line 352
  43. theorem OAI.LeanBlast.SecondKahnKalai.retentionFactor_le_one line 358
  44. theorem OAI.LeanBlast.SecondKahnKalai.capacityReserve_zero line 361
  45. theorem OAI.LeanBlast.SecondKahnKalai.capacityReserve_pos line 364
  46. theorem OAI.LeanBlast.SecondKahnKalai.capacityReserve_lower line 371
  47. theorem OAI.LeanBlast.SecondKahnKalai.capacityReserve_upper line 379
  48. theorem OAI.LeanBlast.SecondKahnKalai.antitone_capacityReserve line 390
  49. theorem OAI.LeanBlast.SecondKahnKalai.capacityReserve_succ line 403
  50. theorem OAI.LeanBlast.SecondKahnKalai.capacityReserve_div_le_half line 408