OAI/NumberTheory/JointDickman/Amplification/UnionSelection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.bernoulli_union_survival line 13

   Source documentation

   Independent form choices work equally for finite sets of zeros, such as lines in a residue plane. Intersections between the sets cause no loss.

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

   Mentions: OAI.JointDickman.bernoulliSubsetMass

2. theorem OAI.JointDickman.bernoulli_union_density line 44

   Source documentation

   The mean density of the surviving residue set is the exact residue average of all retained form weights.

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

   Mentions: OAI.JointDickman.bernoulliSubsetMass