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

rdist_add_rdist_eq

PFR.RhoFunctional · PFR/RhoFunctional.lean:1388 to 1395

Source documentation

$d[X_1;X_1]+d[X_2;X_2]= 2d[X_1;X_2]+(I_2-I_1)$ .

Exact Lean statement

lemma rdist_add_rdist_eq :
    d[ X₁ # X₁ ] + d[ X₂ # X₂ ] = 2 * k + (I₂ - I₁)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rdist_add_rdist_eq :    d[ X₁ # X₁ ] + d[ X₂ # X₂ ] = 2 * k + (I₂ - I₁) := by  have : d[X₁ + X₂' # X₂ + X₁'] + d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁'] + I₁ = 2 * k :=    rdist_add_rdist_add_condMutual_eq _ _ _ _ hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep.reindex_four_abdc  have : d[X₁ # X₁] + d[X₂ # X₂]      = d[X₁ + X₂' # X₂ + X₁'] + d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁'] + I₂ :=    I_two_aux h₁ h₂ h_indep hX₁ hX₂ hX₁' hX₂'  linarith