Translation-Invariance Setup for Indicator Functions

Defines the hypothesis that an indicator 1_B is ae translation-invariant on an open interval I, and reduces the ae statement from I ∩ (I+t) to compact subintervals J ⊂⊂ I using the margin δ₀ = min(a - α, β - b).

Reference: lamportform.tex, Section 6, Lemma 6, Steps 1–3 (lines 542–576).

Hypothesis definition

structure ConnesLean.IndicatorTranslationInvariant (B I : Set ℝ) (ε : ℝ) : Prop

The indicator 1_B is ae translation-invariant on an open interval I.

Concretely: B ⊆ I, I is an open interval Ioo α β, and for all t ∈ (0, ε), the indicator 1_B satisfies 1_B(u) = 1_B(u - t) a.e. on the overlap I ∩ preimage (· - t) I.

Reference: lamportform.tex, Lemma 6 hypothesis.

• ε_pos : 0 < ε
• B_measurable : MeasurableSet B
• B_subset : B ⊆ I
• I_open : ∃ (α : ℝ) (β : ℝ), α < β ∧ I = Set.Ioo α β
• ae_shift (t : ℝ) : 0 < t → t < ε → ∀ᵐ (u : ℝ) ∂MeasureTheory.volume.restrict (I ∩ (fun (x : ℝ) => x - t) ⁻¹' I), B.indicator 1 u = B.indicator 1 (u - t)

Margin of compact subinterval

def ConnesLean.compactMargin (α β a b : ℝ) : ℝ

The margin of Icc a b inside Ioo α β: δ₀ = min(a - α, β - b). Positive when α < a and b < β, i.e. Icc a b ⊆ Ioo α β with room to spare.

Equations

• ConnesLean.compactMargin α β a b = min (a - α) (β - b)

theorem ConnesLean.compactMargin_pos {α β a b : ℝ} (hαa : α < a) (hbβ : b < β) : 0 < compactMargin α β a b

The margin is positive when Icc a b sits strictly inside Ioo α β.

Subset containment under shifts

theorem ConnesLean.icc_subset_ioo_inter_shift {α β a b t : ℝ} (hαa : α < a) (hbβ : b < β) (ht_pos : 0 < t) (ht_bound : t < compactMargin α β a b) : Set.Icc a b ⊆ Set.Ioo α β ∩ (fun (x : ℝ) => x - t) ⁻¹' Set.Ioo α β

For t < δ₀, the compact interval Icc a b is contained in Ioo α β ∩ preimage (·-t) (Ioo α β). This means both u ∈ I and u - t ∈ I for every u ∈ J.

Restricting the ae hypothesis to compact subintervals

theorem ConnesLean.indicator_ae_shift_on_compact {B I : Set ℝ} {ε : ℝ} (h : IndicatorTranslationInvariant B I ε) {α β a b : ℝ} (hI : I = Set.Ioo α β) (hαa : α < a) (hbβ : b < β) {t : ℝ} (ht_pos : 0 < t) (ht_ε : t < ε) (ht_δ : t < compactMargin α β a b) : ∀ᵐ (u : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), B.indicator 1 u = B.indicator 1 (u - t)

Step 2: The ae shift-invariance transfers from I ∩ (I+t) to any compact J = Icc a b ⊆ I when t is small enough.

Given the IndicatorTranslationInvariant hypothesis, for any compact Icc a b with α < a, b < β (where I = Ioo α β), and any t ∈ (0, min(ε, δ₀)):

1_B(u) = 1_B(u - t) a.e. on Icc a b.

Reference: lamportform.tex, Lemma 6, Step 2.

theorem ConnesLean.indicator_ae_shift_forall_small {B I : Set ℝ} {ε : ℝ} (h : IndicatorTranslationInvariant B I ε) {α β a b : ℝ} (hI : I = Set.Ioo α β) (hαa : α < a) (hbβ : b < β) : have δ := min ε (compactMargin α β a b); 0 < δ ∧ ∀ (t : ℝ), 0 < t → t < δ → ∀ᵐ (u : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), B.indicator 1 u = B.indicator 1 (u - t)

Step 3: Quantified version — the ae shift-invariance holds for all sufficiently small positive t, on any compact Icc a b ⊆ I.

The threshold is δ = min(ε, compactMargin α β a b).