Fubini slab estimates using a coordinate with nonzero covector coefficient. The argument retains the maximum norm and introduces no Euclidean norm comparison.

theorem KamProject.Arnold1963.realLebesgue_le_box_of_fiber {n : ℕ} (c r : RealSpace n) (hr : ∀ (i : Fin n), 0 < r i) (j : Fin n) {s : Set (RealSpace n)} (hs : MeasurableSet s) (hsub : s ⊆ realSlice (realCenteredPolydisc c r)) {L : ℝ} (hL : 0 ≤ L) (hfib : ∀ (x : RealSpace n), MeasureTheory.volume {y : ℝ | Function.update x j y ∈ s} ≤ ENNReal.ofReal L) : (realLebesgue n) s ≤ ENNReal.ofReal (L / (2 * r j)) * realVolume (realCenteredPolydisc c r)

theorem KamProject.Arnold1963.polydisc_slab_coordinate_le {n : ℕ} (c r ℓ : RealSpace n) (hr : ∀ (i : Fin n), 0 < r i) (j : Fin n) (hj : ℓ j ≠ 0) (b a : ℝ) (ha : 0 ≤ a) : realVolume (realCenteredPolydisc c r ∩ complexSlab ℓ b a) ≤ ENNReal.ofReal (a / (|ℓ j| * r j)) * realVolume (realCenteredPolydisc c r)

theorem KamProject.Arnold1963.realCenteredPolydisc_typeD {n : ℕ} (hn : 0 < n) (c r : RealSpace n) (hr : ∀ (j : Fin n), 0 < r j) : TypeD (realCenteredPolydisc c r) (polydiscTypeConstant r)