Skip to main content
therefore
Sign inSign up
Open navigation
teorth/PFR
Source indexedlemma · leanprover/lean4:v4.33.0-rc1

rdist_add_rdist_add_condMutual_eq

PFR.FirstEstimate · PFR/FirstEstimate.lean:59 to 76

Source documentation

The sum of d[X1+X~2;X2+X~1]+d[X1∣X1+X~2;X2∣X2+X~1]d[X_1+\tilde X_2;X_2+\tilde X_1] + d[X_1|X_1+\tilde X_2; X_2|X_2+\tilde X_1] and I[X1+X2:X~1+X2 ∣ X1+X2+X~1+X~2]I[X_1+ X_2 : \tilde X_1 + X_2 \,|\, X_1 + X_2 + \tilde X_1 + \tilde X_2] is equal to 2k2k.

Exact Lean statement

lemma rdist_add_rdist_add_condMutual_eq [Module (ZMod 2) G] :
    d[X₁ + X₂' # X₂ + X₁'] + d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁']
      + I[X₁ + X₂ : X₁' + X₂ | X₁ + X₂ + X₁' + X₂'] = 2 * k

Complete declaration

Lean source

Canonical source
Full Lean sourceLean 4
lemma rdist_add_rdist_add_condMutual_eq [Module (ZMod 2) G] :    d[X₁ + X₂' # X₂ + X₁'] + d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁']      + I[X₁ + X₂ : X₁' + X₂ | X₁ + X₂ + X₁' + X₂'] = 2 * k := by  cases nonempty_fintype G  have h0 : ![X₁, X₂, X₂', X₁'] 0 = X₁ := rfl  have h1 : ![X₁, X₂, X₂', X₁'] 1 = X₂ := rfl  have h2 : ![X₁, X₂, X₂', X₁'] 2 = X₂' := rfl  have h3 : ![X₁, X₂, X₂', X₁'] 3 = X₁' := rfl  have h := sum_of_rdist_eq_char_2 ![X₁, X₂, X₂', X₁'] h_indep    (fun i => by fin_cases i <;> assumption)  rw [h0, h1, h2, h3] at h  have heq : d[X₂' # X₁'] = k := by    rw [rdist_symm]    apply h₁.symm.rdist_congr h₂.symm  rw [heq] at h  convert h.symm using 1  · congr 2 <;> abel  · ring