An exotic invariant mean on periodic L^∞ functions (Lemma 3.2)

Lemma 3.2 (lem:exotic-mean). Let L^∞_per be the space of 1-periodic elements of L^∞(ℝ; ℝ). There exists a linear map m : L^∞_per → ℝ such that

• (a) m(f) ≥ 0 whenever f ≥ 0 almost everywhere, and m(1) = 1;
• (b) m(f(· - a)) = m(f) for all f ∈ L^∞_per and a ∈ ℝ;
• (c) m(f) ≠ ∫_0^1 f(s) ds for some f ∈ L^∞_per.

The paper quotes this classical fact from the literature; here it is proved. The final statement is ExoticMean.exotic_mean.

Proof

Let V ⊆ L^∞_per be the subspace of functions vanishing a.e. on some open dense set. The constants are at distance |c| from V (constant_separation). A Hahn–Banach argument combined with finite Cesàro averages of translations (ALCS/Background/InvariantHahnBanach.lean) gives a translation-invariant functional m of norm ≤ 1 with m(1) = 1 and m = 0 on V (exists_strong_mean); positivity follows from ‖m‖ ≤ 1 and m(1) = 1. For (c), take the indicator of a periodic open dense set of small measure (exists_small_periodic_open): its mean is 1 while its integral over a period is < 1/2.

Formalization choices

• L^∞_per (LinftyPer) is the subspace of L^∞(ℝ) fixed by the translation by 1; translations act on a.e. classes (shift, translate).
• Positivity (Positive) is an a.e. property of the class, not of a representative.
• exists_strong_mean proves more than needed (vanishing on V); this extra property is used in Proposition 3.3 and does not appear in the statement of exotic_mean.

theorem AbstractLinearControl.ExoticMean.instFactLeENNRealOfNatTop_leanPool : Fact (1 ≤ ⊤)

Generic L^∞ helpers (also used in Proposition 3.3)

theorem AbstractLinearControl.ExoticMean.linfty_norm_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp ℝ ⊤ μ)) {C : ℝ} (hC : 0 ≤ C) (hf : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ C) : ‖f‖ ≤ C

theorem AbstractLinearControl.ExoticMean.linfty_ae_norm_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp ℝ ⊤ μ)) : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ‖f‖

def AbstractLinearControl.ExoticMean.linftyConst {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (c : ℝ) : ↥(MeasureTheory.Lp ℝ ⊤ μ)

A constant is in L∞ even if the underlying measure has infinite mass.

Equations

• AbstractLinearControl.ExoticMean.linftyConst μ c = MeasureTheory.MemLp.toLp (fun (x : α) => c) ⋯

theorem AbstractLinearControl.ExoticMean.linftyConst_ae {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (c : ℝ) : ↑↑(linftyConst μ c) =ᵐ[μ] fun (x : α) => c

noncomputable def AbstractLinearControl.ExoticMean.linftyIndicator {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) (hs : MeasurableSet s) : ↥(MeasureTheory.Lp ℝ ⊤ μ)

A measurable indicator, as an actual L∞ equivalence class.

Equations

• AbstractLinearControl.ExoticMean.linftyIndicator μ s hs = MeasureTheory.MemLp.toLp (s.indicator fun (x : α) => 1) ⋯

theorem AbstractLinearControl.ExoticMean.linftyIndicator_ae {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) (hs : MeasurableSet s) : ↑↑(linftyIndicator μ s hs) =ᵐ[μ] s.indicator fun (x : α) => 1

Translations and periodic functions

@[reducible, inline]

noncomputable abbrev AbstractLinearControl.ExoticMean.Ambient : AddSubgroup (ℝ →ₘ[MeasureTheory.volume] ℝ)

L^∞(ℝ).

Equations

• AbstractLinearControl.ExoticMean.Ambient = MeasureTheory.Lp ℝ ⊤ MeasureTheory.volume

noncomputable def AbstractLinearControl.ExoticMean.shift (a : ℝ) : ↥Ambient →ₗ[ℝ] ↥Ambient

shift a f is the a.e. class of r ↦ f (r-a).

Equations

• AbstractLinearControl.ExoticMean.shift a = MeasureTheory.Lp.compMeasurePreservingₗ ℝ (fun (r : ℝ) => -a + r) ⋯

theorem AbstractLinearControl.ExoticMean.shift_ae (a : ℝ) (f : ↥Ambient) : ↑↑((shift a) f) =ᵐ[MeasureTheory.volume] fun (r : ℝ) => ↑↑f (-a + r)

theorem AbstractLinearControl.ExoticMean.shift_zero (f : ↥Ambient) : (shift 0) f = f

theorem AbstractLinearControl.ExoticMean.shift_add (a b : ℝ) (f : ↥Ambient) : (shift (a + b)) f = (shift a) ((shift b) f)

theorem AbstractLinearControl.ExoticMean.shift_commute (a b : ℝ) (f : ↥Ambient) : (shift a) ((shift b) f) = (shift b) ((shift a) f)

theorem AbstractLinearControl.ExoticMean.norm_shift (a : ℝ) (f : ↥Ambient) : ‖(shift a) f‖ = ‖f‖

def AbstractLinearControl.ExoticMean.periodicSubspace : Submodule ℝ ↥Ambient

L^∞_per: the subspace of L^∞(ℝ) fixed by the translation by 1, i.e. the a.e. 1-periodic functions. (This avoids choosing periodic representatives.)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev AbstractLinearControl.ExoticMean.LinftyPer : Submodule ℝ ↥Ambient

Almost-everywhere periodic bounded functions, with their inherited norm.

Equations

• AbstractLinearControl.ExoticMean.LinftyPer = AbstractLinearControl.ExoticMean.periodicSubspace

noncomputable def AbstractLinearControl.ExoticMean.translate (a : ℝ) : ↥LinftyPer →ₗ[ℝ] ↥LinftyPer

The real-translation action on the periodic subspace.

Equations

• One or more equations did not get rendered due to their size.

theorem AbstractLinearControl.ExoticMean.translate_ae (a : ℝ) (f : ↥LinftyPer) : ↑↑↑((translate a) f) =ᵐ[MeasureTheory.volume] fun (r : ℝ) => ↑↑↑f (r - a)

theorem AbstractLinearControl.ExoticMean.translate_zero (f : ↥LinftyPer) : (translate 0) f = f

theorem AbstractLinearControl.ExoticMean.translate_add (a b : ℝ) (f : ↥LinftyPer) : (translate (a + b)) f = (translate a) ((translate b) f)

theorem AbstractLinearControl.ExoticMean.norm_translate (a : ℝ) (f : ↥LinftyPer) : ‖(translate a) f‖ = ‖f‖

theorem AbstractLinearControl.ExoticMean.shift_const (a c : ℝ) : (shift a) (linftyConst MeasureTheory.volume c) = linftyConst MeasureTheory.volume c

noncomputable def AbstractLinearControl.ExoticMean.one : ↥LinftyPer

The periodic class of the constant one function.

Equations

• AbstractLinearControl.ExoticMean.one = ⟨AbstractLinearControl.ExoticMean.linftyConst MeasureTheory.volume 1, AbstractLinearControl.ExoticMean.one._proof_1⟩

theorem AbstractLinearControl.ExoticMean.one_ae : ↑↑↑one =ᵐ[MeasureTheory.volume] fun (x : ℝ) => 1

theorem AbstractLinearControl.ExoticMean.translate_one (a : ℝ) : (translate a) one = one

noncomputable def AbstractLinearControl.ExoticMean.integral01 (f : ↥LinftyPer) : ℝ

The ordinary Lebesgue integral over [0,1]. Ioc is the usual set-integral implementation of the interval integral; changing either endpoint does not change an integral for Lebesgue measure.

Equations

• AbstractLinearControl.ExoticMean.integral01 f = ∫ (r : ℝ) in Set.Ioc 0 1, ↑↑↑f r

def AbstractLinearControl.ExoticMean.Positive (m : ↥LinftyPer →ₗ[ℝ] ℝ) : Prop

Positivity is explicitly an a.e. property, not pointwise positivity of Mathlib's arbitrarily chosen Lp representative.

Equations

• AbstractLinearControl.ExoticMean.Positive m = ∀ (f : ↥AbstractLinearControl.ExoticMean.LinftyPer), (∀ᵐ (r : ℝ), 0 ≤ ↑↑↑f r) → 0 ≤ m f

The open-dense vanishing subspace

def AbstractLinearControl.ExoticMean.vanishingOnDenseOpen : Submodule ℝ ↥LinftyPer

The subspace V of periodic functions vanishing a.e. on some open dense set.

Equations

• One or more equations did not get rendered due to their size.

theorem AbstractLinearControl.ExoticMean.translate_mem_vanishing (a : ℝ) (f : ↥LinftyPer) (hf : f ∈ vanishingOnDenseOpen) : (translate a) f ∈ vanishingOnDenseOpen

theorem AbstractLinearControl.ExoticMean.constant_separation (c : ℝ) (v : ↥LinftyPer) (hv : v ∈ vanishingOnDenseOpen) : |c| ≤ ‖c • one + v‖

theorem AbstractLinearControl.ExoticMean.positive_of_norm_le_one (m : ↥LinftyPer →L[ℝ] ℝ) (hm : ‖m‖ ≤ 1) (h1 : m one = 1) : Positive ↑m

Positivity follows from normalization and the norm bound, with the unscaled argument ‖f‖ 1 - f; this also handles f = 0.

theorem AbstractLinearControl.ExoticMean.exists_strong_mean : ∃ (m : ↥LinftyPer →L[ℝ] ℝ), ‖m‖ ≤ 1 ∧ Positive ↑m ∧ m one = 1 ∧ (∀ (a : ℝ) (f : ↥LinftyPer), m ((translate a) f) = m f) ∧ ∀ v ∈ vanishingOnDenseOpen, m v = 0

The invariant mean, with the extra property that it vanishes on functions vanishing a.e. on an open dense set (used in Proposition 3.3).

Small periodic open dense sets

structure AbstractLinearControl.ExoticMean.PeriodicSet : Type

A Borel set with the exact period needed for the indicator class.

• carrier : Set ℝ

  The measurable periodic subset of the real line.

• measurable : MeasurableSet self.carrier
• period (r : ℝ) : -1 + r ∈ self.carrier ↔ r ∈ self.carrier

noncomputable def AbstractLinearControl.ExoticMean.PeriodicSet.indicator (O : PeriodicSet) : ↥LinftyPer

The periodic indicator as an almost-everywhere bounded-function class.

Equations

• O.indicator = ⟨AbstractLinearControl.ExoticMean.linftyIndicator MeasureTheory.volume O.carrier ⋯, ⋯⟩

theorem AbstractLinearControl.ExoticMean.PeriodicSet.indicator_ae (O : PeriodicSet) : ↑↑↑O.indicator =ᵐ[MeasureTheory.volume] O.carrier.indicator fun (x : ℝ) => 1

theorem AbstractLinearControl.ExoticMean.PeriodicSet.mean_indicator (m : ↥LinftyPer →L[ℝ] ℝ) (h1 : m one = 1) (hV : ∀ v ∈ vanishingOnDenseOpen, m v = 0) (O : PeriodicSet) (hOo : IsOpen O.carrier) (hOd : Dense O.carrier) : m O.indicator = 1

theorem AbstractLinearControl.ExoticMean.PeriodicSet.integral_indicator (O : PeriodicSet) : integral01 O.indicator = (MeasureTheory.volume (O.carrier ∩ Set.Ioc 0 1)).toReal

theorem AbstractLinearControl.ExoticMean.exists_small_periodic_open (ε : ℝ) (hε : 0 < ε) : ∃ (O : PeriodicSet), IsOpen O.carrier ∧ Dense O.carrier ∧ (MeasureTheory.volume (O.carrier ∩ Set.Ioc 0 1)).toReal < ε

Outer regularity around a countable dense null set gives a small open dense set on the circle; pulling it back makes it genuinely periodic.

Lemma 3.2

theorem AbstractLinearControl.ExoticMean.exotic_mean : ∃ (m : ↥LinftyPer →ₗ[ℝ] ℝ), (Positive m ∧ m one = 1) ∧ (∀ (f : ↥LinftyPer) (a : ℝ), m ((translate a) f) = m f) ∧ ∃ (f : ↥LinftyPer), m f ≠ integral01 f

Lemma 3.2 (lem:exotic-mean). There is a linear map m : L^∞_per → ℝ which is (a) positive and normalized, (b) invariant under every real translation, and (c) different from the Lebesgue integral over a period.