Quantitative bounds for the actual gradient-slot source

The five terms of the localized equation are estimated from the improved velocity norm, the initial gradient norm, the supplied pressure-gradient norm, and the original force smallness. The formula includes the pressure gradient in the order-two slot. No potential or Hölder estimate is assumed.

The past-time convective heat source

The improved velocity exponent and initial gradient exponent give the convective source estimate by scalar Morrey Hölder and the finite-sum triangle inequality. Only the cutoff's nonpositive-time values are used.

theorem CKN.Core.Endgame.past_convection_source_morrey_le (q : ℝ) (KU KD : ENNReal) (hq : 5 / 2 < q) (φ : Foundation.Parabolic.ParabolicPoint → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (i : Fin 3) (hφ : AEMeasurable φ MeasureTheory.volume) (hφbound : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → |φ z| ≤ 1) (hφsupp : ∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8) → φ z = 0) (hu : ∀ (j : Fin 3), AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z j) MeasureTheory.volume) (hDu : ∀ (j : Fin 3), AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) MeasureTheory.volume) (hUN : ∀ (j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 25 ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z j) ≤ KU) (hDN : ∀ (j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) : AEMeasurable ({z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0}.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => φ z * Step3.localizedConvection u Du z i) MeasureTheory.volume ∧ Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9)) ({z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0}.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => φ z * Step3.localizedConvection u Du z i) ≤ 3 * KU * KD

Component source bounds give the actual past convection source's measurability and quantitative paper-exponent Morrey bound.

noncomputable def CKN.Core.Endgame.causalGradientMorreyBound (q ε₀ C : ℝ) (KU KD KP : ENNReal) : ENNReal

The numerical bound for a component of the final order-two source.

Equations

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

theorem CKN.Core.Endgame.causalGradientMorreyBound_lt_top (q ε₀ C : ℝ) {KU KD KP : ENNReal} (hq : 5 / 2 < q) (hKU : KU < ⊤) (hKD : KD < ⊤) (hKP : KP < ⊤) : causalGradientMorreyBound q ε₀ C KU KD KP < ⊤

Finite input bounds give a finite numerical source bound.

theorem CKN.Core.Endgame.causal_gradient_source_of_suitableWeakSolution (q ε₀ C : ℝ) (KU KD KP : ENNReal) (hq : 5 / 2 < q) (hC : 0 ≤ C) {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {u f Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hφ : φ ∈ spaceTimeTestFunction Ω I) (hφrange : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ φ z ∧ φ z ≤ 1) (hsupp : ∀ z ∈ tsupport φ, z.2 ≤ 0 → Foundation.Parabolic.parabolicHomeomorph.symm z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)) (hder : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), z.2 ≤ 0 → |timePartial φ z| ≤ C ∧ |spatialLaplacian (fun (x : Foundation.Parabolic.Vec3) => φ (x, z.2)) z.1| ≤ C) (hU : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 25 ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) (hD : ∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) (hDp : ∀ (i : Fin 3), AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) MeasureTheory.volume) (hP : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9)) ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) ≤ KP) (hsmall : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀) (i : Fin 3) : AEMeasurable (causalGradientSourceComponent φ u Du f Dp i) MeasureTheory.volume ∧ Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9)) (causalGradientSourceComponent φ u Du f Dp i) ≤ causalGradientMorreyBound q ε₀ C KU KD KP

The concrete past gradient-slot source has the paper exponent and an explicit uniform bound. The pressure-gradient field must be supplied with its indicated component norms; its weak-gradient characterization is needed separately in the representation theorem, not in this algebraic estimate.