LocalMoment.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Local positive moments without independence

The probabilistic summation in lem:local-moment of paper 031-01. The distribution may live on an arbitrary countable set, and all component correlations are allowed. A geometric bound on the maximum valuation implies a positive moment bound.

def OAI.DukePrimeDegree.valuationTail line 23
Source documentation
Upper tail of a natural-number-valued random variable, written for a nonnegative discrete mass function.
```
noncomputable def valuationTail {Ω : Type*} (p : Ω → ℝ≥0∞) (j : Ω → ℕ)
    (a : ℕ) : ℝ≥0∞ := ∑' ω, if a ≤ j ω then p ω else 0
```
theorem OAI.DukePrimeDegree.valuationTail_sup_le_sum line 29
Source documentation
The tail of a maximum is bounded by the sum of the component tails. No independence assumption is present. The positive threshold also covers the possibility of an empty index type.
```
theorem valuationTail_sup_le_sum {Ω I : Type*} [Fintype I]
    (p : Ω → ℝ≥0∞) (j : I → Ω → ℕ) (a : ℕ) (ha : 0 < a) :
    valuationTail p (fun ω => Finset.univ.sup (fun i => j i ω)) a ≤
      ∑ i, valuationTail p (j i) a := by
…
```
Mentions: OAI.DukePrimeDegree.valuationTail

theorem OAI.DukePrimeDegree.moment_le_of_valuation_tail line 52

Source documentation

A tail bound controls the local norm moment. In the application, r = ℓ^(n*s), t = ℓ⁻¹, and C = n.

theorem moment_le_of_valuation_tail {Ω : Type*}
    (p : Ω → ℝ≥0∞) (j : Ω → ℕ) (r t C : ℝ≥0∞)
    (htotal : ∑' ω, p ω = 1)
    (htail : ∀ a : ℕ, valuationTail p j (a + 1) ≤ C * t ^ (a + 1)) :
    (∑' ω, p ω * r ^ j ω) ≤
      1 + C * ∑' a : ℕ, (r * t) ^ (a + 1) := by
…

Mentions: OAI.DukePrimeDegree.valuationTail

theorem OAI.DukePrimeDegree.moment_le_geometric_bound line 91

Source documentation

Closed-form version of the same estimate. For a rational prime ℓ and s = 1/(2*n), the ratio r*t becomes ℓ^(-1/2) < 1.

theorem moment_le_geometric_bound {Ω : Type*}
    (p : Ω → ℝ≥0∞) (j : Ω → ℕ) (r t C : ℝ≥0∞)
    (htotal : ∑' ω, p ω = 1)
    (htail : ∀ a : ℕ, valuationTail p j (a + 1) ≤ C * t ^ (a + 1)) :
    (∑' ω, p ω * r ^ j ω) ≤ 1 + C * ((r * t) * (1 - r * t)⁻¹) := by
…

Mentions: OAI.DukePrimeDegree.valuationTail

theorem OAI.DukePrimeDegree.moment_sup_le_geometric_bound line 101

Source documentation

Component tail estimates imply the local norm-moment estimate, with precisely the number of components as the union-bound factor.

theorem moment_sup_le_geometric_bound {Ω I : Type*} [Fintype I]
    (p : Ω → ℝ≥0∞) (j : I → Ω → ℕ) (r t : ℝ≥0∞)
    (htotal : ∑' ω, p ω = 1)
    (htail : ∀ i a, valuationTail p (j i) (a + 1) ≤ t ^ (a + 1)) :
    (∑' ω, p ω * r ^ Finset.univ.sup (fun i => j i ω)) ≤
      1 + (Fintype.card I : ℝ≥0∞) * ((r * t) * (1 - r * t)⁻¹) := by
…

Mentions: OAI.DukePrimeDegree.valuationTail