OAI/NumberTheory/JointDickman/Probability/SiteGoodEvent.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.finiteProbability_or_le line 11
2. def OAI.JointDickman.siteTotalSquare line 20
3. theorem OAI.JointDickman.siteTotalSquare_expectation line 24
4. theorem OAI.JointDickman.siteTotalSquare_bad_probability line 34
5. def OAI.JointDickman.SiteKernelGood line 48

   Source documentation

   The one common event used before taking a finite union of concentration tails. Its complement is charged once, not once per column sample.

   def SiteKernelGood {ι A : Type*} [Fintype ι]
       (E H : ι → ι → A → A → ℝ) (d Q : ℝ) (x : ι → A) : Prop :=
   …

6. theorem OAI.JointDickman.siteKernelGood_bad_probability line 52