Norming estimates for weak continuity in L^3

• shared internal estimates used to upgrade the all-time L² representative.

theorem instFactLeENNRealOfNat_leanPool_1 : Fact (1 ≤ 2)

theorem instFactNeENNRealOfNatTop_leanPool_1 : Fact (2 ≠ ⊤)

theorem instFactLeENNRealOfNatOfRealHDivReal_leanPool : Fact (1 ≤ ENNReal.ofReal (3 / 2))

noncomputable def ESS.weakContL3L2ToLThreeHalvesLinear (μ : MeasureTheory.Measure CKN.Foundation.Parabolic.Vec3) [MeasureTheory.IsFiniteMeasure μ] : ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 2 μ) →ₗ[ℝ] ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 (ENNReal.ofReal (3 / 2)) μ)

The canonical inclusion from L² to L^{3/2} on a finite-measure spatial domain.

Equations

• ESS.weakContL3L2ToLThreeHalvesLinear μ = { toFun := fun (f : ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 2 μ)) => MeasureTheory.MemLp.toLp ↑↑f ⋯, map_add' := ⋯, map_smul' := ⋯ }

theorem ESS.weakContL3L2ToLThreeHalves_bound (μ : MeasureTheory.Measure CKN.Foundation.Parabolic.Vec3) [MeasureTheory.IsFiniteMeasure μ] (f : ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 2 μ)) : ‖(weakContL3L2ToLThreeHalvesLinear μ) f‖ ≤ (μ Set.univ ^ (1 / 6)).toReal * ‖f‖

noncomputable def ESS.weakContL3L2ToLThreeHalves (μ : MeasureTheory.Measure CKN.Foundation.Parabolic.Vec3) [MeasureTheory.IsFiniteMeasure μ] : ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 2 μ) →L[ℝ] ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 (ENNReal.ofReal (3 / 2)) μ)

The continuous inclusion of spatial L² into L^{3/2} on a finite measure set.

Equations

• ESS.weakContL3L2ToLThreeHalves μ = (ESS.weakContL3L2ToLThreeHalvesLinear μ).mkContinuous (μ Set.univ ^ (1 / 6)).toReal ⋯

theorem ESS.weakContL3_pairing_bound_of_dense (μ : MeasureTheory.Measure CKN.Foundation.Parabolic.Vec3) [MeasureTheory.IsFiniteMeasure μ] (ψ : ℕ → ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 2 μ)) (hψ : DenseRange ψ) (v : ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 2 μ)) (C : ℝ) (hbound : ∀ (n : ℕ), |inner ℝ v (ψ n)| ≤ C * ‖(weakContL3L2ToLThreeHalves μ) (ψ n)‖) (x : ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 2 μ)) : |inner ℝ v x| ≤ C * ‖(weakContL3L2ToLThreeHalves μ) x‖

A pairing estimate on a dense family extends to every L² test.

theorem ESS.weakContL3_inner_holder {μ : MeasureTheory.Measure CKN.Foundation.Parabolic.Vec3} {f g : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.L2Vec3} (hf₂ : MeasureTheory.MemLp f 2 μ) (hg₂ : MeasureTheory.MemLp g 2 μ) (hf₃ : MeasureTheory.MemLp f 3 μ) (hg₃₂ : MeasureTheory.MemLp g (ENNReal.ofReal (3 / 2)) μ) : |inner ℝ (MeasureTheory.MemLp.toLp f hf₂) (MeasureTheory.MemLp.toLp g hg₂)| ≤ (MeasureTheory.eLpNorm f 3 μ).toReal * (MeasureTheory.eLpNorm g (ENNReal.ofReal (3 / 2)) μ).toReal

Hölder bounds the pairing of an L³ field with an L^{3/2} test.

theorem ESS.weakContL3_integral_holder {μ : MeasureTheory.Measure CKN.Foundation.Parabolic.Vec3} {f g : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.L2Vec3} (hf₃ : MeasureTheory.MemLp f 3 μ) (hg₃₂ : MeasureTheory.MemLp g (ENNReal.ofReal (3 / 2)) μ) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => inner ℝ (f x) (g x)) μ ∧ |∫ (x : CKN.Foundation.Parabolic.Vec3), inner ℝ (f x) (g x) ∂μ| ≤ (MeasureTheory.eLpNorm f 3 μ).toReal * (MeasureTheory.eLpNorm g (ENNReal.ofReal (3 / 2)) μ).toReal

Hölder controls the integrated vector pairing for arbitrary L³ and L^{3/2} fields.

theorem ESS.weakContL3_norming_bound {μ : MeasureTheory.Measure CKN.Foundation.Parabolic.Vec3} [MeasureTheory.IsFiniteMeasure μ] (v : ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 2 μ)) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (w : ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 2 μ)), |inner ℝ v w| ≤ C * ‖(weakContL3L2ToLThreeHalves μ) w‖) : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => ↑↑v x) 3 μ ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => ↑↑v x) 3 μ ≤ ENNReal.ofReal C

A uniform bound against L² tests controls the L³ norm of the field.