Raw I1 #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.caccioppoli_timePartial_contDiff
{ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
:
ContDiff ℝ ↑⊤ fun (z : Foundation.Parabolic.Vec3 × ℝ) => timePartial ψ z
noncomputable def
CKN.caccioppoliI1HeatCutoffRaw
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{x₀ : Foundation.Parabolic.Vec3}
{t₀ ρ ε r : ℝ}
(hρ : 0 < ρ)
(hε : 0 < ε)
:
Raw energy contribution from the time derivative and Laplacian of the heat cutoff.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CKN.caccioppoli_admissible_heat_cutoff_exists
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{z₀ : Foundation.Parabolic.ParabolicPoint}
{ρ r : ℝ}
(hr : 0 < r)
(hρ : 0 < ρ)
(hI : IsOpen I)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 ρ) ⊆ spaceTimeSet Ω I)
:
Existence of an admissible time increment for the Caccioppoli heat cut-off,
matching the choice of ε₀ at the start of the proof of Lemma lem:caccioppoli
(paper/ckn.tex §13): if a parabolic cylinder lies in the space-time domain
spaceTimeSet Ω I and I is open, then there is 0 < ε < r ^ 2 whose forward
time interval Icc t₀ (t₀ + ε) lies in I. The witness is a function of the
geometry alone, so no suitable-weak-solution data enters its construction.
theorem
CKN.caccioppoli_heat_cutoff_testFunction
{Ω : 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)
{x₀ : Foundation.Parabolic.Vec3}
{t₀ ρ ε r : ℝ}
(hρ : 0 < ρ)
(hε : 0 < ε)
(hr : 0 < r)
(hεr : ε < r ^ 2)
(hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I)
(hfuture : Set.Icc t₀ (t₀ + ε) ⊆ I)
:
backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r ∈ spaceTimeTestFunction Ω I ∧ ∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r z
theorem
CKN.caccioppoli_I1_heat_cutoff_raw_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)
{x₀ : Foundation.Parabolic.Vec3}
{t₀ ρ ε r : ℝ}
(hρ : 0 < ρ)
(hε : 0 < ε)
(hr : 0 < r)
(hscale : r ≤ ρ / 2)
(hεr : ε < r ^ 2)
(hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I)
(hfuture : Set.Icc t₀ (t₀ + ε) ⊆ I)
:
theorem
CKN.caccioppoli_I1_heat_cutoff_raw_normalized
{Ω : 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)
{x₀ : Foundation.Parabolic.Vec3}
{t₀ ρ ε r C₂₅ : ℝ}
(hρ : 0 < ρ)
(hε : 0 < ε)
(hr : 0 < r)
(hscale : r ≤ ρ / 2)
(hεr : ε < r ^ 2)
(hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I)
(hfuture : Set.Icc t₀ (t₀ + ε) ⊆ I)
(hKbound : (32 + 3 * cutoffSecondDerivativeConstant) * 8000000 + 6 * cutoffGradientConstant * 5000000 ≤ C₂₅ ^ 2)
: