Bounded C^{2,α} maps

This file constructs the normed space of bounded twice continuously differentiable maps whose first derivative is bounded and whose second derivative is bounded and globally Hölder continuous, and proves that it is Banach when the codomain is Banach. Its max norm is equivalent to the usual C^{2,α} norm

‖f‖_∞ + ‖Df‖_∞ + ‖D²f‖_∞ + [D²f]_α.

An element is represented recursively by a bounded value field and a C^{1,α} first-derivative field, subject to the Fréchet derivative identity. The derivative data is therefore uniquely determined. The identity is closed under uniform convergence, which makes the resulting space complete when the codomain is complete. This is the bounded global C^{2,α} target space used by Schauder estimates.

Main declarations

• TauCeti.C2HolderSpace: bounded C² maps with bounded first derivative and bounded globally α-Hölder second derivative.
• TauCeti.C2HolderSpace.fderiv: the bounded continuous first derivative field.
• TauCeti.C2HolderSpace.secondFDeriv: the globally Hölder second derivative field.
• TauCeti.C2HolderSpace.instCompleteSpace: completeness when the codomain is complete.

References

L. C. Evans, Partial Differential Equations, Section 6.3; D. Gilbarg and N. Trudinger, Elliptic Partial Differential Equations of Second Order, Section 4.1.

@[irreducible]

def TauCeti.C2HolderSpace (α : NNReal) (E : Type u) (F : Type v) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : Type (max u v)

The space of bounded C² maps whose first derivative is bounded and whose second derivative is bounded and globally α-Hölder. Its inherited product norm is

max ‖f‖_∞ (max ‖Df‖_∞ (‖D²f‖_∞ + [D²f]_α)).

Equations

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

@[irreducible]

noncomputable instance TauCeti.C2HolderSpace.instNormedAddCommGroup {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddCommGroup (C2HolderSpace α E F)

Equations

• TauCeti.C2HolderSpace.instNormedAddCommGroup = id inferInstance

@[irreducible]

noncomputable instance TauCeti.C2HolderSpace.instNormedSpace {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ (C2HolderSpace α E F)

Equations

• TauCeti.C2HolderSpace.instNormedSpace = id inferInstance

def TauCeti.C2HolderSpace.toBoundedContinuousFunction {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : BoundedContinuousFunction E F

The underlying bounded continuous function.

Equations

• f.toBoundedContinuousFunction = (↑f).1

@[irreducible]

instance TauCeti.C2HolderSpace.instCoeFun {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : CoeFun (C2HolderSpace α E F) fun (x : C2HolderSpace α E F) => E → F

A bounded C^{2,α} element coerces to its underlying function from E to F.

Equations

• TauCeti.C2HolderSpace.instCoeFun = { coe := fun (f : TauCeti.C2HolderSpace α E F) => ⇑(↑f).1 }

@[simp]

theorem TauCeti.C2HolderSpace.toBoundedContinuousFunction_apply {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) (x : E) : f.toBoundedContinuousFunction x = CoeFun.coe f x

def TauCeti.C2HolderSpace.fderivC1 {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : C1HolderSpace α E (E →L[ℝ] F)

The first derivative field, retaining its C^{1,α} structure.

Equations

• f.fderivC1 = (↑f).2

noncomputable def TauCeti.C2HolderSpace.fderiv {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : BoundedContinuousFunction E (E →L[ℝ] F)

The first derivative as a bounded continuous field.

Equations

• f.fderiv = TauCeti.C1HolderSpace.valueL f.fderivC1

noncomputable def TauCeti.C2HolderSpace.secondFDeriv {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : HolderSpace α E (E →L[ℝ] E →L[ℝ] F)

The second derivative as a bounded globally Hölder field.

Equations

• f.secondFDeriv = TauCeti.C1HolderSpace.fderivL f.fderivC1

@[simp]

theorem TauCeti.C2HolderSpace.toBoundedContinuousFunction_fderivC1 {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : f.fderivC1.toBoundedContinuousFunction = f.fderiv

@[simp]

theorem TauCeti.C2HolderSpace.fderiv_fderivC1 {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : f.fderivC1.fderiv = f.secondFDeriv

noncomputable def TauCeti.C2HolderSpace.mk {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : BoundedContinuousFunction E F) (f' : BoundedContinuousFunction E (E →L[ℝ] F)) (f'' : HolderSpace α E (E →L[ℝ] E →L[ℝ] F)) (hf : ∀ (x : E), HasFDerivAt (⇑f) (f' x) x) (hf' : ∀ (x : E), HasFDerivAt (⇑f') (↑f''.toHolderSubmodule x) x) : C2HolderSpace α E F

Construct a bounded C^{2,α} map from a function and two compatible derivative fields.

Equations

• TauCeti.C2HolderSpace.mk f f' f'' hf hf' = ⟨(f, TauCeti.C1HolderSpace.mk f' f'' hf'), ⋯⟩

@[simp]

theorem TauCeti.C2HolderSpace.toBoundedContinuousFunction_mk {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : BoundedContinuousFunction E F) (f' : BoundedContinuousFunction E (E →L[ℝ] F)) (f'' : HolderSpace α E (E →L[ℝ] E →L[ℝ] F)) (hf : ∀ (x : E), HasFDerivAt (⇑f) (f' x) x) (hf' : ∀ (x : E), HasFDerivAt (⇑f') (↑f''.toHolderSubmodule x) x) : (mk f f' f'' hf hf').toBoundedContinuousFunction = f

@[simp]

theorem TauCeti.C2HolderSpace.fderivC1_mk {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : BoundedContinuousFunction E F) (f' : BoundedContinuousFunction E (E →L[ℝ] F)) (f'' : HolderSpace α E (E →L[ℝ] E →L[ℝ] F)) (hf : ∀ (x : E), HasFDerivAt (⇑f) (f' x) x) (hf' : ∀ (x : E), HasFDerivAt (⇑f') (↑f''.toHolderSubmodule x) x) : (mk f f' f'' hf hf').fderivC1 = C1HolderSpace.mk f' f'' hf'

@[simp]

theorem TauCeti.C2HolderSpace.fderiv_mk {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : BoundedContinuousFunction E F) (f' : BoundedContinuousFunction E (E →L[ℝ] F)) (f'' : HolderSpace α E (E →L[ℝ] E →L[ℝ] F)) (hf : ∀ (x : E), HasFDerivAt (⇑f) (f' x) x) (hf' : ∀ (x : E), HasFDerivAt (⇑f') (↑f''.toHolderSubmodule x) x) : (mk f f' f'' hf hf').fderiv = f'

@[simp]

theorem TauCeti.C2HolderSpace.secondFDeriv_mk {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : BoundedContinuousFunction E F) (f' : BoundedContinuousFunction E (E →L[ℝ] F)) (f'' : HolderSpace α E (E →L[ℝ] E →L[ℝ] F)) (hf : ∀ (x : E), HasFDerivAt (⇑f) (f' x) x) (hf' : ∀ (x : E), HasFDerivAt (⇑f') (↑f''.toHolderSubmodule x) x) : (mk f f' f'' hf hf').secondFDeriv = f''

noncomputable def TauCeti.C2HolderSpace.const {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (c : F) : C2HolderSpace α E F

The constant map as a bounded C^{2,α} map.

Equations

• TauCeti.C2HolderSpace.const c = TauCeti.C2HolderSpace.mk (BoundedContinuousFunction.const E c) (BoundedContinuousFunction.const E 0) 0 ⋯ ⋯

@[simp]

theorem TauCeti.C2HolderSpace.const_apply {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (c : F) (x : E) : CoeFun.coe (const c) x = c

@[simp]

theorem TauCeti.C2HolderSpace.fderiv_const {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (c : F) : (const c).fderiv = 0

@[simp]

theorem TauCeti.C2HolderSpace.secondFDeriv_const {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (c : F) : (const c).secondFDeriv = 0

theorem TauCeti.C2HolderSpace.hasFDerivAt {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) (x : E) : HasFDerivAt (CoeFun.coe f) (f.fderiv x) x

The recorded first derivative is the Fréchet derivative of the underlying function.

@[simp]

theorem TauCeti.C2HolderSpace.fderiv_eq {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) (x : E) : _root_.fderiv ℝ (CoeFun.coe f) x = f.fderiv x

The first derivative accessor agrees with Mathlib's fderiv.

theorem TauCeti.C2HolderSpace.fderiv_eq_fderiv {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : _root_.fderiv ℝ (CoeFun.coe f) = ⇑f.fderiv

The Fréchet derivative agrees with the recorded derivative field.

theorem TauCeti.C2HolderSpace.differentiable {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : Differentiable ℝ (CoeFun.coe f)

A bounded C^{2,α} map is differentiable.

theorem TauCeti.C2HolderSpace.hasFDerivAt_fderiv {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) (x : E) : HasFDerivAt (⇑f.fderiv) (↑f.secondFDeriv.toHolderSubmodule x) x

The recorded second derivative is the Fréchet derivative of the first derivative field.

@[simp]

theorem TauCeti.C2HolderSpace.fderiv_fderiv_eq {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) (x : E) : _root_.fderiv ℝ (⇑f.fderiv) x = ↑f.secondFDeriv.toHolderSubmodule x

The second derivative accessor agrees with the Fréchet derivative of the first derivative field.

theorem TauCeti.C2HolderSpace.contDiff_two {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : ContDiff ℝ 2 (CoeFun.coe f)

A bounded C^{2,α} map is twice continuously differentiable.

theorem TauCeti.C2HolderSpace.memHolder_secondFDeriv {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : MemHolder α fun (x : E) => _root_.fderiv ℝ (_root_.fderiv ℝ (CoeFun.coe f)) x

The second Fréchet derivative of the underlying function is globally α-Hölder.

theorem TauCeti.C2HolderSpace.memHolder_iteratedFDeriv_two {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : MemHolder α (iteratedFDeriv ℝ 2 (CoeFun.coe f))

The canonical second iterated Fréchet derivative is globally α-Hölder.

theorem TauCeti.C2HolderSpace.ext {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f g : C2HolderSpace α E F} (h : ∀ (x : E), CoeFun.coe f x = CoeFun.coe g x) : f = g

Two bounded C^{2,α} maps are equal when their underlying functions agree pointwise.

theorem TauCeti.C2HolderSpace.ext_iff {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f g : C2HolderSpace α E F} : f = g ↔ ∀ (x : E), CoeFun.coe f x = CoeFun.coe g x

noncomputable def TauCeti.C2HolderSpace.fderivC1L {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : C2HolderSpace α E F →L[ℝ] C1HolderSpace α E (E →L[ℝ] F)

Returning the C^{1,α} first-derivative field is a continuous linear map.

Equations

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

@[simp]

theorem TauCeti.C2HolderSpace.fderivC1L_apply {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : fderivC1L f = f.fderivC1

@[simp]

theorem TauCeti.C2HolderSpace.fderivC1_const {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (c : F) : (const c).fderivC1 = 0

@[simp]

theorem TauCeti.C2HolderSpace.fderivC1_zero {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : fderivC1 0 = 0

@[simp]

theorem TauCeti.C2HolderSpace.fderivC1_add {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f g : C2HolderSpace α E F) : (f + g).fderivC1 = f.fderivC1 + g.fderivC1

@[simp]

theorem TauCeti.C2HolderSpace.fderivC1_smul {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (c : ℝ) (f : C2HolderSpace α E F) : (c • f).fderivC1 = c • f.fderivC1

noncomputable def TauCeti.C2HolderSpace.valueL {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : C2HolderSpace α E F →L[ℝ] BoundedContinuousFunction E F

Forgetting the derivatives defines a continuous linear map to bounded continuous functions.

Equations

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

@[simp]

theorem TauCeti.C2HolderSpace.valueL_apply {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : valueL f = f.toBoundedContinuousFunction

noncomputable def TauCeti.C2HolderSpace.fderivL {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : C2HolderSpace α E F →L[ℝ] BoundedContinuousFunction E (E →L[ℝ] F)

Returning the first derivative defines a continuous linear map to bounded continuous fields.

Equations

• TauCeti.C2HolderSpace.fderivL = TauCeti.C1HolderSpace.valueL ∘SL TauCeti.C2HolderSpace.fderivC1L

@[simp]

theorem TauCeti.C2HolderSpace.fderivL_apply {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : fderivL f = f.fderiv

noncomputable def TauCeti.C2HolderSpace.secondFDerivL {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : C2HolderSpace α E F →L[ℝ] HolderSpace α E (E →L[ℝ] E →L[ℝ] F)

Returning the second derivative defines a continuous linear map to its Hölder space.

Equations

• TauCeti.C2HolderSpace.secondFDerivL = TauCeti.C1HolderSpace.fderivL ∘SL TauCeti.C2HolderSpace.fderivC1L

@[simp]

theorem TauCeti.C2HolderSpace.secondFDerivL_apply {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : secondFDerivL f = f.secondFDeriv

@[simp]

theorem TauCeti.C2HolderSpace.toBoundedContinuousFunction_zero {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : toBoundedContinuousFunction 0 = 0

@[simp]

theorem TauCeti.C2HolderSpace.fderiv_zero {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : fderiv 0 = 0

@[simp]

theorem TauCeti.C2HolderSpace.secondFDeriv_zero {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : secondFDeriv 0 = 0

@[simp]

theorem TauCeti.C2HolderSpace.toBoundedContinuousFunction_add {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f g : C2HolderSpace α E F) : (f + g).toBoundedContinuousFunction = f.toBoundedContinuousFunction + g.toBoundedContinuousFunction

@[simp]

theorem TauCeti.C2HolderSpace.fderiv_add {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f g : C2HolderSpace α E F) : (f + g).fderiv = f.fderiv + g.fderiv

@[simp]

theorem TauCeti.C2HolderSpace.secondFDeriv_add {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f g : C2HolderSpace α E F) : (f + g).secondFDeriv = f.secondFDeriv + g.secondFDeriv

@[simp]

theorem TauCeti.C2HolderSpace.toBoundedContinuousFunction_smul {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (c : ℝ) (f : C2HolderSpace α E F) : (c • f).toBoundedContinuousFunction = c • f.toBoundedContinuousFunction

@[simp]

theorem TauCeti.C2HolderSpace.fderiv_smul {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (c : ℝ) (f : C2HolderSpace α E F) : (c • f).fderiv = c • f.fderiv

@[simp]

theorem TauCeti.C2HolderSpace.secondFDeriv_smul {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (c : ℝ) (f : C2HolderSpace α E F) : (c • f).secondFDeriv = c • f.secondFDeriv

@[simp]

theorem TauCeti.C2HolderSpace.zero_apply {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (x : E) : CoeFun.coe 0 x = 0

@[simp]

theorem TauCeti.C2HolderSpace.add_apply {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f g : C2HolderSpace α E F) (x : E) : CoeFun.coe (f + g) x = CoeFun.coe f x + CoeFun.coe g x

@[simp]

theorem TauCeti.C2HolderSpace.smul_apply {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (c : ℝ) (f : C2HolderSpace α E F) (x : E) : CoeFun.coe (c • f) x = c • CoeFun.coe f x

theorem TauCeti.C2HolderSpace.norm_eq_max {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : ‖f‖ = max ‖f.toBoundedContinuousFunction‖ (max ‖f.fderiv‖ ‖f.secondFDeriv‖)

The C^{2,α} norm is the maximum of the two supremum norms and the second-derivative Hölder norm.

theorem TauCeti.C2HolderSpace.norm_toBoundedContinuousFunction_le {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : ‖f.toBoundedContinuousFunction‖ ≤ ‖f‖

The supremum norm of the function is controlled by its C^{2,α} norm.

theorem TauCeti.C2HolderSpace.norm_fderiv_le {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : ‖f.fderiv‖ ≤ ‖f‖

The supremum norm of the first derivative is controlled by its C^{2,α} norm.

theorem TauCeti.C2HolderSpace.norm_secondFDeriv_le {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : C2HolderSpace α E F) : ‖f.secondFDeriv‖ ≤ ‖f‖

The Hölder norm of the second derivative is controlled by its C^{2,α} norm.

instance TauCeti.C2HolderSpace.instCompleteSpace {α : NNReal} {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] : CompleteSpace (C2HolderSpace α E F)

Bounded C^{2,α} maps into a Banach space form a Banach space.