PrimeSetWeights.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Finite prime-selection and fair-split weights

The independent prime-set model and its fair splits satisfy exact finite identities without prime asymptotics or analytic equidistribution premises.

def OAI.JointDickman.bernoulliSubsetMass line 20
Source documentation
The independent-selection mass of a subset of P. All sums of these masses below are restricted to P.powerset.
```
noncomputable def bernoulliSubsetMass {α : Type*} [DecidableEq α]
    (P : Finset α) (q : α → ℝ) (S : Finset α) : ℝ :=
…
```
theorem OAI.JointDickman.bernoulliSubsetMass_nonneg line 24
theorem OAI.JointDickman.bernoulliSubsetMass_sum line 33

theorem OAI.JointDickman.bernoulliSubsetMass_tilt line 41

Source documentation

The exact finite product formula for a multiplicative tilt.

theorem bernoulliSubsetMass_tilt {α : Type*} [DecidableEq α]
    (P : Finset α) (q v : α → ℝ) :
    ∑ S ∈ P.powerset, bernoulliSubsetMass P q S * (∏ p ∈ S, v p) =
      ∏ p ∈ P, (1 - q p + q p * v p) := by
…

Mentions: OAI.JointDickman.bernoulliSubsetMass

theorem OAI.JointDickman.bernoulliSubsetMass_complement_formula line 55

theorem OAI.JointDickman.primeProduct_injective line 69

Source documentation

Products of distinct prime sets remember their set of factors.

theorem primeProduct_injective {P : Finset ℕ} (hP : ∀ p ∈ P, p.Prime)
    {S T : Finset ℕ} (hS : S ⊆ P) (hT : T ⊆ P)
    (heq : (∏ p ∈ S, p) = ∏ p ∈ T, p) : S = T := by
…

def OAI.JointDickman.primeProductMass line 78
Source documentation
The prime-product pushforward of independent Bernoulli z/p selection; this is the manuscript's ν_z on the finite allowed prime set.
```
noncomputable def primeProductMass (P : Finset ℕ) (z : ℝ) (n : ℕ) : ℝ :=
…
```
theorem OAI.JointDickman.primeProductMass_at_product line 82

theorem OAI.JointDickman.primeProductMass_exact line 99

Source documentation

Exact ν_z mass, factored into the all-absent probability and the local odds ratios.

theorem primeProductMass_exact {P S : Finset ℕ} (z : ℝ)
    (hP : ∀ p ∈ P, p.Prime) (hS : S ⊆ P)
    (hz : ∀ p ∈ P, 1 - z / (p : ℝ) ≠ 0) :
    primeProductMass P z (∏ p ∈ S, p) =
      (∏ p ∈ P, (1 - z / (p : ℝ))) *
        ∏ p ∈ S, ((z / (p : ℝ)) / (1 - z / (p : ℝ))) := by
…

Mentions: OAI.JointDickman.primeProductMass

theorem OAI.JointDickman.primeProductMass_eq_zero line 108
theorem OAI.JointDickman.primeProductMass_sum line 119
Source documentation
The pushforward mass is normalized on its finite set of prime products.
```
theorem primeProductMass_sum {P : Finset ℕ} (z : ℝ)
    (hP : ∀ p ∈ P, p.Prime) :
    ∑ n ∈ P.powerset.image (fun S => ∏ p ∈ S, p), primeProductMass P z n = 1 := by
…
```
Mentions: OAI.JointDickman.primeProductMass
theorem OAI.JointDickman.bernoulliSubsetMass_half line 136
Source documentation
Probability 1/2 at each member of a fixed site gives the uniform fair-split mass, including the empty site.
```
theorem bernoulliSubsetMass_half {α : Type*} [DecidableEq α]
    {S T : Finset α} (hT : T ⊆ S) :
    bernoulliSubsetMass S (fun _ => (1 / 2 : ℝ)) T = (1 / 2 : ℝ) ^ S.card := by
…
```
Mentions: OAI.JointDickman.bernoulliSubsetMass

theorem OAI.JointDickman.fairSplit_weight_identity line 146

Source documentation

The coefficient and remaining-site weight convert a sum over divisors into a fair-split expectation, with total normalization L * R.

theorem fairSplit_weight_identity {α : Type*} [DecidableEq α]
    {S T : Finset α} (hT : T ⊆ S) (L R : ℝ) (hR : 0 ≤ R) :
    (L * Real.sqrt R * (1 / 2 : ℝ) ^ T.card) *
        (Real.sqrt R * (1 / 2 : ℝ) ^ (S \ T).card) =
      L * R * (1 / 2 : ℝ) ^ S.card := by
…

theorem OAI.JointDickman.bernoulliSubsetMass_tilt_tail line 159

Source documentation

A finite positive-tilt Markov bound, before any prime-sum estimate.

theorem bernoulliSubsetMass_tilt_tail {α : Type*} [DecidableEq α]
    (P : Finset α) (q v : α → ℝ) (r : ℝ)
    (hq : ∀ p ∈ P, 0 ≤ q p ∧ q p ≤ 1)
    (hv : ∀ p ∈ P, 0 ≤ v p) :
    r * (∑ S ∈ P.powerset, if r ≤ ∏ p ∈ S, v p then
      bernoulliSubsetMass P q S else 0) ≤
      ∏ p ∈ P, (1 - q p + q p * v p) := by
…

Mentions: OAI.JointDickman.bernoulliSubsetMass

theorem OAI.JointDickman.bernoulliSubsetMass_count_exp line 177

Source documentation

Exact exponential moment of the number of selected primes.

theorem bernoulliSubsetMass_count_exp {α : Type*} [DecidableEq α]
    (P : Finset α) (q : α → ℝ) (t : ℝ) :
    ∑ S ∈ P.powerset, bernoulliSubsetMass P q S * Real.exp (t * S.card) =
      ∏ p ∈ P, (1 - q p + q p * Real.exp t) := by
…

Mentions: OAI.JointDickman.bernoulliSubsetMass

theorem OAI.JointDickman.bernoulliSubsetMass_count_tail line 189

Source documentation

Exponential upper tail for the selected-prime count. Prime estimates are needed only afterward to bound the explicit product on the right.

theorem bernoulliSubsetMass_count_tail {α : Type*} [DecidableEq α]
    (P : Finset α) (q : α → ℝ) (k : ℕ) {t : ℝ} (ht : 0 ≤ t)
    (hq : ∀ p ∈ P, 0 ≤ q p ∧ q p ≤ 1) :
    (∑ S ∈ P.powerset, if k ≤ S.card then bernoulliSubsetMass P q S else 0) ≤
      Real.exp (-t * k) * ∏ p ∈ P, (1 - q p + q p * Real.exp t) := by
…

Mentions: OAI.JointDickman.bernoulliSubsetMass