lintegral_comp_polarCoord_symm — Mathlib

English

A corresponding identity holds for the nonnegative integral with a product of real components.

Русский

Соответствующее тождество имеет место для линеграла с произведением вещественных компонент.

LaTeX

$$$\\int_{(\\mathrm{polarCoord}(K)).\\mathrm{target}} \\Big(\\prod_{w:\\{ w\\mid IsComplex w\\}} .\\ofReal (x.2 w).1\\Big) \\cdot f((\\mathrm{polarCoord}(K)).\\mathrm{symm}x) \\, dx = \\int_{x} f(x) \\, dx$$

Lean4

protected theorem lintegral_comp_polarCoord_symm (f : mixedSpace K → ℝ≥0∞) :
    ∫⁻ x in (mixedEmbedding.polarCoord K).target,
        (∏ w : { w // IsComplex w }, .ofReal (x.2 w).1) * f ((mixedEmbedding.polarCoord K).symm x) =
      ∫⁻ x, f x :=
  by
  rw [←
    (volume_preserving_mixedSpaceToRealMixedSpace_symm K).lintegral_comp_emb
      (mixedSpaceToRealMixedSpace K).symm.measurableEmbedding,
    ← lintegral_comp_polarCoordReal_symm, polarCoord_target_eq_polarCoordReal_target, polarCoord_symm_eq,
    Function.comp_def]

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