Fading memory, time invariance, moving averages and convolution functionals, in discrete and continuous time
DefinitionBoydChuaThis module fixes the objects of Boyd and Chua's approximation theory for nonlinear operators, in both the discrete-time setting (Section VI of the source) and the continuous-time setting (Sections III-IV).
Time convention — read this first. As in the published ReservoirESN definitions, the index counts steps into the PAST: u 0 is the present value and u k (resp. u t) the value k steps (resp. t units of time) earlier. A sequence or function is therefore the complete history of a signal up to now. Under this convention every operator defined here is causal, and the weight discounts the distant past. Read with the opposite convention the same code would describe an anticausal filter, so the convention is not cosmetic.
Discrete time. Shift j u is the history as it stood j steps ago. IsTimeInvariant N says the output at any instant is the present-time output applied to the shifted history; since the shift on the naturals is not invertible, this already forces the output at instant j to ignore the j most recent samples, which is causality. PointwiseFMP H M w is fading memory as stated in the source: H is continuous at every point of the ball of radius M, for the weighted supremum seminorm, with the modulus δ allowed to depend on the input as well as on the tolerance. OperatorFMP applies this to the present-time functional of an operator. Ball M is the ball of radius M in scalar signals, as a subtype of the product space; the product topology is what makes it compact. NLMA p u is the nonlinear moving-average operator of window length m: the output at any instant is the polynomial p evaluated on the last m samples.
Continuous time. IsWeightingC is the continuous weighting: positive, at most one, decreasing on the half-line, tending to zero — the constraints are imposed only where they are used, on non-negative times. SlewBdd M₁ M₂ u is the admissible input class of the source: amplitude bounded by M₁ and slew-rate bounded by M₂ on the past half-line. The slew bound is the equicontinuity that makes the class compact; it has no discrete counterpart and cannot be dropped. ShiftC, IsTimeInvariantC and PointwiseFMPC mirror their discrete analogues, with one difference stated explicitly: since the real shift is invertible, time invariance is required only for shifts into the past, so that causality is imposed rather than assumed. AdmissibleKernel w g asks that g be measurable and that the integral of |g|/w over the positive half-line be finite — condition (4.3) of the source; measurability is a separate field because it does not follow from integrability of |g|/w when w is not assumed measurable. Gconv g u is the pairing of a kernel against a signal; composed with ShiftC it is the convolution operator of Fig. 3.
Nothing here is proved: this module only fixes the vocabulary.
import Mathlib
import Definitions.Def_ReservoirESN
set_option autoImplicit false
open Filter Topology MeasureTheory ReservoirESN
/-!
# Boyd-Chua 1985 : memoire evanescente et approximation par moyenne mobile non lineaire
## Convention d'indexation — a lire avant tout le reste
Comme dans `ReservoirESN`, **l'indice `k` compte les pas vers le PASSE** : `u 0` est la
valeur presente, `u k` la valeur `k` instants plus tot. Une suite `u : ℕ → ℝ` est donc
l'historique complet d'un signal jusqu'au present, et non un signal indexe par le futur.
Toutes les definitions de ce fichier se lisent sous cette convention, et elles y sont
*causales* :
* `Shift j u` est l'historique tel qu'il etait `j` instants plus tot — l'operateur
`P U_{-t}` de la source ;
* `NLMA p u k = p (u k, u (k+1), …, u (k+m-1))` est la moyenne mobile
`p (u(t), u(t-1), …, u(t-m+1))` de la source, avec `t = -k` ;
* `w k` amortit le passe lointain, d'ou « memoire evanescente ».
Lu avec la convention inverse (indice = temps croissant), le meme code decrirait un
filtre anticausal. La convention n'est pas cosmetique.
-/
namespace BoydChua
/-- **Decalage temporel.** L'indice `k` compte les pas vers le passe (convention de
`ReservoirESN`) : `Shift j u` est l'entree vue par un observateur place `j` pas plus
tard, donc `(Shift j u) k = u (k + j)`. C'est l'operateur `U_{-t}` de la source. -/
def Shift {E : Type*} (j : ℕ) (u : ℕ → E) : ℕ → E := fun k => u (k + j)
/-- **Operateur invariant dans le temps.** Un tel operateur est entierement determine
par sa fonctionnelle « sortie a l'instant present », conformement a l'equation (2.1.1)
de la source : `Nu(t) = F P U_{-t} u`. -/
def IsTimeInvariant {E : Type*} (N : (ℕ → E) → (ℕ → ℝ)) : Prop :=
∀ (u : ℕ → E) (j : ℕ), N u j = N (Shift j u) 0
/-- **Memoire evanescente au sens de Boyd-Chua** (Section III, (3.1)) : la continuite
est *ponctuelle*, le `δ` dependant de l'entree `u` autant que de `ε`. C'est la
definition de la source, formellement plus faible que la version uniforme
`ReservoirESN.FunctionalFMP`. -/
def PointwiseFMP {E : Type*} [NormedAddCommGroup E]
(H : (ℕ → E) → ℝ) (M : ℝ) (w : ℕ → ℝ) : Prop :=
∀ u : ℕ → E, UnifBdd M u → ∀ ε > 0, ∃ δ > 0, ∀ v : ℕ → E, UnifBdd M v →
WeightedBound w (fun k => u k - v k) δ → |H u - H v| < ε
/-- Un operateur `N` a **memoire evanescente** lorsque sa fonctionnelle presente en a une. -/
def OperatorFMP {E : Type*} [NormedAddCommGroup E]
(N : (ℕ → E) → (ℕ → ℝ)) (M : ℝ) (w : ℕ → ℝ) : Prop :=
PointwiseFMP (fun u => N u 0) M w
/-- **La boule de rayon `M` de `l^∞`**, vue comme sous-type de l'espace produit `ℕ → ℝ`.
La topologie est celle de la convergence simple ; le jalon 1 montre qu'elle coincide
avec celle de la norme ponderee sur cette boule. -/
abbrev Ball (M : ℝ) : Type := {u : ℕ → ℝ // UnifBdd M u}
/-- **Operateur a moyenne mobile non lineaire** (NLMA, Fig. 5) de longueur `m` et de
non-linearite polynomiale `p` : la sortie presente est `p(u(k), u(k-1), …, u(k-m+1))`,
c'est-a-dire, en indexation vers le passe, `p(u(k), u(k+1), …, u(k+m-1))`. -/
noncomputable def NLMA {m : ℕ} (p : MvPolynomial (Fin m) ℝ) (u : ℕ → ℝ) : ℕ → ℝ :=
fun k => MvPolynomial.eval (fun i : Fin m => u ((i : ℕ) + k)) p
/-! ## Temps continu (Sections III-IV de la source) -/
/-- Ponderation en temps continu : decroissante de `(0,1]` vers `0`. -/
structure IsWeightingC (w : ℝ → ℝ) : Prop where
pos : ∀ t ≥ (0:ℝ), 0 < w t
le_one : ∀ t ≥ (0:ℝ), w t ≤ 1
antitone : AntitoneOn w (Set.Ici 0)
tendsto_zero : Tendsto w atTop (nhds 0)
/-- `u t` est la valeur du signal `t` unites de temps AVANT le present. -/
structure SlewBdd (M₁ M₂ : ℝ) (u : ℝ → ℝ) : Prop where
bdd : ∀ t ≥ (0:ℝ), |u t| ≤ M₁
lipschitz : LipschitzOnWith (Real.toNNReal M₂) u (Set.Ici 0)
def WeightedBoundC (w : ℝ → ℝ) (z : ℝ → ℝ) (c : ℝ) : Prop :=
∀ t ≥ (0:ℝ), |z t| * w t ≤ c
def ShiftC (r : ℝ) (u : ℝ → ℝ) : ℝ → ℝ := fun t => u (t + r)
def IsTimeInvariantC (N : (ℝ → ℝ) → (ℝ → ℝ)) : Prop :=
∀ (u : ℝ → ℝ), ∀ r ≥ (0:ℝ), N u r = N (ShiftC r u) 0
def PointwiseFMPC (H : (ℝ → ℝ) → ℝ) (M₁ M₂ : ℝ) (w : ℝ → ℝ) : Prop :=
∀ u, SlewBdd M₁ M₂ u → ∀ ε > 0, ∃ δ > 0, ∀ v, SlewBdd M₁ M₂ v →
WeightedBoundC w (fun t => u t - v t) δ → |H u - H v| < ε
/-- Noyau admissible : `∫₀^∞ |g| / w < ∞`, condition (4.3) de la source. -/
structure AdmissibleKernel (w g : ℝ → ℝ) : Prop where
meas : AEStronglyMeasurable g (volume.restrict (Set.Ioi 0))
integrable : IntegrableOn (fun t => |g t| / w t) (Set.Ioi 0) volume
/-- Fonctionnelle de convolution `G_g u = ∫₀^∞ g(t) u(t) dt`, ou `u t` est la valeur
`t` unites avant le present : c'est `∫ g(t) u(-t) dt` de la source. -/
noncomputable def Gconv (g u : ℝ → ℝ) : ℝ :=
∫ t in Set.Ioi (0:ℝ), g t * u t
end BoydChua
Read-back
What the Lean code literally says, in plain math · claude-opus-5
Discrete part. Fix a normed space E. Shifting a one-sided sequence by j re-indexes it as (Shift j u)(k) = u(k+j). An operator N, mapping E-valued sequences to real-valued sequences, is time-invariant when for every input u and every index j the output at j equals the output at 0 of the j-shifted input; such an operator is entirely determined by the single functional u maps to N u 0. A real functional H has the pointwise fading-memory property at radius M for a weight w when: for every u with all norms at most M, and every positive e, there is a positive d such that every v with all norms at most M satisfying the weighted bound d on u - v obeys |H u - H v| < e. This is exactly continuity of H restricted to the M-ball for the weighted sup-seminorm; d is allowed to depend on u, so this is pointwise, not uniform, continuity. An operator has the operator fading-memory property when its instant-zero functional has the pointwise one - the property is imposed at time zero only. Given a polynomial p in m real variables, the polynomial moving average NLMA p u takes at index k the value p(u k, u(k+1), ..., u(k+m-1)): the window runs upward from k. Whether that window is the recent past or the near future is fixed by the indexing convention, which the module header states explicitly - the index counts steps into the past, so the window is the last m samples and the operator is causal. Shift and NLMA are on the same convention, and the identity NLMA p u k = NLMA p (Shift k u) 0 holds definitionally.
Continuous part. Every condition is imposed on the half-line only. w is a weighting when it is strictly positive and at most one at every non-negative time, antitone there, and tends to zero at infinity; nothing is required of w at negative times, which are never read. u is slew-bounded with constants M1, M2 when it is bounded by M1 and Lipschitz with constant max(M2,0), both on the non-negative half-line. If M2 is not positive the Lipschitz constant is zero and the class degenerates to constants, so the theorems using it carry a positivity hypothesis. The weighted bound reads |z t| * w t <= c for non-negative t; the shift is (ShiftC r u)(t) = u(t+r); an operator is time-invariant when N u r = N (ShiftC r u) 0, but only for non-negative r - which is what imposes causality, the real shift being invertible unlike the integer one. A kernel g is admissible for w when g is almost-everywhere strongly measurable on the positive half-line and |g|/w is integrable there; measurability is a separate field because it does not follow from integrability of |g|/w unless w is assumed measurable. The associated functional is the pairing of g against the signal. Admissibility is precisely what makes that functional Lipschitz for the weighted seminorm, with constant the integral of |g|/w.
Confirmed by the mission captain (proposal self-audit).