Null or Conull Conclusion — Lemma 6

Completes Lemma 6: a translation-invariant indicator on an open interval is either ae-null or ae-conull. Uses Lebesgue differentiation on compact subsets to establish the dichotomy, then exhaustion by increasing compact intervals for the global result.

Reference: lamportform.tex, Section 6, Lemma 6, Steps 8–10 (lines 617–639).

Helper lemmas

Exhaustion of Ioo by Icc

theorem ConnesLean.ioo_subset_iUnion_icc {α β : ℝ} : Set.Ioo α β ⊆ ⋃ (n : ℕ), Set.Icc (α + 1 / (↑n + 2)) (β - 1 / (↑n + 2))

The open interval (α, β) is covered by the increasing sequence of compact intervals [α + 1/(n+2), β - 1/(n+2)].

Null or conull on compact subintervals

theorem ConnesLean.indicator_null_or_conull_on_compact {B I : Set ℝ} {ε : ℝ} (h : IndicatorTranslationInvariant B I ε) {α β c d : ℝ} (hI : I = Set.Ioo α β) (hαc : α < c) (hdβ : d < β) : c < d → MeasureTheory.volume (B ∩ Set.Icc c d) = 0 ∨ MeasureTheory.volume (Set.Icc c d \ B) = 0

On any compact [c, d] ⊂ (α, β), either B is ae-null or ae-conull.

Proof by contradiction: suppose both B ∩ [c, d] and [c, d] \ B have positive measure. By localAverage_const_of_indicator_invariant, the local average of 1_B is constant on [c+η, d-η]. By localAverage_tendsto_ae, this constant converges to 1_B(x) ae. At a point of B, the limit is 1; at a point outside B, it is 0. But the convergent sequence is the same, so 1 = 0 by tendsto_nhds_unique. Contradiction.

Main theorem

theorem ConnesLean.null_or_conull_of_translation_invariant {B I : Set ℝ} {ε : ℝ} (h : IndicatorTranslationInvariant B I ε) : MeasureTheory.volume B = 0 ∨ MeasureTheory.volume (I \ B) = 0

Lemma 6 (Null or Conull): If the indicator 1_B is ae translation-invariant on an open interval I, then either B is ae-null (volume B = 0) or B is ae-conull (volume (I \ B) = 0).

Proof: Pick an anchor interval [c₀, d₀] ⊂ I. By the compact-case theorem, either B ∩ [c₀, d₀] or [c₀, d₀] \ B is null. Exhaust I by increasing compact intervals K_n ⊇ [c₀, d₀]. For each K_n, the compact-case alternative must agree with the anchor (otherwise the anchor interval would have zero measure). Countable union gives the global result.

Reference: lamportform.tex, Lemma 6 conclusion.