Cauchy Schwarz Energy

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

theorem CIV.integral_abs_mul_abs_le_sqrt_mul_sqrt {m : ℕ} (F c : CKN.Vec m → ℝ) (hF : MeasureTheory.MemLp F 2 MeasureTheory.volume) (hc : MeasureTheory.MemLp c 2 MeasureTheory.volume) : ∫ (x : CKN.Vec m), |F x| * |c x| ≤ √(∫ (x : CKN.Vec m), F x ^ 2) * √(∫ (x : CKN.Vec m), c x ^ 2)

The Cauchy-Schwarz inequality for the Bochner integral on Vec m, in the square-root form the comparison energy estimate consumes.

theorem CIV.two_mul_mul_le_two_mul_abs_mul_abs {m : ℕ} (Phi c chi dfac : CKN.Vec m → ℝ) (x : CKN.Vec m) (hd0 : 0 ≤ dfac x) (hd1 : dfac x ≤ 1) (hchi0 : 0 ≤ chi x) (hchi1 : chi x ≤ 1) : 2 * Phi x * dfac x * c x * chi x ^ 2 ≤ 2 * |Phi x * chi x| * |c x|

The pointwise bound feeding the Cauchy-Schwarz step: a factor in [0, 1] and a cutoff in [0, 1] can both be discarded, at the cost of absolute values.