A system without integral representation (Proposition 3.3)

Proposition 3.3 (prop:no-representation). There exists an abstract linear control system (𝕋, Φ) with p = ∞, X = U = ℝ and 𝕋_t = Id for all t ≥ 0, such that

• (i) κ(t) = t for every t ≥ 0;
• (ii) (𝕋, Φ) admits no integral representation;
• (iii) (𝕋, Φ) is not E_F-admissible, for any Young function F.

The final statement is ExoticMean.Counterexample.no_representation.

Proof

• Steps 1–2 (exists_local_control_from_mean, using ALCS/Examples/Periodization.lean): with the exotic mean m of Lemma 3.2, J = m ∘ P and Φ_t u = J(1_{(0,t]} u).
• Step 3 (LocalControlData.smallIndicators): for a periodic open dense set O of small measure, m(1_O) = 1 while |O ∩ (0, 1]| is small. (The paper uses a set E with J(1_E) ≠ |E|; here the mean vanishes on functions vanishing on an open dense set, which directly gives inputs of small support with output 1.)
• Steps 4–5 (not_integral_of_smallIndicators, not_EF_of_smallIndicators).

Formalization choices

• Since A = 0, the extrapolation space X_{-1} is ℝ, so an integral representation (eq:representation) is given by a real bounded operator B (HasIntegralRepresentation).
• YoungFunction only records F(0) = 0, nonnegativity, convexity, continuity and growth at infinity: it contains all Young functions of the paper, so (iii) is proved for a larger class. The Luxemburg norm luxemburg is defined by its infimum formula.
• EFAdmissible asks for eq:orlicz at all times t ≥ 0, for inputs whose modular is finite (which is automatic for L^∞ inputs and finite-valued F).
• Intervals [0, t) of the paper become (0, t], which only changes null sets.

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

@[reducible, inline]

noncomputable abbrev AbstractLinearControl.ExoticMean.Counterexample.Input : AddSubgroup (ℝ →ₘ[muPlus] ℝ)

Bounded scalar inputs on the nonnegative half-line.

Equations

• AbstractLinearControl.ExoticMean.Counterexample.Input = MeasureTheory.Lp ℝ ⊤ AbstractLinearControl.muPlus

@[reducible, inline]

abbrev AbstractLinearControl.ExoticMean.Counterexample.ScalarSystem : Type

Scalar-state, scalar-input systems with bounded inputs.

Equations

• AbstractLinearControl.ExoticMean.Counterexample.ScalarSystem = AbstractLinearControl.ALCS ℝ ℝ ℝ ⊤

noncomputable def AbstractLinearControl.ExoticMean.Counterexample.inputOne : ↥Input

The constant unit input.

Equations

• AbstractLinearControl.ExoticMean.Counterexample.inputOne = AbstractLinearControl.ExoticMean.linftyConst AbstractLinearControl.muPlus 1

noncomputable def AbstractLinearControl.ExoticMean.Counterexample.inputIndicator (A : Set ℝ) (hA : MeasurableSet A) : ↥Input

The input represented by the indicator of a measurable set.

Equations

• AbstractLinearControl.ExoticMean.Counterexample.inputIndicator A hA = AbstractLinearControl.ExoticMean.linftyIndicator AbstractLinearControl.muPlus A hA

def AbstractLinearControl.ExoticMean.Counterexample.cell : Set ℝ

The choice (0,1] rather than [0,1) changes only null endpoints.

Equations

• AbstractLinearControl.ExoticMean.Counterexample.cell = Set.Ioc 0 1

theorem AbstractLinearControl.ExoticMean.Counterexample.cell_measurable : MeasurableSet cell

theorem AbstractLinearControl.ExoticMean.Counterexample.cell_subset_halfline : cell ⊆ Set.Ici 0

theorem AbstractLinearControl.ExoticMean.Counterexample.inputOne_norm_le : ‖inputOne‖ ≤ 1

theorem AbstractLinearControl.ExoticMean.Counterexample.ae_on_cell {p : ℝ → Prop} (hp : ∀ᵐ (r : ℝ) ∂muPlus, p r) : ∀ᵐ (r : ℝ) ∂MeasureTheory.volume.restrict cell, p r

theorem AbstractLinearControl.ExoticMean.Counterexample.cell_measure_ne_top : MeasureTheory.volume cell ≠ ⊤

theorem AbstractLinearControl.ExoticMean.Counterexample.measure_ne_top_of_subset_cell {A : Set ℝ} (hA : A ⊆ cell) : MeasureTheory.volume A ≠ ⊤

theorem AbstractLinearControl.ExoticMean.Counterexample.inputIndicator_integral {A : Set ℝ} (hA : MeasurableSet A) (hAC : A ⊆ cell) : ∫ (r : ℝ) in cell, ↑↑(inputIndicator A hA) r = (MeasureTheory.volume A).toReal

Step 2: the input maps Φ_t u = J(1_{(0,t]} u)

noncomputable def AbstractLinearControl.ExoticMean.Counterexample.rawPeriodization (t : ℝ) (u : ↥Input) (r : ℝ) : ℝ

The periodization r ↦ Σ_{k ∈ ℤ} (1_{(0,t]} u)(r + k) (raw formula).

Equations

• AbstractLinearControl.ExoticMean.Counterexample.rawPeriodization t u r = ∑' (k : ℤ), (Set.Ioc 0 t).indicator (fun (s : ℝ) => ↑↑u s) (r + ↑k)

structure AbstractLinearControl.ExoticMean.Counterexample.LocalControlData (m : ↥LinftyPer →L[ℝ] ℝ) : Type

The input maps Φ_t u = m(P(1_{(0,t]} u)) of Step 2, before packaging as continuous linear maps, together with the properties used in Steps 3–5. They are constructed in exists_local_control_from_mean.

• out : ℝ → ↥Input →ₗ[ℝ] ℝ

  The response at each time, before its continuity bound is bundled.

• formula (t : ℝ) : 0 ≤ t → ∀ (u : ↥Input), ∃ (g : ↥LinftyPer), ↑↑↑g =ᵐ[MeasureTheory.volume] rawPeriodization t u ∧ (self.out t) u = m g

  The exact formula m(P(1_(0,t] u)), on a.e. classes.

• bound (t : ℝ) : 0 ≤ t → ∀ (u : ↥Input), ‖(self.out t) u‖ ≤ t * ‖u‖
• one_value (t : ℝ) : 0 ≤ t → (self.out t) inputOne = t
• composition (τ t : ℝ) : 0 ≤ τ → 0 ≤ t → ∀ (u v w : ↥Input), ↑↑w =ᵐ[muPlus] concat τ ↑↑u ↑↑v → (self.out (τ + t)) w = (self.out τ) u + (self.out t) v
• periodic_test (O : PeriodicSet) : (self.out 1) (inputIndicator (O.carrier ∩ cell) ⋯) = m O.indicator

theorem AbstractLinearControl.ExoticMean.Counterexample.exists_local_control_from_mean (m : ↥LinftyPer →L[ℝ] ℝ) (hpos : Positive ↑m) (h1 : m one = 1) (hT : ∀ (a : ℝ) (f : ↥LinftyPer), m ((translate a) f) = m f) : Nonempty (LocalControlData m)

Steps 1–2 of the proof of Proposition 3.3: from a positive, normalized, translation-invariant mean m, the maps Φ_t u = J(1_{(0,t]} u) satisfy the bound |Φ_t u| ≤ t ‖u‖, Φ_t 1 = t, the composition property with T = Id, and recover m on periodic indicators.

noncomputable def AbstractLinearControl.ExoticMean.Counterexample.LocalControlData.phi {m : ↥LinftyPer →L[ℝ] ℝ} (D : LocalControlData m) (t : ℝ) : ↥Input →L[ℝ] ℝ

Values at negative times are irrelevant to ALCS; set them to zero.

Equations

• D.phi t = if ht : 0 ≤ t then (D.out t).mkContinuous t ⋯ else 0

theorem AbstractLinearControl.ExoticMean.Counterexample.LocalControlData.phi_apply {m : ↥LinftyPer →L[ℝ] ℝ} (D : LocalControlData m) (t : ℝ) (ht : 0 ≤ t) (u : ↥Input) : (D.phi t) u = (D.out t) u

noncomputable def AbstractLinearControl.ExoticMean.Counterexample.LocalControlData.system {m : ↥LinftyPer →L[ℝ] ℝ} (D : LocalControlData m) : ScalarSystem

The system of Proposition 3.3: T_t = Id and the input maps of Step 2.

Equations

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

theorem AbstractLinearControl.ExoticMean.Counterexample.LocalControlData.system_T {m : ↥LinftyPer →L[ℝ] ℝ} (D : LocalControlData m) (t : ℝ) : D.system.T t = ContinuousLinearMap.id ℝ ℝ

theorem AbstractLinearControl.ExoticMean.Counterexample.LocalControlData.kappa {m : ↥LinftyPer →L[ℝ] ℝ} (D : LocalControlData m) (t : ℝ) (ht : 0 ≤ t) : ‖D.system.Φ t‖ = t

Property (i) of Proposition 3.3: κ(t) = ‖Φ t‖ = t. The upper bound is eq:J-bound; the constant input 1 attains it.

Integral representation (eq:representation) and E_F-admissibility (eq:orlicz)

def AbstractLinearControl.ExoticMean.Counterexample.HasIntegralRepresentation (S : ScalarSystem) : Prop

Integral representation eq:representation, Φ_t u = ∫_0^t T_{t-s} B u(s) ds, with B : ℝ → ℝ. For T = Id the generator is A = 0 and X_{-1} = ℝ, so this is the representation of the paper specialized to the systems considered here.

Equations

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

theorem AbstractLinearControl.ExoticMean.Counterexample.scalar_form_of_representation (S : ScalarSystem) (hT : ∀ (t : ℝ), S.T t = ContinuousLinearMap.id ℝ ℝ) (h : HasIntegralRepresentation S) : ∃ (b : ℝ), ∀ (t : ℝ), 0 ≤ t → ∀ (u : ↥Input), (S.Φ t) u = b * ∫ (s : ℝ) in Set.Ioc 0 t, ↑↑u s

structure AbstractLinearControl.ExoticMean.Counterexample.YoungFunction : Type

Young functions. This class contains the Young functions of the paper (it does not require F(r)/r → 0 at 0 nor F(r)/r → ∞ at ∞); the proofs only use F(0) = 0 and F ≥ 0.

• toFun : ℝ → ℝ

  The scalar function defining the Orlicz modular.

• zero : self.toFun 0 = 0
• nonneg (x : ℝ) : 0 ≤ x → 0 ≤ self.toFun x
• convex : ConvexOn ℝ (Set.Ici 0) self.toFun
• continuous : ContinuousOn self.toFun (Set.Ici 0)
• growth : Filter.Tendsto self.toFun Filter.atTop Filter.atTop

noncomputable def AbstractLinearControl.ExoticMean.Counterexample.modular (F : YoungFunction) (t : ℝ) (u : ↥Input) (lam : ℝ) : ENNReal

The modular is an extended nonnegative integral, so divergence is not silently converted to the real number zero.

Equations

• AbstractLinearControl.ExoticMean.Counterexample.modular F t u lam = ∫⁻ (s : ℝ) in Set.Ioc 0 t, ENNReal.ofReal (F.toFun (|↑↑u s| / lam))

def AbstractLinearControl.ExoticMean.Counterexample.InHeart (F : YoungFunction) (t : ℝ) (u : ↥Input) : Prop

Membership of the restriction to (0,t] in the Orlicz heart.

Equations

• AbstractLinearControl.ExoticMean.Counterexample.InHeart F t u = ∀ (lam : ℝ), 0 < lam → AbstractLinearControl.ExoticMean.Counterexample.modular F t u lam < ⊤

noncomputable def AbstractLinearControl.ExoticMean.Counterexample.luxemburg (F : YoungFunction) (t : ℝ) (u : ↥Input) : ℝ

The Luxemburg gauge, by its infimum definition, not an abstract norm postulated to tend to zero.

Equations

• AbstractLinearControl.ExoticMean.Counterexample.luxemburg F t u = sInf {lam : ℝ | 0 < lam ∧ AbstractLinearControl.ExoticMean.Counterexample.modular F t u lam ≤ 1}

theorem AbstractLinearControl.ExoticMean.Counterexample.luxemburg_le (F : YoungFunction) (t : ℝ) (u : ↥Input) {lam : ℝ} (hlam : 0 < lam) (hmod : modular F t u lam ≤ 1) : luxemburg F t u ≤ lam

def AbstractLinearControl.ExoticMean.Counterexample.EFAdmissible (S : ScalarSystem) (F : YoungFunction) : Prop

E_F-admissibility, estimate eq:orlicz: |Φ_t u| ≤ C_t ‖u‖_{F,t} for every t.

Equations

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

theorem AbstractLinearControl.ExoticMean.Counterexample.indicator_modular (F : YoungFunction) {A : Set ℝ} (hA : MeasurableSet A) (hAC : A ⊆ cell) (lam : ℝ) : modular F 1 (inputIndicator A hA) lam = ENNReal.ofReal ((MeasureTheory.volume A).toReal * F.toFun (1 / lam))

theorem AbstractLinearControl.ExoticMean.Counterexample.indicator_inHeart (F : YoungFunction) {A : Set ℝ} (hA : MeasurableSet A) (hAC : A ⊆ cell) : InHeart F 1 (inputIndicator A hA)

Steps 4–5: the two obstructions

def AbstractLinearControl.ExoticMean.Counterexample.SmallIndicators (S : ScalarSystem) : Prop

Step 3: indicators of sets of arbitrarily small measure with output exactly one.

Equations

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

theorem AbstractLinearControl.ExoticMean.Counterexample.not_integral_of_smallIndicators (S : ScalarSystem) (hT : ∀ (t : ℝ), S.T t = ContinuousLinearMap.id ℝ ℝ) (hsmall : SmallIndicators S) : ¬HasIntegralRepresentation S

theorem AbstractLinearControl.ExoticMean.Counterexample.not_EF_of_smallIndicators (S : ScalarSystem) (hsmall : SmallIndicators S) (F : YoungFunction) : ¬EFAdmissible S F

theorem AbstractLinearControl.ExoticMean.Counterexample.LocalControlData.smallIndicators {m : ↥LinftyPer →L[ℝ] ℝ} (D : LocalControlData m) (h1 : m one = 1) (hV : ∀ v ∈ vanishingOnDenseOpen, m v = 0) : SmallIndicators D.system

theorem AbstractLinearControl.ExoticMean.Counterexample.counterexample_from_data {m : ↥LinftyPer →L[ℝ] ℝ} (D : LocalControlData m) (h1 : m one = 1) (hV : ∀ v ∈ vanishingOnDenseOpen, m v = 0) : (∀ (t : ℝ), 0 ≤ t → D.system.T t = ContinuousLinearMap.id ℝ ℝ) ∧ (∀ (t : ℝ), 0 ≤ t → ‖D.system.Φ t‖ = t) ∧ ¬HasIntegralRepresentation D.system ∧ ∀ (F : YoungFunction), ¬EFAdmissible D.system F

Steps 3–5 of the proof of Proposition 3.3: the system built from LocalControlData has properties (i), (ii), (iii), provided the mean vanishes on vanishingOnDenseOpen.

theorem AbstractLinearControl.ExoticMean.Counterexample.no_representation : ∃ (S : ALCS ℝ ℝ ℝ ⊤), (∀ (t : ℝ), 0 ≤ t → S.T t = ContinuousLinearMap.id ℝ ℝ) ∧ (∀ (t : ℝ), 0 ≤ t → ‖S.Φ t‖ = t) ∧ ¬HasIntegralRepresentation S ∧ ∀ (F : YoungFunction), ¬EFAdmissible S F

Proposition 3.3 (prop:no-representation). There is an abstract linear control system with p = ∞, X = U = ℝ and T_t = Id such that (i) κ(t) = t for t ≥ 0, (ii) it has no integral representation, (iii) it is not E_F-admissible for any Young function F.