Documentation

LeanPool.CIVAxisymmetric.Reduction.AnalyticBoundOnMonotone

Analytic Bound On Monotone #

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

source
theorem CIV.analyticBoundOn_mono_const {g : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {R' M M' a : ℝ} {J : Set ℝ} (ha : 0 < a) (hM : M ≤ M') (h : AnalyticBoundOn g R' J M a) :
AnalyticBoundOn g R' J M' a

Monotonicity of AnalyticBoundOn/eq:analytic:interior:force in the constant M: increasing M preserves the bound.

source
theorem CIV.analyticBoundOn_mono_scale {g : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {R' M a a' : ℝ} {J : Set ℝ} (hM : 0 ≤ M) (ha' : 0 < a') (haa' : a' ≤ a) (h : AnalyticBoundOn g R' J M a) :
AnalyticBoundOn g R' J M a'

Monotonicity of AnalyticBoundOn/eq:analytic:interior:force in the analyticity rate a: decreasing a (with 0 < a' ≤ a) preserves the bound.

source
theorem CIV.analyticBoundOn_mono_ball {g : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {R' R'' M a : ℝ} {J : Set ℝ} (hR'' : R'' ≤ R') (h : AnalyticBoundOn g R' J M a) :
AnalyticBoundOn g R'' J M a

Monotonicity of AnalyticBoundOn/eq:analytic:interior:force in the spatial radius R': shrinking the ball preserves the bound.

source
theorem CIV.analyticBoundOn_mono_time {g : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {R' M a : ℝ} {J J' : Set ℝ} (hJ : J' ⊆ J) (h : AnalyticBoundOn g R' J M a) :
AnalyticBoundOn g R' J' M a

Monotonicity of AnalyticBoundOn/eq:analytic:interior:force in the time set J: shrinking the time set preserves the bound.

source
theorem CIV.analyticBoundOn_mono {g : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {R' R'' M M' a a' : ℝ} {J J' : Set ℝ} (ha' : 0 < a') (hM : 0 ≤ M) (hMM' : M ≤ M') (haa' : a' ≤ a) (hR'' : R'' ≤ R') (hJ : J' ⊆ J) (h : AnalyticBoundOn g R' J M a) :
AnalyticBoundOn g R'' J' M' a'

Composite monotonicity of AnalyticBoundOn/eq:analytic:interior:force in all four parameters: the bound can be transferred to a smaller ball, a smaller time set, a larger constant, and a slower analyticity rate simultaneously.