OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationResourceBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Cardinality budgets for the representation resource event

These inequalities turn the actual leaf-product counts and the valid-entry encoding into the resource moments. The remaining input is the deterministic integer allocation estimate for each leaf and entry envelope.

  1. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.pow_two_add line 19
  2. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.leaf_card_entropy line 26

    Source documentation

    Direct binomial counting of the prescribed top/local choices and arbitrary background choices. This includes empty and full prescribed subsets.

    theorem leaf_card_entropy (L : RepresentationLeaf ι)
    (ht : L.topCount ≤ L.top.card) (hl : L.localCount ≤ L.mixer.card) :
    (L.occurrences.card : ℝ) ≤ (2 : ℝ) ^
      ((L.top.card : ℝ) * binaryEntropy ((L.topCount : ℝ) / L.top.card) +
       (L.mixer.card : ℝ) * binaryEntropy ((L.localCount : ℝ) / L.mixer.card) + L.background.card) := by
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationLeaf, OAI.LowSpaceSubsetSum.binaryEntropy

  3. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.entropy_power_cap line 40
  4. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.leaf_card_of_allocation line 53

    Source documentation

    The allocation estimate supplies an entropy inequality; no leaf count is assumed. The finite cardinality follows from direct combination counting.

    theorem leaf_card_of_allocation (L : RepresentationLeaf ι)
    (ht : L.topCount ≤ L.top.card) (hl : L.localCount ≤ L.mixer.card)
    {u beta : ℝ} (hu : 0 < u)
    (hAllocation : (L.top.card : ℝ) * binaryEntropy ((L.topCount : ℝ) / L.top.card) +
       (L.mixer.card : ℝ) * binaryEntropy ((L.localCount : ℝ) / L.mixer.card) + L.background.card ≤
         beta / 2 + Real.logb 2 (u ^ 10)) :
    (L.occurrences.card : ℝ) ≤ u ^ 10 * (2 : ℝ) ^ (beta / 2) :=
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationLeaf, OAI.LowSpaceSubsetSum.binaryEntropy

  5. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.child_card_bound line 63
  6. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.parent_card_bound line 79
  7. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.divide_by_modulus line 94

    Source documentation

    The five-power loss is exactly the proved lower bound for a nested modulus.

    theorem divide_by_modulus {u N p beta ell : ℝ} (hu : 0 < u) (hp : 0 < p)
    (a : ℕ) (hN : N ≤ u ^ a * (2 : ℝ) ^ beta)
    (hmod : (2 : ℝ) ^ ell / u ^ 5 ≤ p) :
    N / p ≤ u ^ (a + 5) * (2 : ℝ) ^ (beta - ell) := by
…
  8. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.divide_by_two_moduli line 109

    Source documentation

    Two independent low filters incur two five-power modulus losses.

    theorem divide_by_two_moduli {u N p q beta ell0 ell : ℝ}
    (hu : 0 < u) (hp : 0 < p) (hq : 0 < q) (a : ℕ)
    (hN : N ≤ u ^ a * (2 : ℝ) ^ beta)
    (hmod0 : (2 : ℝ) ^ ell0 / u ^ 5 ≤ p)
    (hmod : (2 : ℝ) ^ ell / u ^ 5 ≤ q) :
    N / (p * q) ≤ u ^ (a + 10) * (2 : ℝ) ^ (beta - ell0 - ell) := by
…
  9. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.pair_budget line 120
  10. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.tuple_budget line 146
  11. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.entry_card_entropy line 173

    Source documentation

    Exact entropy envelope for distinct valid entries. Local multiplicity is removed by the distinct sumset before any low filter is considered.

    theorem entry_card_entropy (a : ι → ℤ) (L : Fin 4 → RepresentationLeaf ι)
    (ht : RepresentationUniverse.DisjointFour (L 0).top (L 1).top (L 2).top (L 3).top)
    (hk : (L 0).topCount + (L 1).topCount + (L 2).topCount + (L 3).topCount ≤
      (RepresentationUniverse.topDomain L).card) :
    ((RepresentationUniverse.validEntries a L).card : ℝ) ≤ (2 : ℝ) ^
      ((RepresentationUniverse.topDomain L).card * binaryEntropy
        (((L 0).topCount + (L 1).topCount + (L 2).topCount + (L 3).topCount : ℕ) /
          ((RepresentationUniverse.topDomain L).card : ℝ)) +
      (RepresentationUniverse.backgroundDomain L).card +
      ((RepresentationUniverse.mixerDomain L).card - deficiency a (RepresentationUniverse.mixerDomain L))) := by
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationLeaf, OAI.LowSpaceSubsetSum.RepresentationUniverse.DisjointFour, OAI.LowSpaceSubsetSum.RepresentationUniverse.topDomain, OAI.LowSpaceSubsetSum.RepresentationUniverse.validEntries, OAI.LowSpaceSubsetSum.binaryEntropy, OAI.LowSpaceSubsetSum.RepresentationUniverse.backgroundDomain, OAI.LowSpaceSubsetSum.RepresentationUniverse.mixerDomain, OAI.LowSpaceSubsetSum.deficiency

  12. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.entry_budget_of_allocation line 203

    Source documentation

    The entry moment follows from the allocation inequality and the actual modulus lower bound, with exactly the paper's ten-power loss.

    theorem entry_budget_of_allocation (a : ι → ℤ) (L : Fin 4 → RepresentationLeaf ι)
    (ht : RepresentationUniverse.DisjointFour (L 0).top (L 1).top (L 2).top (L 3).top)
    (hk : (L 0).topCount + (L 1).topCount + (L 2).topCount + (L 3).topCount ≤
      (RepresentationUniverse.topDomain L).card)
    {u ell0 p0 lambda : ℝ} (hu : 0 < u) (hp0 : 0 < p0)
    (hm0 : (2 : ℝ) ^ ell0 / u ^ 5 ≤ p0)
    (hAllocation : (RepresentationUniverse.topDomain L).card * binaryEntropy
        (((L 0).topCount + (L 1).topCount + (L 2).topCount + (L 3).topCount : ℕ) /
          ((RepresentationUniverse.topDomain L).card : ℝ)) +
      (RepresentationUniverse.backgroundDomain L).card +
      ((RepresentationUniverse.mixerDomain L).card - deficiency a (RepresentationUniverse.mixerDomain L)) ≤
        (lambda + ell0) + Real.logb 2 (u ^ 5)) :
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationLeaf, OAI.LowSpaceSubsetSum.RepresentationUniverse.DisjointFour, OAI.LowSpaceSubsetSum.RepresentationUniverse.topDomain, OAI.LowSpaceSubsetSum.binaryEntropy, OAI.LowSpaceSubsetSum.RepresentationUniverse.backgroundDomain, OAI.LowSpaceSubsetSum.RepresentationUniverse.mixerDomain, OAI.LowSpaceSubsetSum.deficiency

  13. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.entry_budget line 221

    Source documentation

    Entries are bounded through the actual finite envelope, before any residue is exposed, rather than by an assumed filtered-entry expectation.

    theorem entry_budget (a : ι → ℤ) (L : Fin 4 → RepresentationLeaf ι)
    (ht : RepresentationUniverse.DisjointFour (L 0).top (L 1).top (L 2).top (L 3).top)
    {u ell0 p0 lambda : ℝ} (hu : 0 < u) (hp0 : 0 < p0)
    (hm0 : (2 : ℝ) ^ ell0 / u ^ 5 ≤ p0)
    (hEnvelope :
      (((RepresentationUniverse.topDomain L).card.choose ((L 0).topCount + (L 1).topCount +
        (L 2).topCount + (L 3).topCount) * 2 ^ (RepresentationUniverse.backgroundDomain L).card *
          distinctSumCount a (RepresentationUniverse.mixerDomain L) : ℕ) : ℝ) ≤
            u ^ 5 * (2 : ℝ) ^ (lambda + ell0)) :
    ((RepresentationUniverse.validEntries a L).card : ℝ) / p0 ≤ u ^ 10 * (2 : ℝ) ^ lambda := by
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationLeaf, OAI.LowSpaceSubsetSum.RepresentationUniverse.DisjointFour, OAI.LowSpaceSubsetSum.RepresentationUniverse.topDomain, OAI.LowSpaceSubsetSum.RepresentationUniverse.backgroundDomain, OAI.LowSpaceSubsetSum.distinctSumCount, OAI.LowSpaceSubsetSum.RepresentationUniverse.mixerDomain, OAI.LowSpaceSubsetSum.RepresentationUniverse.validEntries