Theta Upper Semicontinuity Basic

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

def CKN.subtractMapProd (z : Foundation.Parabolic.ParabolicPoint) : C(Foundation.Parabolic.Vec3 × ℝ, Foundation.Parabolic.Vec3 × ℝ)

Continuous translation by the negative of a fixed parabolic point in product coordinates.

Equations

• CKN.subtractMapProd z = { toFun := fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => (w.1 - z.1, w.2 - z.2), continuous_toFun := ⋯ }

theorem CKN.time_slice_energy_eq_ofReal {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {x : Foundation.Parabolic.Vec3} {r s : ℝ} (hInt : MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (y, s)) ^ 2) (Foundation.Parabolic.vec3Ball x r) MeasureTheory.volume) : ENNReal.ofReal (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x r, Foundation.Parabolic.vec3EuclideanNorm (u (y, s)) ^ 2) = Foundation.Parabolic.Integration.timeSliceBallEnergy x r s fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u w)

theorem CKN.velocity_slice_integrable {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) {x : Foundation.Parabolic.Vec3} {r : ℝ} (hball : Foundation.Parabolic.vec3Ball x r ⊆ Ω') : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (y, s)) ^ 2) (Foundation.Parabolic.vec3Ball x r) MeasureTheory.volume

theorem CKN.alpha_sq_le_of_essSup {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {z : Foundation.Parabolic.ParabolicPoint} {x₀ : Foundation.Parabolic.Vec3} {rho r a b : ℝ} (hrho : 0 < rho) (hball : Foundation.Parabolic.vec3Ball z.1 rho ⊆ Foundation.Parabolic.vec3Ball x₀ r) (hinterval : Set.Ioc (z.2 - rho ^ 2) z.2 ⊆ Set.Ioc a b) (hInt : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc a b), MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (y, s)) ^ 2) (Foundation.Parabolic.vec3Ball x₀ r) MeasureTheory.volume) (hfinite : essSup (fun (x : ℝ) => Foundation.Parabolic.Integration.timeSliceBallEnergy x₀ r x fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u w)) (MeasureTheory.volume.restrict (Set.Ioc a b)) ≠ ⊤) : alpha u z rho ^ 2 ≤ rho⁻¹ * (essSup (fun (s : ℝ) => ENNReal.ofReal (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, Foundation.Parabolic.vec3EuclideanNorm (u (y, s)) ^ 2)) (MeasureTheory.volume.restrict (Set.Ioc a b))).toReal

theorem CKN.eventually_cylinder_subset_of_open {z₀ : Foundation.Parabolic.ParabolicPoint} {r : ℝ} {U : Set Foundation.Parabolic.ParabolicPoint} (hr : 0 < r) (hU : IsOpen U) (hK : closure (Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 r) ⊆ U) : ∀ᶠ (z : Foundation.Parabolic.ParabolicPoint) in nhds z₀, Foundation.Parabolic.parabolicCylinder z.1 z.2 r ⊆ U

theorem CKN.gradient_integrable_of_meas {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {K B : Set Foundation.Parabolic.ParabolicPoint} (hmeasB : MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => spatialGradientSq u Du w) (MeasureTheory.volume.restrict B)) (hKB : K ⊆ B) (hfin : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in K, ENNReal.ofReal (spatialGradientSq u Du w) ≠ ⊤) : MeasureTheory.IntegrableOn (fun (w : Foundation.Parabolic.ParabolicPoint) => spatialGradientSq u Du w) K MeasureTheory.volume

theorem CKN.pressure_integrable_of_meas {p : Foundation.Parabolic.ParabolicPoint → ℝ} {K B : Set Foundation.Parabolic.ParabolicPoint} (hmeasB : MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => |p w| ^ (3 / 2)) (MeasureTheory.volume.restrict B)) (hKB : K ⊆ B) (hfin : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in K, ENNReal.ofReal (|p w| ^ (3 / 2)) ≠ ⊤) : MeasureTheory.IntegrableOn (fun (w : Foundation.Parabolic.ParabolicPoint) => |p w| ^ (3 / 2)) K MeasureTheory.volume

theorem CKN.euclidean_triangle (a b : Foundation.Parabolic.Vec3) : Foundation.Parabolic.vec3EuclideanNorm (a + b) ≤ Foundation.Parabolic.vec3EuclideanNorm a + Foundation.Parabolic.vec3EuclideanNorm b

theorem CKN.mem_euclideanClosedBall_of_vec3Norm_le {x y : Foundation.Parabolic.Vec3} {R : ℝ} (hR : 0 ≤ R) (hxy : Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ R) : y ∈ euclideanClosedBall x R

theorem CKN.cylinder_integral_tendsto_of_open {g : Foundation.Parabolic.ParabolicPoint → ℝ} {z₀ : Foundation.Parabolic.ParabolicPoint} {r : ℝ} {G : Set Foundation.Parabolic.ParabolicPoint} (hG : IsOpen G) (hr : 0 < r) (hK : closure (Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 r) ⊆ G) (hg : MeasureTheory.IntegrableOn g G MeasureTheory.volume) : Filter.Tendsto (fun (z : Foundation.Parabolic.ParabolicPoint) => ∫ (x : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, g x) (nhds z₀) (nhds (∫ (x : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 r, g x))