Divergence-freeness of finite stream velocities (Lemma r.LeBron, step (b))

The IsDivFree (distributional divergence on each slice) holds for streamVel Ψ with Ψ admissible: the classical divergence vanishes (streamVel_vecDiv_eq_zero) and the velocity is smooth, so integration by parts against compactly supported smooth tests gives zero.

theorem AVenhance.Infra.FullTheorem.isDivFree_of_vecDiv_zero {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : ∀ (t : ℝ) (i : Fin 2), ContDiff ℝ 1 fun (x : Homogenization.Vec 2) => b t x i) (hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), vecDiv (b t) x = 0) : IsDivFree b

A time-indexed family of C¹ fields with vanishing classical divergence is IsDivFree.

theorem AVenhance.Infra.FullTheorem.isDivFree_streamVel {Ψ : ℝ → Homogenization.Vec 2 → ℝ} (hΨ : IsAdmissibleStream Ψ) : IsDivFree (streamVel Ψ)

The velocity of an admissible stream is IsDivFree.