Public statement.

noncomputable def AVenhance.barNorm (n : ℕ) (R : ℝ) (f : Homogenization.Vec 2 → ℝ) : ENNReal

e.barf (source 933-936): ⟦f⟧_{n,R} = (n+1)²/(n! Rⁿ) · sup_{|α|=n} ‖∂^α f‖_{L^∞(ℝ²)}, for f ∈ C^∞(ℝ²) and radius R > 0 (every use below has R > 0). The supremum over multi-indices |α| = n is the supremum over ordered coordinate tuples i : Fin n → Fin 2 of the iterated derivative on basis vectors (for C^n functions all orderings of one multi-index agree by symmetry of the derivative). ℝ≥0∞-valued, so no supremum is junk; R⁻ⁿ is taken in ℝ≥0∞, so R ≤ 0 gives ⊤ (never a vacuous bound).

Equations

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