Chernoff count le

lemma chernoff_count_le (f : Prob Bool) (n : ℕ) {t : ℝ} (t0 : 0 ≤ t) :    (count f n).pr (λ x ↦ n * f.prob true + t ≤ x) ≤ (-2 * t^2 / n).exp := by  generalize hp : f.prob true = p  by_cases tz : t = 0  · simp only [tz, pow_two, mul_zero, zero_div, Real.exp_zero, zero_pow]; apply pr_le_one  replace t0 := (Ne.symm tz).lt_of_le t0; clear tz  by_cases nz : n = 0  · simp only [nz, count, Nat.cast_zero, zero_mul, zero_add, pr, exp_pure, div_zero, Real.exp_zero]    split; rfl; norm_num  have h : ∀ s, 0 < s → (count f n).pr (λ x ↦ n * p + t ≤ x) ≤ (-s*t + n * s^2 / 8).exp := by    intros s s0    simp only [←@mul_le_mul_left _ _ (_ * _ + _) _ _ _ _ _ _ s0, ←@Real.exp_le_exp (_ * _) _]    apply le_trans (markov' _ _ (λ _ _ ↦ le_of_lt (Real.exp_pos _)) (Real.exp_pos _))    simp only [exp_count]    have le := hoeffdings_lemma' f (le_of_lt s0)    generalize hz : f.exp (λ x ↦ (s * bif x then 1 else 0).exp) = z; simp only [hz] at le ⊢    have z0 : 0 ≤ z := by rw [←hz]; apply exp_nonneg; intro x _; apply Real.exp_nonneg    rw [div_le_iff (Real.exp_pos _), ←Real.exp_add]    apply le_trans (pow_le_pow_left z0 le n); clear le z0 hz z    simp only [hp, ←Real.rpow_natCast, ←Real.exp_mul]    simp only [Real.rpow_natCast, Real.exp_le_exp, mul_comm _ (n:ℝ), mul_add, mul_div, ←add_assoc,      ←mul_assoc]    simp only [add_comm _ (s*t), ←add_assoc]; simp only [neg_mul, add_right_neg, zero_add]    simp only [add_comm (_ / _)]; apply add_le_add_right; rfl  apply le_trans (h (4*t/n) (by positivity)); simp only [Real.exp_le_exp]; apply le_of_eq  simp only [Nat.cast_ofNat, Nat.cast_pow, neg_mul, div_pow, mul_pow, ←mul_assoc, mul_div, pow_two,    div_eq_mul_inv, mul_inv, Nat.cast_mul, mul_pow, pow_two]  ring_nf  rw [pow_two (n:ℝ)⁻¹, ←mul_assoc, mul_assoc _ (n:ℝ), mul_inv_cancel (Nat.cast_ne_zero.mpr nz),    mul_one]  ring