Divergence-free transport cancellation along a path #
For a bounded measurable divergence-free periodic drift and a path that is periodic H¹ for almost
every time, the transport pairing ∫ b·Dw w vanishes on every truncated time cell. This is the
statement of weak_solution_divFree_drift_pairing_zero without the weak-equation hypothesis.
theorem
AVenhance.Infra.Section5.RelativeError.forced_drift_memLp_two
{b Dw : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hDw :
∀ (i : Fin 2),
MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => Dw p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube))
(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)
:
MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (b p.1 p.2) (Dw p.1 p.2)) 2
(MeasureTheory.volume.restrict timeCube)
The transport density of a bounded drift against an L² gradient is in L².
theorem
AVenhance.Infra.Section5.RelativeError.drift_pairing_region_zero
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{w : ℝ → Homogenization.Vec 2 → ℝ}
{Dw : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hw : MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => w p.1 p.2) 2 (MeasureTheory.volume.restrict timeCube))
(hDw :
∀ (i : Fin 2),
MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => Dw p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube))
(hH1 : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 1), IsPeriodicH1With (w s) (Dw s))
(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)
(hb_per : ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (b t))
(hdiv : IsDivFree b)
{t : ℝ}
(ht : t ∈ Set.Icc 0 1)
:
∫ (p : ℝ × Homogenization.Vec 2) in Parabolic.WeakUniqueness.weakEnergyRegion t, Homogenization.vecDot (b p.1 p.2) (Dw p.1 p.2) * w p.1 p.2 = 0
Divergence-free transport cancels on every truncated time cell for an H¹ path.