Lemma U: a weak solution is a mode system #
The real Fourier coefficients of a weak solution of the advection-diffusion equation with a
bounded divergence-free drift form a ModeSystem with energy density ‖Dθ(r)‖².
noncomputable def
AVenhance.Infra.FullTheorem.LemmaU.modePath
(M : ℕ)
(θ : ℝ → Homogenization.Vec 2 → ℝ)
(a : Parabolic.FourierGalerkin.RealFourierIndex M)
(r : ℝ)
:
Coefficient path of mode a.
Equations
Instances For
noncomputable def
AVenhance.Infra.FullTheorem.LemmaU.modeDrift
(M : ℕ)
(b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2)
(κ : ℝ)
(θ : ℝ → Homogenization.Vec 2 → ℝ)
(D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2)
(a : Parabolic.FourierGalerkin.RealFourierIndex M)
(r : ℝ)
:
The part of the forcing not accounted for by dissipation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AVenhance.Infra.FullTheorem.LemmaU.modePath_eq_cellCoeff
(M : ℕ)
(θ : ℝ → Homogenization.Vec 2 → ℝ)
(a : Parabolic.FourierGalerkin.RealFourierIndex M)
(r : ℝ)
:
theorem
AVenhance.Infra.FullTheorem.LemmaU.weak_modeSystem
{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 : ℕ)
:
ModeSystem κ (2 * B) (modeLam M) (modePath M θ) (modeDrift M b κ θ D) (fun (r : ℝ) => gradNormSq (D r))
(l2NormSq θ₀ / (2 * κ))
The mode system of a weak solution.