Statement file: weak_wellposed (Roots). This file contains exactly one declaration of the formalization's public statement surface.

theorem AVenhance.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

Weak well-posedness