RankProbability.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic and zero-set estimates for random prime controls

A nonzero integer has few distinct prime divisors. Bounds for joint zero-coordinate events then control the probability that independent prime coordinates divide every entry of a random integral vector.

lemma OAI.TwoPointCorrelations.card_primeFactors_le_log_two line 19
lemma OAI.TwoPointCorrelations.card_prime_divisors_le_log line 27

lemma OAI.TwoPointCorrelations.FiniteLaw.prime_divisibility_probability line 38

Source documentation

A nonzero integer can be hit only by its distinct prime divisors.

lemma prime_divisibility_probability (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (μ : FiniteLaw P) (α : ℝ) (hα : 0 ≤ α) (hμ : ∀ p, μ.weight p ≤ α)
    (z : ℤ) (hz : z ≠ 0) :
    μ.probability (fun p => (p.val : ℤ) ∣ z) ≤ α * (Nat.log 2 z.natAbs : ℝ) := by
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw

theorem OAI.TwoPointCorrelations.FiniteLaw.zero_set_product_bound line 62

Source documentation

Expanding by zero-coordinate subsets converts joint zero estimates into a product estimate. This does not require independence of the zero events.

theorem zero_set_product_bound {Y ι : Type*} [Fintype Y] [Fintype ι] [DecidableEq ι]
    (μ : FiniteLaw Y) (v : Y → ι → ℤ) (α β : ℝ) (hβ : 0 ≤ β)
    (hzero : ∀ S : Finset ι,
      μ.average (fun y => ∏ i ∈ S, if v y i = 0 then (1 : ℝ) else 0) ≤ α ^ S.card) :
    μ.average (fun y => ∏ i, if v y i = 0 then (1 : ℝ) else β) ≤
      (α + β) ^ Fintype.card ι := by
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw