Barrier Support

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.posPart_sub_barrier_eq_zero_of_norm_ge {m : ℕ} {M σ K τ₀ τ Minf : ℝ} (hσ : 0 < σ) (hK : 0 ≤ K) (hM : 0 ≤ M) (hτ : τ₀ ≤ τ) {v : CKN.Vec m → ℝ} (hv : ∀ (x : CKN.Vec m), |v x| ≤ Minf) (x : CKN.Vec m) (hx : Minf / σ ≤ ‖x‖) : max (v x - barrier m M σ K τ₀ (x, τ)) 0 = 0

theorem CIV.posPart_mollifySlice_sub_barrier_eq_zero {m : ℕ} {ε M σ K τ₀ τ Minf : ℝ} (hε : 0 < ε) (hσ : 0 < σ) (hK : 0 ≤ K) (hM : 0 ≤ M) (hτ : τ₀ ≤ τ) {q : CKN.Vec m × ℝ → ℝ} (h_meas : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ)) MeasureTheory.volume) (h_bdd : ∀ᵐ (y : CKN.Vec m), |q (y, τ)| ≤ Minf) (x : CKN.Vec m) (hx : Minf / σ ≤ ‖x‖) : max (mollifySlice m ε q (x, τ) - barrier m M σ K τ₀ (x, τ)) 0 = 0

theorem CIV.posPart_sq_le_of_le {a b : ℝ} (h : a ≤ b) : max (a - b) 0 ^ 2 = 0