Tensor-indexed pressure estimates

The pressure is identified with the sum of nine separately indexed operator outputs. Component estimates then give an extended-valued norm bound and the real pressure norm bound. Compact support is not needed for this consumption step once the component estimates are supplied.

theorem CKN.Core.Endgame.pressure_memLp_and_eLpNorm_le_of_tensor_bounds (T : Fin 3 → Fin 3 → (Foundation.Parabolic.Vec3 → ℝ) → Foundation.Parabolic.Vec3 → ℝ) (G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ) {p₁ : Foundation.Parabolic.Vec3 → ℝ} {C : ℝ} (hTG : ∀ (i j : Fin 3), MeasureTheory.MemLp (T i j (G i j)) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hbound : ∀ (i j : Fin 3), MeasureTheory.eLpNorm (T i j (G i j)) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hident : p₁ =ᵐ[MeasureTheory.volume] fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ∑ j : Fin 3, T i j (G i j) x) : MeasureTheory.MemLp p₁ (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm p₁ (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ ENNReal.ofReal C * ∑ i : Fin 3, ∑ j : Fin 3, MeasureTheory.eLpNorm (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume

Component bounds and the actual tensor-sum identification give pressure membership and an extended-valued norm estimate at exponent 3/2.

theorem CKN.Core.Endgame.pressure_lpNorm_le_of_tensor_bounds (T : Fin 3 → Fin 3 → (Foundation.Parabolic.Vec3 → ℝ) → Foundation.Parabolic.Vec3 → ℝ) (G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ) {p₁ : Foundation.Parabolic.Vec3 → ℝ} {C C₁₁ E : ℝ} (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hTG : ∀ (i j : Fin 3), MeasureTheory.MemLp (T i j (G i j)) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hbound : ∀ (i j : Fin 3), MeasureTheory.eLpNorm (T i j (G i j)) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hident : p₁ =ᵐ[MeasureTheory.volume] fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ∑ j : Fin 3, T i j (G i j) x) (hsource : ∑ i : Fin 3, ∑ j : Fin 3, MeasureTheory.lpNorm (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ E ^ (2 / 3)) (hC : 0 ≤ C) (hconst : C ≤ C₁₁) (hE : 0 ≤ E) : MeasureTheory.lpNorm p₁ (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C₁₁ * E ^ (2 / 3)

A summed tensor-input norm bound yields the literal real pressure norm estimate, retaining each operator and source index.