Unit-data control of interior Dirichlet energy

The force coefficient in the gamma-form Caccioppoli estimate has an absolute upper bound. Applying the display on a doubled interior cylinder produces an explicit energy coefficient before any solution is chosen.

noncomputable def CKN.Core.Step4.caccioppoliForceAbsolute : ℝ

An absolute bound for the force coefficient in the gamma display.

Equations

• CKN.Core.Step4.caccioppoliForceAbsolute = √(12000000 * (4 * Real.pi / 3))

theorem CKN.Core.Step4.caccioppoli_force_coefficient_le_absolute {q : ℝ} (hq : 5 / 2 < q) : caccioppoliC₂₆ q ≤ caccioppoliForceAbsolute

The force coefficient is bounded uniformly for every admissible exponent.

noncomputable def CKN.Core.Step4.interiorBetaDataConstant (ρ : ℝ) : ℝ

The explicit half-radius beta coefficient.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.Core.Step4.interiorDirichletDataConstant (ρ : ℝ) : ℝ

The corresponding explicit Dirichlet-energy coefficient.

Equations

• CKN.Core.Step4.interiorDirichletDataConstant ρ = ρ / 2 * CKN.Core.Step4.interiorBetaDataConstant ρ ^ 2

theorem CKN.Core.Step4.interior_dirichlet_bound_of_unit_data (ε : ℝ) (hε : 0 ≤ ε) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) {Ω : 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) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hsmall : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 + ENNReal.ofReal |p w| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q ≤ ENNReal.ofReal ε) (hQ : Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ ⊆ Foundation.Parabolic.parabolicCylinder 0 0 1) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 (ρ / 2), ENNReal.ofReal (spatialGradientSq u Du w) ≤ ENNReal.ofReal (interiorDirichletDataConstant ρ) * (ENNReal.ofReal ε + 1)

A doubled cylinder inside the unit data cylinder has an explicit Dirichlet bound independent of the velocity and gradient Morrey budgets.