Space-time weights in L^{5/3}

The spatial weight (1 + |y|)^{-3} lies in L^{5/3}(ℝ³) and the time weight r^{-1/2} on (0, τ) lies in L^{5/3}(ℝ), since 5 > 3 and 5/6 < 1. A product of such weights pairs integrably, by Hölder's inequality, with a space-time function in L^{5/2}; this is the integrability used for the forced heat response against a test field in prop:pv-local-solution.

theorem ESS.memLp_one_add_norm_rpow_neg_three : MeasureTheory.MemLp (fun (y : CKN.Foundation.Parabolic.Vec3) => (1 + ‖y‖) ^ (-3)) (ENNReal.ofReal (5 / 3)) MeasureTheory.volume

The spatial weight (1 + |y|)^{-3} lies in L^{5/3}(ℝ³).

theorem ESS.memLp_inv_sqrt_indicator {τ : ℝ} (hτ : 0 < τ) : MeasureTheory.MemLp (fun (r : ℝ) => (Set.Ioo 0 τ).indicator (fun (r : ℝ) => (√r)⁻¹) r) (ENNReal.ofReal (5 / 3)) MeasureTheory.volume

The time weight r^{-1/2} on (0, τ) lies in L^{5/3}(ℝ).

theorem ESS.integrable_mul_spaceTime_weight {g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : MeasureTheory.MemLp g (ENNReal.ofReal (5 / 2)) MeasureTheory.volume) {b : ℝ → ℝ} (hb : MeasureTheory.MemLp b (ENNReal.ofReal (5 / 3)) MeasureTheory.volume) : MeasureTheory.Integrable (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => g q * (b q.2 * (1 + ‖q.1‖) ^ (-3))) MeasureTheory.volume

A space-time function in L^{5/2} pairs integrably with the product of an L^{5/3} time weight and the spatial weight (1 + |y|)^{-3}.