Source indexedlemma · leanprover/lean4:v4.33.0-rc1

construct_good

PFR.Endgame · PFR/Endgame.lean:417 to 424

Source documentation

If $T_1, T_2, T_3$ are $G$ -valued random variables with $T_1+T_2+T_3=0$ holds identically and

$\delta := \sum_{1 \leq i < j \leq 3} I[T_i;T_j]$

Then there exist random variables $T'_1, T'_2$ such that

$d[T'_1;T'_2] + \eta (d[X_1^0;T'_1] - d[X_1^0;X _1]) + \eta(d[X_2^0;T'_2] - d[X_2^0;X_2])$

is at most

(d[X^0_i;T_j] - d[X^0_i; X_i]) \biggr).$$

Exact Lean statement

lemma construct_good :
    k ≤ δ + (p.η/3) * (δ + c[T₁ # T₁] + c[T₂ # T₂] + c[T₃ # T₃])

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma construct_good :    k ≤ δ + (p.η/3) * (δ + c[T₁ # T₁] + c[T₂ # T₂] + c[T₃ # T₃]) := by  have v2 := construct_good_prelim p X₁ X₂ h_min (by rw [← hT]; abel) hT₁ hT₃ hT₂  have v3 := construct_good_prelim p X₁ X₂ h_min (by rw [← hT]; abel) hT₂ hT₁ hT₃  have v6 := construct_good_prelim p X₁ X₂ h_min (by rw [← hT]; abel) hT₃ hT₂ hT₁  simp only [mutualInfo, entropy_comm hT₂ hT₁, entropy_comm hT₃ hT₁, entropy_comm hT₃ hT₂]    at *  linarith

If T1,T2,T3T_1, T_2, T_3T1​,T2​,T3​ are GGG-valued random variables with T1+T2+T3=0T_1+T_2+T_3=0T1​+T2​+T3​=0 holds identically and

Lean source

If $T_1, T_2, T_3$ are $G$ -valued random variables with $T_1+T_2+T_3=0$ holds identically and