Theorems · Theorem · information theory

hammingNorm_comp_le_hammingNorm

∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {γ : ι → Type u_4}
  [inst_2 : (i : ι) → DecidableEq (γ i)] [inst_3 : (i : ι) → Zero (β i)] [inst_4 : (i : ι) → Zero (γ i)]
  (f : (i : ι) → γ i → β i) {x : (i : ι) → γ i},
  (∀ (i : ι), f i 0 = 0) → (hammingNorm fun i => f i (x i)) ≤ hammingNorm x

Defined in

Mathlib.InformationTheory.Hamming

Cited by

1 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqDecidableEqZeroZero