Public statement.

def AVenhance.IsThetaAnalytic (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) : Prop

e.theta0.anal (3835-3838) = e.theta0.anal.encore (8030-8035): with ‖∇ⁿ f‖_X := max_{|α|=n} ‖∂^α f‖_X (e.nabla.n, 944) the two displays coincide. The maximum over multi-indices is expressed as a bound for every ordered coordinate tuple i : Fin n → Fin 2 (as in barNorm; equal for C^n functions by symmetry of the derivative), for every n ∈ ℕ = {1,2,…}.

Equations

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