Lemma U: the drift term on a time slice

For a bounded drift, the drift pairing g_t = b_t · Dθ_t of a.e. time slice lies in L² of the cell with ‖g_t‖² ≤ 2 B² ‖Dθ_t‖², and the forcing weakModeForcing of a real mode splits as ⟨g_t, ψ_a⟩ + κ λ_a ⟨θ_t, ψ_a⟩.

theorem AVenhance.Infra.FullTheorem.LemmaU.vecNormSq_nonneg' (x : Homogenization.Vec 2) : 0 ≤ Homogenization.vecNormSq x

theorem AVenhance.Infra.FullTheorem.LemmaU.gradNormSq_nonneg (Du : Homogenization.Vec 2 → Homogenization.Vec 2) : 0 ≤ gradNormSq Du

theorem AVenhance.Infra.FullTheorem.LemmaU.l2NormSq_nonneg (f : Homogenization.Vec 2 → ℝ) : 0 ≤ l2NormSq f

theorem AVenhance.Infra.FullTheorem.LemmaU.vecDot_sq_le {u v : Homogenization.Vec 2} {B : ℝ} (hu : ‖u‖ ≤ B) : Homogenization.vecDot u v ^ 2 ≤ 2 * B ^ 2 * Homogenization.vecNormSq v

Pointwise bound of the drift pairing for a sup-norm-bounded drift.

theorem AVenhance.Infra.FullTheorem.LemmaU.integrable_vecNormSq_cell {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (hD : Homogenization.GradMemL2On unitCube Du) : MeasureTheory.Integrable (fun (x : Homogenization.Vec 2) => Homogenization.vecNormSq (Du x)) (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.FullTheorem.LemmaU.integrable_vecNormSq_timeCube {D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hD : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => D p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)) : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecNormSq (D p.1 p.2)) (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.FullTheorem.LemmaU.integrable_vecDot_gradMode {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (hD : Homogenization.GradMemL2On unitCube Du) (M : ℕ) (a : Parabolic.FourierGalerkin.RealFourierIndex M) : MeasureTheory.Integrable (fun (x : Homogenization.Vec 2) => Homogenization.vecDot (Du x) (spaceGrad (Parabolic.FourierGalerkin.realFourierModeAmbient M a) x)) (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.FullTheorem.LemmaU.drift_slice_ae {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ B : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} {D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hB : ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ B) (hu : IsWeakSolutionGrad b κ θ₀ θ D) (M : ℕ) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 1), IsPeriodicH1With (θ t) (D t) ∧ (Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => Homogenization.vecDot (b t x) (D t x)) ∧ (l2NormSq fun (x : Homogenization.Vec 2) => Homogenization.vecDot (b t x) (D t x)) ≤ 2 * B ^ 2 * gradNormSq (D t) ∧ ∀ (a : Parabolic.FourierGalerkin.RealFourierIndex M), Parabolic.WeakUniqueness.weakModeForcing b κ D (Parabolic.FourierGalerkin.realFourierModeAmbient M a) t = cellCoeff M (fun (x : Homogenization.Vec 2) => Homogenization.vecDot (b t x) (D t x)) a + κ * (modeLam M a * cellCoeff M (θ t) a)

The slice facts for the drift pairing.