Bounds for linear forms over normed fields

This file records a Cramer's-rule bound for two linear forms in two variables and its uniform consequence for a finite family of pairwise non-proportional linear forms.

Main results

• TauCeti.norm_det_mul_max_norm_le: a Cramer's-rule bound for two linear forms.
• TauCeti.half_max_norm_le_norm_sub_of_mul_le: if x is large compared with y, then ‖x - α y‖ is at least half of max(‖x‖, ‖y‖).
• TauCeti.exists_pos_mul_max_norm_le_norm_of_pairwise: all but a smallest member of a finite family of pairwise non-proportional linear forms are uniformly bounded below.

theorem TauCeti.half_max_norm_le_norm_sub_of_mul_le {R : Type u_1} [NormedRing R] (α x y : R) (hbig : 2 * (‖α‖ + 1) * ‖y‖ ≤ ‖x‖) : max ‖x‖ ‖y‖ / 2 ≤ ‖x - α * y‖

If ‖x‖ ≥ 2 (‖α‖ + 1) ‖y‖, then ‖x - α y‖ ≥ max(‖x‖, ‖y‖) / 2.

theorem TauCeti.norm_det_mul_max_norm_le {𝕜 : Type u_1} [NormedField 𝕜] (a b a' b' x y : 𝕜) : ‖a * b' - b * a'‖ * max ‖x‖ ‖y‖ ≤ (‖a‖ + ‖b‖ + ‖a'‖ + ‖b'‖) * (‖a * x + b * y‖ + ‖a' * x + b' * y‖)

Cramer's rule bound for two linear forms L = a x + b y and L' = a' x + b' y in two variables: the determinant D = a b' - b a' satisfies ‖D‖ max(‖x‖, ‖y‖) ≤ (‖a‖ + ‖b‖ + ‖a'‖ + ‖b'‖) (‖L‖ + ‖L'‖).

theorem TauCeti.exists_pos_mul_max_norm_le_norm_of_pairwise {𝕜 : Type u_1} [NormedField 𝕜] {T : Finset (𝕜 × 𝕜)} (hT : (↑T).Pairwise fun (ℓ ℓ' : 𝕜 × 𝕜) => ℓ.1 * ℓ'.2 - ℓ.2 * ℓ'.1 ≠ 0) : ∃ (c : ℝ), 0 < c ∧ ∀ (x y : 𝕜), ∀ ℓ₀ ∈ T, (∀ ℓ ∈ T, ‖ℓ₀.1 * x + ℓ₀.2 * y‖ ≤ ‖ℓ.1 * x + ℓ.2 * y‖) → ∀ ℓ ∈ T, ℓ ≠ ℓ₀ → c * max ‖x‖ ‖y‖ ≤ ‖ℓ.1 * x + ℓ.2 * y‖

Among pairwise non-proportional linear forms ℓ.1 x + ℓ.2 y, ℓ ∈ T, in two variables, all but one are large at every point: there is c > 0 such that if ℓ₀ ∈ T minimizes ‖ℓ.1 x + ℓ.2 y‖, then every other ℓ ∈ T has ‖ℓ.1 x + ℓ.2 y‖ ≥ c max(‖x‖, ‖y‖).