Lift continuous multilinear maps and power series to bounded continuous function spaces. The norm bounds support analytic integration over compact parameter sets.

noncomputable def KamProject.Arnold1963.boundedMultilinearLift {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℂ E] {m : ℕ} (p : E [×m]→L[ℂ] ℂ) : BoundedContinuousFunction X E [×m]→L[ℂ] BoundedContinuousFunction X ℂ

Pointwise multilinear evaluation on bounded continuous functions, retaining an operator norm bound.

Equations

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

@[simp]

theorem KamProject.Arnold1963.boundedMultilinearLift_apply {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℂ E] {m : ℕ} (p : E [×m]→L[ℂ] ℂ) (v : Fin m → BoundedContinuousFunction X E) (x : X) : ((boundedMultilinearLift p) v) x = p fun (j : Fin m) => (v j) x

theorem KamProject.Arnold1963.norm_boundedMultilinearLift_le {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℂ E] {m : ℕ} (p : E [×m]→L[ℂ] ℂ) : ‖boundedMultilinearLift p‖ ≤ ‖p‖

noncomputable def KamProject.Arnold1963.boundedSeriesLift {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℂ E] (p : FormalMultilinearSeries ℂ E ℂ) : FormalMultilinearSeries ℂ (BoundedContinuousFunction X E) (BoundedContinuousFunction X ℂ)

A formal power series lifted coefficientwise to bounded continuous functions.

Equations

• KamProject.Arnold1963.boundedSeriesLift p m = KamProject.Arnold1963.boundedMultilinearLift (p m)

theorem KamProject.Arnold1963.radius_boundedSeriesLift_le {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℂ E] (p : FormalMultilinearSeries ℂ E ℂ) : p.radius ≤ (boundedSeriesLift p).radius

theorem KamProject.Arnold1963.boundedSeriesLift_sum_apply {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℂ E] (p : FormalMultilinearSeries ℂ E ℂ) {v : BoundedContinuousFunction X E} (hv : v ∈ Metric.eball 0 p.radius) (x : X) : ((boundedSeriesLift p).sum v) x = p.sum (v x)

noncomputable def KamProject.Arnold1963.boundedConstCLM {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℂ E] : E →L[ℂ] BoundedContinuousFunction X E

The continuous linear map sending a vector to its constant function.

Equations

• KamProject.Arnold1963.boundedConstCLM = { toFun := BoundedContinuousFunction.const X, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

@[simp]

theorem KamProject.Arnold1963.boundedConstCLM_apply {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℂ E] (v : E) (x : X) : (boundedConstCLM v) x = v

noncomputable def KamProject.Arnold1963.boundedIntegralCLM {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : BoundedContinuousFunction X ℂ →L[ℂ] ℂ

Integration against a finite measure as a continuous complex linear functional.

Equations

• KamProject.Arnold1963.boundedIntegralCLM μ = { toFun := fun (f : BoundedContinuousFunction X ℂ) => ∫ (x : X), f x ∂μ, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (μ.real Set.univ) ⋯