CycleColoring.lean`

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.CubeShuffle.CycleColoring.Coloring line 15
Source documentation
A coloring of the selected vertices constant along every retained edge of an oriented permutation graph. Off the selected set its value is fixed.
```
abbrev Coloring (p : Equiv.Perm α) (S : Finset α) :=
…
```
instance OAI.CubeShuffle.CycleColoring.(instance at line 19) line 19
def OAI.CubeShuffle.CycleColoring.boundary line 22
def OAI.CubeShuffle.CycleColoring.root line 25
lemma OAI.CubeShuffle.CycleColoring.root_mem line 28
abbrev OAI.CubeShuffle.CycleColoring.Seed line 31
def OAI.CubeShuffle.CycleColoring.record line 34
lemma OAI.CubeShuffle.CycleColoring.orbit_subset_of_predecessor_closed line 38
lemma OAI.CubeShuffle.CycleColoring.record_injective line 49
lemma OAI.CubeShuffle.CycleColoring.card_coloring_le line 82
Source documentation
Every open chain has a boundary seed and every complete cycle has one free bit. In particular a parallel pair of matching edges is treated as a cycle.
```
lemma card_coloring_le (p : Equiv.Perm α) (S : Finset α) :
    Fintype.card (Coloring p S) ≤
      2 ^ ((boundary p S).card + Fintype.card (RoutingNetwork.SelectedCycle p S)) := by
…
```
Mentions: OAI.CubeShuffle.CycleColoring.Coloring, OAI.CubeShuffle.CycleColoring.boundary, OAI.CubeShuffle.RoutingNetwork.SelectedCycle
lemma OAI.CubeShuffle.CycleColoring.boundary_card line 89
lemma OAI.CubeShuffle.CycleColoring.card_coloring_le_edges line 96
abbrev OAI.CubeShuffle.CycleColoring.OppositeColoring line 108
Source documentation
A binary assignment with opposite values on each marked matching edge.
```
abbrev OppositeColoring (p : Equiv.Perm α) (S : Finset α) :=
…
```
instance OAI.CubeShuffle.CycleColoring.(instance at line 112) line 112
def OAI.CubeShuffle.CycleColoring.bipartitionFlip line 117
Source documentation
Flipping one bipartition converts opposite matching assignments into constant colorings. The construction includes the unmarked-value convention.
```
noncomputable def bipartitionFlip (p : Equiv.Perm α) (S : Finset α)
    (χ : α → Bool) (hχ : ∀ x, χ (p x) = !(χ x))
    (f : OppositeColoring p S) : Coloring p S := by
…
```
Mentions: OAI.CubeShuffle.CycleColoring.OppositeColoring, OAI.CubeShuffle.CycleColoring.Coloring
lemma OAI.CubeShuffle.CycleColoring.bipartitionFlip_injective line 129
lemma OAI.CubeShuffle.CycleColoring.card_opposite_le line 144
def OAI.CubeShuffle.CycleColoring.alternatingPerm line 153
Source documentation
Alternating traversal of the identity matching and the p-matching on two halves. A fixed point of p is precisely a parallel-edge alternating cycle.
```
def alternatingPerm (p : Equiv.Perm α) : Equiv.Perm (Bool × α) where
…
```
lemma OAI.CubeShuffle.CycleColoring.alternatingPerm_flip line 160
lemma OAI.CubeShuffle.CycleColoring.alternating_step_sameCycle line 166
lemma OAI.CubeShuffle.CycleColoring.alternating_sameCycle_snd line 174
lemma OAI.CubeShuffle.CycleColoring.alternating_zero_sameCycle line 186
lemma OAI.CubeShuffle.CycleColoring.alternating_sameCycle_zero line 199
lemma OAI.CubeShuffle.CycleColoring.alternating_sameCycle_iff line 207
lemma OAI.CubeShuffle.CycleColoring.orbit_alternating line 215
lemma OAI.CubeShuffle.CycleColoring.boolFiber_childJoin line 221
def OAI.CubeShuffle.CycleColoring.projectCycle line 226
lemma OAI.CubeShuffle.CycleColoring.selected_alternating_eq line 237
lemma OAI.CubeShuffle.CycleColoring.projectCycle_injective line 245
lemma OAI.CubeShuffle.CycleColoring.card_alternating_cycles_le line 251
lemma OAI.CubeShuffle.mem_image_perm_iff line 262
lemma OAI.CubeShuffle.card_childJoin line 272
lemma OAI.CubeShuffle.alternating_internal line 285
lemma OAI.CubeShuffle.alternating_boundary_card line 294
lemma OAI.CubeShuffle.compatible_assignment_bound line 308
Source documentation
Literal component-count exponent in FAC.1, after identifying the two perfect matchings with the identity and p matchings on their two halves. The complete alternating cycles are bounded by the projection-side cycles.
```
lemma compatible_assignment_bound (p : Equiv.Perm α) (A B : Finset α) :
    Fintype.card (CycleColoring.OppositeColoring (CycleColoring.alternatingPerm p) (childJoin A B)) ≤
      2 ^ ((A ∪ B).card + (A ∪ B.image p).card - (A.card+B.card) +
        Fintype.card (RoutingNetwork.SelectedCycle p A)) := by
…
```
Mentions: OAI.CubeShuffle.CycleColoring.OppositeColoring, OAI.CubeShuffle.CycleColoring.alternatingPerm, OAI.CubeShuffle.childJoin, OAI.CubeShuffle.RoutingNetwork.SelectedCycle
lemma OAI.CubeShuffle.finiteMean_nonneg line 321
lemma OAI.CubeShuffle.boolFiber_headTail line 325
lemma OAI.CubeShuffle.prod_childMarks line 340
def OAI.CubeShuffle.headAverage line 351
lemma OAI.CubeShuffle.finiteMean_headAverage line 354
lemma OAI.CubeShuffle.pairSwitch_product_bound line 362
lemma OAI.CubeShuffle.butterflyPerm_step line 387
lemma OAI.CubeShuffle.butterfly_product_bound line 404
Source documentation
A weighted form of the inverse-image cylinder bound. Its orientation is specified by the actual butterfly action on each selected input.
```
lemma butterfly_product_bound (d : ℕ) (S : Finset (Card d))
    (p : Card d → ℝ) (hp : ∀ x, 0 ≤ p x) :
    finiteMean (fun ω : SwitchIndex d → Bool =>
      ∏ x ∈ S, p (butterflyPerm d (decodeButterfly d ω) x)) ≤ (finiteMean p)^S.card := by
…
```
Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.butterflyPerm, OAI.CubeShuffle.decodeButterfly
def OAI.CubeShuffle.inverseButterflyMarks line 457
lemma OAI.CubeShuffle.inverseButterflyMarks_inclusion line 463
Source documentation
The central-mark inclusion estimate in the orientation required by the recursive Beneš network, derived rather than assumed from reversibility.
```
lemma inverseButterflyMarks_inclusion (d : ℕ) (A S : Finset (Card d)) :
    inclusionMoment (inverseButterflyMarks d A) S ≤
      ((A.card : ℝ)/(2:ℝ)^d)^S.card := by
…
```
Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.inclusionMoment, OAI.CubeShuffle.inverseButterflyMarks