WeightedSieve.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Reducing local weights by random forbidding

The upper sieve is applied to deterministic forbidden congruences. Randomly forbidding each form converts that bound to the product of its local weights, without changing the remainder. The transfer below is exact on finite sets; the deterministic upper-sieve estimate is a separate published input.

def OAI.JointDickman.avoidsSelected line 19

Source documentation

A point survives if none of its vanishing forms is selected.

noncomputable def avoidsSelected {ι : Type*} [DecidableEq ι]
    (S E : Finset ι) : ℝ := if Disjoint S E then 1 else 0

theorem OAI.JointDickman.avoidsSelected_eq_product line 22

theorem OAI.JointDickman.bernoulliSubsetMass_avoids line 38

Source documentation

Average survival is exactly the product of the retained local weights.

theorem bernoulliSubsetMass_avoids {ι : Type*} [DecidableEq ι]
    (P E : Finset ι) (hE : E ⊆ P) (θ : ι → ℝ) :
    (∑ S ∈ P.powerset, bernoulliSubsetMass P (fun i => 1 - θ i) S * avoidsSelected S E) =
      ∏ i ∈ E, θ i := by
…

Mentions: OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.avoidsSelected

theorem OAI.JointDickman.randomized_sifted_mass line 59

Source documentation

Exact finite expectation identity for a population of points.

theorem randomized_sifted_mass {ι X : Type*} [DecidableEq ι] [Fintype X]
    (P : Finset ι) (E : X → Finset ι) (hE : ∀ x, E x ⊆ P)
    (w : X → ℝ) (θ : ι → ℝ) :
    (∑ S ∈ P.powerset, bernoulliSubsetMass P (fun i => 1 - θ i) S *
      ∑ x, w x * avoidsSelected S (E x)) = ∑ x, w x * ∏ i ∈ E x, θ i := by
…

Mentions: OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.avoidsSelected

theorem OAI.JointDickman.upper_sieve_reducing_weights line 82

Source documentation

A deterministic upper-sieve estimate for every choice of forbidden forms transfers to reducing weights with the same remainder and constant. The second population can be the product of the local residue spaces.

theorem upper_sieve_reducing_weights {ι X Y : Type*} [DecidableEq ι]
    [Fintype X] [Fintype Y] (P : Finset ι)
    (E : X → Finset ι) (F : Y → Finset ι)
    (hE : ∀ x, E x ⊆ P) (hF : ∀ y, F y ⊆ P)
    (w : X → ℝ) (v : Y → ℝ) (θ : ι → ℝ)
    (hθ : ∀ i ∈ P, 0 ≤ θ i ∧ θ i ≤ 1) (C R : ℝ)
    (hupper : ∀ S ⊆ P, (∑ x, w x * avoidsSelected S (E x)) ≤
      C * (∑ y, v y * avoidsSelected S (F y)) + R) :
    (∑ x, w x * ∏ i ∈ E x, θ i) ≤
      C * (∑ y, v y * ∏ i ∈ F y, θ i) + R := by
…

Mentions: OAI.JointDickman.avoidsSelected