ProbabilityScales.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.QuantitativeVanDerWaerden.Parameters.log_prime_slack line 12
theorem OAI.QuantitativeVanDerWaerden.Parameters.log_two_le_power_log line 21
def OAI.QuantitativeVanDerWaerden.Parameters.richEnvelope line 32
Source documentation
The exact exponent appearing in the rich-progression union bound.
```
def richEnvelope (k : ℕ) : ℝ :=
…
```
theorem OAI.QuantitativeVanDerWaerden.Parameters.richEnvelope_tendsto line 36
def OAI.QuantitativeVanDerWaerden.Parameters.affineEnvelope line 71
Source documentation
Envelope for twice the affine-signature count times the survival bound.
```
def affineEnvelope (C : ℝ) (k : ℕ) : ℝ :=
…
```
theorem OAI.QuantitativeVanDerWaerden.Parameters.affineEnvelope_tendsto line 75
theorem OAI.QuantitativeVanDerWaerden.Parameters.affine_risk_le line 80
def OAI.QuantitativeVanDerWaerden.Parameters.rowEnvelope line 97
Source documentation
A global-row envelope, from log T ≤ C k^(3/10) log k.
```
def rowEnvelope (C : ℝ) (k : ℕ) : ℝ :=
…
```
theorem OAI.QuantitativeVanDerWaerden.Parameters.rowEnvelope_tendsto line 101
theorem OAI.QuantitativeVanDerWaerden.Parameters.eventually_row_risk_le line 106
theorem OAI.QuantitativeVanDerWaerden.Parameters.eventually_perturbation_budget line 134
Source documentation
One threshold suffices to make both perturbation union bounds less than one. The scalar entropy constant is fixed before the number of colors is introduced.
```
theorem eventually_perturbation_budget {C : ℝ} (hC : 0 ≤ C) :
    ∀ᶠ k : ℕ in atTop, richEnvelope k + affineEnvelope C k < 1 := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.richEnvelope, OAI.QuantitativeVanDerWaerden.Parameters.affineEnvelope