ButterflyRoutes.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

def OAI.CubeShuffle.SwitchIndex line 11
Source documentation
One index for each independent coin of the recursive butterfly.
```
def SwitchIndex : ℕ → Type
  | 0 => Empty
  | d + 1 => Sum (Card d) (Bool × SwitchIndex d)
```
Mentions: OAI.CubeShuffle.Card
instance OAI.CubeShuffle.(instance at line 15) line 15
instance OAI.CubeShuffle.(instance at line 20) line 20

def OAI.CubeShuffle.decodeButterfly line 26

Source documentation

Decode an independent bit at every switch into the actual routing object.

def decodeButterfly : (d : ℕ) → (SwitchIndex d → Bool) → Butterfly d
  | 0, _ => ()
  | d + 1, ω => (fun y => ω (Sum.inl y), fun ε =>
      decodeButterfly d (fun i => ω (Sum.inr (ε,i))))

Mentions: OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.Butterfly

def OAI.CubeShuffle.encodeButterfly line 31
lemma OAI.CubeShuffle.decode_encodeButterfly line 36
lemma OAI.CubeShuffle.encode_decodeButterfly line 46
def OAI.CubeShuffle.butterflyCoinEquiv line 58
Source documentation
Thus the bit experiment and independent recursive butterfly experiment are exactly the same finite probability space, up to a bijection.
```
def butterflyCoinEquiv (d : ℕ) : (SwitchIndex d → Bool) ≃ Butterfly d where
…
```
Mentions: OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.Butterfly

def OAI.CubeShuffle.routeDomain line 65

Source documentation

Switches on the unique possible route from x to y.

noncomputable def routeDomain : (d : ℕ) → Card d → Card d → Finset (SwitchIndex d)
  | 0, _, _ => ∅
  | d + 1, x, y => by
      classical
      exact insert (Sum.inl (Fin.tail y))
        ((routeDomain d (Fin.tail x) (Fin.tail y)).image (fun i => Sum.inr (x 0,i)))

/-- Required coin values on the unique route. Values off its domain are unused. -/

Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex

def OAI.CubeShuffle.routeValue line 73

Source documentation

Required coin values on the unique route. Values off its domain are unused.

def routeValue : (d : ℕ) → Card d → Card d → SwitchIndex d → Bool
  | 0, _, _, i => nomatch i
  | _d + 1, x, y, Sum.inl _ => Bool.xor (x 0) (y 0)
  | d + 1, x, y, Sum.inr (_,i) => routeValue d (Fin.tail x) (Fin.tail y) i

Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex

lemma OAI.CubeShuffle.card_routeDomain line 78
lemma OAI.CubeShuffle.xor_eq_iff line 90
lemma OAI.CubeShuffle.butterfly_endpoint_iff line 95
Source documentation
The endpoint test is exactly a fixed set of coin requirements. The route is UNIQUE; there is no sum over paths and no adaptively unspecified target.
```
lemma butterfly_endpoint_iff (d : ℕ) (ω : SwitchIndex d → Bool) (x y : Card d) :
    butterflyPerm d (decodeButterfly d ω) x = y ↔
      ∀ i ∈ routeDomain d x y, ω i = routeValue d x y i := by
…
```
Mentions: OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.Card, OAI.CubeShuffle.butterflyPerm, OAI.CubeShuffle.decodeButterfly, OAI.CubeShuffle.routeDomain, OAI.CubeShuffle.routeValue

lemma OAI.CubeShuffle.mean_coinCylinder line 131

Source documentation

Exact probability of any prescribed collection of independent fair bits.

lemma mean_coinCylinder {ι : Type*} [Fintype ι] [DecidableEq ι]
    (s : Finset ι) (v : ι → Bool) :
    finiteMean (fun ω : ι → Bool => if ∀ i ∈ s, ω i = v i then (1 : ℝ) else 0) =
      1 / (2 : ℝ) ^ s.card := by
…

Mentions: OAI.CubeShuffle.finiteMean

def OAI.CubeShuffle.exposedCoins line 158
Source documentation
Fix all previously exposed bits, leaving every other bit independent fair.
```
def exposedCoins {ι : Type*} [DecidableEq ι] (R : Finset ι) (η ω : ι → Bool) : ι → Bool :=
…
```
lemma OAI.CubeShuffle.mean_coinCylinder_exposed line 161
lemma OAI.CubeShuffle.butterfly_closure_probability line 196
Source documentation
Literal source closing-path formula: zero on inconsistent exposures, otherwise 2^u/n, with u the number of already exposed route switches and n = 2^d. There is no supposition that a favorable route is independent.
```
lemma butterfly_closure_probability (d : ℕ) (x y : Card d)
    (R : Finset (SwitchIndex d)) (η : SwitchIndex d → Bool) :
    finiteMean (fun ω : SwitchIndex d → Bool =>
      if butterflyPerm d (decodeButterfly d (exposedCoins R η ω)) x = y then (1 : ℝ) else 0) =
      if (∀ i ∈ routeDomain d x y ∩ R, η i = routeValue d x y i) then
        (2 : ℝ) ^ (routeDomain d x y ∩ R).card / (2 : ℝ) ^ d else 0 := by
…
```
Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.butterflyPerm, OAI.CubeShuffle.decodeButterfly, OAI.CubeShuffle.exposedCoins, OAI.CubeShuffle.routeDomain, OAI.CubeShuffle.routeValue
lemma OAI.CubeShuffle.butterfly_single_card_uniform line 219

def OAI.CubeShuffle.switchUsers line 232

Source documentation

The two distinct INPUT labels whose paths traverse a given switch. This records encounters without any independence or random-route assumption.

def switchUsers : (d : ℕ) → Butterfly d → SwitchIndex d → Card d × Card d
  | 0, _, i => nomatch i
  | d + 1, b, Sum.inl y =>
      (Fin.cons false ((butterflyPerm d (b.2 false)).symm y),
       Fin.cons true ((butterflyPerm d (b.2 true)).symm y))
  | d + 1, b, Sum.inr (ε,i) =>
      (Fin.cons ε (switchUsers d (b.2 ε) i).1,
       Fin.cons ε (switchUsers d (b.2 ε) i).2)

Mentions: OAI.CubeShuffle.Butterfly, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.Card, OAI.CubeShuffle.butterflyPerm

lemma OAI.CubeShuffle.switchUsers_ne line 241
lemma OAI.CubeShuffle.cons_eq_iff line 256
lemma OAI.CubeShuffle.mem_routeDomain_iff_user line 267
Source documentation
A switch is on a label's actual route iff the label is one of its two users. In particular all incidental meetings are accounted for exactly once.
```
lemma mem_routeDomain_iff_user (d : ℕ) (b : Butterfly d) (x : Card d) (i : SwitchIndex d) :
    i ∈ routeDomain d x (butterflyPerm d b x) ↔
      (switchUsers d b i).1 = x ∨ (switchUsers d b i).2 = x := by
…
```
Mentions: OAI.CubeShuffle.Butterfly, OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.routeDomain, OAI.CubeShuffle.butterflyPerm, OAI.CubeShuffle.switchUsers
lemma OAI.CubeShuffle.card_switches_using line 306
lemma OAI.CubeShuffle.switch_incidence_sum line 320
Source documentation
Every input path has degree exactly d in the multigraph of shared switches. The identity also holds for arbitrary (not necessarily positive) weights.
```
lemma switch_incidence_sum (d : ℕ) (b : Butterfly d) (w : Card d → ℝ) :
    ∑ i : SwitchIndex d, (w (switchUsers d b i).1 + w (switchUsers d b i).2) =
      (d : ℝ) * ∑ x : Card d, w x := by
…
```
Mentions: OAI.CubeShuffle.Butterfly, OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.switchUsers
lemma OAI.CubeShuffle.weighted_switch_min_bound line 349
Source documentation
The weighted threshold estimate in the rotation argument. It applies to any weights and so in particular to 1/j on selected length-j cycles.
```
lemma weighted_switch_min_bound (d : ℕ) (b : Butterfly d) (w : Card d → ℝ) :
    ∑ i : SwitchIndex d, min (w (switchUsers d b i).1) (w (switchUsers d b i).2) ≤
      (d : ℝ) / 2 * ∑ x : Card d, w x := by
…
```
Mentions: OAI.CubeShuffle.Butterfly, OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.switchUsers
lemma OAI.CubeShuffle.mem_childMarks line 364
lemma OAI.CubeShuffle.mem_topMeetings line 377
lemma OAI.CubeShuffle.encounters_eq_switch_sum line 395
Source documentation
Both users marked is exactly the encounter predicate; its sum is the recursive quantity already bounded by entropy.
```
lemma encounters_eq_switch_sum (d : ℕ) (b : Butterfly d) (s : Finset (Card d)) :
    encounters d b s = ∑ i : SwitchIndex d,
      if (switchUsers d b i).1 ∈ s ∧ (switchUsers d b i).2 ∈ s then 1 else 0 := by
…
```
Mentions: OAI.CubeShuffle.Butterfly, OAI.CubeShuffle.Card, OAI.CubeShuffle.encounters, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.switchUsers
lemma OAI.CubeShuffle.marked_switch_entropy_bound line 423