Boundary-layer estimates for polydiscs, with the sum of inverse radii as the type constant. The estimate also covers erosion beyond an individual coordinate radius.

noncomputable def KamProject.Arnold1963.polydiscTypeConstant {n : ℕ} (r : RealSpace n) : ℝ

The reciprocal-radius coefficient controlling boundary and slab losses in a polydisc.

Equations

• KamProject.Arnold1963.polydiscTypeConstant r = ∑ j : Fin n, (r j)⁻¹

theorem KamProject.Arnold1963.polydisc_boundary_le {n : ℕ} (c r : RealSpace n) (hr : ∀ (j : Fin n), 0 < r j) (d₁ d₂ : NNReal) (hd : d₁ ≤ d₂) : realVolume (erosion (realCenteredPolydisc c r) d₁ \ erosion (realCenteredPolydisc c r) d₂) ≤ ENNReal.ofReal (polydiscTypeConstant r * (↑d₂ - ↑d₁)) * realVolume (realCenteredPolydisc c r)