Norm bounds and pointwise operators on bounded continuous functions

This file records norm estimates for operations on bounded continuous functions, and the operator of pointwise application of a bounded continuous family of continuous linear maps.

The main estimate, TauCeti.norm_boundedContinuousFunction_comp_le, bounds the sup norm of the postcomposition N ∘ f of a bounded continuous function f by an ε-Lipschitz map N by ‖N 0‖ + ε * ‖f‖. Thus a globally Lipschitz nonlinearity maps bounded continuous functions to bounded ones with an explicit affine norm bound. In TauCeti.Analysis.ODE.LyapunovPerron.Basic it supplies the uniform bound on the forcing term s ↦ N (γ s) that makes the Lyapunov–Perron integral converge and defines the Lyapunov–Perron operator on bounded continuous curves.

BoundedContinuousFunction.applyCLM applies a bounded continuous family φ of continuous linear maps pointwise, (φ, h) ↦ (t ↦ φ t (h t)), as a continuous bilinear map, and BoundedContinuousFunction.norm_applyCLM_apply_le bounds the operator norm of applyCLM φ by ‖φ‖. The derivative of a superposition operator f ↦ G ∘ f at f is applyCLM of the family t ↦ G' (f t) of derivatives of G; see TauCeti.Analysis.Calculus.FDeriv.BoundedContinuousFunction.

theorem TauCeti.norm_boundedContinuousFunction_comp_le {T : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace T] [SeminormedAddCommGroup X] [SeminormedAddCommGroup Y] {N : X → Y} {ε : NNReal} (hN : LipschitzWith ε N) (f : BoundedContinuousFunction T X) : ‖BoundedContinuousFunction.comp N hN f‖ ≤ ‖N 0‖ + ↑ε * ‖f‖

Postcomposition by an ε-Lipschitz map N has norm at most ‖N 0‖ + ε * ‖f‖.

noncomputable def BoundedContinuousFunction.applyCLM {α : Type u_1} {𝕜 : Type u_2} {X : Type u_3} {Y : Type u_4} [TopologicalSpace α] [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup X] [NormedSpace 𝕜 X] [SeminormedAddCommGroup Y] [NormedSpace 𝕜 Y] : BoundedContinuousFunction α (X →L[𝕜] Y) →L[𝕜] BoundedContinuousFunction α X →L[𝕜] BoundedContinuousFunction α Y

Pointwise application (φ, h) ↦ (t ↦ φ t (h t)) of a bounded continuous family φ of continuous linear maps to a bounded continuous function h, as a continuous bilinear map.

Equations

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

@[simp]

theorem BoundedContinuousFunction.applyCLM_apply {α : Type u_1} {𝕜 : Type u_2} {X : Type u_3} {Y : Type u_4} [TopologicalSpace α] [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup X] [NormedSpace 𝕜 X] [SeminormedAddCommGroup Y] [NormedSpace 𝕜 Y] (φ : BoundedContinuousFunction α (X →L[𝕜] Y)) (h : BoundedContinuousFunction α X) (t : α) : ((applyCLM φ) h) t = (φ t) (h t)

theorem BoundedContinuousFunction.norm_applyCLM_apply_le {α : Type u_1} {𝕜 : Type u_2} {X : Type u_3} {Y : Type u_4} [TopologicalSpace α] [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup X] [NormedSpace 𝕜 X] [SeminormedAddCommGroup Y] [NormedSpace 𝕜 Y] (φ : BoundedContinuousFunction α (X →L[𝕜] Y)) : ‖applyCLM φ‖ ≤ ‖φ‖

Pointwise application of φ has operator norm at most the sup norm of φ.