OAI/NumberTheory/TwoPoint/Bounds/BernoulliTail.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact exponential moments and elementary upper tails for the finite independent Boolean laws used by the two prime-degree deletions.

  1. lemma OAI.TwoPointCorrelations.FiniteLaw.probability_lt_exp_bound line 14
  2. def OAI.TwoPointCorrelations.booleanCount line 30
  3. lemma OAI.TwoPointCorrelations.booleanCount_eq_card line 33
  4. lemma OAI.TwoPointCorrelations.booleanLaw_exp_average line 37
  5. lemma OAI.TwoPointCorrelations.independent_boolean_exp_average line 43
  6. lemma OAI.TwoPointCorrelations.independent_boolean_exp_bound line 57
  7. theorem OAI.TwoPointCorrelations.independent_boolean_tail line 77

    Source documentation

    The entire bound is a finite product identity followed by exponential Markov; no probability theorem is assumed.

    theorem independent_boolean_tail {ι : Type*} [Fintype ι] [DecidableEq ι]
    (q : ι → ℝ) (hq0 : ∀ i, 0 ≤ q i) (hq1 : ∀ i, q i ≤ 1)
    (t M a : ℝ) (ht : 0 ≤ t) (hM : (∑ i, q i) ≤ M) :
    (FiniteLaw.independent (fun i => booleanLaw (q i) (hq0 i) (hq1 i))).probability
      (fun b => a < booleanCount b) ≤
        Real.exp ((Real.exp t - 1) * M - t * a) := by
…

    Mentions: OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.booleanLaw, OAI.TwoPointCorrelations.booleanCount