Bounded Affine

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

theorem CIV.eq_zero_of_abs_mul_le_of_nonneg {c M : ℝ} (h : ∀ (R : ℝ), 0 ≤ R → |R * c| ≤ M) : c = 0

If |R * c| ≤ M for all nonnegative R, then c = 0.

theorem CIV.eq_zero_of_abs_affine_le {c d M : ℝ} (h : ∀ (R : ℝ), |R * c + d| ≤ M) : c = 0

If |R * c + d| ≤ M for all real R, then c = 0.

theorem CIV.eq_zero_of_forall_abs_le_of_tendsto_zero {a : ℝ} {b : ℕ → ℝ} (hb : Filter.Tendsto b Filter.atTop (nhds 0)) (h : ∀ (n : ℕ), |a| ≤ b n) : a = 0

If |a| ≤ b n for all n and b n → 0, then a = 0.

theorem CIV.eq_zero_of_forall_nonneg_abs_affine_le {c d M : ℝ} (h : ∀ (R : ℝ), 0 ≤ R → |c * R + d| ≤ M) : c = 0

If |c * R + d| ≤ M for all R ≥ 0, then c = 0. The proof is by contradiction: if c ≠ 0, pick R = (M + |d| + 1) / |c| (with sign adjusted so R ≥ 0) to force |c * R + d| ≥ M + 1 > M.