Mollification and Constancy of Translation-Invariant Indicators

Proves that if 1_B is ae translation-invariant on an open interval I, its rectangular local average is constant on compact subintervals. Uses forward shift of ae properties, change of variables for local averages, and telescoping iteration via Nat.floor step counting.

Reference: lamportform.tex, Section 6, Lemma 6, Steps 4–5 (lines 577–599).

Local average (rectangular mollifier)

def ConnesLean.localAverage (f : ℝ → ℝ) (η u : ℝ) : ℝ

The local average of f with radius η at point u: (2η)⁻¹ ∫_{u-η}^{u+η} f(s) ds.

This is the simplest rectangular mollifier. When f = 1_B, this gives the density of B in the interval [u-η, u+η].

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

Equations

• ConnesLean.localAverage f η u = (2 * η)⁻¹ * ∫ (s : ℝ) in u - η..u + η, f s

theorem ConnesLean.localAverage_apply (f : ℝ → ℝ) (η u : ℝ) : localAverage f η u = (2 * η)⁻¹ * ∫ (s : ℝ) in u - η..u + η, f s

Forward shift of ae properties

theorem ConnesLean.ae_indicator_forward_shift {f : ℝ → ℝ} {a b t : ℝ} (h : ∀ᵐ (u : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), f u = f (u - t)) : ∀ᵐ (x : ℝ), x ∈ Set.Icc (a - t) (b - t) → f (x + t) = f x

Forward shift: if f(u) = f(u-t) ae on Icc a b, then f(x+t) = f(x) ae for x ∈ Icc (a-t) (b-t).

Uses translation invariance of Lebesgue measure (measure_preimage_add_right): null sets are preserved under shifts, so ae properties transfer.

Translation invariance of local average

theorem ConnesLean.localAverage_shift_eq {f : ℝ → ℝ} {a b t η u : ℝ} (hη : 0 < η) (ht : 0 < t) (h_ae : ∀ᵐ (u : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), f u = f (u - t)) (h_contain : Set.Icc (u - η) (u + η + t) ⊆ Set.Icc a b) : localAverage f η (u + t) = localAverage f η u

The local average is shift-invariant when the underlying function is ae shift-invariant.

If f(u) = f(u-t) ae on Icc a b, and [u-η, u+η+t] ⊆ [a, b], then localAverage f η (u+t) = localAverage f η u.

Proof: change of variables s ↦ s+t maps the shifted integration interval back to the original, then integral_congr_ae applies the ae hypothesis.

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

Constancy via telescoping

theorem ConnesLean.localAverage_const_on_compact {f : ℝ → ℝ} {a b η δ : ℝ} (hδ : 0 < δ) (h_shift : ∀ (u t : ℝ), a ≤ u - η → u + η + t ≤ b → 0 < t → t < δ → localAverage f η (u + t) = localAverage f η u) (v : ℝ) : a + η ≤ v → v ≤ b - η → localAverage f η v = localAverage f η (a + η)

The local average is constant on [a+η, b-η] when the underlying function is ae shift-invariant for all small shifts.

This is the telescoping argument: any point v ∈ [a+η, b-η] can be connected to a+η by a chain of small shifts, each preserving the local average. Uses Nat.floor to compute the number of intermediate steps.

Reference: lamportform.tex, Lemma 6, Step 5 (constancy of mollified function).

Connection to IndicatorTranslationInvariant

theorem ConnesLean.localAverage_const_of_indicator_invariant {B I : Set ℝ} {ε : ℝ} (h : IndicatorTranslationInvariant B I ε) {α β a b : ℝ} (hI : I = Set.Ioo α β) (hαa : α < a) (hbβ : b < β) {η : ℝ} (hη : 0 < η) (v : ℝ) : a + η ≤ v → v ≤ b - η → localAverage (B.indicator 1) η v = localAverage (B.indicator 1) η (a + η)

The local average of 1_B is constant on compact subintervals when 1_B is ae translation-invariant on an open interval.

Combines:

• indicator_ae_shift_forall_small (from TranslationInvariance.lean): ae shift-invariance on Icc a b for all small t.
• localAverage_shift_eq: each small shift preserves the local average.
• localAverage_const_on_compact: telescoping gives constancy.

Reference: lamportform.tex, Lemma 6, conclusion of Step 5.

Lebesgue differentiation

theorem ConnesLean.closedBall_average_eq_localAverage (f : ℝ → ℝ) (x r : ℝ) (hr : 0 < r) : ⨍ (y : ℝ) in Metric.closedBall x r, f y = localAverage f r x

The local average equals the closed-ball average for Lebesgue measure on ℝ. This is the bridge between our localAverage definition and Mathlib's setAverage over closedBall.

theorem ConnesLean.localAverage_tendsto_ae (f : ℝ → ℝ) (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) : ∀ᵐ (x : ℝ), Filter.Tendsto (fun (η : ℝ) => localAverage f η x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x))

Lebesgue differentiation: localAverage f η x → f x ae as η → 0⁺.

For any locally integrable f, the rectangular average over [x-η, x+η] converges to f(x) at almost every x as the radius η → 0⁺.

Proof: connect localAverage to the closed-ball average via closedBall_average_eq_localAverage, then apply Mathlib's IsUnifLocDoublingMeasure.ae_tendsto_average with centered balls.

Reference: lamportform.tex, Lemma 6, Step 5 (convergence of mollifier).