WordSwitches.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Boolean words are uniquely specified by their initial bit and their switches. This gives the exact binomial count used in the path-type sum.

def OAI.Problem335.WordSwitches.switches line 14
Source documentation
Internal positions where adjacent bits differ. A word has n + 1 letters.
```
def switches {n : ℕ} (w : Fin (n + 1) → Bool) : Finset (Fin n) :=
…
```
theorem OAI.Problem335.WordSwitches.mem_switches line 17
def OAI.Problem335.WordSwitches.encode line 22
Source documentation
The initial letter and switch set encode a nonempty word.
```
def encode {n : ℕ} (w : Fin (n + 1) → Bool) : Bool × Finset (Fin n) :=
…
```
theorem OAI.Problem335.WordSwitches.bool_eq_of_ne_iff line 25
theorem OAI.Problem335.WordSwitches.encode_injective line 29
theorem OAI.Problem335.WordSwitches.encode_bijective line 44
Source documentation
Every initial letter and set of switch positions specifies exactly one word.
```
theorem encode_bijective (n : ℕ) : Function.Bijective (@encode n) := by
…
```
Mentions: OAI.Problem335.WordSwitches.encode
def OAI.Problem335.WordSwitches.wordEquiv line 49
theorem OAI.Problem335.WordSwitches.wordEquiv_apply line 53
def OAI.Problem335.WordSwitches.countEquiv line 57
Source documentation
The switch-count restriction of the word encoding.
```
noncomputable def countEquiv (n j : ℕ) :
    {w : Fin (n + 1) → Bool // (switches w).card = j} ≃
      Bool × {s : Finset (Fin n) // s.card = j} :=
…
```
Mentions: OAI.Problem335.WordSwitches.switches
theorem OAI.Problem335.WordSwitches.card_words_with_switches line 68
Source documentation
Exactly 2 * choose n j words of length n + 1 have j switches.
```
theorem card_words_with_switches (n j : ℕ) :
    Fintype.card {w : Fin (n + 1) → Bool // (switches w).card = j} =
      2 * n.choose j := by
…
```
Mentions: OAI.Problem335.WordSwitches.switches

theorem OAI.Problem335.WordSwitches.sum_pow_switches line 75

Source documentation

The switch-count generating function.

theorem sum_pow_switches {R : Type*} [CommSemiring R] (n : ℕ) (x : R) :
    (∑ w : Fin (n + 1) → Bool, x ^ (switches w).card) =
      2 * (1 + x) ^ n := by
…

Mentions: OAI.Problem335.WordSwitches.switches

theorem OAI.Problem335.WordSwitches.sum_pow_switches_le_exp line 89
Source documentation
An exponential upper bound for a switch-penalized word sum.
```
theorem sum_pow_switches_le_exp (n : ℕ) (x : ℝ) (hx : 0 ≤ x) :
    (∑ w : Fin (n + 1) → Bool, x ^ (switches w).card) ≤
      2 * Real.exp ((n : ℝ) * x) := by
…
```
Mentions: OAI.Problem335.WordSwitches.switches