Raw I3

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

theorem CKN.caccioppoli_heat_cutoff_gradient_sum_bound {x₀ : Foundation.Parabolic.Vec3} {t₀ ρ ε r : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (hr : 0 < r) : r ≤ ρ / 2 → ∀ {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ), ∑ i : Fin 3, |spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r w) i z| ≤ 3 * (cutoffGradientConstant / ρ * (1000 / r) + 300000 * r ^ 2 / r ^ 4)