WordRuns.lean`

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Counts of true runs, and their relation to adjacent switches.

def OAI.Problem335.WordRuns.riseCount line 12
Source documentation
Number of transitions from false to true.
```
def riseCount {n : ℕ} (w : Fin (n + 1) → Bool) : ℕ :=
…
```
def OAI.Problem335.WordRuns.fallCount line 16
Source documentation
Number of transitions from true to false.
```
def fallCount {n : ℕ} (w : Fin (n + 1) → Bool) : ℕ :=
…
```
def OAI.Problem335.WordRuns.runCount line 20
Source documentation
True runs are counted by their first letters.
```
def runCount {n : ℕ} (w : Fin (n + 1) → Bool) : ℕ :=
…
```
def OAI.Problem335.WordRuns.endpointRunCount line 24
Source documentation
In a mixed word, the number of true runs touching an endpoint.
```
def endpointRunCount {n : ℕ} (w : Fin (n + 1) → Bool) : ℕ :=
…
```
def OAI.Problem335.WordRuns.interiorRunCount line 28
Source documentation
Number of true runs not touching an endpoint.
```
def interiorRunCount {n : ℕ} (w : Fin (n + 1) → Bool) : ℕ :=
…
```
theorem OAI.Problem335.WordRuns.riseCount_cons line 31
theorem OAI.Problem335.WordRuns.fallCount_cons line 38
theorem OAI.Problem335.WordRuns.switches_card_eq_rises_add_falls line 46
Source documentation
Every switch is exactly a rise or a fall.
```
theorem switches_card_eq_rises_add_falls {n : ℕ} (w : Fin (n + 1) → Bool) :
    (WordSwitches.switches w).card = riseCount w + fallCount w := by
…
```
Mentions: OAI.Problem335.WordSwitches.switches, OAI.Problem335.WordRuns.riseCount, OAI.Problem335.WordRuns.fallCount
theorem OAI.Problem335.WordRuns.rise_first_eq_fall_last line 56
Source documentation
Incoming and outgoing changes balance, up to the endpoint bits.
```
theorem rise_first_eq_fall_last {n : ℕ} (w : Fin (n + 1) → Bool) :
    riseCount w + (w 0).toNat = fallCount w + (w (Fin.last n)).toNat := by
…
```
Mentions: OAI.Problem335.WordRuns.riseCount, OAI.Problem335.WordRuns.fallCount
theorem OAI.Problem335.WordRuns.all_true_of_no_rises line 72
Source documentation
With no rises, a true last letter forces the entire word to be true.
```
theorem all_true_of_no_rises {n : ℕ} (w : Fin (n + 1) → Bool)
    (h : riseCount w = 0) (hlast : w (Fin.last n) = true) :
    ∀ i, w i = true := by
…
```
Mentions: OAI.Problem335.WordRuns.riseCount
theorem OAI.Problem335.WordRuns.endpointRunCount_le_runCount line 94
Source documentation
If there is a false letter, each true endpoint belongs to a distinct run.
```
theorem endpointRunCount_le_runCount {n : ℕ} (w : Fin (n + 1) → Bool)
    (hfalse : ∃ i, w i = false) : endpointRunCount w ≤ runCount w := by
…
```
Mentions: OAI.Problem335.WordRuns.endpointRunCount, OAI.Problem335.WordRuns.runCount
theorem OAI.Problem335.WordRuns.endpointRunCount_le_two line 109
theorem OAI.Problem335.WordRuns.switches_card_eq_two_interior_add_endpoint line 116
Source documentation
For a mixed word, switches equal twice the interior true runs plus endpoint runs. In fact only the existence of a false letter is needed.
```
theorem switches_card_eq_two_interior_add_endpoint {n : ℕ}
    (w : Fin (n + 1) → Bool) (hfalse : ∃ i, w i = false) :
    (WordSwitches.switches w).card =
      2 * interiorRunCount w + endpointRunCount w := by
…
```
Mentions: OAI.Problem335.WordSwitches.switches, OAI.Problem335.WordRuns.interiorRunCount, OAI.Problem335.WordRuns.endpointRunCount
theorem OAI.Problem335.WordRuns.two_runCount_eq_switches_add_endpoint line 128
Source documentation
A version valid even for the all-true word: each run has two boundary ends, except that endpoints do not contribute switches.
```
theorem two_runCount_eq_switches_add_endpoint {n : ℕ}
    (w : Fin (n + 1) → Bool) :
    2 * runCount w = (WordSwitches.switches w).card + endpointRunCount w := by
…
```
Mentions: OAI.Problem335.WordRuns.runCount, OAI.Problem335.WordSwitches.switches, OAI.Problem335.WordRuns.endpointRunCount