Local Equation Representation #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Localized equation and heat-potential representation #
The cutoff-tested S3 identity is the distribution-free entry point for the local equation. The source terms below are the paper's displayed formulas. The pressure representation is recorded as a structural decomposition, while the pointwise estimate is proved directly from the explicit heat kernels.
def
CKN.Core.Step3.localizedVelocity
(φ : Foundation.Parabolic.ParabolicPoint → ℝ)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
:
Velocity multiplied by the localization cutoff.
Equations
- CKN.Core.Step3.localizedVelocity φ u z = φ z • u z
Instances For
def
CKN.Core.Step3.localizedConvection
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3)
:
Convective derivative of velocity, expressed through its selected weak gradient.
Equations
- CKN.Core.Step3.localizedConvection u Du z i = ∑ j : Fin 3, u z j * Du z i j
Instances For
noncomputable def
CKN.Core.Step3.localizedEquationG
(φ : Foundation.Parabolic.ParabolicPoint → ℝ)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3)
(f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
:
Scalar-source part of the localized heat equation before putting convection in divergence form.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CKN.Core.Step3.localizedEquationH
(φ : Foundation.Parabolic.ParabolicPoint → ℝ)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
:
Divergence-source contribution from differentiating the localization cutoff.
Equations
- CKN.Core.Step3.localizedEquationH φ u i z = (-2 * CKN.spatialPartial φ i z) • u z