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

dist_diff_bound_1

PFR.ImprovedPFR · PFR/ImprovedPFR.lean:468 to 557

Mathematical statement

Exact Lean statement

lemma dist_diff_bound_1 :
      (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₁])
    ≤ (16 * k + 6 * d[X₁ # X₁] + 2 * d[X₂ # X₂]) / 4 + (H[X₁ + X₁'] - H[X₂ + X₂']) / 4
      + (H[X₂ | X₂ + X₂'] - H[X₁ | X₁ + X₁']) / 4

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma dist_diff_bound_1 :      (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₁])    ≤ (16 * k + 6 * d[X₁ # X₁] + 2 * d[X₂ # X₂]) / 4 + (H[X₁ + X₁'] - H[X₂ + X₂']) / 4      + (H[X₂ | X₂ + X₂'] - H[X₁ | X₁ + X₁']) / 4 := by  have I1 := gen_ineq_01 p.X₀₁ p.hmeas1 X₁ X₂ X₂' X₁' hX₁ hX₂ hX₂' hX₁' h_indep.reindex_four_abcd  have I2 := gen_ineq_00 p.X₀₁ p.hmeas1 X₁ X₂ X₁' X₂' hX₁ hX₂ hX₁' hX₂' h_indep.reindex_four_abdc  have I3 := gen_ineq_10 p.X₀₁ p.hmeas1 X₁ X₂' X₂ X₁' hX₁ hX₂' hX₂ hX₁' h_indep.reindex_four_acbd  have I4 := gen_ineq_10 p.X₀₁ p.hmeas1 X₁ X₂' X₁' X₂ hX₁ hX₂' hX₁' hX₂ h_indep.reindex_four_acdb  have I5 := gen_ineq_00 p.X₀₁ p.hmeas1 X₁ X₁' X₂ X₂' hX₁ hX₁' hX₂ hX₂' h_indep.reindex_four_adbc  have I6 := gen_ineq_01 p.X₀₁ p.hmeas1 X₁ X₁' X₂' X₂ hX₁ hX₁' hX₂' hX₂ h_indep.reindex_four_adcb  have C1 : U + X₂' + X₁' = S := by abel  have C2 : W + X₂ + X₂' = S := by abel  have C3 : X₁ + X₂' + X₂ + X₁' = S := by abel  have C4 : X₁ + X₂' + X₁' + X₂ = S := by abel  have C5 : W + X₂' + X₂ = S := by abel  have C7 : X₂ + X₁' = V := by abel  have C8 : X₁ + X₁' = W := by abel  have C9 : d[X₁ # X₂'] = d[X₁ # X₂] := h₂.symm.rdist_congr_right hX₁.aemeasurable  have C10 : d[X₂ # X₁'] = d[X₁' # X₂] := rdist_symm  have C11 : d[X₁ # X₁'] = d[X₁ # X₁] := h₁.symm.rdist_congr_right hX₁.aemeasurable  have C12 : d[X₁' # X₂'] = d[X₁ # X₂] := h₁.symm.rdist_congr h₂.symm  have C13 : d[X₂ # X₂'] = d[X₂ # X₂] := h₂.symm.rdist_congr_right hX₂.aemeasurable  have C14 : d[X₁' # X₂] = d[X₁ # X₂] := h₁.symm.rdist_congr_left hX₂.aemeasurable  have C15 : H[X₁' + X₂'] = H[U] := by    apply ProbabilityTheory.IdentDistrib.entropy_congr    have I : IdentDistrib (⟨X₁, X₂⟩) (⟨X₁', X₂'⟩) := h₁.prodMk h₂ (h_indep.indepFun zero_ne_one)        (h_indep.indepFun (show 3 ≠ 2 by decide))    exact I.symm.comp measurable_add  have C16 : H[X₂'] = H[X₂] := h₂.symm.entropy_congr  have C17 : H[X₁'] = H[X₁] := h₁.symm.entropy_congr  have C18 : d[X₂' # X₁'] = d[X₁' # X₂'] := rdist_symm  have C19 : H[X₂' + X₁'] = H[U] := by rw [add_comm]; exact C15  have C20 : d[X₂' # X₂] = d[X₂ # X₂] := h₂.symm.rdist_congr_left hX₂.aemeasurable  have C21 : H[V] = H[U] := by    apply ProbabilityTheory.IdentDistrib.entropy_congr    have I : IdentDistrib (⟨X₁', X₂⟩) (⟨X₁, X₂⟩) := by      apply h₁.symm.prodMk (.refl hX₂.aemeasurable)        (h_indep.indepFun (show 3 ≠ 1 by decide)) (h_indep.indepFun zero_ne_one)    exact I.comp measurable_add  have C22 : H[X₁ + X₂'] = H[X₁ + X₂] := by    apply ProbabilityTheory.IdentDistrib.entropy_congr    have I : IdentDistrib (⟨X₁, X₂'⟩) (⟨X₁, X₂⟩) := by      apply (IdentDistrib.refl hX₁.aemeasurable).prodMk h₂.symm        (h_indep.indepFun (show 0 ≠ 2 by decide)) (h_indep.indepFun zero_ne_one)    exact I.comp measurable_add  have C23 : X₂' + X₂ = X₂ + X₂' := by abel  have C24 : H[X₁ | X₁ + X₂'] = H[X₁ | X₁ + X₂] := by    apply IdentDistrib.condEntropy_eq hX₁ (hX₁.add hX₂') hX₁ (hX₁.add hX₂)    have I : IdentDistrib (⟨X₁, X₂'⟩) (⟨X₁, X₂⟩) := by      exact (IdentDistrib.refl hX₁.aemeasurable).prodMk h₂.symm        (h_indep.indepFun (show 0 ≠ 2 by decide)) (h_indep.indepFun zero_ne_one)    exact I.comp (measurable_fst.prodMk measurable_add)  have C25 : H[X₂ | V] = H[X₂ | X₁ + X₂] := by    apply IdentDistrib.condEntropy_eq hX₂ (hX₁'.add hX₂) hX₂ (hX₁.add hX₂)    have I : IdentDistrib (⟨X₁', X₂⟩) (⟨X₁, X₂⟩) := by      exact h₁.symm.prodMk (IdentDistrib.refl hX₂.aemeasurable)        (h_indep.indepFun (show 3 ≠ 1 by decide)) (h_indep.indepFun zero_ne_one)    exact I.comp (measurable_snd.prodMk measurable_add)  have C26 : H[X₂' | X₂' + X₁'] = H[X₂ | X₁ + X₂] := by    rw [add_comm]    apply IdentDistrib.condEntropy_eq hX₂' (hX₁'.add hX₂') hX₂ (hX₁.add hX₂)    have I : IdentDistrib (⟨X₁', X₂'⟩) (⟨X₁, X₂⟩) := h₁.symm.prodMk h₂.symm        (h_indep.indepFun (show 3 ≠ 2 by decide)) (h_indep.indepFun zero_ne_one)    exact I.comp (measurable_snd.prodMk measurable_add)  have C27 : H[X₂' | X₂ + X₂'] = H[X₂ | X₂ + X₂'] := by    conv_lhs => rw [add_comm]    apply IdentDistrib.condEntropy_eq hX₂' (hX₂'.add hX₂) hX₂ (hX₂.add hX₂')    have I : IdentDistrib (⟨X₂', X₂⟩) (⟨X₂, X₂'⟩) := h₂.symm.prodMk h₂        (h_indep.indepFun (show 2 ≠ 1 by decide)) (h_indep.indepFun (show 1 ≠ 2 by decide))    exact I.comp (measurable_fst.prodMk measurable_add)  have C28 : H[X₁' | X₁' + X₂'] = H[X₁ | X₁ + X₂] := by    apply IdentDistrib.condEntropy_eq hX₁' (hX₁'.add hX₂') hX₁ (hX₁.add hX₂)    have I : IdentDistrib (⟨X₁', X₂'⟩) (⟨X₁, X₂⟩) := h₁.symm.prodMk h₂.symm        (h_indep.indepFun (show 3 ≠ 2 by decide)) (h_indep.indepFun zero_ne_one)    exact I.comp (measurable_fst.prodMk measurable_add)  have C29 : H[X₁' | V] = H[X₁ | X₁ + X₂] := by    apply IdentDistrib.condEntropy_eq hX₁' (hX₁'.add hX₂) hX₁ (hX₁.add hX₂)    have I : IdentDistrib (⟨X₁', X₂⟩) (⟨X₁, X₂⟩) :=      h₁.symm.prodMk (IdentDistrib.refl hX₂.aemeasurable)      (h_indep.indepFun (show 3 ≠ 1 by decide)) (h_indep.indepFun zero_ne_one)    exact I.comp (measurable_fst.prodMk measurable_add)  have C30 : H[X₂ | X₁ + X₂] = H[X₁ | X₁ + X₂] := by    have := condEntropy_of_injective ℙ hX₁ (hX₁.add hX₂) _ (fun p ↦ add_right_injective p)    convert! this with ω    simp [add_comm (X₁ ω), add_assoc (X₂ ω), ZModModule.add_self]  simp only [C1, C2, C3, C4, C5, C7, C8, C9, C10, C11, C12, C13, C14, C15, C16, C17, C18, C19,    C20, C21, C22, C23, C24, C25, C26, C27, C28, C29, C30] at I1 I2 I3 I4 I5 I6 ⊢  linarith only [I1, I2, I3, I4, I5, I6]