The distributive Haar characters of ℝ and ℂ

This file computes distribHaarChar in the case of the actions of ℝˣ on ℝ and of ℂˣ on ℂ.

This lets us know what volume (x • s) is in terms of ‖x‖ and volume s, when x is a real/complex number and s is a set of reals/complex numbers.

Main declarations

• distribHaarChar_real: distribHaarChar ℝ is the usual norm on ℝ.
• distribHaarChar_complex: distribHaarChar ℂ is the usual norm on ℂ squared.
• Real.volume_real_smul: volume (x • s) = ‖x‖₊ * volume s for all x : ℝ and s : Set ℝ.
• Complex.volume_complex_smul: volume (z • s) = ‖z‖₊ ^ 2 * volume s for all z : ℂ and s : Set ℂ.

theorem Real.volume_real_smul (x : ℝ) (s : Set ℝ) : MeasureTheory.volume (x • s) = ↑‖x‖₊ * MeasureTheory.volume s

theorem distribHaarChar_real (x : ℝˣ) : (MeasureTheory.Measure.distribHaarChar ℝ) x = ‖↑x‖₊

The distributive Haar character of the action of ℝˣ on ℝ is the usual norm.

This means that volume (x • s) = ‖x‖ * volume s for all x : ℝ and s : Set ℝ. See Real.volume_real_smul.

theorem distribHaarChar_complex (z : ℂˣ) : (MeasureTheory.Measure.distribHaarChar ℂ) z = ‖↑z‖₊ ^ 2

The distributive Haar character of the action of ℂˣ on ℂ is the usual norm squared.

This means that volume (z • s) = ‖z‖ ^ 2 * volume s for all z : ℂ and s : Set ℂ. See Complex.volume_complex_smul.

theorem Complex.volume_complex_smul (z : ℂ) (s : Set ℂ) : MeasureTheory.volume (z • s) = ↑‖z‖₊ ^ 2 * MeasureTheory.volume s