Weak well-posedness for bounded periodic drifts

This module assembles existence and uniqueness under the exact root hypotheses.

theorem AVenhance.Proofs.weak_wellposed_exists (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (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)) (κ : ℝ) (hκ : 0 < κ) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀_L2 : Homogenization.MemL2On unitCube θ₀) : ∃ (θ : ℝ → Homogenization.Vec 2 → ℝ), IsWeakSolution b κ θ₀ θ

Existence in the exact weak-solution class, under the weak well-posedness data hypotheses.

theorem AVenhance.Proofs.weak_wellposed (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (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)) (κ : ℝ) (hκ : 0 < κ) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀_L2 : Homogenization.MemL2On unitCube θ₀) : ∃ (θ : ℝ → Homogenization.Vec 2 → ℝ), IsWeakSolution b κ θ₀ θ ∧ ∀ (θ' : ℝ → Homogenization.Vec 2 → ℝ), IsWeakSolution b κ θ₀ θ' → ∀ t ∈ Set.Icc 0 1, θ' t =ᵐ[MeasureTheory.volume.restrict unitCube] θ t

Exact weak well-posedness weak well-posedness: existence in the class and cell-a.e. uniqueness at every time.