Continuity core for the Dirichlet statistic

This file formalizes the dominated-convergence step used to establish the continuity needed in the proof of Theorem 2.1. It proves that membership in the moving halfspace stabilizes away from its boundary, and consequently that dirichletK is sequentially continuous at every parameter whose boundary hyperplane has zero product-exponential measure.

def Feige.kLinear {ι : Type u_1} [Fintype ι] (y : ι → ℝ) (e : Option ι → NNReal) : ℝ

The affine functional defining the moving halfspace in kEvent.

Equations

• Feige.kLinear y e = ∑ i : ι, (y i - 1) * ↑(e (some i))

theorem Feige.continuous_kLinear {ι : Type u_1} [Fintype ι] (e : Option ι → NNReal) : Continuous fun (y : ι → ℝ) => kLinear y e

theorem Feige.eventually_mem_kEvent_iff {ι : Type u_1} [Fintype ι] {L : Filter ℕ} {yseq : ℕ → ι → ℝ} {y : ι → ℝ} (hy : Filter.Tendsto yseq L (nhds y)) (e : Option ι → NNReal) (hne : kLinear y e ≠ ↑(e none)) : ∀ᶠ (n : ℕ) in L, e ∈ kEvent (yseq n) ↔ e ∈ kEvent y

Away from the boundary, membership in kEvent is eventually constant under convergence of the parameter vector.

def Feige.kBoundary {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : Set (Option ι → NNReal)

The boundary set for a fixed parameter.

Equations

• Feige.kBoundary y = {e : Option ι → NNReal | Feige.kLinear y e = ↑(e none)}

theorem Feige.measurableSet_kBoundary {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : MeasurableSet (kBoundary y)

theorem Feige.ae_eventually_mem_kEvent_iff {ι : Type u_1} [Fintype ι] {yseq : ℕ → ι → ℝ} {y : ι → ℝ} (hy : Filter.Tendsto yseq Filter.atTop (nhds y)) (hboundary : (expProductMeasure ι) (kBoundary y) = 0) : ∀ᵐ (e : Option ι → NNReal) ∂expProductMeasure ι, ∀ᶠ (n : ℕ) in Filter.atTop, e ∈ kEvent (yseq n) ↔ e ∈ kEvent y

Almost-everywhere stabilization of the moving indicators, assuming only the geometrically isolated boundary-null statement.

theorem Feige.tendsto_measure_kEvent {ι : Type u_1} [Fintype ι] {yseq : ℕ → ι → ℝ} {y : ι → ℝ} (hy : Filter.Tendsto yseq Filter.atTop (nhds y)) (hboundary : (expProductMeasure ι) (kBoundary y) = 0) : Filter.Tendsto (fun (n : ℕ) => (expProductMeasure ι) (kEvent (yseq n))) Filter.atTop (nhds ((expProductMeasure ι) (kEvent y)))

Dominated convergence for the event probabilities.

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

Sequential continuity of dirichletK, reduced to the boundary hyperplane having measure zero.