Time integrability from a finite spatial slice estimate

The component estimates for eq:pressure-gradient-morrey supply all temporal obligations on compactly interior source balls. A finite spatial estimate then transfers them to the entire carrier in prop:bootstrap.

noncomputable def CKN.Core.Endgame.theoremATranslatedSliceMajorant (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) (x : Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (s : ℝ) : ENNReal

The explicit slice majorant in coordinates translated to a source centre.

Equations

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

theorem CKN.Core.Endgame.theoremA_origin_majorant_time_of_spatial_inclusion {Ω : 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) (hρ : 0 < ρ) (hball : closure (Foundation.Parabolic.vec3Ball 0 ρ) ⊆ Ω) : (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, Step4.originSliceGradientMajorant u Du p f (0, 0) hρ s ≠ ⊤) ∧ ∀ (T : Set ℝ), IsCompact (closure T) → closure T ⊆ I → MeasureTheory.Integrable (fun (s : ℝ) => (Step4.originSliceGradientMajorant u Du p f (0, 0) hρ s).toReal) (MeasureTheory.volume.restrict T)

Compact containment of the source ball suffices for both temporal obligations of the complete origin majorant.

theorem CKN.Core.Endgame.theoremA_translated_majorant_time {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q ρ : ℝ} {x : Foundation.Parabolic.Vec3} {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) (hρ : 0 < ρ) (hball : closure (Foundation.Parabolic.vec3Ball x ρ) ⊆ Ω) : (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, theoremATranslatedSliceMajorant u Du p f x hρ s ≠ ⊤) ∧ ∀ (T : Set ℝ), IsCompact (closure T) → closure T ⊆ I → MeasureTheory.Integrable (fun (s : ℝ) => (theoremATranslatedSliceMajorant u Du p f x hρ s).toReal) (MeasureTheory.volume.restrict T)

Translating the source centre preserves the full-interval finiteness and compact-time integrability of the explicit slice majorant.

theorem CKN.Core.Endgame.theoremA_carrier_slice_time_of_finite_cover (hCarrierFiniteCoverEstimate : ∀ (R₁ : ℝ), 0 < R₁ → R₁ < 3 / 4 → ∃ (n : ℕ) (x : Fin n → Foundation.Parabolic.Vec3) (ρ : ℝ) (hρ : 0 < ρ), (∀ (j : Fin n), closure (Foundation.Parabolic.vec3Ball (x j) ρ) ⊆ Foundation.Parabolic.vec3Ball 0 1) ∧ ∀ {Ω : 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}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → ∀ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), Measurable Dp → (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) → ∀ (i : Fin 3), ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁)) ≤ ∑ j : Fin n, theoremATranslatedSliceMajorant u Du p f (x j) hρ s) {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q R₁ : ℝ} {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} : IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → 0 < R₁ → R₁ < 3 / 4 → ∀ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), Measurable Dp → (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) → (∀ (i : Fin 3), ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁)) ≠ ⊤) ∧ ∀ (i : Fin 3) (T : Set ℝ), IsCompact (closure T) → closure T ⊆ I → MeasureTheory.Integrable (fun (s : ℝ) => (MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁))).toReal) (MeasureTheory.volume.restrict T)

A finite spatial slice estimate supplies all carrier time obligations. The source centres and radius are chosen before the suitable solution.