Real-centered complex polydiscs and the volumes of their real slices after erosion.

def KamProject.Arnold1963.realCenteredPolydisc {n : ℕ} (c r : RealSpace n) : Set (ComplexSpace n)

The closed coordinate polydisc centered at a real vector.

Equations

• KamProject.Arnold1963.realCenteredPolydisc c r = {z : KamProject.Arnold1963.ComplexSpace n | ∀ (j : Fin n), ‖z j - ↑(c j)‖ ≤ r j}

theorem KamProject.Arnold1963.realSlice_realCenteredPolydisc {n : ℕ} (c r : RealSpace n) : realSlice (realCenteredPolydisc c r) = Set.univ.pi fun (j : Fin n) => Set.Icc (c j - r j) (c j + r j)

theorem KamProject.Arnold1963.isClosed_realCenteredPolydisc {n : ℕ} (c r : RealSpace n) : IsClosed (realCenteredPolydisc c r)

theorem KamProject.Arnold1963.isCompact_realCenteredPolydisc {n : ℕ} (c r : RealSpace n) : IsCompact (realCenteredPolydisc c r)

theorem KamProject.Arnold1963.realVolume_realCenteredPolydisc {n : ℕ} (c r : RealSpace n) : realVolume (realCenteredPolydisc c r) = ∏ j : Fin n, ENNReal.ofReal (2 * r j)

theorem KamProject.Arnold1963.mem_realSlice_erosion_polydisc {n : ℕ} (c r : RealSpace n) (t : NNReal) (x : RealSpace n) : x ∈ realSlice (erosion (realCenteredPolydisc c r) t) ↔ ∀ (j : Fin n), |x j - c j| + ↑t ≤ r j

theorem KamProject.Arnold1963.realSlice_erosion_polydisc {n : ℕ} (c r : RealSpace n) (t : NNReal) : realSlice (erosion (realCenteredPolydisc c r) t) = realSlice (realCenteredPolydisc c fun (j : Fin n) => r j - ↑t)

theorem KamProject.Arnold1963.realVolume_erosion_polydisc {n : ℕ} (c r : RealSpace n) (t : NNReal) : realVolume (erosion (realCenteredPolydisc c r) t) = ∏ j : Fin n, ENNReal.ofReal (2 * (r j - ↑t))