Consumers

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

Consumer-shaped interfaces for the two downstream Caccioppoli displays.

theorem CKN.caccioppoli_gamma_display {Ω : 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) {C₂₅ C₂₆ : ℝ} (hC₂₅ : 0 ≤ C₂₅) (hC₂₆ : 0 ≤ C₂₆) (hK₁ : 6000 * ((Real.pi * 4 / 3) ^ (1 / 3) * ((32 + 3 * cutoffSecondDerivativeConstant) * 8000000 + 6 * cutoffGradientConstant * 5000000)) ≤ C₂₅ ^ 2) (hK₂ : 6000 * (3 * (1500 * cutoffGradientConstant + 900000)) ≤ C₂₅ ^ 2) (hK₃ : 6000 * (3000 * cutoffGradientConstant + 1800000) ≤ C₂₅ ^ 2) (hK₄ : 6000 * (2000 * (4 * Real.pi / 3) ^ (1 / (q / (q - 1)) - 1 / 3)) ≤ C₂₆ ^ 2) {z : Foundation.Parabolic.ParabolicPoint} {r ρ : ℝ} : 0 < ρ → 0 < r → r ≤ ρ / 2 → closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → alpha u z r + beta u Du z r ≤ C₂₅ * (r / ρ * gamma u z ρ + (r / ρ) ^ (-1) * gamma u z ρ ^ (3 / 2) + (r / ρ) ^ (-1) * delta p z ρ * gamma u z ρ ^ (1 / 2)) + C₂₆ * (r / ρ) ^ (-1 / 2) * gamma u z ρ ^ (1 / 2) * lambda q f z ρ ^ (1 / 2)

The solution-level gamma-form Caccioppoli estimate.

theorem CKN.caccioppoli_theta_display {Ω : 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) {C₂₇ C₂₅ C₂₆ : ℝ} (hC₂₅ : caccioppoliC₂₅ ≤ C₂₅) (hC₂₆ : caccioppoliC₂₆ q ≤ C₂₆) (hC₂₇ : 0 < C₂₇) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} : 0 < ρ → closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → alpha u z (iterationKappa C₂₇ * ρ) + beta u Du z (iterationKappa C₂₇ * ρ) ≤ C₂₅ * (iterationKappa C₂₇ * ρ / ρ) * alpha u z ρ + C₂₅ * (iterationKappa C₂₇ * ρ / ρ)⁻¹ * √(alpha u z ρ) * √(beta u Du z ρ) * √(gamma u z ρ) + C₂₅ * (iterationKappa C₂₇ * ρ / ρ)⁻¹ * delta p z ρ * √(gamma u z ρ) + C₂₆ * (iterationKappa C₂₇ * ρ / ρ) ^ (-1 / 2) * √(gamma u z ρ) * √(lambda q f z ρ)

The theta-decay display supplied by the public Caccioppoli theorem.