Commit 2023-03-24 18:51 2077901a

View on Github →

feat: port InformationTheory.Hamming (#2891)

Estimated changes

Modified Mathlib.lean

Created Mathlib/InformationTheory/Hamming.lean

added theorem Hamming.dist_eq_hammingDist

added theorem Hamming.nndist_eq_hammingDist

added theorem Hamming.nnnorm_eq_hammingNorm

added theorem Hamming.norm_eq_hammingNorm

added def Hamming.ofHamming

added theorem Hamming.ofHamming_add

added theorem Hamming.ofHamming_inj

added theorem Hamming.ofHamming_neg

added theorem Hamming.ofHamming_smul

added theorem Hamming.ofHamming_sub

added theorem Hamming.ofHamming_symm_eq

added theorem Hamming.ofHamming_toHamming

added theorem Hamming.ofHamming_zero

added def Hamming.toHamming

added theorem Hamming.toHamming_add

added theorem Hamming.toHamming_inj

added theorem Hamming.toHamming_neg

added theorem Hamming.toHamming_ofHamming

added theorem Hamming.toHamming_smul

added theorem Hamming.toHamming_sub

added theorem Hamming.toHamming_symm_eq

added theorem Hamming.toHamming_zero

added def Hamming

added theorem eq_of_hammingDist_eq_zero

added def hammingDist

added theorem hammingDist_comm

added theorem hammingDist_comp

added theorem hammingDist_comp_le_hammingDist

added theorem hammingDist_eq_hammingNorm

added theorem hammingDist_eq_zero

added theorem hammingDist_le_card_fintype

added theorem hammingDist_lt_one

added theorem hammingDist_ne_zero

added theorem hammingDist_nonneg

added theorem hammingDist_pos

added theorem hammingDist_self

added theorem hammingDist_smul

added theorem hammingDist_smul_le_hammingDist

added theorem hammingDist_triangle

added theorem hammingDist_triangle_left

added theorem hammingDist_triangle_right

added theorem hammingDist_zero_left

added theorem hammingDist_zero_right

added def hammingNorm

added theorem hammingNorm_comp

added theorem hammingNorm_comp_le_hammingNorm

added theorem hammingNorm_eq_zero

added theorem hammingNorm_le_card_fintype

added theorem hammingNorm_lt_one

added theorem hammingNorm_ne_zero_iff

added theorem hammingNorm_nonneg

added theorem hammingNorm_pos_iff

added theorem hammingNorm_smul

added theorem hammingNorm_smul_le_hammingNorm

added theorem hammingNorm_zero

added theorem hamming_zero_eq_dist

added theorem swap_hammingDist