Theorems · Theorem · number theory

NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral

∀ {K : Type u_1} [inst : Field K] {A : Set (NumberField.mixedEmbedding.mixedSpace K)} [inst_1 : NumberField K],
  NumberField.mixedEmbedding.normAtComplexPlaces ⁻¹' NumberField.mixedEmbedding.normAtComplexPlaces '' A = A →
    MeasurableSet A →
      MeasureTheory.volume A =
        ENNReal.ofReal (2 * Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
          ∫⁻ (x : NumberField.mixedEmbedding.realSpace K) in NumberField.mixedEmbedding.normAtComplexPlaces '' A,
            ∏ w, ENNReal.ofReal (x ↑w)

If the measurable set A is norm-stable at complex places in the sense that normAtComplexPlaces⁻¹ (normAtComplexPlaces '' A) = A, then its volume can be computed via an integral over normAtComplexPlaces '' A.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldNumberField