Uniqueness in the weak-solution class

Subtracting two weak solutions gives a zero-data weak solution. Its energy vanishes, and the cellwise L² norm identity implies equality almost everywhere on every time slice.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weak_solutionGrad_unique {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ η : ℝ → Homogenization.Vec 2 → ℝ} {D E : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hθ₀ : Homogenization.MemL2On unitCube θ₀) (hη : IsWeakSolutionGrad b κ θ₀ η E) (hθ : IsWeakSolutionGrad b κ θ₀ θ D) (hb_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) (hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C) (hκ : 0 < κ) (t : ℝ) : t ∈ Set.Icc 0 1 → η t =ᵐ[MeasureTheory.volume.restrict unitCube] θ t

Two weak solutions with the same datum agree cell-a.e. at every time.