SimultaneousCountPowers.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The simultaneous count at the manuscript's polynomial thresholds.

theorem OAI.LipschitzHilbert.simultaneous_separated_count_powers line 19

Source documentation

The finite-family version of §6's simultaneous-count proposition: an S exp(-J L) exceptional set and the uniform D/100 list bound. The small-time hypothesis is stated in the precise strength used by the proved Lipschitz transfer, and all numerical choices are explicit.

theorem simultaneous_separated_count_powers {ι : Type*} [Fintype ι] [DecidableEq ι]
    (T : ι → SlopeBox) (u : ℝ × ℝ → ℝ) {Lip : ℝ≥0} (hu : LipschitzWith Lip u)
    {L a k p t c c0 B m J : ℝ} {M : ℕ}
    (hL : 15 ≤ L) (ha : 0 ≤ a)
    (hap : a + 1 ≤ p) (hkp : k + 1 ≤ p) (ht : 2 * a + p + 1 ≤ t)
    (hlarge : 240 * (1 + c) * (|Real.log 768| + |2 * p| + J) ≤ L)
    (hM : 0 < M) (hc0 : 0 ≤ c0) (hc : 4 * (c0 + 1) + 1 ≤ c)
    (hcM : c ≤ M) (hB : 1 < B) (hMB : (M : ℝ) = B ^ 2) (hm : B ^ 2 ≤ m)
    (d : ι → ℝ) (E : ι → Set (ℝ × ℝ))
    (hE : ∀ i, MeasurableSet (E i))
    (hfinite : ∀ i, (volume.prod volume) (E i) ≠ ∞)
    (hbox : ∀ i, ∀ w ∈ E i, (T i).radius w ≤ L ^ a)
…

Mentions: OAI.LipschitzHilbert.SlopeBox