MovingPatternUniformBudget.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform costs of the actual internal equality patterns

theorem OAI.Ostmann.movingPattern_class_card_le line 10

theorem OAI.Ostmann.movingPattern_loss_le line 22

Source documentation

The representative-prior loss is bounded independently of how the internal slots coincide.

theorem movingPattern_loss_le (n r : ℕ) (hr : r ≤ 4 * n * 2 ^ n)
    (E : ℝ) (hE : 0 ≤ E) :
    (2 : ℝ) ^ r * E ^ (4 * n * 2 ^ n - r) ≤
      (max 2 E) ^ (4 * n * 2 ^ n) := by
…

theorem OAI.Ostmann.movingPattern_quotient_card_le line 33
theorem OAI.Ostmann.movingPattern_error_sum_le line 42
Source documentation
Summing every original equality pattern introduces only a depth-dependent factor. The number of protected bulk slots never appears in this cost.
```
theorem movingPattern_error_sum_le (n : ℕ) (E D : ℝ) (hE : 0 ≤ E) (hD : 0 ≤ D) :
    letI := sampleSetoidFintype (Bool × MovingSampleIndex n)
…
```
Mentions: OAI.Ostmann.sampleSetoidFintype, OAI.Ostmann.MovingSampleIndex