Two-sided tube boundary layers. Right limits extend open-slab bounds to closed slabs.

theorem KamProject.Arnold1963.TypeD.realVolume_ne_top {n : ℕ} {Ω : Set (ComplexSpace n)} {D : ℝ} (h : TypeD Ω D) : realVolume Ω ≠ ⊤

theorem KamProject.Arnold1963.TypeD.closed_slab {n : ℕ} {Ω : Set (ComplexSpace n)} {D : ℝ} (h : TypeD Ω D) (ℓ : RealSpace n) (c a : ℝ) (hℓ : 0 < covectorLength ℓ) (ha : 0 ≤ a) : realVolume (Ω ∩ {z : ComplexSpace n | ‖realCovectorPairing ℓ z - ↑c‖ ≤ a}) ≤ ENNReal.ofReal (D * ↑n * (2 * a / covectorLength ℓ)) * realVolume Ω

theorem KamProject.Arnold1963.realCovectorPairing_complexify {n : ℕ} (ℓ x : RealSpace n) : realCovectorPairing ℓ (complexify x) = ↑(∑ j : Fin n, ℓ j * x j)

theorem KamProject.Arnold1963.TypeD.tube_layer {n : ℕ} {Ω : Set (ComplexSpace n)} {D : ℝ} (h : TypeD Ω D) (ℓ : RealSpace n) (c a₁ a₂ : ℝ) (hℓ : 0 < covectorLength ℓ) (_ha₁ : 0 ≤ a₁) (haa : a₁ ≤ a₂) : realVolume (Ω ∩ {z : ComplexSpace n | a₁ ≤ ‖realCovectorPairing ℓ z - ↑c‖ ∧ ‖realCovectorPairing ℓ z - ↑c‖ < a₂}) ≤ ENNReal.ofReal (2 * D * ↑n * ((a₂ - a₁) / covectorLength ℓ)) * realVolume Ω