Stability Product Swap

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_eLpNorm_tendsto_swap {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (ν : MeasureTheory.Measure β) [MeasureTheory.SFinite ν] (p : ENNReal) (F : ℕ → α × β → E) (G : α × β → E) (hF : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n - G) (μ.prod ν)) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) p (μ.prod ν)) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (z : β × α) => F n (z.2, z.1) - G (z.2, z.1)) p (ν.prod μ)) Filter.atTop (nhds 0)

Strong convergence on a product measure is unchanged by interchanging the space and time coordinates (thm:stability).