L² energy uniqueness for smooth periodic advection-diffusion solutions.

theorem AVenhance.Infra.Classical.Uniqueness.continuous_spaceGrad_component {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i : Fin 2) : Continuous fun (x : Homogenization.Vec 2) => spaceGrad f x i

theorem AVenhance.Infra.Classical.Uniqueness.continuous_spaceLap {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : Continuous (spaceLap f)

theorem AVenhance.Infra.Classical.Uniqueness.continuous_vecDot {f g : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : Homogenization.Vec 2) => Homogenization.vecDot (f x) (g x)

theorem AVenhance.Infra.Classical.streamVel_classical_unique (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) {θ ψ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsClassicalSol (streamVel φ) κ F θ₀ θ) (hψ : IsClassicalSol (streamVel φ) κ F θ₀ ψ) (t : ℝ) : 0 ≤ t → ∀ (x : Homogenization.Vec 2), ψ t x = θ t x