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 initial 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.bootstrap_past_convection_source_morrey_le (KU KD : ENNReal) (φ : 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 (11 / 16) → φ z = 0) (hu : ∀ (j : Fin 3), AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z j) MeasureTheory.volume) (hDu : ∀ (j : Fin 3), AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) MeasureTheory.volume) (hUN : ∀ (j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 3) ((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).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 (11 / 16)).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) (25 / 11) ({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.

theorem CKN.Core.Endgame.bootstrap_indicated_components_aemeasurable {Ω : 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) (hunit : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) : (∀ (i : Fin 3), AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) MeasureTheory.volume) ∧ (∀ (i j : Fin 3), AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) MeasureTheory.volume) ∧ AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator p) MeasureTheory.volume ∧ ∀ (i : Fin 3), AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => f z i) MeasureTheory.volume

Every component of the velocity, weak gradient, pressure, and force, indicated to the intermediate one-sided cylinder, is globally a.e. measurable. All measurability is supplied by the local solution clauses.

theorem CKN.Core.Endgame.bootstrap_cutoff_coefficients_zero {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hsupp : ∀ z ∈ tsupport φ, z.2 ≤ 0 → Foundation.Parabolic.parabolicHomeomorph.symm z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)) {z : Foundation.Parabolic.ParabolicPoint} (ht : z.2 ≤ 0) (hz : z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)) : φ z = 0 ∧ timePartial φ z = 0 ∧ (∀ (j : Fin 3), spatialPartial φ j z = 0) ∧ spatialLaplacian (fun (x : Foundation.Parabolic.Vec3) => φ (x, z.2)) z.1 = 0

Past cutoff coefficients vanish outside the larger initial cylinder.

theorem CKN.Core.Endgame.bootstrap_literal_sources_zero_on_past {R : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hsupp : ∀ z ∈ tsupport φ, z.2 ≤ 0 → Foundation.Parabolic.parabolicHomeomorph.symm z ∈ Foundation.Parabolic.parabolicCylinder 0 0 R) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (f Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) {z : Foundation.Parabolic.ParabolicPoint} (ht : z.2 ≤ 0) (hz : z ∉ Foundation.Parabolic.parabolicCylinder 0 0 R) : Step4.localizedGradientSourceG φ u Du f Dp z = 0 ∧ ∀ (j : Fin 3), Step4.localizedGradientSourceH φ u j z = 0

Both literal source slots vanish outside any cylinder containing the cutoff's past support. This statement also applies to the smaller support cylinder used inside the initial norm carrier.

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

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

Equations

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

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

Finite input bounds give a finite numerical source bound.

theorem CKN.Core.Endgame.bootstrap_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 (11 / 16)) (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 / 3) ((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).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 (11 / 16)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) (hDp : ∀ (i : Fin 3), AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) MeasureTheory.volume) (hP : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11) ((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).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) (25 / 11) (causalGradientSourceComponent φ u Du f Dp i) ≤ bootstrapGradientMorreyBound 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.