RepresentationAllocatedSurvival.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The surviving representation and the resource event in the same trial

def OAI.LowSpaceSubsetSum.backgroundChild line 12
Source documentation
Combine each adjacent pair of leaves into its parent child.
```
def backgroundChild (b : Fin 2 × Fin 4) : Fin 4 :=
…
```
theorem OAI.LowSpaceSubsetSum.backgroundChild_eq_iff line 15
def OAI.LowSpaceSubsetSum.RepresentationSetup.allocatedChildAssignment line 27
Source documentation
The four-child assignment used in the survival proof is obtained from the same computed eight-leaf assignment used for the resource counts.
```
def allocatedChildAssignment (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000) :
    BackgroundAssignment n :=
…
```
Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.RepresentationSetup.BackgroundAssignment
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.allocated_child_background line 32

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.allocated_representation_with_resources line 46

Source documentation

The concrete computed allocation retains a representation and the unconditional ambient resource event with probability at least .9 u^-100.

theorem allocated_representation_with_resources (hn : 180000000 ≤ n)
    (hmean : meanDeficiency R.originalWeights Finset.univ R.halfSize <
      (153 / 20000 : ℝ) * n)
    (hden : (R.halfSize : ℝ) + 1 <
      (2 : ℝ) ^ ((1 / 1500 : ℝ) * R.halfSize))
    (hscale : Real.logb 2 (inputScale R.input : ℝ) ≤ (n : ℝ) / 1000000000) :
    let hlog := representation_log_budget (by omega : 10000 ≤ n)
…

Mentions: OAI.LowSpaceSubsetSum.meanDeficiency, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.representation_log_budget