measurable_polarSpaceCoord_symm — Mathlib

English

An integral identity holds for the polarSpaceCoord_symm transformation of f.

Русский

Справедливость интегрального тождества для преобразования polarSpaceCoord_symm применительно к f.

LaTeX

$$$\\int_{(polarSpaceCoord(K)).target} \\Big(\\prod_{w:\\{ w\\mid IsComplex w\\}} x.fst w.1\\Big) \\cdot f((polarSpaceCoord(K)).symm x) \\, dx = \\int_x f(x) \\, dx$$$

Lean4

theorem measurable_polarSpaceCoord_symm [NumberField K] : Measurable (polarSpaceCoord K).symm :=
  by
  rw [polarSpaceCoord, OpenPartialHomeomorph.transHomeomorph_symm_apply]
  exact (measurable_polarCoord_symm K).comp (Homeomorph.measurable _)

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