I1 #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.caccioppoli_I1_heat_operator
{η : Foundation.Parabolic.Vec3 × ℝ → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{t₀ r : ℝ}
{z : Foundation.Parabolic.ParabolicPoint}
(hη : ContDiff ℝ (↑⊤) η)
(ht : z.2 - t₀ < r ^ 2)
:
timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => backwardHeatCutoff η x₀ t₀ r w) z + ∑ i : Fin 3,
spatialSecondPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => backwardHeatCutoff η x₀ t₀ r w) i i z = (timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => η w) z + ∑ i : Fin 3, spatialSecondPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => η w) i i z) * Foundation.Heat.backwardHeatTestFunction r (z.1 - x₀) (z.2 - t₀) + 2 * ∑ i : Fin 3,
spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => η w) i z * (r ^ 2 * Foundation.Heat.heatKernelSpaceDerivative (z.1 - x₀) (r ^ 2 - (z.2 - t₀)) i)
theorem
CKN.caccioppoli_I1_toReal_lintegral_bound
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{U H : α → ENNReal}
{C E : ENNReal}
:
theorem
CKN.caccioppoli_I1_velocity_energy_bound
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(z : Foundation.Parabolic.ParabolicPoint)
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
:
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 2 ≤ ENNReal.ofReal (ρ ^ 3 * alpha u z ρ ^ 2)
theorem
CKN.caccioppoli_I1_cutoff_annulus_pointwise
{x₀ : Foundation.Parabolic.Vec3}
{t₀ ρ R r : ℝ}
(hρ : 0 < ρ)
(hR : ρ / 2 < R)
(hr : 0 < r)
(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))
:
|timePartial
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
backwardHeatCutoff (caccioppoliCutoff x₀ t₀ ρ R hρ hR) x₀ t₀ r w)
z + ∑ i : Fin 3,
spatialSecondPartial
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
backwardHeatCutoff (caccioppoliCutoff x₀ t₀ ρ R hρ hR) x₀ t₀ r w)
i i z| ≤ (32 / (R ^ 2 - (ρ / 2) ^ 2) + 3 * (cutoffSecondDerivativeConstant / ρ ^ 2)) * (8000000 * r ^ 2 / ρ ^ 3) + 6 * (cutoffGradientConstant / ρ) * (5000000 * r ^ 2 / ρ ^ 4)
theorem
CKN.caccioppoli_I1_heat_cutoff_annulus_pointwise
{x₀ : Foundation.Parabolic.Vec3}
{t₀ ρ ε r : ℝ}
(hρ : 0 < ρ)
(hε : 0 < ε)
(hr : 0 < r)
(hscale : r ≤ ρ / 2)
:
ε < r ^ 2 →
∀ {z : Foundation.Parabolic.ParabolicPoint} (ht : z.2 ≤ t₀)
(hp :
(z.1 - x₀, z.2 - t₀) ∈ Foundation.Parabolic.parabolicCylinder 0 0 ρ \ Foundation.Parabolic.parabolicCylinder 0 0 (ρ / 2)),
|timePartial
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r w)
z + ∑ i : Fin 3,
spatialSecondPartial
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r w)
i i z| ≤ (32 / ρ ^ 2 + 3 * (cutoffSecondDerivativeConstant / ρ ^ 2)) * (8000000 * r ^ 2 / ρ ^ 3) + 6 * (cutoffGradientConstant / ρ) * (5000000 * r ^ 2 / ρ ^ 4)
theorem
CKN.caccioppoli_I1_heat_cutoff_inner_zero
{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
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r w)
z + ∑ i : Fin 3,
spatialSecondPartial
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r w)
i i z = 0
theorem
CKN.caccioppoli_I1_heat_cutoff_pointwise_on_cylinder
{x₀ : Foundation.Parabolic.Vec3}
{t₀ ρ ε r : ℝ}
(hρ : 0 < ρ)
(hε : 0 < ε)
(hr : 0 < r)
(hscale : r ≤ ρ / 2)
(hεr : ε < r ^ 2)
{z : Foundation.Parabolic.ParabolicPoint}
(ht : z.2 ≤ t₀)
(hz : (z.1 - x₀, z.2 - t₀) ∈ Foundation.Parabolic.parabolicCylinder 0 0 ρ)
:
|timePartial
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r w)
z + ∑ i : Fin 3,
spatialSecondPartial
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r w)
i i z| ≤ (32 / ρ ^ 2 + 3 * (cutoffSecondDerivativeConstant / ρ ^ 2)) * (8000000 * r ^ 2 / ρ ^ 3) + 6 * (cutoffGradientConstant / ρ) * (5000000 * r ^ 2 / ρ ^ 4)