P4: Abstract EVI skeleton (definitions and statements only)

This file provides lightweight definitions for the EVI predicate on a metric space, a Dini-type upper differential, and statement-shaped properties for contraction, mixed-error EVI for a pair of evolutions, and a Mosco-style convergence scaffold. Heavy analytical proofs are intentionally deferred to later phases; here we only fix APIs and types.

noncomputable def Frourio.d2 {X : Type u_1} [PseudoMetricSpace X] (x y : X) : ℝ

Equations

• Frourio.d2 x y = dist x y ^ 2

noncomputable def Frourio.DiniUpperE (φ : ℝ → ℝ) (t : ℝ) : EReal

Equations

• Frourio.DiniUpperE φ t = Filter.limsup (fun (h : ℝ) => ↑((φ (t + h) - φ t) / h)) (nhdsWithin 0 (Set.Ioi 0))

theorem Frourio.DiniUpperE_shift (φ : ℝ → ℝ) (s u : ℝ) : DiniUpperE (fun (τ : ℝ) => φ (s + τ)) u = DiniUpperE φ (s + u)

Time shift: t ↦ s + t just shifts the evaluation point (EReal form).

theorem Frourio.DiniUpperE_add_const (φ : ℝ → ℝ) (c t : ℝ) : DiniUpperE (fun (x : ℝ) => φ x + c) t = DiniUpperE φ t

Adding a constant does not change the upper Dini derivative (EReal form).

theorem Frourio.DiniUpper_nonpos_of_nonincreasing (φ : ℝ → ℝ) (t : ℝ) (Hmono : ∀ ⦃s u : ℝ⦄, s ≤ u → φ u ≤ φ s) : DiniUpperE φ t ≤ 0

noncomputable def Frourio.DiniUpper (φ : ℝ → ℝ) (t : ℝ) : ℝ

Equations

• Frourio.DiniUpper φ t = Filter.limsup (fun (h : ℝ) => (φ (t + h) - φ t) / h) (nhdsWithin 0 (Set.Ioi 0))

theorem Frourio.DiniUpper_shift (φ : ℝ → ℝ) (s t : ℝ) : DiniUpper (fun (τ : ℝ) => φ (s + τ)) t = DiniUpper φ (s + t)

Time shift: t ↦ s + t just shifts the evaluation point (Real form).

theorem Frourio.DiniUpper_add_const (ψ : ℝ → ℝ) (c t : ℝ) : DiniUpper (fun (τ : ℝ) => ψ τ + c) t = DiniUpper ψ t

Adding a constant to the function does not change the upper Dini derivative (Real form).

Convenience lemmas for Phase P1: constants, add-constant, and time rescale.

theorem Frourio.DiniUpperE_const (c t : ℝ) : DiniUpperE (fun (x : ℝ) => c) t = 0

Upper Dini derivative into EReal for a constant map is 0.

theorem Frourio.DiniUpper_const (c t : ℝ) : DiniUpper (fun (x : ℝ) => c) t = 0

Upper Dini derivative (real) for a constant map is 0.

theorem Frourio.DiniUpperE_bounds_const_upper (c t : ℝ) : ∃ (M : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), ((fun (x : ℝ) => c) (t + h) - (fun (x : ℝ) => c) t) / h ≤ M

Forward difference quotients of a constant map are eventually bounded above by 0.

theorem Frourio.DiniUpperE_bounds_const_lower (c t : ℝ) : ∃ (m : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), m ≤ ((fun (x : ℝ) => c) (t + h) - (fun (x : ℝ) => c) t) / h

Forward difference quotients of a constant map are eventually bounded below by 0.

theorem Frourio.DiniUpper_timeRescale_const (σ c t : ℝ) : DiniUpper (fun (τ : ℝ) => (fun (x : ℝ) => c) (σ * τ)) t = σ * DiniUpper (fun (x : ℝ) => c) (σ * t)

structure Frourio.EVIProblem (X : Type u_1) [PseudoMetricSpace X] : Type u_1

• E : X → ℝ
• lam : ℝ

def Frourio.IsEVISolution {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u : ℝ → X) : Prop

Equations

• Frourio.IsEVISolution P u = ∀ (t : ℝ) (v : X), 1 / 2 * Frourio.DiniUpper (fun (τ : ℝ) => Frourio.d2 (u τ) v) t + P.lam * Frourio.d2 (u t) v ≤ P.E v - P.E (u t)

def Frourio.timeRescale {X : Type u_1} (σ : ℝ) (u : ℝ → X) : ℝ → X

Time-rescale of a curve u by a positive factor σ (skeleton).

Equations

• Frourio.timeRescale σ u t = u (σ * t)

def Frourio.DiniUpper_timeRescale_pred (σ : ℝ) (φ : ℝ → ℝ) (t : ℝ) : Prop

Statement-level helper: scaling rule for upper Dini derivative under time reparameterization t ↦ σ t (to be proven in later phases).

Equations

• Frourio.DiniUpper_timeRescale_pred σ φ t = (Frourio.DiniUpper (fun (τ : ℝ) => φ (σ * τ)) t = σ * Frourio.DiniUpper φ (σ * t))

def Frourio.DiniUpper_add_le_pred (φ ψ : ℝ → ℝ) (t : ℝ) : Prop

Equations

• Frourio.DiniUpper_add_le_pred φ ψ t = (Frourio.DiniUpper (fun (τ : ℝ) => φ τ + ψ τ) t ≤ Frourio.DiniUpper φ t + Frourio.DiniUpper ψ t)

theorem Frourio.DiniUpper_add_le_pred_const_left (c : ℝ) (ψ : ℝ → ℝ) (t : ℝ) : DiniUpper_add_le_pred (fun (x : ℝ) => c) ψ t

Left constant: DiniUpper (c + ψ) ≤ DiniUpper c + DiniUpper ψ holds with equality.

theorem Frourio.DiniUpper_add_le_pred_const_right (φ : ℝ → ℝ) (c t : ℝ) : DiniUpper_add_le_pred φ (fun (x : ℝ) => c) t

Right constant: DiniUpper (φ + c) ≤ DiniUpper φ + DiniUpper c holds with equality.

theorem Frourio.DiniUpperE_add_le (φ ψ : ℝ → ℝ) (t : ℝ) (h1 : DiniUpperE φ t ≠ ⊥ ∨ DiniUpperE ψ t ≠ ⊤) (h2 : DiniUpperE φ t ≠ ⊤ ∨ DiniUpperE ψ t ≠ ⊥) : DiniUpperE (fun (τ : ℝ) => φ τ + ψ τ) t ≤ DiniUpperE φ t + DiniUpperE ψ t

EReal subadditivity for the upper Dini derivative, under the standard exclusions for EReal addition at (⊥, ⊤) and (⊤, ⊥) encoded in mathlib's limsup_add_le hypotheses.

theorem Frourio.DiniUpper_eq_toReal_of_finite (φ : ℝ → ℝ) (t : ℝ) (_hfin : DiniUpperE φ t ≠ ⊤ ∧ DiniUpperE φ t ≠ ⊥) (hub : ∃ (M : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), (φ (t + h) - φ t) / h ≤ M) (hlb : ∃ (m : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), m ≤ (φ (t + h) - φ t) / h) : DiniUpper φ t = (DiniUpperE φ t).toReal

Identification of Real/EReal DiniUpper under finiteness.