Periodization and the invariant functional J (Step 1 of Proposition 3.3)

Let m be a positive, normalized, translation-invariant mean on L^∞_per (Lemma 3.2). For a bounded measurable f vanishing outside a bounded interval (TestFunction), its periodization P f (r) = Σ_{k ∈ ℤ} f (r + k) is a finite sum for every r, and J(f) = m(P f) is linear, positive and translation invariant. This file proves:

• mean_interval : J(1_{(a,b]}) = b - a (equation eq:J-intervals);
• mean_support_bound : |J(f)| ≤ (b - a) ‖f‖_∞ if f vanishes outside (a, b] (equation eq:J-bound);
• periodize_shifted, periodize_add, periodize_smul, raw_cell_recovery : the compatibility of P with translations, sums, scalars and periodic functions.

All identities involving representatives hold almost everywhere; ae_shifts handles the countably many integer translates of a null set at once. The paper uses intervals [a, b); here they are (a, b], which only changes null sets.

structure AbstractLinearControl.ExoticMean.Periodization.TestFunction : Type

A bounded measurable function ℝ → ℝ vanishing outside a bounded interval.

• val : ℝ → ℝ

  The bounded measurable test function.

• measurable : MeasureTheory.StronglyMeasurable self.val
• supported : ∃ (n : ℕ), ∀ x ∉ Set.Icc (-↑n) ↑n, self.val x = 0
• bounded : ∃ (C : ℝ), ∀ᵐ (x : ℝ), ‖self.val x‖ ≤ C

noncomputable def AbstractLinearControl.ExoticMean.Periodization.raw (f : ℝ → ℝ) (r : ℝ) : ℝ

The periodization P f (r) = Σ_{k ∈ ℤ} f (r + k) (raw formula).

Equations

• AbstractLinearControl.ExoticMean.Periodization.raw f r = ∑' (k : ℤ), f (r + ↑k)

noncomputable def AbstractLinearControl.ExoticMean.Periodization.window (n : ℕ) (r : ℝ) : Finset ℤ

The integers k with r + k ∈ [-n, n].

Equations

• AbstractLinearControl.ExoticMean.Periodization.window n r = Finset.Icc ⌈-↑n - r⌉ ⌊↑n - r⌋

theorem AbstractLinearControl.ExoticMean.Periodization.outside_window (f : TestFunction) {n : ℕ} (hn : ∀ x ∉ Set.Icc (-↑n) ↑n, f.val x = 0) (r : ℝ) (k : ℤ) (hk : k ∉ window n r) : f.val (r + ↑k) = 0

theorem AbstractLinearControl.ExoticMean.Periodization.finite_shifts (f : TestFunction) (r : ℝ) : Function.HasFiniteSupport fun (k : ℤ) => f.val (r + ↑k)

theorem AbstractLinearControl.ExoticMean.Periodization.TestFunction.summable_shifts (f : TestFunction) (r : ℝ) : Summable fun (k : ℤ) => f.val (r + ↑k)

theorem AbstractLinearControl.ExoticMean.Periodization.raw_eq_sum (f : TestFunction) {n : ℕ} (hn : ∀ x ∉ Set.Icc (-↑n) ↑n, f.val x = 0) (r : ℝ) : raw f.val r = ∑ k ∈ window n r, f.val (r + ↑k)

theorem AbstractLinearControl.ExoticMean.Periodization.window_card_le (n : ℕ) (r : ℝ) : (window n r).card ≤ 2 * n + 1

theorem AbstractLinearControl.ExoticMean.Periodization.raw_int_shift (f : ℝ → ℝ) (r : ℝ) (j : ℤ) : raw f (r + ↑j) = raw f r

theorem AbstractLinearControl.ExoticMean.Periodization.TestFunction.raw_measurable (f : TestFunction) : MeasureTheory.StronglyMeasurable (raw f.val)

theorem AbstractLinearControl.ExoticMean.Periodization.ae_shifts {p : ℝ → Prop} (hp : ∀ᵐ (r : ℝ), p r) : ∀ᵐ (r : ℝ), ∀ (k : ℤ), p (r + ↑k)

A single exceptional set covers all integer translates.

theorem AbstractLinearControl.ExoticMean.Periodization.raw_bound (f : TestFunction) : ∃ (C : ℝ), ∀ᵐ (r : ℝ), ‖raw f.val r‖ ≤ C

theorem AbstractLinearControl.ExoticMean.Periodization.TestFunction.raw_memLp (f : TestFunction) : MeasureTheory.MemLp (raw f.val) ⊤ MeasureTheory.volume

noncomputable def AbstractLinearControl.ExoticMean.Periodization.periodize (f : TestFunction) : ↥LinftyPer

The periodization P f, as an element of L^∞_per.

Equations

• AbstractLinearControl.ExoticMean.Periodization.periodize f = ⟨MeasureTheory.MemLp.toLp (AbstractLinearControl.ExoticMean.Periodization.raw f.val) ⋯, ⋯⟩

theorem AbstractLinearControl.ExoticMean.Periodization.TestFunction.periodize_ae (f : TestFunction) : ↑↑↑(periodize f) =ᵐ[MeasureTheory.volume] raw f.val

theorem AbstractLinearControl.ExoticMean.Periodization.periodize_congr (f g : TestFunction) (heq : f.val =ᵐ[MeasureTheory.volume] g.val) : periodize f = periodize g

theorem AbstractLinearControl.ExoticMean.Periodization.periodize_add (f g h : TestFunction) (heq : f.val =ᵐ[MeasureTheory.volume] fun (r : ℝ) => g.val r + h.val r) : periodize f = periodize g + periodize h

theorem AbstractLinearControl.ExoticMean.Periodization.periodize_smul (f g : TestFunction) (c : ℝ) (heq : f.val =ᵐ[MeasureTheory.volume] fun (r : ℝ) => c * g.val r) : periodize f = c • periodize g

theorem AbstractLinearControl.ExoticMean.Periodization.periodize_le (f g : TestFunction) (hle : ∀ᵐ (r : ℝ), f.val r ≤ g.val r) : ∀ᵐ (r : ℝ), ↑↑↑(periodize f) r ≤ ↑↑↑(periodize g) r

theorem AbstractLinearControl.ExoticMean.Periodization.mean_le (m : ↥LinftyPer →L[ℝ] ℝ) (hpos : Positive ↑m) (f g : TestFunction) (hle : ∀ᵐ (r : ℝ), f.val r ≤ g.val r) : m (periodize f) ≤ m (periodize g)

noncomputable def AbstractLinearControl.ExoticMean.Periodization.supportedInterval (a b : ℝ) (f : ℝ → ℝ) (hf : MeasureTheory.StronglyMeasurable f) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ᵐ (r : ℝ), r ∈ Set.Ioc a b → ‖f r‖ ≤ C) : TestFunction

1_{(a,b]} f, for f bounded on (a, b].

Equations

• AbstractLinearControl.ExoticMean.Periodization.supportedInterval a b f hf C hC hbound = { val := (Set.Ioc a b).indicator f, measurable := ⋯, supported := ⋯, bounded := ⋯ }

noncomputable def AbstractLinearControl.ExoticMean.Periodization.interval (a b c : ℝ) : TestFunction

The constant c on (a, b], zero elsewhere.

Equations

• AbstractLinearControl.ExoticMean.Periodization.interval a b c = AbstractLinearControl.ExoticMean.Periodization.supportedInterval a b (fun (x : ℝ) => c) ⋯ ‖c‖ ⋯ ⋯

def AbstractLinearControl.ExoticMean.Periodization.shifted (a : ℝ) (f : TestFunction) : TestFunction

The translate f (· - a).

Equations

• AbstractLinearControl.ExoticMean.Periodization.shifted a f = { val := fun (r : ℝ) => f.val (-a + r), measurable := ⋯, supported := ⋯, bounded := ⋯ }

theorem AbstractLinearControl.ExoticMean.Periodization.periodize_shifted (a : ℝ) (f : TestFunction) : periodize (shifted a f) = (translate a) (periodize f)

theorem AbstractLinearControl.ExoticMean.Periodization.periodize_interval_shift (a b : ℝ) : periodize (interval a b 1) = (translate a) (periodize (interval 0 (b - a) 1))

theorem AbstractLinearControl.ExoticMean.Periodization.interval_split (a b c : ℝ) (hab : a ≤ b) (hbc : b ≤ c) : (interval a c 1).val =ᵐ[MeasureTheory.volume] fun (r : ℝ) => (interval a b 1).val r + (interval b c 1).val r

theorem AbstractLinearControl.ExoticMean.Periodization.periodize_unit : periodize (interval 0 1 1) = one

theorem AbstractLinearControl.ExoticMean.Periodization.raw_cell_recovery (f : ℝ → ℝ) (hf : Function.Periodic f 1) (r : ℝ) : raw ((Set.Ioc 0 1).indicator f) r = f r

theorem AbstractLinearControl.ExoticMean.Periodization.mean_interval (m : ↥LinftyPer →L[ℝ] ℝ) (hpos : Positive ↑m) (h1 : m one = 1) (hT : ∀ (a : ℝ) (f : ↥LinftyPer), m ((translate a) f) = m f) (a b : ℝ) (hab : a ≤ b) : m (periodize (interval a b 1)) = b - a

Interval calibration J(1_{(a,b]}) = b - a (equation eq:J-intervals), where J = m ∘ P. The function q(t) = J(1_{(0,t]}) is additive and monotone with q(1) = 1; squeezing between integers gives q(t) = t.

theorem AbstractLinearControl.ExoticMean.Periodization.mean_support_bound (m : ↥LinftyPer →L[ℝ] ℝ) (hpos : Positive ↑m) (h1 : m one = 1) (hT : ∀ (a : ℝ) (f : ↥LinftyPer), m ((translate a) f) = m f) (f : TestFunction) (a b C : ℝ) (hab : a ≤ b) (_hC : 0 ≤ C) (hf : ∀ᵐ (r : ℝ), ‖f.val r‖ ≤ (Set.Ioc a b).indicator (fun (x : ℝ) => C) r) : ‖m (periodize f)‖ ≤ (b - a) * C

The support bound eq:J-bound: if |f| ≤ C on (a, b] and f = 0 elsewhere, then |J(f)| ≤ (b - a) C.