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

theorem AVenhance.Infra.Section4.ThetaClassicalUniqueness.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.Section4.ThetaClassicalUniqueness.continuous_spaceLap {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : Continuous (spaceLap f)

theorem AVenhance.Infra.Section4.ThetaClassicalUniqueness.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.Section4.ThetaClassicalUniqueness.theta_smooth_spaceGrad_sub {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : (spaceGrad fun (x : Homogenization.Vec 2) => f x - g x) = fun (x : Homogenization.Vec 2) => spaceGrad f x - spaceGrad g x

theorem AVenhance.Infra.Section4.ThetaClassicalUniqueness.thetaSpaceGrad_contDiff {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (spaceGrad f)

theorem AVenhance.Infra.Section4.ThetaClassicalUniqueness.theta_smooth_spaceLap_sub {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : (spaceLap fun (x : Homogenization.Vec 2) => f x - g x) = fun (x : Homogenization.Vec 2) => spaceLap f x - spaceLap g x

theorem AVenhance.Infra.Section4.ThetaClassicalUniqueness.thetaTime_continuous_integrableOn_unitCellAt {f : Homogenization.Vec 2 → ℝ} (a : Homogenization.Vec 2) (hf : Continuous f) : MeasureTheory.IntegrableOn f (Torus.unitCellAt 2 a) MeasureTheory.volume

theorem AVenhance.Infra.Section4.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

theorem AVenhance.Infra.Section4.theta_continuous_periodic_eq_zero_of_l2NormSq_eq_zero {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : IsZ2Periodic f) (hzero : l2NormSq f = 0) : f = 0

A continuous periodic datum whose torus L² norm vanishes is pointwise zero. The shifted open cell lets periodicity move the integral away from cell-boundary representatives.