The force increment on an interior pressure collar

The difference of the two classical gradients is the gradient of the annular force potential. Its coefficient is uniform for collars of radius at least one over 128, without an additive data-independent remainder.

noncomputable def CKN.Core.Step4.gapForceIncrement (z : Foundation.Parabolic.ParabolicPoint) {ρ : ℝ} (hρ : 0 < ρ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (i : Fin 3) (w : Foundation.Parabolic.ParabolicPoint) : ℝ

The force-potential increment in the actual pressure decomposition.

Equations

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

noncomputable def CKN.Core.Step4.gapForceIncrementCoefficient : ℝ

An absolute coefficient for the force increment on either half-gap collar.

Equations

• CKN.Core.Step4.gapForceIncrementCoefficient = 400 * CKN.Core.Step4.sliceForcePotentialConstant * CKN.cutoffGradientConstant * 128 ^ 3

theorem CKN.Core.Step4.gapForceIncrementCoefficient_nonneg : 0 ≤ gapForceIncrementCoefficient

The absolute force-increment coefficient is nonnegative.

theorem CKN.Core.Step4.gap_force_increment_eq_pressureP8_ae_of_sws {Ω : 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) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3), ∀ x ∈ Foundation.Parabolic.vec3Ball z.1 (ρ / 2), gapForceIncrement z hρ u p f i (x, s) = classicalGradient (pressureP8 (mollifiedBallCutoff z.1 hρ) f s) x i

Suitability identifies the force increment with the annular force potential's derivative on almost every slice of the half-collar.

theorem CKN.Core.Step4.gap_force_increment_majorant_of_sws {Ω : 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) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) (hlo : 1 / 128 ≤ ρ) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3), ∀ x ∈ Foundation.Parabolic.vec3Ball z.1 (ρ / 2), ‖gapForceIncrement z hρ u p f i (x, s)‖ₑ ≤ ENNReal.ofReal gapForceIncrementCoefficient * ∫⁻ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f (y, s)))

The force increment is bounded by the slice force mass, uniformly for collar radii at least one over 128.