Time transfer for the centered HDot⁻¹ bounds #
If at every t ∈ (0,1) the HDot⁻¹ norm of a slice is bounded by an affine combination of the
slice
energies ‖V_j(t)‖_{L²_x} of three fields continuous on [0,1] × ℝ², then the time-L²(HDot⁻¹)
norm is bounded by the same combination of the space-time norms (with a factor 2).
theorem
AVenhance.Infra.Section5.Contracts.sd_time_transfer
{f : ℝ → Homogenization.Vec 2 → ℝ}
{V : Fin 3 → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{P : Fin 3 → ℝ}
{P₂ : ℝ}
(hP : ∀ (j : Fin 3), 0 ≤ P j)
(hP₂ : 0 ≤ P₂)
(hV :
∀ (j : Fin 3) (i : Fin 2),
ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => V j p.1 p.2 i) (Set.Icc 0 1 ×ˢ Set.univ))
(hpt : ∀ t ∈ Set.Ioo 0 1, hMinusOneNorm (f t) ≤ ENNReal.ofReal (∑ j : Fin 3, P j * √(gradNormSq (V j t)) + P₂))
: