Public statement.

noncomputable def AVenhance.hMinusOneNorm (h : Homogenization.Vec 2 → ℝ) : ENNReal

‖h‖_{HDot⁻¹(𝕋²)} = sup { ∫_{(0,1)²} h φ : φ ∈ C^∞ periodic, ‖∇φ‖_{L²} ≤ 1 } (the source uses the norm in e.bigbound (7017-7021) and 7047-7078 without a formula). ℝ≥0∞-valued: ⊤ if h has nonzero mean (constants are admissible φ), so no junk value.

Equations

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