OAI/NumberTheory/JointDickman/Amplification/RestrictedRootComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.restrictedRootMass_eq_categorical line 12
2. theorem OAI.JointDickman.restrictedRootMass_l1_crude line 34

   Source documentation

   Even at a defective prime, each individual root test occupies at most one allowed residue. No distinctness assumption is used here.

   theorem restrictedRootMass_l1_crude {α : Type*} [DecidableEq α]
       (I : Finset α) {p : ℕ} (hp : p.Prime) (root : α → ZMod p)
       (U : Finset (ZMod p)) (hU : 0 < U.card) :
       (∑ S : I.powerset, |restrictedRootMass I root U S-
         bernoulliSubsetMass I (fun _ => 1/(p : ℝ)) S.val|) ≤
         2*(I.card : ℝ)/(U.card : ℝ)+2*(I.card : ℝ)/(p : ℝ) := by
   …

   Mentions: OAI.JointDickman.restrictedRootMass, OAI.JointDickman.bernoulliSubsetMass

3. theorem OAI.JointDickman.restrictedRootMass_l1_good line 60