theorem Janson.JansonSetup.mu_nonneg (J : JansonSetup) : 0 ≤ J.mu

The expectation parameter $\mu = \mathbb{E}[X]$ in a Janson setup is nonnegative.

theorem Janson.JansonSetup.delta_nonneg (J : JansonSetup) : 0 ≤ J.delta

The dependency parameter $\Delta = \sum_{i \sim j} \Pr(A_i \cap A_j)$ in a Janson setup is nonnegative.

theorem Janson.JansonSetup.probSubset_nonneg (J : JansonSetup) (T : Finset (Fin J.N)) : 0 ≤ J.probSubset T

The probability of any particular subset $T \subseteq [N]$ being the realized set of indicators is nonnegative.

theorem Janson.JansonSetup.sum_probSubset_eq_one (J : JansonSetup) : ∑ T ∈ Finset.univ.powerset, J.probSubset T = 1

The product-measure probabilities J.probSubset T form a probability distribution: they sum to $1$ over all subsets $T \subseteq [N]$.

theorem JansonInequality.one_sub_exp_neg_le {l : ℝ} (_hl : 0 ≤ l) : 1 - Real.exp (-l) ≤ l

Linear upper bound: $1 - e^{-l} \leq l$.

theorem JansonInequality.one_sub_exp_neg_nonneg {l : ℝ} (hl : 0 ≤ l) : 0 ≤ 1 - Real.exp (-l)

Nonnegativity of $1 - e^{-l}$ for $l \geq 0$.

theorem JansonInequality.le_one_sub_exp_neg {l : ℝ} (hl : 0 ≤ l) : l - l ^ 2 / 2 ≤ 1 - Real.exp (-l)

Quadratic lower bound: $l - l^2/2 \leq 1 - e^{-l}$ for $l \geq 0$.

theorem JansonInequality.optimal_lambda_value {mu Delta t : ℝ} (hpos : 0 < mu + Delta) : -(t / (mu + Delta)) * t + (t / (mu + Delta)) ^ 2 * (mu + Delta) / 2 = -(t ^ 2 / (2 * (mu + Delta)))

Algebraic simplification at the optimal $\lambda_0 = t/(\mu + \Delta)$: $-\lambda_0 t + \lambda_0^2 (\mu + \Delta)/2 = -t^2/(2(\mu + \Delta))$.

theorem JansonInequality.janson_III_intermediate_bound (J : Janson.JansonSetup) (t : ℝ) (ht_nonneg : 0 ≤ t) (ht_le : t ≤ J.mu) (l : ℝ) : 0 ≤ l → J.probLowerTail t ≤ Real.exp (l * (J.mu - t)) * Real.exp (-(1 - Real.exp (-l)) * J.mu + (1 - Real.exp (-l)) ^ 2 * J.delta / 2)

Intermediate Markov/MGF-style bound used in the proof of Janson III: for every $\lambda \geq 0$, $\Pr(X \leq \mu - t) \leq e^{\lambda(\mu - t)} \exp!\big(-(1 - e^{-\lambda})\mu

• (1 - e^{-\lambda})^2 \Delta / 2\big)$.

theorem JansonInequality.janson_III_prob_le_one (J : Janson.JansonSetup) (t : ℝ) : J.probLowerTail t ≤ 1

The lower-tail probability $\Pr(X \leq \mu - t)$ is bounded above by $1$, as a probability must be.

theorem JansonInequality.janson_inequality_III (J : Janson.JansonSetup) (t : ℝ) (ht_nonneg : 0 ≤ t) (ht_le : t ≤ J.mu) : J.probLowerTail t ≤ Real.exp (-(t ^ 2 / (2 * (J.mu + J.delta))))

Janson inequality III (Theorem 8.2.2, lower tail). For any $0 \leq t \leq \mu$, $\Pr(X \leq \mu - t) \leq \exp\!\left(-\dfrac{t^2}{2(\mu + \Delta)}\right)$.