English
The L-integral of expMapBasis over a measurable set s equals a product of factors involving regulator, finrank, nrComplexPlaces, and a scaled integral over s, with expMapBasis evaluated on s.
Русский
L-интеграл expMapBasis над измеримым множеством s равен произведению множителей, включающих регулятор, finrank, nrComplexPlaces, и масштабированному интегралу по s с учетом expMapBasis на s.
LaTeX
$$$\int\int^- x\in expMapBasis'' s, f x = (2)^{-1}^{nrComplexPlaces K} \cdot reg(K) \cdot (\operatorname{finrank} K) \cdot \int^- x\in s, \exp( x_{w_0} \cdot \operatorname{finrank} K) \cdot \prod_{w\in { w // IsComplex w }} (\expMapBasis (fun w \mapsto x w) w)^{-1} \cdot f(\expMapBasis x)$$$
Lean4
/-- The set that parametrizes `normAtAllPlaces '' (normLeOne K)`, see
`normAtAllPlaces_normLeOne_eq_image`.
-/
abbrev paramSet : Set (realSpace K) :=
Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Ico 0 1
