hammingNorm_comp_le_hammingNorm — Mathlib

English

If f_i: γ_i → β_i with f_i(0) = 0, then the Hamming norm of the composed vector is bounded by that of the original: hammingNorm(i ↦ f_i(x_i)) ≤ hammingNorm(x).

Русский

При композиции координат через f_i(0)=0 норма Хэмминга не увеличивается: hammingNorm(i ↦ f_i(x_i)) ≤ hammingNorm(x).

LaTeX

$$$\mathrm{hammingNorm}(i \mapsto f(i, x_i)) \le \mathrm{hammingNorm}(x)$$$

Lean4

theorem hammingNorm_comp_le_hammingNorm (f : ∀ i, γ i → β i) {x : ∀ i, γ i} (hf : ∀ i, f i 0 = 0) :
    (hammingNorm fun i => f i (x i)) ≤ hammingNorm x := by
  simpa only [← hammingDist_zero_right, hf] using hammingDist_comp_le_hammingDist f (y := fun _ ↦ 0)

Похожие утверждения