structure Janson.JansonSetup : Type

A Janson setup consists of $N$ independent Bernoulli variables with success probabilities prob i ∈ [0,1] and a family of $k$ "bad events" indexed by subsets $S_i \subseteq \{0,\dots,N-1\}$, where event $i$ occurs iff every coordinate in $S_i$ is present in the random subset.

• N : ℕ
• k : ℕ
• prob : Fin self.N → ℝ
• S : Fin self.k → Finset (Fin self.N)
• prob_nonneg (i : Fin self.N) : 0 ≤ self.prob i
• prob_le_one (i : Fin self.N) : self.prob i ≤ 1

def Janson.JansonSetup.probEvent (J : JansonSetup) (i : Fin J.k) : ℝ

Probability that the $i$-th bad event $A_i$ occurs, i.e. $\mathbb{P}(A_i) = \prod_{j \in S_i} p_j$.

def Janson.JansonSetup.mu (J : JansonSetup) : ℝ

The expected number of bad events, $\mu = \sum_{i=1}^{k} \mathbb{P}(A_i)$.

def Janson.JansonSetup.dep (J : JansonSetup) (i j : Fin J.k) : Prop

Dependency relation between bad events: events $A_i$ and $A_j$ are dependent iff $i \ne j$ and $S_i \cap S_j \ne \emptyset$.

@[implicit_reducible]

instance Janson.instDecidableDep (J : JansonSetup) (i j : Fin J.k) : Decidable (J.dep i j)

Decidability of the dependency relation.

def Janson.JansonSetup.probJoint (J : JansonSetup) (i j : Fin J.k) : ℝ

Joint probability $\mathbb{P}(A_i \cap A_j) = \prod_{l \in S_i \cup S_j} p_l$.

def Janson.JansonSetup.delta (J : JansonSetup) : ℝ

The dependency parameter $\Delta = \sum_{i \sim j} \mathbb{P}(A_i \cap A_j)$, summed over ordered dependent pairs $(i,j)$.

def Janson.JansonSetup.probNone (J : JansonSetup) : ℝ

Probability that none of the bad events occur, i.e. $\mathbb{P}(\bigcap_i \overline{A_i})$, expressed as a sum over the random subset $T$ of coordinates that are present.

def Janson.JansonSetup.probSubset (J : JansonSetup) (T : Finset (Fin J.N)) : ℝ

Probability that the random subset of present coordinates equals exactly $T$.

def Janson.JansonSetup.countEvents (J : JansonSetup) (T : Finset (Fin J.N)) : ℕ

Given a subset $T$ of present coordinates, counts the number of bad events $A_i$ that occur, i.e. the number of indices $i$ with $S_i \subseteq T$.

noncomputable def Janson.JansonSetup.probLowerTail (J : JansonSetup) (t : ℝ) : ℝ

Lower-tail probability $\mathbb{P}(X \le \mu - t)$ where $X = \sum_i \mathbf{1}_{A_i}$ counts how many bad events occur.

theorem Janson.janson_chain_rule_harris (J : JansonSetup) : ∃ (r : Fin J.k → ℝ), (∀ (i : Fin J.k), r i ≤ 1) ∧ J.probNone = ∏ i : Fin J.k, (1 - r i) ∧ ∑ i : Fin J.k, r i ≥ J.mu - J.delta / 2

Chain-rule lemma underpinning Janson's inequality: there exist factors $r_i \le 1$ such that $\mathbb{P}(\text{no bad event}) = \prod_i (1 - r_i)$ and $\sum_i r_i \ge \mu - \Delta/2$. This is the Harris-style decomposition used in the proof of Theorem 8.1.2.

theorem Janson.janson_inequality_I (J : JansonSetup) : J.probNone ≤ Real.exp (-J.mu + J.delta / 2)

Theorem 8.1.2 (Janson I). For a Janson setup with $k$ bad events, $$ \mathbb{P}(X = 0) \le \exp(-\mu + \Delta/2), $$ where $X$ counts the bad events that occur, $\mu = \mathbb{E}[X]$, and $\Delta$ is the total dependency parameter.

def Janson.mu_triangles (n : ℕ) (p : ℝ) : ℝ

Expected number of triangles in $G(n,p)$: $\mu = \binom{n}{3} p^3$.

def Janson.delta_triangles (n : ℕ) (p : ℝ) : ℝ

Janson dependency parameter for triangles in $G(n,p)$: counts ordered pairs of triangles sharing an edge, weighted by the joint probability $p^5$.

theorem Janson.triangle_free_delta_over_mu_tendsto (p : ℕ → ℝ) (hp_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < p n) (hp_small : Filter.Tendsto (fun (n : ℕ) => p n * √↑n) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => delta_triangles n (p n) / mu_triangles n (p n)) Filter.atTop (nhds 0)

Auxiliary asymptotic estimate: if $p(n) \sqrt{n} \to 0$ then $\Delta_{\triangle}(n, p(n)) / \mu_{\triangle}(n, p(n)) \to 0$.

theorem Janson.choose_three_cast (n : ℕ) (hn : 3 ≤ n) : ↑(n.choose 3) = ↑n * (↑n - 1) * (↑n - 2) / 6

Closed-form for $\binom{n}{3}$ cast to $\mathbb{R}$: $\binom{n}{3} = n(n-1)(n-2)/6$.

theorem Janson.const_div_n_mul_sqrt_tendsto (c : ℝ) : Filter.Tendsto (fun (n : ℕ) => c / ↑n * √↑n) Filter.atTop (nhds 0)

Auxiliary limit: $(c/n) \sqrt{n} = c/\sqrt{n} \to 0$ as $n \to \infty$.

theorem Janson.mu_triangles_tendsto (c : ℝ) (hc : 0 < c) : Filter.Tendsto (fun (n : ℕ) => mu_triangles n (c / ↑n)) Filter.atTop (nhds (c ^ 3 / 6))

Asymptotic limit: $\mu_{\triangle}(n, c/n) = \binom{n}{3}(c/n)^3 \to c^3/6$.

theorem Janson.cor_triangle_free_delta_over_mu (c : ℝ) (hc : 0 < c) : Filter.Tendsto (fun (n : ℕ) => delta_triangles n (c / ↑n) / mu_triangles n (c / ↑n)) Filter.atTop (nhds 0)

Specialization of triangle_free_delta_over_mu_tendsto to $p = c/n$: $\Delta_{\triangle}(n, c/n) / \mu_{\triangle}(n, c/n) \to 0$.

theorem Janson.delta_triangles_tendsto_zero (c : ℝ) (hc : 0 < c) : Filter.Tendsto (fun (n : ℕ) => delta_triangles n (c / ↑n)) Filter.atTop (nhds 0)

Auxiliary limit: $\Delta_{\triangle}(n, c/n) \to 0$ as $n \to \infty$.

theorem Janson.corollary_8_1_7 (c : ℝ) (hc : 0 < c) (prob_tf : ℕ → ℝ) (hprob_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < prob_tf n) (_hprob_le : ∀ᶠ (n : ℕ) in Filter.atTop, prob_tf n ≤ 1) (h_upper : ∀ᶠ (n : ℕ) in Filter.atTop, prob_tf n ≤ Real.exp (-mu_triangles n (c / ↑n) + delta_triangles n (c / ↑n) / 2)) (h_lower : ∀ᶠ (n : ℕ) in Filter.atTop, Real.exp (-mu_triangles n (c / ↑n)) ≤ prob_tf n) : Filter.Tendsto (fun (n : ℕ) => -Real.log (prob_tf n)) Filter.atTop (nhds (c ^ 3 / 6))

Corollary 8.1.7. Abstract form: if a probability sequence is sandwiched between $\exp(-\mu_n)$ and $\exp(-\mu_n + \Delta_n/2)$ for the triangle counts in $G(n, c/n)$, then $-\log(\text{prob}_n) \to c^3/6$.

noncomputable def Janson.triangleFreeProb (n : ℕ) (p : ↑unitInterval) : ℝ

Probability that $G(n,p)$ is triangle-free, computed under the binomial random graph measure on $\mathrm{Fin}\, n$.

noncomputable def Janson.triangleFreeProb_cn (c : ℝ) (n : ℕ) : ℝ

Triangle-free probability at edge density $p = c/n$, returning $0$ if $c/n$ falls outside the unit interval.

theorem Janson.janson_upper_bound_triangles (c : ℝ) (hc : 0 < c) : ∀ᶠ (n : ℕ) in Filter.atTop, triangleFreeProb_cn c n ≤ Real.exp (-mu_triangles n (c / ↑n) + delta_triangles n (c / ↑n) / 2)

Janson upper bound applied to triangles in $G(n, c/n)$: $\mathbb{P}(G \text{ triangle-free}) \le \exp(-\mu + \Delta/2)$.

theorem Janson.harris_lower_bound_triangles (c : ℝ) (hc : 0 < c) : ∀ᶠ (n : ℕ) in Filter.atTop, Real.exp (-mu_triangles n (c / ↑n)) ≤ triangleFreeProb_cn c n

Harris-type lower bound: $\exp(-\mu) \le \mathbb{P}(G(n, c/n) \text{ triangle-free})$.

theorem Janson.triangleFreeProb_cn_pos (c : ℝ) (hc : 0 < c) : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < triangleFreeProb_cn c n

For large $n$, the triangle-free probability is strictly positive.

theorem Janson.triangleFreeProb_cn_le_one (c : ℝ) (hc : 0 < c) : ∀ᶠ (n : ℕ) in Filter.atTop, triangleFreeProb_cn c n ≤ 1

For large $n$, the triangle-free probability is bounded above by $1$.

theorem Janson.corollary_8_1_7_concrete (c : ℝ) (hc : 0 < c) : Filter.Tendsto (fun (n : ℕ) => -Real.log (triangleFreeProb_cn c n)) Filter.atTop (nhds (c ^ 3 / 6))

Concrete instance of Corollary 8.1.7 (Janson) for triangles in $G(n, c/n)$: $$ -\log \mathbb{P}(G(n,c/n) \text{ triangle-free}) \to \frac{c^3}{6}. $$

theorem JansonInequalities.janson_inequality_II {μ Δ v : ℝ} (hμ_pos : 0 < μ) (hΔ_ge_μ : Δ ≥ μ) (hbound : ∀ (q : ℝ), 0 ≤ q → q ≤ 1 → v ≤ Real.exp (-q * μ + q ^ 2 * Δ / 2)) : v ≤ Real.exp (-μ ^ 2 / (2 * Δ))

Theorem 8.1.6/8.1.7/8.1.8 (Janson II). Optimization of the parametric Janson bound: if for every $q \in [0,1]$ we have $v \le \exp(-q\mu + q^2 \Delta / 2)$, then $v \le \exp(-\mu^2 / (2\Delta))$, by choosing $q = \mu/\Delta$.

theorem JansonInequalities.mu_sq_over_delta_isTheta (μ Δ p : ℕ → ℝ) (hμ_theta : μ =Θ[Filter.atTop] fun (n : ℕ) => ↑n ^ 3 * p n ^ 3) (hΔ_theta : Δ =Θ[Filter.atTop] fun (n : ℕ) => ↑n ^ 4 * p n ^ 5) (hp_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < p n) (hn_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < ↑n) (hΔ_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < Δ n) : (fun (n : ℕ) => μ n ^ 2 / (2 * Δ n)) =Θ[Filter.atTop] fun (n : ℕ) => ↑n ^ 2 * p n

Asymptotic identity: if $\mu \asymp n^3 p^3$ and $\Delta \asymp n^4 p^5$, then $\mu^2 / (2\Delta) \asymp n^2 p$, the natural Janson II exponent for triangles.

structure JansonInequalities.TriangleFreeGnpData (p : ℕ → ℝ) : Type

Bundle of asymptotic data for triangles in $G(n, p(n))$: triangle-free probability, Janson parameters $\mu$ and $\Delta$ with their correct asymptotic order.

• prob_tf : ℕ → ℝ
• μ : ℕ → ℝ
• Δ : ℕ → ℝ
• prob_tf_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < self.prob_tf n
• prob_tf_le_one : ∀ᶠ (n : ℕ) in Filter.atTop, self.prob_tf n ≤ 1
• μ_isTheta : self.μ =Θ[Filter.atTop] fun (n : ℕ) => ↑n ^ 3 * p n ^ 3
• Δ_isTheta : self.Δ =Θ[Filter.atTop] fun (n : ℕ) => ↑n ^ 4 * p n ^ 5
• Δ_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < self.Δ n

theorem JansonInequalities.isTheta_natCast_sub_const (k : ℕ) : (fun (n : ℕ) => ↑n - ↑k) =Θ[Filter.atTop] fun (n : ℕ) => ↑n

For any fixed $k \in \mathbb{N}$, $(n - k) \asymp n$ as $n \to \infty$.

def JansonInequalities.triangleFreeGnpData_exists (p : ℕ → ℝ) (hp_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < p n) (hp_le : ∀ᶠ (n : ℕ) in Filter.atTop, p n ≤ 0.99) : TriangleFreeGnpData p

Constructs a TriangleFreeGnpData bundle for a probability sequence $p(n)$ that is eventually positive and bounded away from $1$. The triangle-free probability used is the naive empty-graph bound $(1-p)^{\binom{n}{2}}$ for the lower bound.

theorem JansonInequalities.janson_II_triangle_upper_gnp (p : ℕ → ℝ) (hp_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < p n) (hp_le : ∀ᶠ (n : ℕ) in Filter.atTop, p n ≤ 0.99) : have data := triangleFreeGnpData_exists p hp_pos hp_le; ∀ᶠ (n : ℕ) in Filter.atTop, data.prob_tf n ≤ Real.exp (-data.μ n ^ 2 / (2 * data.Δ n))

Janson II applied to triangles in $G(n, p(n))$ via the bundle from triangleFreeGnpData_exists: $\mathbb{P}(G \text{ triangle-free}) \le \exp(-\mu^2 / (2\Delta))$.

theorem JansonInequalities.triangle_free_empty_graph_bound_gnp (p : ℕ → ℝ) (hp_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < p n) (hp_le : ∀ᶠ (n : ℕ) in Filter.atTop, p n ≤ 0.99) : have data := triangleFreeGnpData_exists p hp_pos hp_le; ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, -Real.log (data.prob_tf n) ≤ C * (↑n ^ 2 * p n)

"Empty-graph" upper bound: the triangle-free probability is at least the probability of no edges, giving $-\log \mathbb{P}(G \text{ triangle-free}) \le C \cdot n^2 p$.

theorem JansonInequalities.janson_I_triangle_bounds_gnp (p : ℕ → ℝ) (hp_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < p n) (hp_le : ∀ᶠ (n : ℕ) in Filter.atTop, p n ≤ 0.99) (hregime : p =O[Filter.atTop] fun (n : ℕ) => ↑n ^ (-1 / 2)) : have data := triangleFreeGnpData_exists p hp_pos hp_le; (∀ᶠ (n : ℕ) in Filter.atTop, 0 < data.μ n) ∧ (∀ᶠ (n : ℕ) in Filter.atTop, data.μ n / 2 ≤ -Real.log (data.prob_tf n)) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, -Real.log (data.prob_tf n) ≤ 2 * data.μ n

Janson I two-sided bounds in the sparse regime $p \lesssim n^{-1/2}$: in this regime $\mu / 2 \le -\log \mathbb{P}(G \text{ triangle-free}) \le 2 \mu$.

theorem JansonInequalities.triangle_free_prob_high_p (p : ℕ → ℝ) (hp_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < p n) (hp_le : ∀ᶠ (n : ℕ) in Filter.atTop, p n ≤ 0.99) (_hregime : (fun (n : ℕ) => ↑n ^ (-1 / 2)) =O[Filter.atTop] p) : have data := triangleFreeGnpData_exists p hp_pos hp_le; (fun (n : ℕ) => -Real.log (data.prob_tf n)) =Θ[Filter.atTop] fun (n : ℕ) => ↑n ^ 2 * p n

In the dense regime $p \gtrsim n^{-1/2}$, the negative-log triangle-free probability satisfies $-\log \mathbb{P}(G \text{ triangle-free}) =\Theta(n^2 p)$.

theorem JansonInequalities.triangle_free_prob_low_p (p : ℕ → ℝ) (hp_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < p n) (hp_le : ∀ᶠ (n : ℕ) in Filter.atTop, p n ≤ 0.99) (hregime : p =O[Filter.atTop] fun (n : ℕ) => ↑n ^ (-1 / 2)) : have data := triangleFreeGnpData_exists p hp_pos hp_le; (fun (n : ℕ) => -Real.log (data.prob_tf n)) =Θ[Filter.atTop] fun (n : ℕ) => ↑n ^ 3 * p n ^ 3

In the sparse regime $p \lesssim n^{-1/2}$, the negative-log triangle-free probability satisfies $-\log \mathbb{P}(G \text{ triangle-free}) =\Theta(n^3 p^3)$, i.e. it is of the order of the expected number of triangles.

theorem JansonInequalities.triangle_free_prob_theta (p : ℕ → ℝ) (hp_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < p n) (hp_le : ∀ᶠ (n : ℕ) in Filter.atTop, p n ≤ 0.99) (hregime_high : (fun (n : ℕ) => ↑n ^ (-1 / 2)) =O[Filter.atTop] p) (hregime_low : p =O[Filter.atTop] fun (n : ℕ) => ↑n ^ (-1 / 2)) : have data := triangleFreeGnpData_exists p hp_pos hp_le; ((fun (n : ℕ) => -Real.log (data.prob_tf n)) =Θ[Filter.atTop] fun (n : ℕ) => ↑n ^ 2 * p n) ∧ (fun (n : ℕ) => -Real.log (data.prob_tf n)) =Θ[Filter.atTop] fun (n : ℕ) => ↑n ^ 3 * p n ^ 3

At the critical scale $p \asymp n^{-1/2}$, both the dense and sparse asymptotics for the negative log triangle-free probability hold simultaneously.

theorem Janson.janson_parametric_bound (J : JansonSetup) (q : ℝ) : 0 ≤ q → q ≤ 1 → J.probNone ≤ Real.exp (-q * J.mu + q ^ 2 * J.delta / 2)

Parametric form of Janson's inequality (Theorem 8.1.10): for every $q \in [0,1]$, $$ \mathbb{P}(X = 0) \le \exp(-q\mu + q^2 \Delta / 2). $$

theorem Janson.janson_inequality_II_full (J : JansonSetup) (hμ_pos : 0 < J.mu) (hΔ_ge_μ : J.delta ≥ J.mu) : J.probNone ≤ Real.exp (-J.mu ^ 2 / (2 * J.delta))

Full form of Janson II (Theorem 8.1.7/8.1.8) for a JansonSetup: assuming $\Delta \ge \mu > 0$, $$ \mathbb{P}(X = 0) \le \exp(-\mu^2 / (2\Delta)). $$