Jointly smooth functions as smooth families on a compact set

This generalizes SmoothPathFamily from a compact real interval to any compact subset of a real normed space. The Fréchet derivative in the supremum norm is proved by a uniform mean-value remainder estimate.

noncomputable def NavierStokes.CompactSmoothFamily.family {P Z E : Type u} [NormedAddCommGroup Z] [NormedAddCommGroup E] (K : Set Z) (F : P × Z → E) (p : P) : C(↑K, E)

The actual slice when continuous, with a zero fallback outside the domain where the hypotheses guarantee continuity.

Equations

• NavierStokes.CompactSmoothFamily.family K F p = if h : Continuous fun (z : ↑K) => F (p, ↑z) then { toFun := fun (z : ↑K) => F (p, ↑z), continuous_toFun := h } else 0

theorem NavierStokes.CompactSmoothFamily.family_apply {P Z E : Type u} [NormedAddCommGroup Z] [NormedAddCommGroup E] (K : Set Z) (F : P × Z → E) (p : P) (hp : Continuous fun (z : ↑K) => F (p, ↑z)) (z : ↑K) : (family K F p) z = F (p, ↑z)

theorem NavierStokes.CompactSmoothFamily.slice_continuous {P Z E : Type u} [NormedAddCommGroup P] [NormedAddCommGroup Z] [NormedAddCommGroup E] {K : Set Z} {U : Set P} {F : P × Z → E} (hF : ContinuousOn F (U ×ˢ K)) {p : P} (hp : p ∈ U) : Continuous fun (z : ↑K) => F (p, ↑z)

theorem NavierStokes.CompactSmoothFamily.continuousOn_family {P Z E : Type u} [NormedAddCommGroup P] [NormedAddCommGroup Z] [NormedAddCommGroup E] {K : Set Z} {U : Set P} {F : P × Z → E} (hF : ContinuousOn F (U ×ˢ K)) : ContinuousOn (family K F) U

noncomputable def NavierStokes.CompactSmoothFamily.flipLinear {P Z E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Z] [NormedAddCommGroup E] [NormedSpace ℝ E] (K : Set Z) : C(↑K, P →L[ℝ] E) →ₗ[ℝ] P →ₗ[ℝ] C(↑K, E)

Flip linear, bundling toFun, toFun, map_add, map_smul and the required compatibility proofs.

Equations

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

theorem NavierStokes.CompactSmoothFamily.norm_flipLinear_le {P Z E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Z] [NormedAddCommGroup E] [NormedSpace ℝ E] (K : Set Z) [CompactSpace ↑K] (g : C(↑K, P →L[ℝ] E)) (v : P) : ‖((flipLinear K) g) v‖ ≤ ‖g‖ * ‖v‖

noncomputable def NavierStokes.CompactSmoothFamily.flipCLM {P Z E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Z] [NormedAddCommGroup E] [NormedSpace ℝ E] (K : Set Z) [CompactSpace ↑K] : C(↑K, P →L[ℝ] E) →L[ℝ] P →L[ℝ] C(↑K, E)

Flip continuous linear map as an element of C(K, P →L[ℝ] E) →L[ℝ] P →L[ℝ] C(K, E).

Equations

• NavierStokes.CompactSmoothFamily.flipCLM K = (NavierStokes.CompactSmoothFamily.flipLinear K).mkContinuous₂ 1 ⋯

theorem NavierStokes.CompactSmoothFamily.flipCLM_apply {P Z E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Z] [NormedAddCommGroup E] [NormedSpace ℝ E] (K : Set Z) [CompactSpace ↑K] (g : C(↑K, P →L[ℝ] E)) (v : P) (z : ↑K) : (((flipCLM K) g) v) z = (g z) v

theorem NavierStokes.CompactSmoothFamily.hasFDerivAt_family {P Z E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Z] [NormedAddCommGroup E] [NormedSpace ℝ E] (K : Set Z) [CompactSpace ↑K] {U : Set P} (hU : IsOpen U) (F : P × Z → E) (G : P × Z → P →L[ℝ] E) (hF : ContinuousOn F (U ×ˢ K)) (hG : ContinuousOn G (U ×ˢ K)) (hderiv : ∀ p ∈ U, ∀ (z : ↑K), HasFDerivAt (fun (q : P) => F (q, ↑z)) (G (p, ↑z)) p) {p : P} (hp : p ∈ U) : HasFDerivAt (family K F) ((flipCLM K) (family K G p)) p

Actual slice derivatives and their joint continuity give the Fréchet derivative of the compact-family map in the supremum norm.

noncomputable def NavierStokes.CompactSmoothFamily.parameterDerivative {P Z E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Z] [NormedSpace ℝ Z] [NormedAddCommGroup E] [NormedSpace ℝ E] (F : P × Z → E) (z : P × Z) : P →L[ℝ] E

Parameter derivative, given by (fderiv ℝ F z).comp (ContinuousLinearMap.inl ℝ P Z).

Equations

• NavierStokes.CompactSmoothFamily.parameterDerivative F z = fderiv ℝ F z ∘SL ContinuousLinearMap.inl ℝ P Z

theorem NavierStokes.CompactSmoothFamily.contDiffOn_family_nat {P Z : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Z] [NormedSpace ℝ Z] (K : Set Z) [CompactSpace ↑K] (U : Set P) (V : Set Z) (hU : IsOpen U) (hV : IsOpen V) (hK : K ⊆ V) (n : ℕ) {W : Type u} [NormedAddCommGroup W] [NormedSpace ℝ W] (F : P × Z → W) : ContDiffOn ℝ (↑n) F (U ×ˢ V) → ContDiffOn ℝ (↑n) (family K F) U

Every finite joint differentiability order lifts to the compact-family space.

theorem NavierStokes.CompactSmoothFamily.contDiffOn_family_of_joint {P Z E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Z] [NormedSpace ℝ Z] [NormedAddCommGroup E] [NormedSpace ℝ E] (K : Set Z) [CompactSpace ↑K] (U : Set P) (V : Set Z) (hU : IsOpen U) (hV : IsOpen V) (hK : K ⊆ V) (F : P × Z → E) (hF : ContDiffOn ℝ (↑⊤) F (U ×ˢ V)) : ContDiffOn ℝ (↑⊤) (family K F) U

Joint smoothness near the compact set gives smoothness in the supremum norm.

theorem NavierStokes.CompactSmoothFamily.iteratedFDeriv_family_apply {P Z E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Z] [NormedSpace ℝ Z] [NormedAddCommGroup E] [NormedSpace ℝ E] (K : Set Z) [CompactSpace ↑K] (U : Set P) (V : Set Z) (hU : IsOpen U) (hV : IsOpen V) (hK : K ⊆ V) (F : P × Z → E) (hF : ContDiffOn ℝ (↑⊤) F (U ×ˢ V)) {p : P} (hp : p ∈ U) (k : ℕ) (v : Fin k → P) (z : ↑K) : ((iteratedFDeriv ℝ k (family K F) p) v) z = (iteratedFDeriv ℝ k (fun (q : P) => F (q, ↑z)) p) v

Evaluating an actual compact-family jet gives the genuine parameter jet of the original fixed-point slice.

theorem NavierStokes.CompactSmoothFamily.family_apply_of_joint {P Z E : Type u} [NormedAddCommGroup P] [NormedAddCommGroup Z] [NormedAddCommGroup E] (K : Set Z) {U : Set P} {V : Set Z} (hK : K ⊆ V) (F : P × Z → E) (hF : ContinuousOn F (U ×ˢ V)) {p : P} (hp : p ∈ U) (z : ↑K) : (family K F p) z = F (p, ↑z)

theorem NavierStokes.CompactSmoothFamily.contDiffOn_family_of_neighborhood {P Z E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Z] [NormedSpace ℝ Z] [NormedAddCommGroup E] [NormedSpace ℝ E] (K : Set Z) [CompactSpace ↑K] (U : Set P) (W : Set (P × Z)) (hW : IsOpen W) (hUK : U ×ˢ K ⊆ W) (F : P × Z → E) (hF : ContDiffOn ℝ (↑⊤) F W) : ContDiffOn ℝ (↑⊤) (family K F) U

An arbitrary open neighborhood of U × K suffices; a fixed product neighborhood is extracted locally at each parameter using compactness.

theorem NavierStokes.CompactSmoothFamily.iteratedFDeriv_family_apply_of_neighborhood {P Z E : Type u} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Z] [NormedSpace ℝ Z] [NormedAddCommGroup E] [NormedSpace ℝ E] (K : Set Z) [CompactSpace ↑K] (U : Set P) (W : Set (P × Z)) (hW : IsOpen W) (hUK : U ×ˢ K ⊆ W) (F : P × Z → E) (hF : ContDiffOn ℝ (↑⊤) F W) {p : P} (hp : p ∈ U) (k : ℕ) (v : Fin k → P) (z : ↑K) : ((iteratedFDeriv ℝ k (family K F) p) v) z = (iteratedFDeriv ℝ k (fun (q : P) => F (q, ↑z)) p) v