ScaleBounds.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

The largest admissible scale

The cutoff is constructed as the first index whose next scale fails. Its existence follows from the Archimedean property and the elementary lower bound scaleSum s ≥ s. No finite search bound or computed large power is used.

theorem OAI.TalagrandThreshold.scaleSum_succ line 25
theorem OAI.TalagrandThreshold.scaleSum_monotone line 29
theorem OAI.TalagrandThreshold.scaleSum_ge_nat line 35
theorem OAI.TalagrandThreshold.scaleSum_le_two_pow line 43
Source documentation
The finite geometric sum is at most twice its largest power.
```
theorem scaleSum_le_two_pow (s : ℕ) : scaleSum s ≤ 2 * (256 : ℝ) ^ s := by
…
```
Mentions: OAI.TalagrandThreshold.scaleSum
theorem OAI.TalagrandThreshold.half_geometric_sum_identity line 51
theorem OAI.TalagrandThreshold.half_geometric_sum_le_one line 60
theorem OAI.TalagrandThreshold.scale_next_fail_exists line 67
Source documentation
Some next scale fails whenever the density is positive.
```
theorem scale_next_fail_exists {p : ℝ} (hp : 0 < p) :
    ∃ s : ℕ, 1 / 2 < p * scaleSum (s + 1) := by
…
```
Mentions: OAI.TalagrandThreshold.scaleSum
def OAI.TalagrandThreshold.maxScale line 81
Source documentation
The largest admissible scale; its irrelevant nonpositive-density value is zero.
```
noncomputable def maxScale (p : ℝ) : ℕ := by
…
```
theorem OAI.TalagrandThreshold.maxScale_eq_find line 85
theorem OAI.TalagrandThreshold.maxScale_next_fail line 90
theorem OAI.TalagrandThreshold.maxScale_admissible line 96
theorem OAI.TalagrandThreshold.maxScale_largest line 108
Source documentation
Every admissible integer is at most the constructed cutoff.
```
theorem maxScale_largest {p : ℝ} (hp : 0 < p) {t : ℕ}
    (ht : p * scaleSum t ≤ 1 / 2) : t ≤ maxScale p := by
…
```
Mentions: OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.maxScale
theorem OAI.TalagrandThreshold.exists_scale line 117
Source documentation
The exact pair of cutoff inequalities used by the rounding argument.
```
theorem exists_scale {p : ℝ} (hp : 0 < p) :
    ∃ s : ℕ, p * scaleSum s ≤ 1 / 2 ∧ 1 / 2 < p * scaleSum (s + 1) :=
…
```
Mentions: OAI.TalagrandThreshold.scaleSum
theorem OAI.TalagrandThreshold.tail_lt_four_mul_p line 122
Source documentation
Failure at the next scale controls the residual color contribution.
```
theorem tail_lt_four_mul_p {p : ℝ} {s : ℕ} (hp : 0 < p)
    (hnext : 1 / 2 < p * scaleSum (s + 1)) :
    1 / (512 : ℝ) ^ (s + 1) < 4 * p := by
…
```
Mentions: OAI.TalagrandThreshold.scaleSum
theorem OAI.TalagrandThreshold.maxScale_tail_lt line 137