Uniform bounds for the right side of the mollified equation

At a time s at which the slice q(·, s) is measurable and essentially bounded by Mq, and the drift slice is bounded and Lipschitz with constant Λ with divergence bounded by Λ, each term of the right side of eq:aniso:comparison:mollified is bounded uniformly in x, with a constant depending only on m, d, ε, Λ and Mq. The bound on the commutator is the one stated after eq:aniso:comparison:mollified.

theorem CIV.abs_integral_kernel_sub_mul_le {m : ℕ} {k K g : CKN.Vec m → ℝ} {M : ℝ} (hK : MeasureTheory.Integrable K MeasureTheory.volume) (hkK : ∀ (w : CKN.Vec m), |k w| ≤ K w) (hg : ∀ᵐ (y : CKN.Vec m), |g y| ≤ M) (x : CKN.Vec m) : |∫ (y : CKN.Vec m), k (x - y) * g y| ≤ M * ∫ (w : CKN.Vec m), K w

Convolution of an essentially bounded function against a kernel dominated by an integrable majorant.

theorem CIV.abs_partialLaplacian_mollifySlice_le {m : ℕ} (d : ℕ) {ε : ℝ} (hε : 0 < ε) {q : CKN.Vec m × ℝ → ℝ} {τ M : ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ M) (x : CKN.Vec m) : |partialLaplacian m d (mollifySlice m ε q) (x, τ)| ≤ M * ∫ (w : CKN.Vec m), |partialLaplacianKernel m d ε w|

theorem CIV.abs_fderiv_mollifierKernel_apply_le {m : ℕ} (ε : ℝ) (w v : CKN.Vec m) : |(fderiv ℝ (mollifierKernel m ε) w) v| ≤ ‖v‖ * ∑ i : Fin m, |(fderiv ℝ (mollifierKernel m ε) w) (CKN.basisVec i)|

theorem CIV.abs_gradPair_mollifySlice_le {m : ℕ} {ε : ℝ} (hε : 0 < ε) {q : CKN.Vec m × ℝ → ℝ} {τ M : ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ M) (x v : CKN.Vec m) : |gradPair m (mollifySlice m ε q) (x, τ) v| ≤ M * (‖v‖ * (mollifierGradConst m / ε))

theorem CIV.abs_diPernaLionsCommutator_le_of_ae {m : ℕ} {ε M : ℝ} {Λ : NNReal} (hε : 0 < ε) (hM : 0 ≤ M) {b : CKN.Vec m → CKN.Vec m} {divb g : CKN.Vec m → ℝ} (hlip : LipschitzWith Λ b) (hdivb : ∀ (y : CKN.Vec m), |divb y| ≤ ↑Λ) (hdivbm : MeasureTheory.AEStronglyMeasurable divb MeasureTheory.volume) (hg : ∀ᵐ (y : CKN.Vec m), |g y| ≤ M) (hgm : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (x : CKN.Vec m) : |diPernaLionsCommutator m ε b divb g x| ≤ ↑Λ * M * (mollifierGradConst m + 1)

The commutator bound |R_ε| ≤ C(m, η) Λ M of eq:aniso:comparison:mollified, for a transported function bounded only almost everywhere.

noncomputable def CIV.mollifiedRHSBound (m d : ℕ) (ε Λ Mq : ℝ) : ℝ

The constant bounding the right side of the mollified equation at a good time.

Equations

• CIV.mollifiedRHSBound m d ε Λ Mq = (Mq * ∫ (w : CKN.Vec m), |CIV.partialLaplacianKernel m d ε w|) + Mq * (Λ * (CIV.mollifierGradConst m / ε)) + Λ * Mq * (CIV.mollifierGradConst m + 1)

theorem CIV.abs_mollifiedRHS_le {m : ℕ} (d : ℕ) {ε Mq : ℝ} {Λ : NNReal} (hε : 0 < ε) (hMq : 0 ≤ Mq) {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q : CKN.Vec m × ℝ → ℝ} {s : ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, s)) MeasureTheory.volume) (hbdd : ∀ᵐ (y : CKN.Vec m), |q (y, s)| ≤ Mq) (hBb : ∀ (x : CKN.Vec m), ‖B (x, s)‖ ≤ ↑Λ) (hBlip : LipschitzWith Λ fun (x : CKN.Vec m) => B (x, s)) (hdiv : ∀ (x : CKN.Vec m), |divB (x, s)| ≤ ↑Λ) (hdivm : MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Vec m) => divB (x, s)) MeasureTheory.volume) (x : CKN.Vec m) : |mollifiedRHS m d ε B divB q x s| ≤ mollifiedRHSBound m d ε (↑Λ) Mq