Theorems · Theorem · real analysis

Complex.integral_comp_pi_polarCoord_symm

∀ {ι : Type u_1} [inst : Fintype ι] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  (f : (ι → ℂ) → E),
  (∫ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => Complex.polarCoord.target,
      (∏ i, (p i).1) • f fun i => ↑Complex.polarCoord.symm (p i)) =
    ∫ (p : ι → ℂ), f p

Defined in

Mathlib.Analysis.SpecialFunctions.PolarCoord

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeNormedAddCommGroupNormedSpace