RelativeError: the classical low-mode trace bridge #
This module connects the transported-test estimate to a classical solution. The Fourier projection supplies the three explicit spectral facts in the theorem: its initial pairing, gradient energy, and differentiated Laplacian bound.
theorem
AVenhance.Infra.Section5.RelativeError.classical_lowMode_trace_bound_of_spectralFacts_euclidean
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ K B G : ℝ}
{g f : Homogenization.Vec 2 → ℝ}
{u : ℝ → Homogenization.Vec 2 → ℝ}
{X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(hb : Flow.SmoothPeriodicField b)
(hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), vecDiv (b t) x = 0)
(hX : IsFlow b X)
(hDb : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b r y‖ ≤ B)
(hmax : max 1 B ≤ κ * K ^ 2)
(hB : 0 ≤ B)
(hκ : 0 < κ)
(hK : 0 < K)
(hG : 0 ≤ G)
(hsol : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g u)
(hf : ContDiff ℝ (↑⊤) f)
(hfper : IsZ2Periodic f)
(hinitial : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, g x * -spaceLap f x = G ^ 2)
(henergy : gradNormSq (spaceGrad f) = G ^ 2)
(hlapGrad :
∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecNormSq (spaceGrad (fun (x : Homogenization.Vec 2) => -spaceLap f x) x) ≤ K ^ 4 * G ^ 2)
:
The short-time trace estimate for a smooth Fourier low mode. The spectral facts are stated separately so the transport and parabolic parts remain independent of the chosen finite Fourier cutoff representation.