Statement file: IsDivFree (Roots). This file contains exactly one declaration of the formalization's public statement surface.

def AVenhance.IsDivFree (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : Prop

Distributional divergence-free on each time slice t ∈ [0,1]. Meaningful only together with local integrability of b t (in the main theorem it is conjoined with IsHolderClass, which gives continuity and boundedness).

Equations

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