logMap_mul — Mathlib

English

logMap(xy) = logMap(x) + logMap(y) when both x and y have nonzero mixed embeddings.

Русский

logMap(xy) = logMap(x) + logMap(y) при условии, что и x, и y имеют ненулевые смешанные вложения.

LaTeX

$$$\logMap(xy) = \logMap(x) + \logMap(y)$ if $\|x\|,\|y\| \neq 0$$$

Lean4

theorem logMap_mul (hx : mixedEmbedding.norm x ≠ 0) (hy : mixedEmbedding.norm y ≠ 0) :
    logMap (x * y) = logMap x + logMap y := by
  ext w
  simp_rw [Pi.add_apply, logMap_apply]
  rw [map_mul, map_mul, Real.log_mul, Real.log_mul hx hy, add_mul]
  · ring
  · exact mixedEmbedding.norm_ne_zero_iff.mp hx w
  · exact mixedEmbedding.norm_ne_zero_iff.mp hy w

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