Appendix B derivative seminorms

The coordinate derivatives of order n are represented by evaluating the iterated Fréchet derivative on coordinate basis vectors. An ordered list of coordinate directions presents a multi-index, and the API groups these lists by their multiplicities. For smooth functions, identifying all orderings of the same multi-index uses the symmetry of iterated derivatives.

@[reducible, inline]

abbrev AVenhance.FaaDiBruno.VecOne (d : ℕ) : Type

The ℓ¹-normed version of the coordinate space. It is used internally to identify the operator norm of a multilinear derivative with the supremum of its coordinate partials.

Equations

• AVenhance.FaaDiBruno.VecOne d = PiLp 1 fun (x : Fin d) => ℝ

noncomputable def AVenhance.FaaDiBruno.vecOneEquiv (d : ℕ) : VecOne d ≃L[ℝ] Homogenization.Vec d

The canonical linear homeomorphism from the ℓ¹ copy to Vec d.

Equations

• AVenhance.FaaDiBruno.vecOneEquiv d = PiLp.continuousLinearEquiv 1 ℝ fun (x : Fin d) => ℝ

noncomputable def AVenhance.FaaDiBruno.liftVecOne {d : ℕ} {F : Type u_1} (f : Homogenization.Vec d → F) : VecOne d → F

The function f viewed on the ℓ¹ copy of the coordinate space.

Equations

• AVenhance.FaaDiBruno.liftVecOne f = f ∘ ⇑(AVenhance.FaaDiBruno.vecOneEquiv d)

@[simp]

theorem AVenhance.FaaDiBruno.liftVecOne_toLp {d : ℕ} {F : Type u_1} (f : Homogenization.Vec d → F) (x : Homogenization.Vec d) : liftVecOne f (WithLp.toLp 1 x) = f x

noncomputable def AVenhance.FaaDiBruno.vecVolume (d : ℕ) : MeasureTheory.Measure (Homogenization.Vec d)

Product Lebesgue measure on the coordinate realization Vec d.

Equations

• AVenhance.FaaDiBruno.vecVolume d = MeasureTheory.Measure.pi fun (x : Fin d) => MeasureTheory.volume

def AVenhance.FaaDiBruno.coordinateVector (d : ℕ) (i : Fin d) : Homogenization.Vec d

The coordinate basis vector associated to i : Fin d.

Equations

• AVenhance.FaaDiBruno.coordinateVector d i = Pi.single i 1

def AVenhance.FaaDiBruno.coordinateVectorOne (d : ℕ) (i : Fin d) : VecOne d

The coordinate vector in the ℓ¹ copy.

Equations

• AVenhance.FaaDiBruno.coordinateVectorOne d i = PiLp.single 1 i 1

@[simp]

theorem AVenhance.FaaDiBruno.coordinateVectorOne_apply {d : ℕ} (i j : Fin d) : (coordinateVectorOne d i).ofLp j = if j = i then 1 else 0

theorem AVenhance.FaaDiBruno.coordinateVectorOne_norm {d : ℕ} (i : Fin d) : ‖coordinateVectorOne d i‖ = 1

theorem AVenhance.FaaDiBruno.Seminorm.coordinateTupleNonempty (d n : ℕ) [Nonempty (Fin d)] : Finset.univ.Nonempty

On the ℓ¹ copy of Vec d, the operator norm of a multilinear map is bounded by its largest value on tuples of coordinate vectors.

def AVenhance.FaaDiBruno.coordinateEvaluationSup {d n : ℕ} [Nonempty (Fin d)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (T : VecOne d [×n]→L[ℝ] F) : ℝ

Maximum norm of a multilinear map evaluated on coordinate basis tuples.

Equations

• AVenhance.FaaDiBruno.coordinateEvaluationSup T = Finset.univ.sup' ⋯ fun (I : Fin n → Fin d) => ‖T fun (j : Fin n) => AVenhance.FaaDiBruno.coordinateVectorOne d (I j)‖

theorem AVenhance.FaaDiBruno.norm_continuousMultilinearMap_le_coordinateEvaluationSup {d n : ℕ} [Nonempty (Fin d)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (T : VecOne d [×n]→L[ℝ] F) : ‖T‖ ≤ coordinateEvaluationSup T

noncomputable def AVenhance.FaaDiBruno.orderedPartial {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ) (f : Homogenization.Vec d → F) (x : Homogenization.Vec d) (I : Fin n → Fin d) : F

The order-n coordinate partial of f, with the coordinate directions listed in I. This is an iterated Fréchet derivative evaluated on basis vectors.

Equations

• AVenhance.FaaDiBruno.orderedPartial n f x I = (iteratedFDeriv ℝ n (AVenhance.FaaDiBruno.liftVecOne f) (WithLp.toLp 1 x)) fun (j : Fin n) => AVenhance.FaaDiBruno.coordinateVectorOne d (I j)

noncomputable def AVenhance.FaaDiBruno.partialSup {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ) (f : Homogenization.Vec d → F) (I : Fin n → Fin d) : ENNReal

The global supremum of the derivative in the multi-index represented by I. For continuous derivatives this is the pointwise representative of the paper's L∞ norm.

Equations

• AVenhance.FaaDiBruno.partialSup n f I = MeasureTheory.eLpNormEssSup (fun (x : Homogenization.Vec d) => AVenhance.FaaDiBruno.orderedPartial n f x I) (AVenhance.FaaDiBruno.vecVolume d)

noncomputable def AVenhance.FaaDiBruno.derivativeSup {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ) (f : Homogenization.Vec d → F) : ENNReal

The order-n derivative L∞ seminorm.

Equations

• AVenhance.FaaDiBruno.derivativeSup n f = ⨆ (I : Fin n → Fin d), AVenhance.FaaDiBruno.partialSup n f I

noncomputable def AVenhance.FaaDiBruno.operatorDerivativeSup {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ) (f : Homogenization.Vec d → F) : ENNReal

The essential supremum of the operator norm of the derivative on the ℓ¹ copy of the coordinate domain.

Equations

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

theorem AVenhance.FaaDiBruno.orderedPartial_norm_le_operatorDerivative {d n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec d → F) (x : Homogenization.Vec d) (I : Fin n → Fin d) : ‖orderedPartial n f x I‖ ≤ ‖iteratedFDeriv ℝ n (liftVecOne f) (WithLp.toLp 1 x)‖

A coordinate derivative is bounded by the operator norm of the full multilinear derivative on the ℓ¹ coordinate space.

theorem AVenhance.FaaDiBruno.derivativeSup_le_operatorDerivativeSup {d n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec d → F) : derivativeSup n f ≤ operatorDerivativeSup n f

The coordinate derivative seminorm is bounded by the operator-derivative essential supremum.

theorem AVenhance.FaaDiBruno.operatorDerivative_ae_le_derivativeSup {d n : ℕ} [Nonempty (Fin d)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec d → F) : ∀ᵐ (x : (i : Fin d) → (fun (x : Fin d) => ℝ) i) ∂vecVolume d, ‖iteratedFDeriv ℝ n (liftVecOne f) (WithLp.toLp 1 x)‖ₑ ≤ derivativeSup n f

noncomputable def AVenhance.FaaDiBruno.snorm {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec d → F) (n : ℕ) (R : ℝ) : ENNReal

The Appendix B seminorm ⟦f⟧_{n,R}. The radius is represented by an extended-real inverse power, so the definition is total; all source estimates assume 0 < R.

Equations

• AVenhance.FaaDiBruno.snorm f n R = ENNReal.ofReal ((↑n + 1) ^ 2 / ↑n.factorial) * (ENNReal.ofReal R)⁻¹ ^ n * AVenhance.FaaDiBruno.derivativeSup n f

theorem AVenhance.FaaDiBruno.contDiff_liftVecOne {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {f : Homogenization.Vec d → F} (hf : ContDiff ℝ (↑n) f) : ContDiff ℝ (↑n) (liftVecOne f)

Smoothness is preserved when the domain is viewed with the equivalent ℓ¹ product norm.