Weak gradients of the rescaled trace #
On each fixed ball, and for all small scales, the rescaled trace
representative of the blow-up sequence in prop:blowup-limit has the
rescaled (measurable) source gradient as its weak spatial gradient on almost
every time slice.
The Euclidean norm on Vec3 satisfies the triangle inequality.
theorem
ESS.blowupLimitAssembly_trace_hasWeakGradientOn
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du Dm : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hDm : Measurable Dm)
(hDmEq : goodPointDomain.indicator Dm =ᵐ[MeasureTheory.volume] goodPointDomain.indicator Du)
(hgrad :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), ∀ (i : Fin 3),
CKN.HasWeakGradientOn (CKN.Foundation.Parabolic.vec3Ball 0 1) (fun (x : CKN.Vec 3) => u (x, t) i)
fun (x : CKN.Vec 3) => Du (x, t) i)
(W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc (-(3 / 4) ^ 2) 0) → CKN.Foundation.Parabolic.Vec3)
(hW : Measurable W)
(htrace :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-(3 / 4) ^ 2) 0), ∃ (ht : t ∈ Set.Icc (-(3 / 4) ^ 2) 0),
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
W (x, ⟨t, ht⟩)) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))]
fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t))
{x₀ : CKN.Foundation.Parabolic.Vec3}
(hx₀ : CKN.Foundation.Parabolic.vec3EuclideanNorm x₀ ≤ 1 / 2)
{t₀ : ℝ}
(ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0)
{r R : ℝ}
(hr : 0 < r)
(hrR : r * R < 1 / 4)
(hrR2 : r ^ 2 * R < 1 / 4)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-R) 0), ∀ (i : Fin 3),
CKN.HasWeakGradientOn (CKN.Foundation.Parabolic.vec3Ball 0 R)
(fun (x : CKN.Vec 3) => blowupLimitTraceRescaling W x₀ t₀ r (x, t) i) fun (x : CKN.Vec 3) =>
blowupGradient x₀ t₀ r Dm (x, t) i
The rescaled trace has the rescaled measurable source gradient as weak spatial gradient on the ball of radius R, for almost every past time, once the rescaled cylinder lies inside the inner source cylinder.