RunSum.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Quantitative run-weight sums for the path-type estimate.

theorem OAI.Problem335.RunSum.switches_card_le_two_interior_add_two line 12
Source documentation
The inequality form also includes the constant all-true word.
```
theorem switches_card_le_two_interior_add_two {n : ℕ} (w : Fin (n + 1) → Bool) :
    (WordSwitches.switches w).card ≤ 2 * WordRuns.interiorRunCount w + 2 := by
…
```
Mentions: OAI.Problem335.WordSwitches.switches, OAI.Problem335.WordRuns.interiorRunCount

theorem OAI.Problem335.RunSum.sum_le_exp_of_switch_bound line 20

Source documentation

A pointwise switch-weight bound gives an exponential bound after summing all words.

theorem sum_le_exp_of_switch_bound (n : ℕ) (q A : ℝ) (hq : 0 ≤ q) (hA : 0 ≤ A)
    (F : (Fin (n + 1) → Bool) → ℝ)
    (hF : ∀ w, F w ≤ A * q ^ (WordSwitches.switches w).card) :
    (∑ w, F w) ≤ 2 * A * Real.exp ((n : ℝ) * q) := by
…

Mentions: OAI.Problem335.WordSwitches.switches

theorem OAI.Problem335.RunSum.sum_pow_two_interiorRuns_le line 33

Source documentation

The sum of the interior-run weights is controlled by the switch generating function.

theorem sum_pow_two_interiorRuns_le (n : ℕ) (q : ℝ) (hq : 0 < q) (hq1 : q ≤ 1) :
    (∑ w : Fin (n + 1) → Bool, q ^ (2 * WordRuns.interiorRunCount w)) ≤
      2 * (q ^ 2)⁻¹ * Real.exp ((n : ℝ) * q) := by
…

Mentions: OAI.Problem335.WordRuns.interiorRunCount

theorem OAI.Problem335.RunSum.sum_inv_pow_interiorRuns_le line 48

Source documentation

A convenient quantitative form of the run-count estimate in the path-word argument.

theorem sum_inv_pow_interiorRuns_le (n : ℕ) :
    (∑ w : Fin (n + 1) → Bool, (((n + 1 : ℕ) : ℝ)⁻¹) ^ WordRuns.interiorRunCount w) ≤
      2 * ((n + 1 : ℕ) : ℝ) * Real.exp (Real.sqrt ((n + 1 : ℕ) : ℝ)) := by
…

Mentions: OAI.Problem335.WordRuns.interiorRunCount

theorem OAI.Problem335.RunSum.two_mul_self_mul_exp_sqrt_le line 75
Source documentation
Absorb the polynomial factor in the elementary run estimate into a square-root exponential.
```
theorem two_mul_self_mul_exp_sqrt_le {x : ℝ} (hx : 1 ≤ x) :
    2 * x * Real.exp (Real.sqrt x) ≤ Real.exp (4 * Real.sqrt x) := by
…
```
theorem OAI.Problem335.RunSum.sum_inv_pow_interiorRuns_le_exp line 94
Source documentation
The full run-weight sum is at most exp (4 sqrt(length)), with an explicit absolute constant.
```
theorem sum_inv_pow_interiorRuns_le_exp (n : ℕ) :
    (∑ w : Fin (n + 1) → Bool, (((n + 1 : ℕ) : ℝ)⁻¹) ^ WordRuns.interiorRunCount w) ≤
      Real.exp (4 * Real.sqrt ((n + 1 : ℕ) : ℝ)) := by
…
```
Mentions: OAI.Problem335.WordRuns.interiorRunCount

theorem OAI.Problem335.RunSum.sum_le_exp_of_interiorRun_bound line 101

Source documentation

Application form: any pointwise run-weight estimate can be summed with the same absolute loss.

theorem sum_le_exp_of_interiorRun_bound (n : ℕ) (C : ℝ)
    (F : (Fin (n + 1) → Bool) → ℝ)
    (hF : ∀ w, F w ≤ Real.exp C * (((n + 1 : ℕ) : ℝ)⁻¹) ^ WordRuns.interiorRunCount w) :
    (∑ w, F w) ≤ Real.exp (C + 4 * Real.sqrt ((n + 1 : ℕ) : ℝ)) := by
…

Mentions: OAI.Problem335.WordRuns.interiorRunCount

theorem OAI.Problem335.RunSum.switches_card_add_endpoint_eq_two_runs line 116
Source documentation
Counting both endpoint bits (including twice for a constant true run) gives an exact balance.
```
theorem switches_card_add_endpoint_eq_two_runs {n : ℕ} (w : Fin (n + 1) → Bool) :
    (WordSwitches.switches w).card + WordRuns.endpointRunCount w =
      2 * WordRuns.runCount w := by
…
```
Mentions: OAI.Problem335.WordSwitches.switches, OAI.Problem335.WordRuns.endpointRunCount, OAI.Problem335.WordRuns.runCount
theorem OAI.Problem335.RunSum.switch_penalty_mul_run_weight_le line 126
Source documentation
Switch penalties pay for all but at most one square scale of the run weights. The constant words are included, so no exceptional-case partition is needed.
```
theorem switch_penalty_mul_run_weight_le {n : ℕ} (w : Fin (n + 1) → Bool)
    {N : ℝ} (hN : 1 ≤ N) :
    N⁻¹ ^ (WordSwitches.switches w).card * N ^ WordRuns.runCount w ≤
      N * (Real.sqrt N)⁻¹ ^ (WordSwitches.switches w).card := by
…
```
Mentions: OAI.Problem335.WordSwitches.switches, OAI.Problem335.WordRuns.runCount
theorem OAI.Problem335.RunSum.sum_switch_penalty_mul_run_weight_le_exp line 156
Source documentation
Direct application to products of interval weights: a factor N per true run, with N⁻¹ per switch, yields the required square-root exponential sum.
```
theorem sum_switch_penalty_mul_run_weight_le_exp (n : ℕ) :
    (∑ w : Fin (n + 1) → Bool,
      (((n + 1 : ℕ) : ℝ)⁻¹) ^ (WordSwitches.switches w).card *
        ((n + 1 : ℕ) : ℝ) ^ WordRuns.runCount w) ≤
      Real.exp (4 * Real.sqrt ((n + 1 : ℕ) : ℝ)) := by
…
```
Mentions: OAI.Problem335.WordSwitches.switches, OAI.Problem335.WordRuns.runCount

theorem OAI.Problem335.RunSum.sum_weighted_switch_penalty_le_exp line 178

Source documentation

Summation interface requiring only a pointwise product-of-runs bound.

theorem sum_weighted_switch_penalty_le_exp (n : ℕ) (C : ℝ)
    (F : (Fin (n + 1) → Bool) → ℝ)
    (hF : ∀ w, F w ≤ Real.exp C * ((n + 1 : ℕ) : ℝ) ^ WordRuns.runCount w) :
    (∑ w, (((n + 1 : ℕ) : ℝ)⁻¹) ^ (WordSwitches.switches w).card * F w) ≤
      Real.exp (C + 4 * Real.sqrt ((n + 1 : ℕ) : ℝ)) := by
…

Mentions: OAI.Problem335.WordRuns.runCount, OAI.Problem335.WordSwitches.switches