Weak solution data around an interior center

Every ball whose radius is the distance to the original boundary inherits the weak derivative data and continuity from the original cylinder.

theorem ESS.uc_center_ball_subset (R : ℝ) (x₀ : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.vec3Ball x₀ (R - CKN.Foundation.Parabolic.vec3EuclideanNorm x₀) ⊆ CKN.Foundation.Parabolic.vec3Ball 0 R

The maximal ball centered at an interior point remains inside the original source ball.

theorem ESS.uc_data_at_center (R T c₁ : ℝ) (x₀ : CKN.Foundation.Parabolic.Vec3) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hcont : ContinuousOn w (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ico 0 T)) (hweak : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo 0 T) w Dw D2w Dtw) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo 0 T), ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) (hineq : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo 0 T)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw z) ≤ c₁ * (CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) + √(CKN.spatialGradientSq w Dw z))) : have R₀ := R - CKN.Foundation.Parabolic.vec3EuclideanNorm x₀; have T₀ := min T 1; ContinuousOn w (CKN.Foundation.Parabolic.vec3Ball x₀ R₀ ×ˢ Set.Ico 0 T₀) ∧ CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball x₀ R₀) (Set.Ioo 0 T₀) w Dw D2w Dtw ∧ ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R₀) (Set.Ioo 0 T₀), ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤ ∧ ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R₀) (Set.Ioo 0 T₀)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw z) ≤ c₁ * (CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) + √(CKN.spatialGradientSq w Dw z))

Continuity, weak derivatives, quadratic data, and the differential inequality restrict to an interior centered cylinder.