CountParameters.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Numerical parameters for the simultaneous direction count

The final steps in §6: a fixed polynomial times a Gaussian tail is below any prescribed exponential budget, and the chosen direction bound has the required factor-one-hundred margin.

theorem OAI.LipschitzHilbert.polynomial_gaussian_le_exponential line 23

Source documentation

An explicit sufficient lower bound for the count-exception budget.

theorem polynomial_gaussian_le_exponential {C c J a L : ℝ}
    (hC : 0 < C) (hc : 0 < c) (hL : 1 ≤ L)
    (hlarge : (|Real.log C| + |a| + J) / c ≤ L) :
    C * L ^ a * Real.exp (-c * L ^ 2) ≤ Real.exp (-J * L) := by
…

theorem OAI.LipschitzHilbert.eventually_polynomial_gaussian_le_exponential line 54
Source documentation
The exceptional budget holds for all sufficiently large L, with no dependence on the number of tops or scales.
```
theorem eventually_polynomial_gaussian_le_exponential (C a J : ℝ) {c : ℝ}
    (hC : 0 < C) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop, C * L ^ a * Real.exp (-c * L ^ 2) ≤ Real.exp (-J * L) := by
…
```
theorem OAI.LipschitzHilbert.count_threshold_product line 62
Source documentation
theta=L^(-a) and Lambda=L^(a+2) give the exact quadratic tail.
```
theorem count_threshold_product {L : ℝ} (hL : 0 < L) (a : ℝ) :
    L ^ (-a) * L ^ (a + 2) = L ^ 2 := by
…
```
theorem OAI.LipschitzHilbert.count_direction_margin line 70
Source documentation
The manuscript's D=L^(a+4) absorbs the count threshold and the reference direction with the stated factor-one-hundred margin.
```
theorem count_direction_margin {L a : ℝ} (hL : 15 ≤ L) (ha : 0 ≤ a) :
    1 + L ^ (a + 2) ≤ L ^ (a + 4) / 100 := by
…
```

theorem OAI.LipschitzHilbert.count_power_budget line 88

Source documentation

With K=L^k, P=L^p, p≥k, theta=L^(-a) and lambda=L^(a+2), the complete reference-family prefactor is absorbed by the exact Gaussian rate supplied by angular counting.

theorem count_power_budget {L k p a c J : ℝ} (hL : 1 ≤ L) (hkp : k ≤ p)
    (hc : 0 ≤ c)
    (hlarge : 240 * (1 + c) * (|Real.log 768| + |2 * p| + J) ≤ L) :
    384 * L ^ k * (L ^ k + L ^ p) *
        Real.exp (-(L ^ (-a) * L ^ (a + 2)) / (240 * (1 + c))) ≤
      Real.exp (-J * L) := by
…

theorem OAI.LipschitzHilbert.eventually_count_power_budget line 123