Theorems · Theorem · number theory

NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {s : Set (NumberField.mixedEmbedding.realSpace K)},
  MeasurableSet s →
    ∀ {f : (NumberField.InfinitePlace K → ℝ) → ENNReal},
      Measurable f →
        ∫⁻ (x : NumberField.mixedEmbedding.realSpace K) in ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis '' s,
            f x =
          2⁻¹ ^ NumberField.InfinitePlace.nrComplexPlaces K * ENNReal.ofReal (NumberField.Units.regulator K) *
              ↑(Module.finrank ℚ K) *
            ∫⁻ (x : NumberField.mixedEmbedding.realSpace K) in s,
              ENNReal.ofReal (Real.exp (x NumberField.Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K))) *
                  (∏ i, ENNReal.ofReal (↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis (fun w => x w) ↑i))⁻¹ *
                f (↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x)

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldNumberField