Public statement.

def AVenhance.IsTransportWeakSolution (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (θ₀ : Homogenization.Vec 2 → ℝ) (θ : ℝ → Homogenization.Vec 2 → ℝ) : Prop

Weak solution on [0,1] × 𝕋² of the transport equation ∂ₜθ + b·∇θ = 0, θ(0) = θ₀ (the κ = 0 limit, source line 10132), in divergence form ∂ₜθ + ∇·(bθ) = 0, which is the same equation for divergence-free b. Same regularity carriers, weak continuity and test class as IsWeakSolutionGrad, minus the H¹ gradient; the drift integrand is required integrable so no integral takes the Bochner junk value.

Equations

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