Finite-tube domain representations and complete erosion loss bounds, relative to the original domain type constant.
def
KamProject.Arnold1963.finiteTubeDomain
{n : ℕ}
{ι : Type u_1}
(Ω : Set (ComplexSpace n))
(s : Finset ι)
(ℓ : ι → RealSpace n)
(c a : ι → ℝ)
(r : NNReal)
:
Set (ComplexSpace n)
An eroded complex domain with finitely many covector-tube exclusions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
KamProject.Arnold1963.finiteTubeDomain_subset
{n : ℕ}
{ι : Type u_1}
(Ω : Set (ComplexSpace n))
(s : Finset ι)
(ℓ : ι → RealSpace n)
(c a : ι → ℝ)
(r : NNReal)
:
finiteTubeDomain Ω s ℓ c a r ⊆ Ω
theorem
KamProject.Arnold1963.erosion_finiteTubeDomain
{n : ℕ}
{ι : Type u_1}
(Ω : Set (ComplexSpace n))
(s : Finset ι)
(ℓ : ι → RealSpace n)
(c a : ι → ℝ)
(r d : NNReal)
(hℓ : ∀ i ∈ s, 0 < covectorLength (ℓ i))
(ha : ∀ i ∈ s, 0 < a i)
:
erosion (finiteTubeDomain Ω s ℓ c a r) d = finiteTubeDomain Ω s ℓ c (fun (i : ι) => a i + ↑d * covectorLength (ℓ i)) (r + d)
theorem
KamProject.Arnold1963.finiteTube_layer_subset
{n : ℕ}
{ι : Type u_1}
(Ω : Set (ComplexSpace n))
(s : Finset ι)
(ℓ : ι → RealSpace n)
(c a : ι → ℝ)
(r d₁ d₂ : NNReal)
(hℓ : ∀ i ∈ s, 0 < covectorLength (ℓ i))
(ha : ∀ i ∈ s, 0 < a i)
:
erosion (finiteTubeDomain Ω s ℓ c a r) d₁ \ erosion (finiteTubeDomain Ω s ℓ c a r) d₂ ⊆
erosion Ω (r + d₁) \ erosion Ω (r + d₂) ∪ ⋃ i ∈ s,
Ω ∩ {z : ComplexSpace n | a i + ↑d₁ * covectorLength (ℓ i) ≤ ‖realCovectorPairing (ℓ i) z - ↑(c i)‖ ∧ ‖realCovectorPairing (ℓ i) z - ↑(c i)‖ < a i + ↑d₂ * covectorLength (ℓ i)}
theorem
KamProject.Arnold1963.TypeD.finiteTube_erosion_layer
{n : ℕ}
{ι : Type u_1}
{Ω : Set (ComplexSpace n)}
{D : ℝ}
(h : TypeD Ω D)
(s : Finset ι)
(ℓ : ι → RealSpace n)
(c a : ι → ℝ)
(r d₁ d₂ : NNReal)
(hd : d₁ ≤ d₂)
(hℓ : ∀ i ∈ s, 0 < covectorLength (ℓ i))
(ha : ∀ i ∈ s, 0 < a i)
:
realVolume (erosion (finiteTubeDomain Ω s ℓ c a r) d₁ \ erosion (finiteTubeDomain Ω s ℓ c a r) d₂) ≤ ENNReal.ofReal (D * (1 + 2 * ↑n * ↑s.card) * (↑d₂ - ↑d₁)) * realVolume Ω