Blowup Tensor Convergence

Convergence of the quadratic velocity tensor in the endpoint blow-up sequence.

theorem ESS.blowup_product_tendsto_LthreeHalves {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (f g : ℕ → α → ℝ) (F G : α → ℝ) (hF : MeasureTheory.MemLp F 3 μ) (hG : MeasureTheory.MemLp G 3 μ) (hf : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : α) => f k z - F z) 3 μ) Filter.atTop (nhds 0)) (hg : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : α) => g k z - G z) 3 μ) Filter.atTop (nhds 0)) (hfb : ∃ B < ⊤, ∀ (k : ℕ), MeasureTheory.eLpNorm (f k) 3 μ ≤ B) (hgb : ∃ B < ⊤, ∀ (k : ℕ), MeasureTheory.eLpNorm (g k) 3 μ ≤ B) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : α) => f k z * g k z - F z * G z) (3 / 2) μ) Filter.atTop (nhds 0)

Strong L³ convergence of two factors, with uniform L³ bounds, gives strong L^(3/2) convergence of their product.

theorem ESS.blowup_component_eLpNorm_le {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (p : ENNReal) (v : α → CKN.Foundation.Parabolic.Vec3) (hv : MeasureTheory.AEStronglyMeasurable v μ) (i : Fin 3) : MeasureTheory.eLpNorm (fun (z : α) => v z i) p μ ≤ MeasureTheory.eLpNorm v p μ

Each scalar component has no larger Lᵖ norm than a vector field.

theorem ESS.blowup_tensor_component_tendsto_LthreeHalves {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (v : ℕ → α → CKN.Foundation.Parabolic.Vec3) (u : α → CKN.Foundation.Parabolic.Vec3) (hu : MeasureTheory.MemLp u 3 μ) (hv : ∀ (k : ℕ), MeasureTheory.MemLp (v k) 3 μ) (hconv : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : α) => v k z - u z) 3 μ) Filter.atTop (nhds 0)) (hbound : ∃ B < ⊤, ∀ (k : ℕ), MeasureTheory.eLpNorm (v k) 3 μ ≤ B) (i j : Fin 3) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : α) => v k z i * v k z j - u z i * u z j) (3 / 2) μ) Filter.atTop (nhds 0)

Strong local L³ convergence of velocity gives strong L^(3/2) convergence of each quadratic tensor component.