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

averaged_construct_good

PFR.ImprovedPFR · PFR/ImprovedPFR.lean:430 to 462

Source documentation

$k$ is at most

\sum_{i=1}^2 \sum_{A,B \in \{U,V,W\}: A \neq B} (d[X^0_i;A|B,S] - d[X^0_i; X_i]).$$

Exact Lean statement

lemma averaged_construct_good :
    k ≤ (I[U : V | S] + I[V : W | S] + I[W : U | S]) + p.η / 6 *
      (((d[p.X₀₁ # U | ⟨V, S⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # U | ⟨W, S⟩] - d[p.X₀₁ # X₁])
      + (d[p.X₀₁ # V | ⟨U, S⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # V | ⟨W, S⟩] - d[p.X₀₁ # X₁])
      + (d[p.X₀₁ # W | ⟨U, S⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # W | ⟨V, S⟩] - d[p.X₀₁ # X₁]))
      + ((d[p.X₀₂ # U | ⟨V, S⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # U | ⟨W, S⟩] - d[p.X₀₂ # X₂])
      + (d[p.X₀₂ # V | ⟨U, S⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # V | ⟨W, S⟩] - d[p.X₀₂ # X₂])
      + (d[p.X₀₂ # W | ⟨U, S⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # W | ⟨V, S⟩] - d[p.X₀₂ # X₂])))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma averaged_construct_good :    k ≤ (I[U : V | S] + I[V : W | S] + I[W : U | S]) + p.η / 6 *      (((d[p.X₀₁ # U | ⟨V, S⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # U | ⟨W, S⟩] - d[p.X₀₁ # X₁])      + (d[p.X₀₁ # V | ⟨U, S⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # V | ⟨W, S⟩] - d[p.X₀₁ # X₁])      + (d[p.X₀₁ # W | ⟨U, S⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # W | ⟨V, S⟩] - d[p.X₀₁ # X₁]))      + ((d[p.X₀₂ # U | ⟨V, S⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # U | ⟨W, S⟩] - d[p.X₀₂ # X₂])      + (d[p.X₀₂ # V | ⟨U, S⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # V | ⟨W, S⟩] - d[p.X₀₂ # X₂])      + (d[p.X₀₂ # W | ⟨U, S⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # W | ⟨V, S⟩] - d[p.X₀₂ # X₂])))    := by  cases nonempty_fintype G  have hS : Measurable S := by fun_prop  have hU : Measurable U := by fun_prop  have hV : Measurable V := by fun_prop  have hW : Measurable W := by fun_prop  have hUVW : U + V + W = 0 := sum_uvw_eq_zero X₁ X₂ X₁'  have hz (a : ℝ) : a = ∑ z, (Measure.real ℙ (S ⁻¹' {z})) * a := by    rw [← Finset.sum_mul, sum_measureReal_preimage_singleton]    · simp only [Finset.coe_univ, Set.preimage_univ, probReal_univ, one_mul]    · intro y hy      apply hS      exact measurableSet_singleton y  rw [hz k, hz (d[p.X₀₁ # X₁]), hz (d[p.X₀₂ # X₂])]  simp only [condMutualInfo_eq_sum' hS, ← Finset.sum_add_distrib, ← mul_add,    condRuzsaDist'_prod_eq_sum', hU, hS, hV, hW, ← Finset.sum_sub_distrib, ← mul_sub,      mul_comm (p.η/6)]  rw [Finset.sum_mul, ← Finset.sum_add_distrib]  apply Finset.sum_le_sum (fun i _hi ↦ ?_)  rcases eq_or_ne (Measure.real ℙ (S ⁻¹' {i})) 0 with h'i|h'i  · simp [h'i]  rw [mul_assoc, ← mul_add]  gcongr  have : IsProbabilityMeasure (ℙ[|S ⁻¹' {i}]) := cond_isProbabilityMeasure_of_real h'i  linarith [construct_good_improved'' h_min (ℙ[|S ⁻¹' {i}]) hUVW hU hV hW]