Slice transport identity against smooth periodic tests #
For a bounded measurable periodic divergence-free field b and a periodic H¹ function u,
∫_cell (b·Du) φ = -∫_cell u (b·∇φ) for every smooth periodic φ. It follows by
polarising the static cancellation ∫ (b·Dv) v = 0 for v = u - φ, u, φ.
theorem
AVenhance.Infra.FullTheorem.TransportLimit.bcoord_memLp_top
{b : Homogenization.Vec 2 → Homogenization.Vec 2}
(hbMeas : MeasureTheory.AEStronglyMeasurable b MeasureTheory.volume)
(hbBound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Homogenization.Vec 2), ‖b x‖ ≤ C)
(i : Fin 2)
:
MeasureTheory.MemLp (fun (x : Homogenization.Vec 2) => b x i) ⊤ (MeasureTheory.volume.restrict unitCube)
Coordinates of a bounded measurable field are essentially bounded on the cell.
theorem
AVenhance.Infra.FullTheorem.TransportLimit.drift_memL2
{b : Homogenization.Vec 2 → Homogenization.Vec 2}
(hbMeas : MeasureTheory.AEStronglyMeasurable b MeasureTheory.volume)
(hbBound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Homogenization.Vec 2), ‖b x‖ ≤ C)
{D : Homogenization.Vec 2 → Homogenization.Vec 2}
(hD : Homogenization.GradMemL2On unitCube D)
:
Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => Homogenization.vecDot (b x) (D x)
The transport pairing of a bounded field with an L² gradient is L².
theorem
AVenhance.Infra.FullTheorem.TransportLimit.slice_transport_identity
{b : Homogenization.Vec 2 → Homogenization.Vec 2}
(hbMeas : MeasureTheory.AEStronglyMeasurable b MeasureTheory.volume)
(hbBound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Homogenization.Vec 2), ‖b x‖ ≤ C)
(hbPer : IsZ2Periodic b)
(hDiv :
∀ (φ : Homogenization.Vec 2 → ℝ),
ContDiff ℝ (↑⊤) φ →
HasCompactSupport φ → ∫ (x : Homogenization.Vec 2), Homogenization.vecDot (b x) (spaceGrad φ x) = 0)
{u : Homogenization.Vec 2 → ℝ}
{Du : Homogenization.Vec 2 → Homogenization.Vec 2}
(hu : IsPeriodicH1With u Du)
{φ : Homogenization.Vec 2 → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hφp : IsZ2Periodic φ)
:
∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (b x) (Du x) * φ x = -∫ (x : Homogenization.Vec 2) in unitCube, u x * Homogenization.vecDot (b x) (spaceGrad φ x)