Lemma U: assembly of the Fourier estimates

For s ≤ t in [0,1], the squared L² increment of a weak solution is the limit of the finite coefficient sums; each of these is bounded by the low/high split with threshold K, and the optimisation over K finishes the proof.

theorem AVenhance.Infra.FullTheorem.LemmaU.cellCoeff_sub (M : ℕ) {f g : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (hg : Homogenization.MemL2On unitCube g) (a : Parabolic.FourierGalerkin.RealFourierIndex M) : cellCoeff M (fun (x : Homogenization.Vec 2) => f x - g x) a = cellCoeff M f a - cellCoeff M g a

theorem AVenhance.Infra.FullTheorem.LemmaU.final_algebra {κ K A2 D2 h B' : ℝ} (hκ : 0 < κ) (hK : 0 < K) (hA2 : 0 ≤ A2) (hD2 : 0 ≤ D2) (hh : 0 ≤ h) : 2 * h * ((κ ^ 2 * (80 * K ^ 2) + B' ^ 2) * (A2 / (2 * κ))) + 4 * (D2 / (36 * K ^ 2) + B' ^ 2 * (A2 / (2 * κ)) / (2 * κ * (36 * K ^ 2))) ≤ (A2 + D2) * (h * (80 * κ * K ^ 2 + B' ^ 2 / κ) + 1 / (9 * K ^ 2) + B' ^ 2 / (36 * κ ^ 2 * K ^ 2))

theorem AVenhance.Infra.FullTheorem.LemmaU.modePath_zero {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {Dθ₀ : Homogenization.Vec 2 → Homogenization.Vec 2} {θ : ℝ → Homogenization.Vec 2 → ℝ} {D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hθ₀ : IsPeriodicH1With θ₀ Dθ₀) (hu : IsWeakSolutionGrad b κ θ₀ θ D) (M : ℕ) (a : Parabolic.FourierGalerkin.RealFourierIndex M) : modePath M θ a 0 = cellCoeff M θ₀ a

theorem AVenhance.Infra.FullTheorem.LemmaU.increment_finite {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ B : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {Dθ₀ : Homogenization.Vec 2 → Homogenization.Vec 2} {θ : ℝ → Homogenization.Vec 2 → ℝ} {D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hκ : 0 < κ) (hB0 : 0 ≤ B) (hb_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) (hb_per : ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (b t)) (hdiv : IsDivFree b) (hB : ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ B) (hθ₀ : IsPeriodicH1With θ₀ Dθ₀) (hu : IsWeakSolutionGrad b κ θ₀ θ D) (M : ℕ) {K : ℝ} (hK : 0 < K) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) (hst : s ≤ t) : ∑ a : Parabolic.FourierGalerkin.RealFourierIndex M, cellCoeff M (fun (x : Homogenization.Vec 2) => θ t x - θ s x) a ^ 2 ≤ 2 * (t - s) * ((κ ^ 2 * (80 * K ^ 2) + (2 * B) ^ 2) * (l2NormSq θ₀ / (2 * κ))) + 4 * (gradNormSq Dθ₀ / (36 * K ^ 2) + (2 * B) ^ 2 * (l2NormSq θ₀ / (2 * κ)) / (2 * κ * (36 * K ^ 2)))

The finite-cutoff increment bound.

theorem AVenhance.Infra.FullTheorem.LemmaU.lemmaU_core {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ B : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {Dθ₀ : Homogenization.Vec 2 → Homogenization.Vec 2} {θ : ℝ → Homogenization.Vec 2 → ℝ} {D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hκ : 0 < κ) (hκ1 : κ ≤ 1) (hB0 : 0 ≤ B) (hb_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) (hb_per : ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (b t)) (hdiv : IsDivFree b) (hB : ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ B) (hθ₀ : IsPeriodicH1With θ₀ Dθ₀) (hu : IsWeakSolutionGrad b κ θ₀ θ D) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) (hst : s ≤ t) : √(l2NormSq fun (x : Homogenization.Vec 2) => θ t x - θ s x) ≤ 20 * (1 + 2 * B) / √κ * (t - s) ^ (1 / 4) * √(l2NormSq θ₀ + gradNormSq Dθ₀)

The s ≤ t case of Lemma U, with drift constant 2B.