RepresentationBudgets.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Concrete ambient resource budgets, including integer prime exponents

def OAI.LowSpaceSubsetSum.representationHbar line 13
def OAI.LowSpaceSubsetSum.RepresentationSetup.filterDeficit line 21
def OAI.LowSpaceSubsetSum.RepresentationSetup.resourceGamma line 24
def OAI.LowSpaceSubsetSum.RepresentationSetup.resourceLambda line 28
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.lowExponent_eq_half_sub line 33
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.floor_lowExponent_lower line 40
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.filterDeficit_le_tau line 45
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.local_filterDeficit_le_max line 48
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.beta_sub_floor_lowExponent line 54
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.twice_beta_sub_floor_lowExponents line 66
Source documentation
The strict tuple slack absorbs both losses from flooring low exponents.
```
theorem twice_beta_sub_floor_lowExponents (z : Layout n) (g : Guesses n)
    (hn : 20000 ≤ n) (j : Fin 2) :
    2 * representationBeta n g j - (⌊R.lowExponent z 0⌋₊ : ℝ) -
      (⌊R.lowExponent z j.succ⌋₊ : ℝ) ≤ (n : ℝ) / 2 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.RepresentationSetup.Guesses, OAI.LowSpaceSubsetSum.representationBeta

theorem OAI.LowSpaceSubsetSum.RepresentationMoments.pair_budget_with_floor line 90

Source documentation

A one-bit loss in each child exponent is absorbed by the polynomial factor in the input scale, while preserving the exact exponential rate.

theorem pair_budget_with_floor {ι : Type*} (L R : Fin 4 → RepresentationLeaf ι)
    {u betaL betaR ellL ellR pL pR gamma : ℝ} (hu : 8 ≤ u)
    (hpL : 0 < pL) (hpR : 0 < pR)
    (hL : ∀ i, ((L i).occurrences.card : ℝ) ≤ u ^ 10 * (2 : ℝ) ^ (betaL / 2))
    (hR : ∀ i, ((R i).occurrences.card : ℝ) ≤ u ^ 10 * (2 : ℝ) ^ (betaR / 2))
    (hmL : (2 : ℝ) ^ ellL / u ^ 5 ≤ pL) (hmR : (2 : ℝ) ^ ellR / u ^ 5 ≤ pR)
    (hgL : betaL - ellL ≤ gamma + 1) (hgR : betaR - ellR ≤ gamma + 1) :
    ((RepresentationUniverse.children L 0).card + (RepresentationUniverse.children L 1).card : ℝ) / pL +
      ((RepresentationUniverse.children R 0).card + (RepresentationUniverse.children R 1).card : ℝ) / pR ≤
        u ^ 26 * (2 : ℝ) ^ gamma := by
…

Mentions: OAI.LowSpaceSubsetSum.RepresentationLeaf, OAI.LowSpaceSubsetSum.RepresentationUniverse.children

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.entry_exponent_with_floor line 125
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.allocated_entry_budget line 161
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.allocated_resource_failure line 184