Geometric domain conditions for boundary layers and slabs. These conditions concern the initial frequency domain and are proved for the polydiscs used in localization.

def KamProject.Arnold1963.realCovectorPairing {n : ℕ} (ℓ : RealSpace n) (z : ComplexSpace n) : ℂ

The complex-linear pairing with a real coordinate covector.

Equations

• KamProject.Arnold1963.realCovectorPairing ℓ z = ∑ j : Fin n, ↑(ℓ j) * z j

def KamProject.Arnold1963.covectorLength {n : ℕ} (ℓ : RealSpace n) : ℝ

The sum of absolute covector coordinates controlling its pairing norm.

Equations

• KamProject.Arnold1963.covectorLength ℓ = ∑ j : Fin n, |ℓ j|

def KamProject.Arnold1963.complexSlab {n : ℕ} (ℓ : RealSpace n) (c a : ℝ) : Set (ComplexSpace n)

The open complex slab cut out by a real covector and scalar center.

Equations

• KamProject.Arnold1963.complexSlab ℓ c a = {z : KamProject.Arnold1963.ComplexSpace n | ‖KamProject.Arnold1963.realCovectorPairing ℓ z - ↑c‖ < a}

structure KamProject.Arnold1963.TypeD {n : ℕ} (Ω : Set (ComplexSpace n)) (D : ℝ) : Prop

Compact positive-volume frequency domains with quantitative boundary and slab-loss bounds.

• constant_pos : 0 < D
• compact : IsCompact Ω
• volume_pos : 0 < realVolume Ω
• boundary (d₁ d₂ : NNReal) : d₁ ≤ d₂ → realVolume (erosion Ω d₁ \ erosion Ω d₂) ≤ ENNReal.ofReal (D * (↑d₂ - ↑d₁)) * realVolume Ω
• slab (ℓ : RealSpace n) (c a : ℝ) : 0 < covectorLength ℓ → 0 ≤ a → realVolume (Ω ∩ complexSlab ℓ c a) ≤ ENNReal.ofReal (D * ↑n * (2 * a / covectorLength ℓ)) * realVolume Ω

theorem KamProject.Arnold1963.realVolume_biUnion_finset_le {n : ℕ} {ι : Type u_1} (s : Finset ι) (f : ι → Set (ComplexSpace n)) : realVolume (⋃ i ∈ s, f i) ≤ ∑ i ∈ s, realVolume (f i)