RepresentationChosenWeights.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Exact weights of the chosen raw representation tuples

theorem OAI.LowSpaceSubsetSum.partition_complement_parts line 11
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.topBlocks_union line 49
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.maskParent_topMask line 60
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.maskParent_localMask line 80
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.maskParent_backgroundMask line 102
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.background_four_union line 122
Source documentation
All four assigned pieces partition the solution outside the mixers.
```
theorem background_four_union (B : BackgroundAssignment n) (z : Layout n) (g : Guesses n) :
    ((R.background B z g 0 ∪ R.background B z g 1) ∪ R.background B z g 2) ∪
      R.background B z g 3 = R.outside z := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.BackgroundAssignment, OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.RepresentationSetup.Guesses
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.solution_halves_outside line 136

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rightParent_parts line 146

Source documentation

The complementary parent's concrete three pieces equal the named set difference.

theorem rightParent_parts (B : BackgroundAssignment n) {h : R.PrimeHistory}
    {r : R.Residues h.2} (hr : R.ResidueSuccess (R.actualOffsets B) h r) :
    R.rightParent B h r =
      ((R.selectedHalves h.1.1.1 0 \ R.chosenMasks (R.actualOffsets B) h r 0) ∪
        R.selectedHalves h.1.1.1 2) ∪
      (R.background B h.1.1.1 h.1.1.2 2 ∪ R.background B h.1.1.1 h.1.1.2 3) := by
…

Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.BackgroundAssignment

def OAI.LowSpaceSubsetSum.RepresentationSetup.maskParentSet line 167
Source documentation
The union of every component of a raw parent.
```
def maskParentSet (z : Layout n) (f : R.Partitions z) (B : Fin n → Fin 2 × Fin 4)
    (D : Fin 3 → Finset (Fin n)) (j : Fin 2) : Finset (Fin n) :=
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.maskParentSet_eq line 173
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosen_parent_sets_eq line 184

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.mask_components_disjoint line 203

Source documentation

Different component types live in disjoint mixer/background regions.

theorem mask_components_disjoint (z : Layout n) (f : R.Partitions z)
    (B : Fin n → Fin 2 × Fin 4) (D : Fin 3 → Finset (Fin n)) (j : Fin 2)
    (i k : Fin 4) :
    Disjoint (R.maskLeafOccurrence z f B D j i).1.1
        (R.maskLeafOccurrence z f B D j k).1.2 ∧
    Disjoint (R.maskLeafOccurrence z f B D j i).1.1
        (R.maskLeafOccurrence z f B D j k).2 ∧
    Disjoint (R.maskLeafOccurrence z f B D j i).1.2
        (R.maskLeafOccurrence z f B D j k).2 := by
…

Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.maskParentOccurrence_weight line 232
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.maskFirstChild_weight line 261

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosen_raw_weights line 295

Source documentation

All six raw tuple weights are the weights used by the survival event.

theorem chosen_raw_weights (h : R.PrimeHistory) (r : R.Residues h.2)
    (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (hr : R.ResidueSuccess (R.actualOffsets (R.allocatedChildAssignment hn hlog)) h r) :
    let B := R.allocatedChildAssignment hn hlog
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosen_raw_filters line 338

Source documentation

The six congruences hold for the actual raw tuples fed to the pair streams.

theorem chosen_raw_filters (h : R.PrimeHistory) (r : R.Residues h.2)
    (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (hr : R.ResidueSuccess (R.actualOffsets (R.allocatedChildAssignment hn hlog)) h r) :
    let B := R.allocatedChildAssignment hn hlog
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize