NumericRankinExponent.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The clamped Rankin exponent for numeric additions

theorem OAI.JointDickman.clamped_numeric_rankin line 13
Source documentation
The entropy exponent from the numeric sieve loses at most the clamp. This includes both the zero-cardinality class and counts exceeding half the prefix mean.
```
theorem clamped_numeric_rankin {x δ : ℝ} (hx : 0 ≤ x) (hδ : 0 < δ) (hδ1 : δ ≤ 1/2) :
    let r := min x (1/2)
…
```
theorem OAI.JointDickman.halfRankinExponent_le_half line 39

theorem OAI.JointDickman.numeric_rankin_exponent_bound line 52

Source documentation

The grid cutoff contributes at most 3Δ when g-γ=2Δ; the clamp contributes at most gδ.

theorem numeric_rankin_exponent_bound {g γ τ x δ : ℝ}
    (hg : 0 ≤ g) (hγ : γ ≤ g) (hx : 0 ≤ x) (hδ : 0 < δ) (hδ1 : δ ≤ 1/2) :
    let r := min x (1/2);
…

theorem OAI.JointDickman.numeric_rankin_prefactor_bound line 69

Source documentation

The prefactor cannot grow with an unbounded cardinality: above the clipping threshold its Rankin contribution is exactly one.

theorem numeric_rankin_prefactor_bound {g τ ℓ : ℝ} {d : ℕ} {δ : ℝ}
    (hg : 0 < g) (hg1 : g ≤ 1) (hℓ : 0 < ℓ) (hτ : τ ≤ 1)
    (hδ : 0 < δ) (hδ1 : δ ≤ 1/2) :
    let q := max δ (min ((d : ℝ)/(g*ℓ)) (1/2))
…

theorem OAI.JointDickman.halfRankinExponent_nonneg line 104