Weak solutions satisfy the divergence-form transport identity up to the viscous term

For θ a weak solution of the advection-diffusion equation with divergence-free drift b and every test function φ, ∫∫ (-θ ∂ₜφ - θ b·∇φ) = ∫ θ₀ φ(0) - κ ∫∫ Dθ·∇φ.

theorem AVenhance.Infra.FullTheorem.TransportLimit.solutionFiniteUnitCube : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.FullTheorem.TransportLimit.openCylinder_measure_eq : MeasureTheory.volume.restrict (Set.Ioo 0 1 ×ˢ Set.univ) = (MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod MeasureTheory.volume

theorem AVenhance.Infra.FullTheorem.TransportLimit.DriftHyp.slice_meas {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (h : DriftHyp b) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 1), MeasureTheory.AEStronglyMeasurable (fun (x : Homogenization.Vec 2) => b t x) MeasureTheory.volume

A.e. in time, the drift slice is measurable.

theorem AVenhance.Infra.FullTheorem.TransportLimit.drift_pairing_swap {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (h : DriftHyp b) {θ : ℝ → Homogenization.Vec 2 → ℝ} {Dθ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hH1 : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 1), IsPeriodicH1With (θ t) (Dθ t)) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsTestFunction φ) (iB : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (b p.1 p.2) (Dθ p.1 p.2) * φ p.1 p.2) (MeasureTheory.volume.restrict timeCube)) (iT : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => θ p.1 p.2 * Homogenization.vecDot (b p.1 p.2) (spaceGrad (φ p.1) p.2)) (MeasureTheory.volume.restrict timeCube)) : ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, Homogenization.vecDot (b p.1 p.2) (Dθ p.1 p.2) * φ p.1 p.2 = -∫ (p : ℝ × Homogenization.Vec 2) in timeCube, θ p.1 p.2 * Homogenization.vecDot (b p.1 p.2) (spaceGrad (φ p.1) p.2)

The b·Dθ φ pairing integrates to minus the θ b·∇φ pairing.

theorem AVenhance.Infra.FullTheorem.TransportLimit.test_bound {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsTestFunction φ) : ∃ (C : ℝ), ∀ p ∈ timeCube, |φ p.1 p.2| ≤ C

Boundedness of a test function on the space-time cell.

theorem AVenhance.Infra.FullTheorem.TransportLimit.time_derivative_continuous {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsTestFunction φ) : Continuous fun (p : ℝ × Homogenization.Vec 2) => deriv (fun (s : ℝ) => φ s p.2) p.1

theorem AVenhance.Infra.FullTheorem.TransportLimit.solution_transport_form {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (h : DriftHyp b) {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} {Dθ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ θ₀ θ Dθ) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsTestFunction φ) : ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, -θ p.1 p.2 * deriv (fun (s : ℝ) => φ s p.2) p.1 - θ p.1 p.2 * Homogenization.vecDot (b p.1 p.2) (spaceGrad (φ p.1) p.2) = (∫ (x : Homogenization.Vec 2) in unitCube, θ₀ x * φ 0 x) - κ * ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, Homogenization.vecDot (Dθ p.1 p.2) (spaceGrad (φ p.1) p.2)

The divergence-form identity for a weak solution, with the viscous remainder.