OAI/Probability/CubeShuffle/DimensionEstimates.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubeShuffle.DimensionEstimates.log_factorial_upper_binary line 8
  2. lemma OAI.CubeShuffle.DimensionEstimates.log_factorial_lower line 28
  3. lemma OAI.CubeShuffle.DimensionEstimates.log_factorial_upper line 42
  4. def OAI.CubeShuffle.DimensionEstimates.fiberWeight line 60
  5. lemma OAI.CubeShuffle.DimensionEstimates.fiberWeight_nonneg line 63
  6. lemma OAI.CubeShuffle.DimensionEstimates.fiberWeight_pos line 66
  7. lemma OAI.CubeShuffle.DimensionEstimates.fiber_sum line 70
  8. lemma OAI.CubeShuffle.DimensionEstimates.sum_fiberWeight line 81
  9. theorem OAI.CubeShuffle.DimensionEstimates.incidence_entropy line 86

    Source documentation

    Entropy subadditivity for a finite simple bipartite incidence set.

    theorem incidence_entropy (f : X → I) (g : X → J)
    (hinj : Function.Injective (fun x => (f x,g x))) :
    (∑ i, fiberWeight f i*Real.log (fiberWeight f i))+
      (∑ j, fiberWeight g j*Real.log (fiberWeight g j)) ≤
        (Fintype.card X:ℝ)*Real.log (Fintype.card X) := by
…

    Mentions: OAI.CubeShuffle.DimensionEstimates.fiberWeight

  10. lemma OAI.CubeShuffle.DimensionEstimates.log_factorial_upper_binary_all line 132
  11. lemma OAI.CubeShuffle.DimensionEstimates.log_fiber_factorials line 139
  12. theorem OAI.CubeShuffle.DimensionEstimates.dimension_log_from_incidence line 153

    Source documentation

    A dimension lower bound using only the actual row and column subgroup orders, incidence injectivity, and elementary factorial estimates.

    theorem dimension_log_from_incidence {X I J : Type*} [Fintype X] [Fintype I] [Fintype J]
    [Nonempty X] (f : X → I) (g : X → J)
    (hinj : Function.Injective (fun x => (f x,g x))) (D : ℕ)
    (hD : (Fintype.card X).factorial ≤ D *
      (∏ i, (Fintype.card {x // f x=i}).factorial) *
      (∏ j, (Fintype.card {x // g x=j}).factorial)) :
    ((2*Real.log 2-1)*(Fintype.card X:ℝ)-
      Real.log 2*((Fintype.card I:ℝ)+Fintype.card J)+1) ≤ Real.log D := by
…
  13. lemma OAI.CubeShuffle.DimensionEstimates.scaled_binEntropy line 183
  14. lemma OAI.CubeShuffle.DimensionEstimates.log_choose_lower_entropy line 193
  15. lemma OAI.CubeShuffle.DimensionEstimates.binEntropy_three_quarters line 215
  16. def OAI.CubeShuffle.DimensionEstimates.entropyGap line 224
  17. lemma OAI.CubeShuffle.DimensionEstimates.entropyGap_pos line 226
  18. lemma OAI.CubeShuffle.DimensionEstimates.entropyGap_eq line 230
  19. lemma OAI.CubeShuffle.DimensionEstimates.binEntropy_tail_lower line 238

    Source documentation

    An elementary exponential-dimension constant up to tail fraction 3/4. It avoids a hook formula or tableau-counting assumption.

    lemma binEntropy_tail_lower (q : ℝ) (hq : 0≤q) (hq' : q≤3/4) :
    q*Real.log 2+entropyGap*q ≤ Real.binEntropy q := by
…

    Mentions: OAI.CubeShuffle.DimensionEstimates.entropyGap

  20. lemma OAI.CubeShuffle.DimensionEstimates.log_dimension_from_binomial line 251
  21. lemma OAI.CubeShuffle.DimensionEstimates.balanced_dimension_coefficient_pos line 269
  22. lemma OAI.CubeShuffle.DimensionEstimates.log_choose_upper line 276
  23. lemma OAI.CubeShuffle.DimensionEstimates.log_choose_lower line 283
  24. lemma OAI.CubeShuffle.DimensionEstimates.footprint_log_bound line 291
  25. lemma OAI.CubeShuffle.DimensionEstimates.log_factorial_le_mul_log line 309
  26. lemma OAI.CubeShuffle.DimensionEstimates.near_row_log_dimension line 315
  27. def OAI.CubeShuffle.DimensionEstimates.nearPower line 348
  28. def OAI.CubeShuffle.DimensionEstimates.nearFraction line 349
  29. def OAI.CubeShuffle.DimensionEstimates.tailPower line 350
  30. def OAI.CubeShuffle.DimensionEstimates.chosenTuple line 352
  31. lemma OAI.CubeShuffle.DimensionEstimates.chosenTuple_bounds line 355
  32. lemma OAI.CubeShuffle.DimensionEstimates.chosenTuple_tail_lower line 379
  33. lemma OAI.CubeShuffle.DimensionEstimates.chosenTuple_log_footprint line 389

    Source documentation

    Quantitative footprint gain at the source's very sparse intermediate tuple size.

    lemma chosenTuple_log_footprint (N j D m : ℕ) (hj : 0<j)
    (hN : 2*j≤N) (hD : N.choose j≤D*2^j)
    (hx : 2≤((N:ℝ)/j)^nearPower)
    (hlog : 8*Real.log 2/nearPower≤Real.log ((N:ℝ)/j))
    (hfoot : D * (chosenTuple N j).choose j ≤ m * N.choose j) :
    nearFraction*Real.log D≤Real.log m := by
…

    Mentions: OAI.CubeShuffle.DimensionEstimates.nearPower, OAI.CubeShuffle.DimensionEstimates.chosenTuple, OAI.CubeShuffle.DimensionEstimates.nearFraction

  34. lemma OAI.CubeShuffle.DimensionEstimates.near_row_log_uniform line 427
  35. lemma OAI.CubeShuffle.DimensionEstimates.chosenTuple_density_bound line 448
  36. lemma OAI.CubeShuffle.DimensionEstimates.near_conditions_eventually line 487

    Source documentation

    All cutoffs are absolute. In particular the near-row density cost can be made smaller than the genuine footprint logarithm, uniformly over that range.

    lemma near_conditions_eventually (C : ℝ) :
    ∀ᶠ x : ℝ in atTop, 2≤x ∧ 2≤x^nearPower ∧ x^(nearPower-1)≤1/2 ∧
      8*Real.log 2/nearPower≤Real.log x ∧ 4*Real.log 2+2≤Real.log x ∧
      C*2^(1+(1/512:ℝ))*x^(-tailPower) ≤ nearFraction/4000 := by
…

    Mentions: OAI.CubeShuffle.DimensionEstimates.nearPower, OAI.CubeShuffle.DimensionEstimates.tailPower, OAI.CubeShuffle.DimensionEstimates.nearFraction

  37. theorem OAI.CubeShuffle.DimensionEstimates.exists_near_cutoff line 509

    Source documentation

    This is the exact simultaneous numerical choice needed by the small-tail regime of the manuscript: an actual integer k and its density/multiplicity gains.

    theorem exists_near_cutoff (C : ℝ) (hC : 0≤C) :
    ∃ X : ℝ, 2≤X ∧ ∀ (N j D m : ℕ), 0<j → X≤(N:ℝ)/j →
      N.choose j≤D*2^j →
      D * (chosenTuple N j).choose j ≤ m * N.choose j →
      j≤chosenTuple N j ∧ chosenTuple N j≤N ∧
      nearFraction*Real.log D≤Real.log m ∧
      C*(chosenTuple N j:ℝ)*((chosenTuple N j:ℝ)/N)^(1/512:ℝ)≤Real.log m/4000 ∧
      (1/2:ℝ)*Real.log N≤Real.log D ∧ (j:ℝ)≤Real.log D := by
…

    Mentions: OAI.CubeShuffle.DimensionEstimates.chosenTuple, OAI.CubeShuffle.DimensionEstimates.nearFraction

  38. lemma OAI.CubeShuffle.DimensionEstimates.amplification_numerical line 537
  39. lemma OAI.CubeShuffle.DimensionEstimates.amplification_absorb line 555
  40. lemma OAI.CubeShuffle.DimensionEstimates.amplification_decay line 560
  41. lemma OAI.CubeShuffle.DimensionEstimates.finset_power_sum line 572
  42. lemma OAI.CubeShuffle.DimensionEstimates.small_sets_count line 577
  43. lemma OAI.CubeShuffle.DimensionEstimates.small_sets_ceil_bound line 603
  44. lemma OAI.CubeShuffle.DimensionEstimates.exists_small_set_rate line 612

    Source documentation

    The exceptional-subset entropy rate can be made arbitrarily small by shrinking its positive fraction, after every other absolute parameter is fixed.

    lemma exists_small_set_rate (κ ε₀ : ℝ) (hκ : 0<κ) (hε₀ : 0<ε₀) :
    ∃ ε : ℝ, 0<ε ∧ ε≤ε₀ ∧ ε<1/2 ∧ ∃ t : ℝ, 0≤t ∧
      t*ε+Real.log (1+Real.exp (-t))≤κ := by
…
  45. lemma OAI.CubeShuffle.DimensionEstimates.log_error_eventually line 636
  46. lemma OAI.CubeShuffle.DimensionEstimates.geometric_ceil_bound line 653
  47. lemma OAI.CubeShuffle.DimensionEstimates.twopow_tendsto line 665
  48. lemma OAI.CubeShuffle.DimensionEstimates.twopow_nat_tendsto line 668
  49. lemma OAI.CubeShuffle.DimensionEstimates.twopow_mul_eventually line 671
  50. lemma OAI.CubeShuffle.DimensionEstimates.exp_two_absorb line 676