MovingThresholds.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The deterministic moving-threshold sandwich

This is the comparison used in the last part of distribution.tex. It does not assume any joint limit: it bounds the actual finite counts at the two sets of thresholds, with the discarded initial segment explicitly counted.

theorem OAI.JointDickman.eventually_power_lower line 19
theorem OAI.JointDickman.movingEvent_implies_fixed line 31
theorem OAI.JointDickman.fixedEvent_implies_moving_away_from_zero line 46
theorem OAI.JointDickman.count_le_count_add_bad line 63
theorem OAI.JointDickman.smallPrefix_count_le line 78
theorem OAI.JointDickman.fixedCount_le_moving_add_prefix line 92
Source documentation
The cost of changing fixed lower thresholds to moving thresholds is at most the discarded initial segment. This is a finite-count estimate.
```
theorem fixedCount_le_moving_add_prefix {δ a b c d : ℝ}
    (hδ : 0 < δ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hca : c < a) (hdb : d < b) :
    ∀ᶠ N : ℕ in atTop,
      empiricalCount (fixedScaleEvent c d N) N ≤
        empiricalCount (movingEvent a b) N + ⌊δ * (N : ℝ)⌋₊ := by
…
```
Mentions: OAI.JointDickman.empiricalCount, OAI.JointDickman.fixedScaleEvent, OAI.JointDickman.movingEvent
theorem OAI.JointDickman.movingCount_le_fixed line 106