MovingGiantSamples.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Constructing the moving-giant tree from the sampled compensation slots

Each reversing node samples four positions per leaf of either child. Their products are inserted into both child regular lists. The constructor proves the required product consistency; it does not ask for a pre-existing diagram.

inductive OAI.Ostmann.MovingGiantSamples line 17

Source documentation

The four actual compensation positions per child leaf at a reversal.

inductive MovingGiantSamples : ℕ → Type
  | leaf : MovingGiantSamples 0
  | node {n : ℕ} (samples : TreeLeafTuple (Fin 4 → ℕ) n)
      (left right : MovingGiantSamples n) : MovingGiantSamples (n + 1)

Mentions: OAI.Ostmann.TreeLeafTuple

def OAI.Ostmann.compensationLeafProducts line 22
def OAI.Ostmann.multiplySmallLeaves line 27
theorem OAI.Ostmann.multiplySmallLeaves_product line 32
def OAI.Ostmann.MovingGiantTree.castConstant line 40
theorem OAI.Ostmann.MovingGiantTree.castConstant_frequency line 43
theorem OAI.Ostmann.MovingGiantTree.castConstant_units line 48
def OAI.Ostmann.buildMovingGiantTree line 55
Source documentation
small contains only the fixed regular factors at the top of this history. Bulk values and the two moving giants do not occur in this constructor.
```
def buildMovingGiantTree : (n : ℕ) → (t : FrequencyTree ℤ n) →
    (small : TreeLeafTuple ℕ n) → MovingGiantSamples n →
      MovingGiantTree n (treeLeafProduct n small)
  | 0, t, small, .leaf => .leaf (frequencyRoot 0 t) (treeLeafProduct 0 small)
  | n + 1, t, small, .node samples left right =>
      let u := compensationLeafProducts n samples
…
```
Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingGiantSamples, OAI.Ostmann.MovingGiantTree, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.frequencyRoot, OAI.Ostmann.compensationLeafProducts
theorem OAI.Ostmann.buildMovingGiantTree_frequency line 67
def OAI.Ostmann.movingGiantFrequencyUnits line 72
def OAI.Ostmann.MovingGiantSamples.UnitsAt line 77
theorem OAI.Ostmann.buildMovingGiantTree_units line 85
Source documentation
Unit conditions for the diagram follow from the actual sampled products and original frequency bounds. They are independent of the bulk variables.
```
theorem buildMovingGiantTree_units {q n : ℕ} [Fact q.Prime] (t : FrequencyTree ℤ n)
    (small : TreeLeafTuple ℕ n) (samples : MovingGiantSamples n)
    (hfreq : movingGiantFrequencyUnits q n t)
    (hsmall : ((treeLeafProduct n small : ℕ) : ZMod q) ≠ 0)
    (hsamples : samples.UnitsAt q) :
    (buildMovingGiantTree n t small samples).UnitsAt q := by
…
```
Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingGiantSamples, OAI.Ostmann.movingGiantFrequencyUnits, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.buildMovingGiantTree
theorem OAI.Ostmann.movingGiantFrequencyUnits_of_bounds line 107
def OAI.Ostmann.MovingGiantSamples.sampleCount line 125
theorem OAI.Ostmann.MovingGiantSamples.sampleCount_eq line 130
Source documentation
The literal internal sample count is the O(k r) count in Section 8.1.
```
theorem MovingGiantSamples.sampleCount_eq {n : ℕ} (samples : MovingGiantSamples n) :
    samples.sampleCount = 2 * n * 2 ^ n := by
…
```
Mentions: OAI.Ostmann.MovingGiantSamples