Chernoff.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.FiniteLaw.prob_mono line 17
lemma OAI.HyperbolicObstruction.FiniteLaw.prob_or_le line 26
lemma OAI.HyperbolicObstruction.FiniteLaw.bernoulli_centered_exp_le line 33
def OAI.HyperbolicObstruction.FiniteLaw.centeredCount line 50
Source documentation
The centered Bernoulli count in a specified trial set. Trials belonging to other table entries are integrated out, not made dependent.
```
def centeredCount {I : Type*} [Fintype I] (p : I → ℝ) (S : Finset I) (w : I → Bool) : ℝ :=
…
```
lemma OAI.HyperbolicObstruction.FiniteLaw.centeredCount_mgf line 53
theorem OAI.HyperbolicObstruction.FiniteLaw.centeredCount_chernoff line 84
Source documentation
Two-sided multiplicative Chernoff estimate, with an explicit constant 4. It suffices for the simultaneous six-letter pair counts.
```
theorem centeredCount_chernoff {I : Type*} [Fintype I] [DecidableEq I]
    (p : I → ℝ) (hp : ∀ i, p i ∈ Set.Icc (0 : ℝ) 1) (S : Finset I)
    {ε : ℝ} (hε : 0 < ε) (hε2 : ε ≤ 2) :
    (bernoulliProduct p hp).prob (fun w => ε*(∑ i ∈ S, p i) ≤ |centeredCount p S w|) ≤
      2*Real.exp (-ε^2*(∑ i ∈ S, p i)/4) := by
…
```
Mentions: OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct, OAI.HyperbolicObstruction.FiniteLaw.prob, OAI.HyperbolicObstruction.FiniteLaw.centeredCount