OAI/NumberTheory/JointDickman/Amplification/HighLowThinning.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.partition_union_inter_left line 11
2. theorem OAI.JointDickman.partition_union_inter_right line 20
3. def OAI.JointDickman.highNoAdditionMass line 27
4. theorem OAI.JointDickman.high_low_thinning_factor line 35

   Source documentation

   The high tail restriction and no high additions leave the low addition law unchanged. In particular, this identity does not condition high second coins on the low-ratio event.

   theorem high_low_thinning_factor {α : Type*} [DecidableEq α]
       (P Q : Finset α) (hd : Disjoint P Q) (q : α → ℝ) (k : ℝ) (F : Finset α → ℝ) :
       (∑ S ∈ (P ∪ Q).powerset, ∑ T ∈ (P ∪ Q).powerset,
         jointRetentionMass (P ∪ Q) q S T *
           (if k ≤ ((S ∩ Q).card : ℝ) ∧ T ∩ Q = ∅ then F (T ∩ P) else 0)) =
         highNoAdditionMass Q q k *
           (∑ U ∈ P.powerset, bernoulliSubsetMass P (fun p => q p / 2) U * F U) := by
   …

   Mentions: OAI.JointDickman.jointRetentionMass, OAI.JointDickman.highNoAdditionMass, OAI.JointDickman.bernoulliSubsetMass

5. theorem OAI.JointDickman.fixed_high_retention_factor line 91

   Source documentation

   The coefficient's high primes are all kept. Low coefficient coins retain their original independent fair law.

   theorem fixed_high_retention_factor {α : Type*} [DecidableEq α]
       (P Q : Finset α) (hd : Disjoint P Q) (F : Finset α → ℝ) :
       (∑ S ∈ (P ∪ Q).powerset, bernoulliSubsetMass (P ∪ Q) (fun _ => (1 / 2 : ℝ)) S *
         (if S ∩ Q = Q then F (S ∩ P) else 0)) =
         (1 / 2 : ℝ)^Q.card * (∑ A ∈ P.powerset, bernoulliSubsetMass P (fun _ => (1 / 2 : ℝ)) A * F A) := by
   …

   Mentions: OAI.JointDickman.bernoulliSubsetMass

6. theorem OAI.JointDickman.high_low_thinning_bound line 124

   Source documentation

   A bounded low-addition test costs its own bound times the high no-change factor, with no conditioning on the rare low event.

   theorem high_low_thinning_bound {α : Type*} [DecidableEq α]
       (P Q : Finset α) (hd : Disjoint P Q) (q : α → ℝ) (k K : ℝ) (hK : 0 ≤ K)
       (hq : ∀ p ∈ P ∪ Q, 0 ≤ q p ∧ q p ≤ 1) (F : Finset α → ℝ)
       (hF : (∑ U ∈ P.powerset, bernoulliSubsetMass P (fun p => q p / 2) U * F U) ≤ K) :
       (∑ S ∈ (P ∪ Q).powerset, ∑ T ∈ (P ∪ Q).powerset,
         jointRetentionMass (P ∪ Q) q S T *
           (if k ≤ ((S ∩ Q).card : ℝ) ∧ T ∩ Q = ∅ then F (T ∩ P) else 0)) ≤
         (1 / 2 : ℝ)^k * K := by
   …

   Mentions: OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.jointRetentionMass