Terms

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.caccioppoli_heat_cutoff_eq_one_on (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ ε r : ℝ) (hρ : 0 < ρ) (hε : 0 < ε) (hr : 0 < r) (hscale : r ≤ ρ / 2) {z : Foundation.Parabolic.Vec3 × ℝ} (hx : z.1 ∈ Foundation.Parabolic.vec3Ball x₀ (ρ / 2)) (ht : z.2 ∈ Set.Ioc (t₀ - r ^ 2) (t₀ + ε / 2)) : caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε z = 1

theorem CKN.caccioppoli_heat_cutoff_derivatives_zero_on_inner (x₀ : Foundation.Parabolic.Vec3) (t₀ ρ ε r : ℝ) (hρ : 0 < ρ) (hε : 0 < ε) (hr : 0 < r) (hscale : r ≤ ρ / 2) {z : Foundation.Parabolic.ParabolicPoint} (hx : z.1 ∈ Foundation.Parabolic.vec3Ball x₀ (ρ / 2)) (ht : z.2 ∈ Set.Ioc (t₀ - r ^ 2) t₀) : timePartial (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) z = 0 ∧ (∀ (i : Fin 3), spatialPartial (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) i z = 0) ∧ ∀ (i j : Fin 3), spatialSecondPartial (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) i j z = 0

theorem CKN.caccioppoli_cutoff_heat_spatialPartial {η : Foundation.Parabolic.Vec3 × ℝ → ℝ} {x₀ : Foundation.Parabolic.Vec3} {t₀ r : ℝ} {z : Foundation.Parabolic.ParabolicPoint} (hη : ContDiff ℝ (↑⊤) η) (ht : z.2 - t₀ < r ^ 2) (i : Fin 3) : spatialPartial (backwardHeatCutoff η x₀ t₀ r) i z = spatialPartial η i z * Foundation.Heat.backwardHeatTestFunction r (z.1 - x₀) (z.2 - t₀) + η z * (r ^ 2 * Foundation.Heat.heatKernelSpaceDerivative (z.1 - x₀) (r ^ 2 - (z.2 - t₀)) i)

theorem CKN.caccioppoli_cutoff_heat_timePartial {η : Foundation.Parabolic.Vec3 × ℝ → ℝ} {x₀ : Foundation.Parabolic.Vec3} {t₀ r : ℝ} {z : Foundation.Parabolic.ParabolicPoint} (hη : ContDiff ℝ (↑⊤) η) (ht : z.2 - t₀ < r ^ 2) : timePartial (backwardHeatCutoff η x₀ t₀ r) z = timePartial η z * Foundation.Heat.backwardHeatTestFunction r (z.1 - x₀) (z.2 - t₀) + η z * (-r ^ 2 * Foundation.Heat.heatKernelTimeDerivative (z.1 - x₀) (r ^ 2 - (z.2 - t₀)))

theorem CKN.caccioppoli_cutoff_le_one {x₀ : Foundation.Parabolic.Vec3} {t₀ ρ R : ℝ} (hρ : 0 < ρ) (hR : ρ / 2 < R) (z : Foundation.Parabolic.Vec3 × ℝ) : caccioppoliCutoff x₀ t₀ ρ R hρ hR z ≤ 1

theorem CKN.caccioppoli_heat_function_upper_on_annulus {x₀ : Foundation.Parabolic.Vec3} {t₀ ρ r : ℝ} (hr : 0 < r) (hρ : 0 < ρ) (hscale : r ≤ ρ / 2) {z : Foundation.Parabolic.ParabolicPoint} (hp : (z.1 - x₀, z.2 - t₀) ∈ Foundation.Parabolic.parabolicCylinder 0 0 ρ \ Foundation.Parabolic.parabolicCylinder 0 0 (ρ / 2)) : Foundation.Heat.backwardHeatTestFunction r (z.1 - x₀) (z.2 - t₀) ≤ 8000000 * r ^ 2 / ρ ^ 3

theorem CKN.caccioppoli_heat_spatial_derivative_abs_on_annulus {x₀ : Foundation.Parabolic.Vec3} {t₀ ρ r : ℝ} (hr : 0 < r) (hρ : 0 < ρ) (hscale : r ≤ ρ / 2) {z : Foundation.Parabolic.ParabolicPoint} (i : Fin 3) (hp : (z.1 - x₀, z.2 - t₀) ∈ Foundation.Parabolic.parabolicCylinder 0 0 ρ \ Foundation.Parabolic.parabolicCylinder 0 0 (ρ / 2)) : |r ^ 2 * Foundation.Heat.heatKernelSpaceDerivative (z.1 - x₀) (r ^ 2 - (z.2 - t₀)) i| ≤ 5000000 * r ^ 2 / ρ ^ 4

theorem CKN.caccioppoli_cutoff_spatial_partial_abs_on_annulus {x₀ : Foundation.Parabolic.Vec3} {t₀ ρ R r : ℝ} (hρ : 0 < ρ) (hR : ρ / 2 < R) (hr : 0 < r) (hscale : r ≤ ρ / 2) {z : Foundation.Parabolic.ParabolicPoint} (i : Fin 3) (hp : (z.1 - x₀, z.2 - t₀) ∈ Foundation.Parabolic.parabolicCylinder 0 0 ρ \ Foundation.Parabolic.parabolicCylinder 0 0 (ρ / 2)) : |spatialPartial (backwardHeatCutoff (caccioppoliCutoff x₀ t₀ ρ R hρ hR) x₀ t₀ r) i z| ≤ 5000000 * r ^ 2 / ρ ^ 4 + 8000000 * cutoffGradientConstant * r ^ 2 / ρ ^ 4