OAI/NumberTheory/JointDickman/Amplification/RootSelection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.bernoulli_root_survival line 13

   Source documentation

   The chance that a residue survives independent choices of forbidden forms is the product of the retained weights of all forms vanishing there.

   theorem bernoulli_root_survival {ι α : Type*} [DecidableEq ι] [DecidableEq α]
       (I : Finset ι) (root : ι → α) (θ : ι → ℝ) (x : α) :
       (∑ S ∈ I.powerset, bernoulliSubsetMass I (fun i => 1 - θ i) S *
         (if x ∈ S.image root then 0 else 1)) =
         ∏ i ∈ I.filter (fun i => root i = x), θ i := by
   …

   Mentions: OAI.JointDickman.bernoulliSubsetMass

2. theorem OAI.JointDickman.root_survival_mean line 43

   Source documentation

   Uniform survival mass for a deterministic root set.

   theorem root_survival_mean {α : Type*} [Fintype α] [DecidableEq α]
       (hα : 0 < Fintype.card α) (T : Finset α) :
       (∑ x : α, (if x ∈ T then (0 : ℝ) else 1)) / Fintype.card α =
         1 - (T.card : ℝ) / Fintype.card α := by
   …

3. theorem OAI.JointDickman.bernoulli_root_density line 58

   Source documentation

   Averaging the local sieve density gives exactly the uniform residue average of the original form weights, even when some roots coincide.

   theorem bernoulli_root_density {ι α : Type*} [DecidableEq ι]
       [Fintype α] [DecidableEq α] (hα : 0 < Fintype.card α)
       (I : Finset ι) (root : ι → α) (θ : ι → ℝ) :
       (∑ S ∈ I.powerset, bernoulliSubsetMass I (fun i => 1 - θ i) S *
         (1 - ((S.image root).card : ℝ) / Fintype.card α)) =
         (∑ x : α, ∏ i ∈ I.filter (fun i => root i = x), θ i) / Fintype.card α := by
   …

   Mentions: OAI.JointDickman.bernoulliSubsetMass