The volume scaling of multiplication on the mixed space

Multiplication by a fixed point c of the mixed space is an ℝ-linear endomorphism whose determinant is the ℝ-algebra norm of c, so it scales Lebesgue measure by the absolute value of that norm. The norm is computed here as one factor per real place and one Complex.normSq per complex place, and its absolute value is mixedEmbedding.norm c.

Specialising to the image of a unit, which has mixed norm one, gives that the unit action on the mixed space leaves the volume of every set unchanged.

Main results

• NumberField.mixedEmbedding.algebraNorm_apply: the ℝ-algebra norm of c, as a product over the places;
• NumberField.mixedEmbedding.abs_algebraNorm: the absolute value of that norm is mixedEmbedding.norm c;
• NumberField.mixedEmbedding.volume_image_mul_left: multiplication by c scales volume by mixedEmbedding.norm c;
• MeasureTheory.SMulInvariantMeasure (𝓞 K)ˣ (mixedSpace K) volume: the unit action preserves volume, so Mathlib's measure_smul and measure_preimage_smul apply.

theorem NumberField.mixedEmbedding.algebraNorm_apply {K : Type u_1} [Field K] [NumberField K] (c : mixedSpace K) : (Algebra.norm ℝ) c = (∏ w : { w : InfinitePlace K // w.IsReal }, c.1 w) * ∏ w : { w : InfinitePlace K // w.IsComplex }, Complex.normSq (c.2 w)

The ℝ-algebra norm of a point of the mixed space. Each real coordinate contributes its own factor and each complex coordinate contributes the norm of multiplication by a complex number, namely Complex.normSq.

theorem NumberField.mixedEmbedding.abs_algebraNorm {K : Type u_1} [Field K] [NumberField K] (c : mixedSpace K) : |(Algebra.norm ℝ) c| = mixedEmbedding.norm c

The absolute ℝ-algebra norm of c is the mixed norm of c. Reach for this rather than algebraNorm_apply when the norm feeds a measure-scaling lemma such as Measure.addHaar_image_linearMap, which asks for the absolute value.

theorem NumberField.mixedEmbedding.volume_image_mul_left {K : Type u_1} [Field K] [NumberField K] (c : mixedSpace K) (A : Set (mixedSpace K)) : MeasureTheory.volume ((fun (x : mixedSpace K) => c * x) '' A) = ENNReal.ofReal (mixedEmbedding.norm c) * MeasureTheory.volume A

Multiplication by c scales volume by the mixed norm of c. The set A is arbitrary, so there is no measurability hypothesis to discharge. Its specialisation to the action of a unit, where the factor is one, is the SMulInvariantMeasure instance below.

instance NumberField.mixedEmbedding.instSMulInvariantMeasureUnitsRingOfIntegersMixedSpaceVolume_tauCeti {K : Type u_1} [Field K] [NumberField K] : MeasureTheory.SMulInvariantMeasure (RingOfIntegers K)ˣ (mixedSpace K) MeasureTheory.volume

The unit action preserves volume. With it, measure_smul and measure_preimage_smul are the volume equations for u • A and (u • ·) ⁻¹' A, and measurePreserving_smul and the IsFundamentalDomain lemmas apply to the unit action. For a general multiplier c, where the factor is mixedEmbedding.norm c, use volume_image_mul_left.