ThreeSeedSampling.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

Three-seed sampling for the tree-matrix repair argument

Choices in different groups on the same axis need not be independent. Three uniform seeds suffice: a common leaf, a row seed and a column seed. The equal-fiber calculation gives uniform marginals.

def OAI.Problem348.TreeSampling.mix line 18
Source documentation
Replace the within-block coordinate of a leaf by that of a second seed.
```
def mix {a b : ℕ} (z u : Fin (a * b)) : Fin (a * b) :=
…
```
theorem OAI.Problem348.TreeSampling.mix_div line 22
theorem OAI.Problem348.TreeSampling.mix_mod line 27
def OAI.Problem348.TreeSampling.splitMix line 33
Source documentation
The output of the mixer and the two unused coordinates determine both seeds.
```
def splitMix {a b : ℕ} :
    (Fin (a * b) × Fin (a * b)) ≃
      (Fin (a * b) × (Fin b × Fin a)) where
…
```
def OAI.Problem348.TreeSampling.fiberOfEquiv line 52
Source documentation
A first-coordinate fiber of a product decomposition is the second factor.
```
def fiberOfEquiv {X : Type uX} {Y : Type uY} {Z : Type uZ} (e : X ≃ Y × Z) (y : Y) :
    {x : X // (e x).1 = y} ≃ Z where
…
```
theorem OAI.Problem348.TreeSampling.card_mix_fiber line 64
Source documentation
Every level-class position occurs equally often in the pair of seeds.
```
theorem card_mix_fiber {a b : ℕ} (x : Fin (a * b)) :
    Fintype.card {p : Fin (a * b) × Fin (a * b) // mix p.1 p.2 = x} =
      a * b := by
…
```
Mentions: OAI.Problem348.TreeSampling.mix
abbrev OAI.Problem348.TreeSampling.Seeds line 74
Source documentation
The three seeds are the common leaf, an axis-one seed and an axis-two seed.
```
abbrev Seeds (m : ℕ) := Fin m × (Fin m × Fin m)
```
def OAI.Problem348.TreeSampling.splitRow line 77
Source documentation
A variable row and an anchor/dummy column, together with unused coordinates.
```
def splitRow {a b : ℕ} :
    Seeds (a * b) ≃ (Fin (a * b) × Fin (a * b)) × (Fin b × Fin a) where
…
```
Mentions: OAI.Problem348.TreeSampling.Seeds
def OAI.Problem348.TreeSampling.splitColumn line 94
Source documentation
An anchor/dummy row and a variable column, with the unused coordinates.
```
def splitColumn {a b : ℕ} :
    Seeds (a * b) ≃ (Fin (a * b) × Fin (a * b)) × (Fin b × Fin a) where
…
```
Mentions: OAI.Problem348.TreeSampling.Seeds
def OAI.Problem348.TreeSampling.splitBoth line 111
Source documentation
Two independent axis seeds, with the common-leaf coordinate unused.
```
def splitBoth {m : ℕ} : Seeds m ≃ (Fin m × Fin m) × Fin m where
…
```
Mentions: OAI.Problem348.TreeSampling.Seeds
theorem OAI.Problem348.TreeSampling.card_row_fiber line 118
Source documentation
Exact protected-cell multiplicity when the row is variable.
```
theorem card_row_fiber {a b : ℕ} (x y : Fin (a * b)) :
    Fintype.card {s : Seeds (a * b) // (mix s.1 s.2.1, s.2.2) = (x,y)} =
      a * b := by
…
```
Mentions: OAI.Problem348.TreeSampling.Seeds, OAI.Problem348.TreeSampling.mix
theorem OAI.Problem348.TreeSampling.card_column_fiber line 128
Source documentation
Exact protected-cell multiplicity when the column is variable.
```
theorem card_column_fiber {a b : ℕ} (x y : Fin (a * b)) :
    Fintype.card {s : Seeds (a * b) // (s.2.1, mix s.1 s.2.2) = (x,y)} =
      a * b := by
…
```
Mentions: OAI.Problem348.TreeSampling.Seeds, OAI.Problem348.TreeSampling.mix
theorem OAI.Problem348.TreeSampling.card_both_fiber line 138
Source documentation
Exact multiplicity for two anchor/dummy positions or two root positions.
```
theorem card_both_fiber {m : ℕ} (x y : Fin m) :
    Fintype.card {s : Seeds m // s.2 = (x,y)} = m := by
…
```
Mentions: OAI.Problem348.TreeSampling.Seeds
theorem OAI.Problem348.TreeSampling.card_seeds line 146
theorem OAI.Problem348.TreeSampling.mix_val line 149
theorem OAI.Problem348.TreeSampling.level_factor line 153
Source documentation
The two coordinates of a depth-i level class multiply to the leaf count.
```
theorem level_factor {h i : ℕ} (hi : i ≤ h) :
    2 ^ i * 2 ^ (h-i) = 2 ^ h := by
…
```
def OAI.Problem348.TreeSampling.mixCast line 158
Source documentation
Transport the mixer to a size presented by an equality rather than a product.
```
def mixCast {a b m : ℕ} (hm : a * b = m) (z u : Fin m) : Fin m :=
…
```
theorem OAI.Problem348.TreeSampling.card_mixCast_row_fiber line 161
theorem OAI.Problem348.TreeSampling.card_mixCast_column_fiber line 166
def OAI.Problem348.TreeSampling.atLevel line 172
Source documentation
The class-coordinate selected at depth i by a common leaf and an axis seed.
```
def atLevel (h i : ℕ) (hi : i ≤ h) (z u : Fin (2 ^ h)) : Fin (2 ^ h) :=
…
```
theorem OAI.Problem348.TreeSampling.atLevel_val line 175
theorem OAI.Problem348.TreeSampling.atLevel_root line 180
Source documentation
Root selections depend only on the corresponding axis seed.
```
@[simp] theorem atLevel_root (h : ℕ) (z u : Fin (2 ^ h)) :
    atLevel h 0 (Nat.zero_le h) z u = u := by
…
```
Mentions: OAI.Problem348.TreeSampling.atLevel
theorem OAI.Problem348.TreeSampling.atLevel_leaf line 186
Source documentation
Both signs at the leaf select the same common leaf, regardless of axis seed.
```
@[simp] theorem atLevel_leaf (h : ℕ) (z u : Fin (2 ^ h)) :
    atLevel h h le_rfl z u = z := by
…
```
Mentions: OAI.Problem348.TreeSampling.atLevel
theorem OAI.Problem348.TreeSampling.atLevel_node line 192
Source documentation
Every selected position lies in the ancestor block of the common leaf.
```
theorem atLevel_node (h i : ℕ) (hi : i ≤ h) (z u : Fin (2 ^ h)) :
    (atLevel h i hi z u).val / (2 ^ (h-i)) = z.val / (2 ^ (h-i)) := by
…
```
Mentions: OAI.Problem348.TreeSampling.atLevel
theorem OAI.Problem348.TreeSampling.ancestor_parent line 198
Source documentation
The sampler's node at a child level has the prescribed parent.
```
theorem ancestor_parent (h i z : ℕ) (hi : i < h) :
    (z / 2 ^ (h - (i+1))) / 2 = z / 2 ^ (h-i) := by
…
```
theorem OAI.Problem348.TreeSampling.card_atLevel_row_fiber line 206
Source documentation
Every variable-row / anchor-column cell has exactly m seed preimages.
```
theorem card_atLevel_row_fiber (h i : ℕ) (hi : i ≤ h) (x y : Fin (2^h)) :
    Fintype.card {s : Seeds (2^h) //
      (atLevel h i hi s.1 s.2.1, s.2.2) = (x,y)} = 2^h :=
…
```
Mentions: OAI.Problem348.TreeSampling.Seeds, OAI.Problem348.TreeSampling.atLevel
theorem OAI.Problem348.TreeSampling.card_atLevel_column_fiber line 212
Source documentation
Every anchor-row / variable-column cell has exactly m seed preimages.
```
theorem card_atLevel_column_fiber (h i : ℕ) (hi : i ≤ h) (x y : Fin (2^h)) :
    Fintype.card {s : Seeds (2^h) //
      (s.2.1, atLevel h i hi s.1 s.2.2) = (x,y)} = 2^h :=
…
```
Mentions: OAI.Problem348.TreeSampling.Seeds, OAI.Problem348.TreeSampling.atLevel