Theorems · Theorem · real analysis

lintegral_comp_pi_polarCoord_symm

∀ {ι : Type u_1} [inst : Fintype ι] (f : (ι → ℝ × ℝ) → ENNReal),
  (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => polarCoord.target,
      (∏ i, ENNReal.ofReal (p i).1) * f fun i => ↑polarCoord.symm (p i)) =
    ∫⁻ (p : ι → ℝ × ℝ), f p

Defined in

Mathlib.Analysis.SpecialFunctions.PolarCoord

Cited by

1 results in Mathlib

Foundations

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

Assumes

Fintype