Apply compact-image bounds to the KAM limit on the periodic phase quotient. Half-open cells compute finite-stage volume, while closed cells supply compactness for the uniform limit.
def
KamProject.Arnold1963.Iteration.InitialData.retainedClosedCell
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
Set (RealPhaseCover n)
The limiting real action domain paired with a closed fundamental angle cell.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
KamProject.Arnold1963.Iteration.InitialData.retainedClosedCell_compact
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
IsCompact (retainedClosedCell b h)
theorem
KamProject.Arnold1963.Iteration.InitialData.retainedCell_subset_closed
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
retainedCell b h ⊆ retainedClosedCell b h
theorem
KamProject.Arnold1963.Iteration.InitialData.realLimitMap_continuous
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
ContinuousOn (realLimitMap b h) (realSlice (limitDomain b h) ×ˢ Set.univ)
theorem
KamProject.Arnold1963.Iteration.InitialData.projected_cumulative_uniform
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
TendstoUniformlyOn (fun (s : ℕ) => torusProjection ∘ realCumulative b h s) (torusProjection ∘ realLimitMap b h)
Filter.atTop (retainedClosedCell b h)
theorem
KamProject.Arnold1963.Iteration.InitialData.projected_limit_continuous
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
ContinuousOn (torusProjection ∘ realLimitMap b h) (retainedClosedCell b h)
theorem
KamProject.Arnold1963.Iteration.InitialData.projected_limit_image
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
torusProjection ∘ realLimitMap b h '' retainedClosedCell b h = torusLimitMap b h '' realSlice (limitDomain b h) ×ˢ Set.univ
theorem
KamProject.Arnold1963.Iteration.InitialData.torusLimitMap_image_compact
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
IsCompact (torusLimitMap b h '' realSlice (limitDomain b h) ×ˢ Set.univ)
theorem
KamProject.Arnold1963.Iteration.InitialData.torusLimitMap_volume_ge
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
realVolume (limitDomain b h) * ENNReal.ofReal (2 * Real.pi) ^ n ≤ MeasureTheory.volume (torusLimitMap b h '' realSlice (limitDomain b h) ×ˢ Set.univ)
theorem
KamProject.Arnold1963.Iteration.InitialData.torusLimitMap_volume_gt
{n : ℕ}
{Ω₀ : Set (ComplexSpace n)}
{δ₁ θ₀ Θ₀ ρ₀ : NNReal}
{κ D : ℝ}
(b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D)
(h : InitialData n Ω₀ δ₁ θ₀ Θ₀ ρ₀ D)
:
ENNReal.ofReal (1 - κ) * MeasureTheory.volume (realSlice h.domain ×ˢ Set.univ) < MeasureTheory.volume (torusLimitMap b h '' realSlice (limitDomain b h) ×ˢ Set.univ)