RunBlocks.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Contiguous true blocks, with an exact block-count and product factorization.

def OAI.Problem335.WordRuns.splitTrueAux line 14

Source documentation

Split a list at false positions, retaining a possibly empty initial block.

def splitTrueAux (p : α → Bool) : List α → List α × List (List α)
  | [] => ([], [])
  | a :: l =>
    let q := splitTrueAux p l
…

def OAI.Problem335.WordRuns.trueBlocks line 21
Source documentation
The nonempty maximal contiguous blocks of positions satisfying p.
```
def trueBlocks (p : α → Bool) (l : List α) : List (List α) :=
…
```
theorem OAI.Problem335.WordRuns.splitTrueAux_fst_nil_cons line 25
theorem OAI.Problem335.WordRuns.splitTrueAux_fst_prefix line 30
Source documentation
The initial block is genuinely a prefix, including when empty.
```
theorem splitTrueAux_fst_prefix (p : α → Bool) (l : List α) :
    (splitTrueAux p l).1 <+: l := by
…
```
Mentions: OAI.Problem335.WordRuns.splitTrueAux
theorem OAI.Problem335.WordRuns.splitTrueAux_flatten line 38
Source documentation
Splitting does not lose or duplicate any selected position.
```
theorem splitTrueAux_flatten (p : α → Bool) (l : List α) :
    (splitTrueAux p l).1 ++ (splitTrueAux p l).2.flatten = l.filter p := by
…
```
Mentions: OAI.Problem335.WordRuns.splitTrueAux
theorem OAI.Problem335.WordRuns.trueBlocks_flatten line 45
theorem OAI.Problem335.WordRuns.trueBlocks_ne_nil line 50
Source documentation
Every retained block is nonempty.
```
theorem trueBlocks_ne_nil (p : α → Bool) (l : List α) {b : List α}
    (hb : b ∈ trueBlocks p l) : b ≠ [] := by
…
```
Mentions: OAI.Problem335.WordRuns.trueBlocks
theorem OAI.Problem335.WordRuns.splitTrueAux_infix line 55
theorem OAI.Problem335.WordRuns.trueBlocks_infix line 75
Source documentation
Every true block is a contiguous interval of the original ordered list.
```
theorem trueBlocks_infix (p : α → Bool) (l : List α) {b : List α}
    (hb : b ∈ trueBlocks p l) : b <:+: l :=
…
```
Mentions: OAI.Problem335.WordRuns.trueBlocks
theorem OAI.Problem335.WordRuns.trueBlocks_all_true line 80
Source documentation
Every member of a true block satisfies the selection predicate.
```
theorem trueBlocks_all_true (p : α → Bool) (l : List α) {b : List α}
    (hb : b ∈ trueBlocks p l) {a : α} (ha : a ∈ b) : p a = true := by
…
```
Mentions: OAI.Problem335.WordRuns.trueBlocks
theorem OAI.Problem335.WordRuns.trueBlocks_length_cons line 87
Source documentation
Adding one letter either extends the first block or creates one new block.
```
theorem trueBlocks_length_cons (p : α → Bool) (a : α) (l : List α) :
    (trueBlocks p (a :: l)).length = (trueBlocks p l).length +
      if p a = true ∧ (splitTrueAux p l).1 = [] then 1 else 0 := by
…
```
Mentions: OAI.Problem335.WordRuns.trueBlocks, OAI.Problem335.WordRuns.splitTrueAux
theorem OAI.Problem335.WordRuns.trueBlocks_ofFn_length line 96
Source documentation
For a nonempty list of word positions, block count is the true run count.
```
theorem trueBlocks_ofFn_length {n : ℕ} (w : Fin (n + 1) → Bool) :
    (trueBlocks w (List.ofFn id)).length = runCount w := by
…
```
Mentions: OAI.Problem335.WordRuns.trueBlocks, OAI.Problem335.WordRuns.runCount

theorem OAI.Problem335.WordRuns.trueBlocks_prod line 136

Source documentation

Products over selected positions factor exactly into products over true blocks.

theorem trueBlocks_prod {R : Type*} [Monoid R] (p : α → Bool) (l : List α) (f : α → R) :
    ((l.filter p).map f).prod =
      ((trueBlocks p l).map (fun b => (b.map f).prod)).prod := by
…

Mentions: OAI.Problem335.WordRuns.trueBlocks

theorem OAI.Problem335.WordRuns.selected_prod_le_pow_runCount line 143

Source documentation

A uniform bound on each interval multiplies once per true run.

theorem selected_prod_le_pow_runCount {n : ℕ} (w : Fin (n + 1) → Bool)
    (f : Fin (n + 1) → ℝ) (B : ℝ) (hf : ∀ i, 0 ≤ f i)
    (hB : ∀ b ∈ trueBlocks w (List.ofFn id), (b.map f).prod ≤ B) :
    (((List.ofFn id).filter w).map f).prod ≤ B ^ runCount w := by
…

Mentions: OAI.Problem335.WordRuns.trueBlocks, OAI.Problem335.WordRuns.runCount

theorem OAI.Problem335.WordRuns.trueBlocks_sum line 159

Source documentation

Additive statistics are also exactly preserved by the block partition.

theorem trueBlocks_sum {R : Type*} [AddMonoid R]
    (p : α → Bool) (l : List α) (g : α → R) :
    ((l.filter p).map g).sum =
      ((trueBlocks p l).map (fun b => (b.map g).sum)).sum := by
…

Mentions: OAI.Problem335.WordRuns.trueBlocks

theorem OAI.Problem335.WordRuns.trueBlocks_countP line 167
Source documentation
Counts in any second layer partition add across the true blocks.
```
theorem trueBlocks_countP (p q : α → Bool) (l : List α) :
    ((trueBlocks p l).map (List.countP q)).sum = (l.filter p).countP q := by
…
```
Mentions: OAI.Problem335.WordRuns.trueBlocks
theorem OAI.Problem335.WordRuns.trueBlocks_sum_length line 172
Source documentation
Total lengths of the runs count exactly the selected positions.
```
theorem trueBlocks_sum_length (p : α → Bool) (l : List α) :
    ((trueBlocks p l).map List.length).sum = (l.filter p).length := by
…
```
Mentions: OAI.Problem335.WordRuns.trueBlocks
theorem OAI.Problem335.WordRuns.prod_run_majorants line 176

theorem OAI.Problem335.WordRuns.selected_prod_le_pow_runCount_mul_exp line 188

Source documentation

Interval majorants with local exponential losses multiply once per run, while the exponential losses add only once per selected position.

theorem selected_prod_le_pow_runCount_mul_exp {n : ℕ}
    (w : Fin (n + 1) → Bool) (f g : Fin (n + 1) → ℝ) (B : ℝ)
    (hf : ∀ i, 0 ≤ f i)
    (hB : ∀ b ∈ trueBlocks w (List.ofFn id),
      (b.map f).prod ≤ B * Real.exp ((b.map g).sum)) :
    (((List.ofFn id).filter w).map f).prod ≤
      B ^ runCount w * Real.exp ((((List.ofFn id).filter w).map g).sum) := by
…

Mentions: OAI.Problem335.WordRuns.trueBlocks, OAI.Problem335.WordRuns.runCount