Exact images of maximum-norm closed balls under linear forms, and erosion of complex tubes.

theorem KamProject.Arnold1963.covectorLength_nonneg {n : ℕ} (ℓ : RealSpace n) : 0 ≤ covectorLength ℓ

theorem KamProject.Arnold1963.realCovectorPairing_add {n : ℕ} (ℓ : RealSpace n) (x y : ComplexSpace n) : realCovectorPairing ℓ (x + y) = realCovectorPairing ℓ x + realCovectorPairing ℓ y

theorem KamProject.Arnold1963.realCovectorPairing_sub {n : ℕ} (ℓ : RealSpace n) (x y : ComplexSpace n) : realCovectorPairing ℓ (x - y) = realCovectorPairing ℓ x - realCovectorPairing ℓ y

theorem KamProject.Arnold1963.norm_realCovectorPairing_le {n : ℕ} (ℓ : RealSpace n) (z : ComplexSpace n) : ‖realCovectorPairing ℓ z‖ ≤ covectorLength ℓ * ‖z‖

theorem KamProject.Arnold1963.covector_has_lift {n : ℕ} (ℓ : RealSpace n) (hℓ : 0 < covectorLength ℓ) (w : ℂ) : ∃ (v : ComplexSpace n), realCovectorPairing ℓ v = w ∧ ‖v‖ ≤ ‖w‖ / covectorLength ℓ

theorem KamProject.Arnold1963.realCovectorPairing_image_closedBall {n : ℕ} (ℓ : RealSpace n) (hℓ : 0 < covectorLength ℓ) (x : ComplexSpace n) (d : NNReal) : realCovectorPairing ℓ '' Metric.closedBall x ↑d = Metric.closedBall (realCovectorPairing ℓ x) (↑d * covectorLength ℓ)

theorem KamProject.Arnold1963.erosion_tube_complement {n : ℕ} (ℓ : RealSpace n) (hℓ : 0 < covectorLength ℓ) (c a : ℝ) (ha : 0 < a) (d : NNReal) : erosion {z : ComplexSpace n | a ≤ ‖realCovectorPairing ℓ z - ↑c‖} d = {z : ComplexSpace n | a + ↑d * covectorLength ℓ ≤ ‖realCovectorPairing ℓ z - ↑c‖}