HostSampling.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The canonical host projections and protected-cell sampling bridge. Three seeds give the cellwise sampling bound.

def OAI.Problem348.Construction.HostSampling.sampleDepth line 16
Source documentation
Anchor and dummy positions use their independent axis seed.
```
def sampleDepth {h : ℕ} : Position h → Option (Fin (h + 1))
  | Sum.inl _ => none
  | Sum.inr (Sum.inl v) => some ⟨depth v, Nat.lt_succ_of_le (depth_le v)⟩
  | Sum.inr (Sum.inr _) => none

/-- The coordinate within the size-`2^h` class of a raw host position. -/
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.depth, OAI.Problem348.Construction.depth_le, OAI.Problem348.Construction.HostSampling.coordinate, OAI.Problem348.Construction.host
def OAI.Problem348.Construction.HostSampling.offset line 22
Source documentation
The coordinate within the size-2^h class of a raw host position.
```
def offset {h : ℕ} : Position h → Fin (2 ^ h)
  | Sum.inl (_, _, x) => x
  | Sum.inr (Sum.inl v) => v.2
  | Sum.inr (Sum.inr x) => x

/-- The selected coordinate in the class containing a given position. -/
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.HostSampling.coordinate
def OAI.Problem348.Construction.HostSampling.coordinate line 28
Source documentation
The selected coordinate in the class containing a given position.
```
def coordinate {h : ℕ} (z u : Fin (2 ^ h)) : Position h → Fin (2 ^ h)
  | Sum.inl _ => u
  | Sum.inr (Sum.inl v) => atLevel h (depth v) (depth_le v) z u
  | Sum.inr (Sum.inr _) => u

/-- Whether both positions of a fixed raw cell are selected. -/
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.depth, OAI.Problem348.Construction.depth_le
def OAI.Problem348.Construction.HostSampling.Selected line 34
Source documentation
Whether both positions of a fixed raw cell are selected.
```
def Selected {h : ℕ} (s : Seeds (2 ^ h)) (r c : Position h) : Prop :=
…
```
Mentions: OAI.Problem348.Construction.Position
instance OAI.Problem348.Construction.HostSampling.(instance at line 37) line 37
def OAI.Problem348.Construction.HostSampling.Protected line 41
Source documentation
Protected cells: at least one anchor/dummy position, or two root positions.
```
def Protected {h : ℕ} (r c : Position h) : Prop :=
…
```
Mentions: OAI.Problem348.Construction.Position
theorem OAI.Problem348.Construction.HostSampling.protected_anchor_left line 45
theorem OAI.Problem348.Construction.HostSampling.protected_anchor_right line 49
theorem OAI.Problem348.Construction.HostSampling.protected_dummy_left line 53
theorem OAI.Problem348.Construction.HostSampling.protected_dummy_right line 57
theorem OAI.Problem348.Construction.HostSampling.protected_roots line 61
theorem OAI.Problem348.Construction.HostSampling.selected_fiber_card line 67
Source documentation
Concrete host protected-cell events all have exactly 2^h seed preimages.
```
theorem selected_fiber_card {h : ℕ} (r c : Position h) (hp : Protected r c) :
    Fintype.card {s : Seeds (2 ^ h) // Selected s r c} = 2 ^ h := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.HostSampling.Protected, OAI.Problem348.Construction.HostSampling.Selected
theorem OAI.Problem348.Construction.HostSampling.selected_fiber_card_mul line 91
Source documentation
Fraction-free marginal equality, directly consumable by finite avoidance.
```
theorem selected_fiber_card_mul {h : ℕ} (r c : Position h) (hp : Protected r c) :
    Fintype.card {s : Seeds (2 ^ h) // Selected s r c} * (2 ^ h) ^ 2 =
      Fintype.card (Seeds (2 ^ h)) := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.HostSampling.Protected, OAI.Problem348.Construction.HostSampling.Selected
theorem OAI.Problem348.Construction.HostSampling.selected_filter_card line 98
Source documentation
The same marginal in the Finset.filter form used by the union bound.
```
theorem selected_filter_card {h : ℕ} (r c : Position h) (hp : Protected r c) :
    (Finset.univ.filter fun s : Seeds (2 ^ h) => Selected s r c).card = 2 ^ h := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.HostSampling.Protected, OAI.Problem348.Construction.HostSampling.Selected
theorem OAI.Problem348.Construction.HostSampling.protected_event_card_le line 103
Source documentation
A subset of the protected event has at most the same frequency.
```
theorem protected_event_card_le {h : ℕ} (r c : Position h)
    (event : Finset (Seeds (2 ^ h)))
    (hevent : ∀ s ∈ event, Protected r c ∧ Selected s r c) :
    event.card ≤ 2 ^ h := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.HostSampling.Protected, OAI.Problem348.Construction.HostSampling.Selected
theorem OAI.Problem348.Construction.HostSampling.guard_frequency line 121
Source documentation
Guard-cell containment in the protected selected-cell event implies the union-bound frequency estimate for each fixed raw cell.
```
theorem guard_frequency {h : ℕ}
    (guards : Seeds (2 ^ h) → Finset (Position h × Position h))
    (hguards : ∀ s rc, rc ∈ guards s →
      Protected rc.1 rc.2 ∧ Selected s rc.1 rc.2)
    (rc : Position h × Position h) :
    (Finset.univ.filter fun s => rc ∈ guards s).card * (2 ^ h) ^ 2 ≤
      Fintype.card (Seeds (2 ^ h)) := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.HostSampling.Protected, OAI.Problem348.Construction.HostSampling.Selected

theorem OAI.Problem348.Construction.HostSampling.transported_guard_frequency line 138

Source documentation

Independent row and column reindexings preserve the protected-cell bound.

theorem transported_guard_frequency {h n : ℕ}
    (row col : Position h ≃ Fin n)
    (guards : Seeds (2 ^ h) → Finset (Fin n × Fin n))
    (hguards : ∀ s rc, rc ∈ guards s →
      Protected (row.symm rc.1) (col.symm rc.2) ∧
      Selected s (row.symm rc.1) (col.symm rc.2))
    (rc : Fin n × Fin n) :
    (Finset.univ.filter fun s => rc ∈ guards s).card * (2 ^ h) ^ 2 ≤
      Fintype.card (Seeds (2 ^ h)) := by
…

Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.HostSampling.Protected, OAI.Problem348.Construction.HostSampling.Selected