Real-slice volume is the product Lebesgue measure on Fin n -> R. It is distinct from complex ambient volume. The physical angle cell has side length 2 * pi; Fourier averaging uses unit cells. Measures retain their extended nonnegative values until finiteness has been proved.

noncomputable def KamProject.Arnold1963.realLebesgue (n : ℕ) : MeasureTheory.Measure (RealSpace n)

Product Lebesgue measure on real action coordinates.

Equations

• KamProject.Arnold1963.realLebesgue n = MeasureTheory.Measure.pi fun (x : Fin n) => MeasureTheory.volume

instance KamProject.Arnold1963.realLebesgue_sigmaFinite (n : ℕ) : MeasureTheory.SigmaFinite (realLebesgue n)

noncomputable def KamProject.Arnold1963.realVolume {n : ℕ} (G : Set (ComplexSpace n)) : ENNReal

The Lebesgue measure of a complex action domain's real slice.

Equations

• KamProject.Arnold1963.realVolume G = (KamProject.Arnold1963.realLebesgue n) (KamProject.Arnold1963.realSlice G)

theorem KamProject.Arnold1963.measurableSet_realSlice_of_isCompact {n : ℕ} {G : Set (ComplexSpace n)} (hG : IsCompact G) : MeasurableSet (realSlice G)

theorem KamProject.Arnold1963.realVolume_mono {n : ℕ} {G H : Set (ComplexSpace n)} (hGH : G ⊆ H) : realVolume G ≤ realVolume H

def KamProject.Arnold1963.realAngleCell (n : ℕ) (L : ℝ) : Set (RealSpace n)

A half-open fundamental angle cell of the specified period.

Equations

• KamProject.Arnold1963.realAngleCell n L = Set.univ.pi fun (x : Fin n) => Set.Ioc 0 L

noncomputable def KamProject.Arnold1963.realPhaseLebesgue (n : ℕ) : MeasureTheory.Measure (RealSpace n × RealSpace n)

Product Lebesgue measure on real action and unwrapped angle coordinates.

Equations

• KamProject.Arnold1963.realPhaseLebesgue n = (KamProject.Arnold1963.realLebesgue n).prod (KamProject.Arnold1963.realLebesgue n)

theorem KamProject.Arnold1963.realLebesgue_angleCell (n : ℕ) (L : ℝ) : (realLebesgue n) (realAngleCell n L) = ENNReal.ofReal L ^ n

theorem KamProject.Arnold1963.realPhaseLebesgue_cell {n : ℕ} (G : Set (ComplexSpace n)) (L : ℝ) : (realPhaseLebesgue n) (realSlice G ×ˢ realAngleCell n L) = realVolume G * ENNReal.ofReal L ^ n

theorem KamProject.Arnold1963.realPhaseLebesgue_physicalCell {n : ℕ} (G : Set (ComplexSpace n)) : (realPhaseLebesgue n) (realSlice G ×ˢ realAngleCell n (2 * Real.pi)) = realVolume G * ENNReal.ofReal (2 * Real.pi) ^ n

theorem KamProject.Arnold1963.realPhaseLebesgue_unitCell {n : ℕ} (G : Set (ComplexSpace n)) : (realPhaseLebesgue n) (realSlice G ×ˢ realAngleCell n 1) = realVolume G