Theta

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

noncomputable def CKN.theta (κ : ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) : ℝ

The iteration quantity θ from the manuscript, eq:theta.

Equations

• CKN.theta κ u Du p z r = CKN.alpha u z r + CKN.beta u Du z r + κ ^ (-4) * CKN.delta p z r ^ 2