Nullity of the moving halfspace boundary

The continuity proof for dirichletK reduces to the fact that the coordinate E₀ has an atomless law and is independent of all other coordinates. This file supplies the atomlessness calculation for the nonnegative exponential law and then applies the product decomposition of a finite Option-indexed product.

theorem Feige.nnexpMeasure_singleton (x : NNReal) : nnexpMeasure {x} = 0

The pushed-forward nonnegative exponential law has no atoms.

instance Feige.nnexpMeasure.nullSingletonClass : MeasureTheory.NullSingletonClass nnexpMeasure

theorem Feige.expProductMeasure_kBoundary (ι : Type u_1) [Fintype ι] (y : ι → ℝ) : (expProductMeasure ι) (kBoundary y) = 0

Every affine boundary in the definition of K is null: after splitting off E₀, every fiber is either empty or a singleton.

theorem Feige.tendsto_dirichletK' {ι : Type u_1} [Fintype ι] {yseq : ℕ → ι → ℝ} {y : ι → ℝ} (hy : Filter.Tendsto yseq Filter.atTop (nhds y)) : Filter.Tendsto (fun (n : ℕ) => dirichletK (yseq n)) Filter.atTop (nhds (dirichletK y))

The Dirichlet statistic is sequentially continuous everywhere.

theorem Feige.continuous_dirichletK {ι : Type u_1} [Fintype ι] : Continuous dirichletK

Continuity of the Dirichlet statistic, used to complete Theorem 2.1.