Weighted bounds for fields with bounded future time support

A uniform weighted bound on a time slab gives a global reciprocal-weight bound when the field vanishes after the slab. The spatial type, normed codomain, lower time endpoint, and positive weight are arbitrary. Periodic and compact-support force estimates supply the slab bound by different compactness arguments.

theorem NavierStokesAndEuler.WeightedDecay.exists_pos_norm_le_div_of_slab_bound {X : Type u_1} {V : Type u_2} [SeminormedAddCommGroup V] {J : ℝ × X → V} {w : ℝ × X → ℝ} {a T : ℝ} (hw : ∀ (t : ℝ), a ≤ t → ∀ (x : X), 0 < w (t, x)) (hzero : ∀ (t : ℝ), T < t → ∀ (x : X), J (t, x) = 0) (hbound : ∃ (M : ℝ), ∀ t ∈ Set.Icc a T, ∀ (x : X), ‖J (t, x)‖ * w (t, x) ≤ M) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), a ≤ t → ∀ (x : X), ‖J (t, x)‖ ≤ C / w (t, x)

Extend a weighted bound on [a, T] to a reciprocal-weight estimate for all t ≥ a, when the field vanishes for t > T.