Documentation

LeanPool.EscauriazaSereginSverak.Endpoint.BlowupGradientComponent

Blowup Gradient Component #

Gradient estimates for the rescaled sequence used in endpoint compactness.

source
theorem ESS.blowup_gradient_component_sq_le (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (i : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) :
CKN.Foundation.Parabolic.vec3EuclideanNorm (Du z i) ^ 2 ≤ CKN.spatialGradientSq u Du z

The squared Euclidean norm of one gradient row is at most the full Dirichlet density.

source
theorem ESS.blowup_gradient_component_eLpNorm_sq_le (S : Set CKN.Foundation.Parabolic.ParabolicPoint) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (i : Fin 3) (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict S)) (hgrad : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialGradientSq u Du z) S MeasureTheory.volume) :
MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (Du z i)) 2 (MeasureTheory.volume.restrict S) ^ 2 ≤ ENNReal.ofReal (∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, CKN.spatialGradientSq u Du z)

A finite Dirichlet integral bounds the squared L² seminorm of each Euclidean gradient row.

source
theorem ESS.blowup_gradient_component_eLpNorm_le_of_integral_bound (S : Set CKN.Foundation.Parabolic.ParabolicPoint) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (i : Fin 3) (C : ℝ) (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict S)) (hgrad : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialGradientSq u Du z) S MeasureTheory.volume) (hbound : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, CKN.spatialGradientSq u Du z ≤ C) :
MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (Du z i)) 2 (MeasureTheory.volume.restrict S) ≤ ENNReal.ofReal C ^ (1 / 2)

A real Dirichlet bound gives a uniform bound for one gradient row's space-time L² seminorm.