Sharp composition bounds

The analytic composition estimate is proved from the ordered-finpartition Faà di Bruno formula, keeping the paper's coordinate seminorms and constants.

@[instance_reducible]

noncomputable def AVenhance.FaaDiBruno.realMeasureSpace : MeasureTheory.MeasureSpace ℝ

Use Lebesgue measure on real time in the integral estimates.

Equations

• AVenhance.FaaDiBruno.realMeasureSpace = Real.measureSpace

noncomputable def AVenhance.FaaDiBruno.liftVecOneEndo {d : ℕ} (g : Homogenization.Vec d → Homogenization.Vec d) : VecOne d → VecOne d

The map g viewed as an endomorphism of the ℓ¹ copy of Vec d.

Equations

• AVenhance.FaaDiBruno.liftVecOneEndo g = ⇑(AVenhance.FaaDiBruno.vecOneEquiv d).symm ∘ AVenhance.FaaDiBruno.liftVecOne g

@[simp]

theorem AVenhance.FaaDiBruno.liftVecOneEndo_apply {d : ℕ} (g : Homogenization.Vec d → Homogenization.Vec d) (x : VecOne d) : liftVecOneEndo g x = (vecOneEquiv d).symm (g ((vecOneEquiv d) x))

theorem AVenhance.FaaDiBruno.liftVecOne_comp_liftVecOneEndo {d : ℕ} (h : Homogenization.Vec d → ℝ) (g : Homogenization.Vec d → Homogenization.Vec d) : liftVecOne (h ∘ g) = liftVecOne h ∘ liftVecOneEndo g

theorem AVenhance.FaaDiBruno.contDiff_liftVecOneEndo {d m : ℕ} (g : Homogenization.Vec d → Homogenization.Vec d) (hg : ContDiff ℝ (↑m) g) : ContDiff ℝ (↑m) (liftVecOneEndo g)

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

theorem AVenhance.FaaDiBruno.Composition.operatorDerivativeF_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

theorem AVenhance.FaaDiBruno.Composition.operatorDerivativeF_pointwise_le_derivativeSup {d n : ℕ} [Nonempty (Fin d)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec d → F) (hf : ContDiff ℝ (↑n) f) (x : Homogenization.Vec d) : ‖iteratedFDeriv ℝ n (liftVecOne f) (WithLp.toLp 1 x)‖ₑ ≤ derivativeSup n f

theorem AVenhance.FaaDiBruno.Composition.vecOneEquiv_symm_opNorm_le_card {d : ℕ} : ‖↑(vecOneEquiv d).symm‖ ≤ ↑d

theorem AVenhance.FaaDiBruno.derivativeSup_le_of_snorm_le {d n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec d → F) {R C : ℝ} (hR : 0 < R) (hs : snorm f n R ≤ ENNReal.ofReal C) : derivativeSup n f ≤ ENNReal.ofReal (C * ↑n.factorial * R ^ n / (↑n + 1) ^ 2)

Recover the paper's coordinate derivative supremum from its normalized seminorm, with the exact factorial and radius factors.

theorem AVenhance.FaaDiBruno.Composition.liftVecOneEndo_deriv_norm_le {d m r : ℕ} [Nonempty (Fin d)] (g : Homogenization.Vec d → Homogenization.Vec d) (hg : ContDiff ℝ (↑m) g) (hr : r ≤ m) (x : Homogenization.Vec d) {D : ℝ} (hD : derivativeSup r g ≤ ENNReal.ofReal D) (hDnonneg : 0 ≤ D) (hDtop : derivativeSup r g ≠ ⊤) : ‖iteratedFDeriv ℝ r (liftVecOneEndo g) (WithLp.toLp 1 x)‖ ≤ ↑d * D

theorem AVenhance.FaaDiBruno.compositionDerivative_norm_le_of_snorm_le {d m r : ℕ} [Nonempty (Fin d)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec d → F) (hf : ContDiff ℝ (↑m) f) (hr : r ≤ m) {C R : ℝ} (hR : 0 < R) (hC : 0 ≤ C) (hs : snorm f r R ≤ ENNReal.ofReal C) (x : Homogenization.Vec d) : ‖iteratedFDeriv ℝ r (liftVecOne f) (WithLp.toLp 1 x)‖ ≤ C * ↑r.factorial * R ^ r / (↑r + 1) ^ 2

The paper's derivative seminorm controls the full iterated derivative on the ℓ¹ coordinate realization, pointwise and with its exact factorial and radius normalization.

theorem AVenhance.FaaDiBruno.orderedPartial_norm_le_of_snorm_le {d m n : ℕ} [Nonempty (Fin d)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec d → F) (hf : ContDiff ℝ (↑m) f) (hn : n ≤ m) {C R : ℝ} (hR : 0 < R) (hC : 0 ≤ C) (hs : snorm f n R ≤ ENNReal.ofReal C) (x : Homogenization.Vec d) (I : Fin n → Fin d) : ‖orderedPartial n f x I‖ ≤ C * ↑n.factorial * R ^ n / (↑n + 1) ^ 2

Pointwise coordinate partials of any order obey the factorial and radius bound supplied by the paper's seminorm. This is the source-side estimate used when differentiating the transport equation.

theorem AVenhance.FaaDiBruno.fderiv_norm_le_of_snorm_one_le {d : ℕ} [Nonempty (Fin d)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec d → F) (hf : ContDiff ℝ 1 f) {C R : ℝ} (hR : 0 < R) (hC : 0 ≤ C) (hs : snorm f 1 R ≤ ENNReal.ofReal C) (x : Homogenization.Vec d) : ‖fderiv ℝ f x‖ ≤ ↑d * C * R / 4

The paper seminorm bound at order one controls the derivative on the original supremum-norm coordinate space. The factor d is the norm cost of passing from the paper's coordinate ℓ¹ realization back to Vec d.

theorem AVenhance.FaaDiBruno.Composition.one_add_sum_le_prod_add_one {α : Type u_1} (s : Finset α) (f : α → ℕ) : 1 + ∑ i ∈ s, f i ≤ ∏ i ∈ s, (f i + 1)

theorem AVenhance.FaaDiBruno.Composition.composition_partSize_sum {n : ℕ} (c : OrderedFinpartition n) : ∑ i : Fin c.length, c.partSize i = n

theorem AVenhance.FaaDiBruno.Composition.orderedFinpartition_shiftFactor {n : ℕ} (hn : 0 < n) (c : OrderedFinpartition n) : (↑n + 1) ^ 2 ≤ (↑c.length + 1) ^ 2 * ∏ i : Fin c.length, (↑(c.partSize i) + 1) ^ 2

theorem AVenhance.FaaDiBruno.snorm_le_of_derivativeSup_le {d n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec d → F) {R C : ℝ} (hR : 0 < R) (hD : derivativeSup n f ≤ ENNReal.ofReal (C * R ^ n * ↑n.factorial / (↑n + 1) ^ 2)) : snorm f n R ≤ ENNReal.ofReal C

theorem AVenhance.FaaDiBruno.Composition.orderedFinpartition_innerCoefficientProduct {n : ℕ} (c : OrderedFinpartition n) (D R : ℝ) : ∏ i : Fin c.length, D * ↑(c.partSize i).factorial * R ^ c.partSize i / (↑(c.partSize i) + 1) ^ 2 = D ^ c.length * ↑(orderedPartitionFactorialProduct c) * R ^ n / ∏ i : Fin c.length, (↑(c.partSize i) + 1) ^ 2

theorem AVenhance.FaaDiBruno.compositionEstimate10528 {d m : ℕ} [Nonempty (Fin d)] (h : Homogenization.Vec d → ℝ) (g : Homogenization.Vec d → Homogenization.Vec d) (hh : ContDiff ℝ (↑m) h) (hg : ContDiff ℝ (↑m) g) {C_h C_g R_h R_g : ℝ} (hCh : 0 < C_h) (hCg : 0 < C_g) (hRh : 0 < R_h) (hRg : 0 < R_g) (hH : ∀ j ≤ m, snorm h j R_h ≤ ENNReal.ofReal C_h) (hG : ∀ (j : ℕ), 1 ≤ j → j ≤ m → snorm g j R_g ≤ ENNReal.ofReal C_g) (n : ℕ) : n ≤ m → snorm (h ∘ g) n (R_g * (1 + ↑d * C_g * R_h)) ≤ ENNReal.ofReal C_h

Proposition 10528 with the paper's sharp constant and radius.