A coordinate-seminorm bridge for the paper barNorm.

theorem AVenhance.FaaDiBruno.BarNormBridge.orderedPartial_eq_barCoordinate {n : ℕ} {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑n) f) (x : Homogenization.Vec 2) (I : Fin n → Fin 2) : orderedPartial n f x I = (iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (I j)

theorem AVenhance.FaaDiBruno.BarNormBridge.derivativeSup_eq_barCoordinates {n : ℕ} {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑n) f) : derivativeSup n f = ⨆ (I : Fin n → Fin 2), MeasureTheory.eLpNorm (fun (x : Homogenization.Vec 2) => (iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (I j)) ⊤ MeasureTheory.volume

theorem AVenhance.FaaDiBruno.barNorm_eq_snorm {n : ℕ} {R : ℝ} {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑n) f) : barNorm n R f = snorm f n R

The §1 paper seminorm is exactly the ordered-coordinate seminorm used by the Appendix B composition and transport estimates.