TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.positiveUnitSlabCoordinateFactor {K : Type u_1} [Field K] [NumberField K] (f : ℝ → ℂ) (w : InfinitePlace K) (x : ℝ) : ℂ

A positive unit slab coordinate factor used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.positiveUnitSlabCoordinateFactor f w x = if w = NumberField.Units.dirichletUnitTheorem.w₀ then (Set.Ioi 0).indicator f x else (Set.Ico 0 1).indicator (fun (x : ℝ) => 1) x

theorem NumberField.Odlyzko.positiveUnitSlab_indicator_eq_prod {K : Type u_1} [Field K] [NumberField K] (f : ℝ → ℂ) (y : mixedEmbedding.realSpace K) : positiveUnitFundamentalParamSet.indicator (fun (z : mixedEmbedding.realSpace K) => f (z Units.dirichletUnitTheorem.w₀)) y = ∏ w : InfinitePlace K, positiveUnitSlabCoordinateFactor f w (y w)

theorem NumberField.Odlyzko.setIntegral_positiveUnitFundamentalParamSet_radial {K : Type u_1} [Field K] [NumberField K] (f : ℝ → ℂ) : ∫ (y : mixedEmbedding.realSpace K) in positiveUnitFundamentalParamSet, f (y Units.dirichletUnitTheorem.w₀) = ∫ (t : ℝ) in Set.Ioi 0, f t

theorem NumberField.Odlyzko.integrableOn_positiveUnitFundamentalParamSet_radial {K : Type u_1} [Field K] [NumberField K] {f : ℝ → ℂ} (hf : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (y : mixedEmbedding.realSpace K) => f (y Units.dirichletUnitTheorem.w₀)) positiveUnitFundamentalParamSet MeasureTheory.volume