The time-Sobolev estimate on Euclidean balls

Clause (iv) of the external Sobolev input is used here in the Euclidean-ball form. The paper's equation (1446--1453) states, for q = 10/3,

`∫{B_r} |v|^(10/3) ≤ C₆ ((∫{B_r} |∇v|²)(∫_{B_r} |v|²)^(2/3)

• r^(-2)(∫_{B_r} |v|²)^(5/3))`.

The text at lines 4649--4671 integrates this same-ball estimate in time to obtain the L∞_t L²_x ∩ L²_t H¹_x to L^(10/3) embedding. This theorem formalizes that time estimate on Euclidean balls. Clauses (i)--(iii) of the external input are independent and are not changed here.

theorem CKN.euclideanBall_eq_vec3Ball_timeSobolev {x₀ : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) : euclideanBall x₀ r = Foundation.Parabolic.vec3Ball x₀ r

noncomputable def CKN.zeroH1Whole : H1Function Set.univ

Zero H¹ function on the whole spatial domain, used as a default slice.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.timeSobolevSlice (x₀ : Foundation.Parabolic.Vec3) (r : ℝ) (hr : 0 < r) (g : Foundation.Parabolic.Vec3 × ℝ → ℝ) (Dg : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) : ℝ → H1Function (euclideanBall x₀ r)

Selected H¹ time slice when one exists, with zero as the default on exceptional times.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.ball_time_sobolev : ∃ (C : ℝ), 0 < C ∧ ∀ (x₀ : Foundation.Parabolic.Vec3) (r : ℝ), 0 < r → ∀ (J : Set ℝ), J.OrdConnected → ∀ (g : Foundation.Parabolic.Vec3 × ℝ → ℝ) (Dg : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3), have U := Foundation.Parabolic.vec3Ball x₀ r; MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict (U ×ˢ J)) → MeasureTheory.AEStronglyMeasurable Dg (MeasureTheory.volume.restrict (U ×ˢ J)) → (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∃ (v : H1Function U), (fun (x : Foundation.Parabolic.Vec3) => g (x, s)) =ᵐ[MeasureTheory.volume.restrict U] v.toFun ∧ (fun (x : Foundation.Parabolic.Vec3) => Dg (x, s)) =ᵐ[MeasureTheory.volume.restrict U] v.grad) → MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (U ×ˢ J)) → MeasureTheory.MemLp Dg 2 (MeasureTheory.volume.restrict (U ×ˢ J)) → have A := essSup (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => g (x, s)) 2 (MeasureTheory.volume.restrict U)) (MeasureTheory.volume.restrict J); A < ⊤ → MeasureTheory.MemLp g (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (U ×ˢ J)) ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (U ×ˢ J)) ^ (10 / 3) ≤ ENNReal.ofReal C * (A ^ (4 / 3) * MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.Vec3 × ℝ) => Foundation.Parabolic.vec3EuclideanNorm (Dg z)) 2 (MeasureTheory.volume.restrict (U ×ˢ J)) ^ 2 + ENNReal.ofReal (r ^ (-2)) * A ^ (10 / 3) * MeasureTheory.volume J)

The Euclidean-ball form of clause (iv) of the external Sobolev input, with one absolute constant.