Fourier coefficients and angle averages from Haar integration on the unit torus, linked to the physical angle period by scaling. The coefficients have uniform bounds and conjugation laws.

@[instance_reducible]

noncomputable def KamProject.Arnold1963.fourierCoefficientMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

Normalized Haar measure for the unit circle used in Fourier coefficient integrals.

Equations

• KamProject.Arnold1963.fourierCoefficientMeasureSpace = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem KamProject.Arnold1963.instIsProbabilityMeasureUnitAddCircleVolume_leanPool : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

noncomputable def KamProject.Arnold1963.unitTorusRepr {n : ℕ} (t : UnitAddTorus (Fin n)) : RealSpace n

Representatives of unit torus coordinates in the interval (0, 1].

Equations

• KamProject.Arnold1963.unitTorusRepr t j = ↑((AddCircle.equivIoc 1 0) (t j))

noncomputable def KamProject.Arnold1963.scaledAngle {n : ℕ} (t : RealSpace n) : ComplexSpace n

Real unit-period coordinates embedded as complex angles with period 2π.

Equations

• KamProject.Arnold1963.scaledAngle t = KamProject.Arnold1963.complexify fun (j : Fin n) => 2 * Real.pi * t j

theorem KamProject.Arnold1963.continuous_scaledAngle (n : ℕ) : Continuous scaledAngle

theorem KamProject.Arnold1963.scaledAngle_mem_strip {n : ℕ} (t : RealSpace n) (ρ : NNReal) : scaledAngle t ∈ angleStrip n ρ

theorem KamProject.Arnold1963.mFourier_eq_fourierMonomial {n : ℕ} (k : FourierIndex n) (t : RealSpace n) : ((UnitAddTorus.mFourier k) fun (j : Fin n) => ↑(t j)) = fourierMonomial k (scaledAngle t)

noncomputable def KamProject.Arnold1963.AnalyticPhaseFunction.torusValue {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (p : ComplexSpace n) (t : UnitAddTorus (Fin n)) : ℂ

Evaluation of a periodic phase function on the unit torus at a fixed action.

Equations

• f.torusValue p t = f.toFun (p, KamProject.Arnold1963.scaledAngle (KamProject.Arnold1963.unitTorusRepr t))

theorem KamProject.Arnold1963.AnalyticPhaseFunction.torusValue_coe {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) (t : RealSpace n) : (f.torusValue p fun (j : Fin n) => ↑(t j)) = f.toFun (p, scaledAngle t)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.continuous_torusValue {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) : Continuous (f.torusValue p)

noncomputable def KamProject.Arnold1963.AnalyticPhaseFunction.onUnitTorus {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (p : ↑G) : C(UnitAddTorus (Fin n), ℂ)

The continuous unit-torus function obtained by fixing an action in the domain.

Equations

• f.onUnitTorus p = { toFun := f.torusValue ↑p, continuous_toFun := ⋯ }

noncomputable def KamProject.Arnold1963.AnalyticPhaseFunction.fourierCoeff {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (p : ComplexSpace n) (k : FourierIndex n) : ℂ

The normalized torus Fourier coefficient at a fixed complex action.

Equations

• f.fourierCoeff p k = UnitAddTorus.mFourierCoeff (f.torusValue p) k

noncomputable def KamProject.Arnold1963.AnalyticPhaseFunction.angleAverage {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (p : ComplexSpace n) : ℂ

The zero Fourier coefficient, representing the angle average.

Equations

• f.angleAverage p = f.fourierCoeff p 0

theorem KamProject.Arnold1963.AnalyticPhaseFunction.fourierCoeff_eq_integral {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (p : ComplexSpace n) (k : FourierIndex n) : f.fourierCoeff p k = UnitAddTorus.mFourierCoeff (f.torusValue p) k

theorem KamProject.Arnold1963.AnalyticPhaseFunction.norm_onUnitTorus_le {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (p : ↑G) : ‖f.onUnitTorus p‖ ≤ f.uniformNorm

theorem KamProject.Arnold1963.AnalyticPhaseFunction.norm_fourierCoeff_le {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) (k : FourierIndex n) : ‖f.fourierCoeff p k‖ ≤ f.uniformNorm

theorem KamProject.Arnold1963.AnalyticPhaseFunction.norm_angleAverage_le {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) : ‖f.angleAverage p‖ ≤ f.uniformNorm

theorem KamProject.Arnold1963.AnalyticPhaseFunction.angleAverage_eq_integral {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (p : ComplexSpace n) : f.angleAverage p = ∫ (t : UnitAddTorus (Fin n)), f.torusValue p t

theorem KamProject.Arnold1963.AnalyticPhaseFunction.norm_sub_angleAverage_le {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p q : ComplexSpace n} (hp : p ∈ G) (hq : q ∈ angleStrip n ρ) : ‖f.toFun (p, q) - f.angleAverage p‖ ≤ 2 * f.uniformNorm

theorem KamProject.Arnold1963.AnalyticPhaseFunction.fourierCoeff_eq_cubeIntegral {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) (k : FourierIndex n) : f.fourierCoeff p k = ∫ (t : RealSpace n) in {t : RealSpace n | ∀ (j : Fin n), t j ∈ Set.Ioc 0 1}, ((UnitAddTorus.mFourier (-k)) fun (j : Fin n) => ↑(t j)) * f.toFun (p, scaledAngle t)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.torusValue_conj {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) (t : UnitAddTorus (Fin n)) : f.torusValue (conjVec p) t = star (f.torusValue p t)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.fourierCoeff_conj {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) (k : FourierIndex n) : f.fourierCoeff (conjVec p) (-k) = star (f.fourierCoeff p k)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.angleAverage_conj {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) : f.angleAverage (conjVec p) = star (f.angleAverage p)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.angleAverage_real_value {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (p : RealSpace n) (hp : complexify p ∈ G) : (f.angleAverage (complexify p)).im = 0

@[simp]

theorem KamProject.Arnold1963.AnalyticPhaseFunction.fourierCoeff_restrict {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {U : Set (ComplexSpace n)} {σ : NNReal} (hUG : U ⊆ G) (hσρ : σ ≤ ρ) (hU : ConjInvariant U) (p : ComplexSpace n) (k : FourierIndex n) : (f.restrict hUG hσρ hU).fourierCoeff p k = f.fourierCoeff p k

@[simp]

theorem KamProject.Arnold1963.AnalyticPhaseFunction.angleAverage_restrict {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {U : Set (ComplexSpace n)} {σ : NNReal} (hUG : U ⊆ G) (hσρ : σ ≤ ρ) (hU : ConjInvariant U) (p : ComplexSpace n) : (f.restrict hUG hσρ hU).angleAverage p = f.angleAverage p

theorem KamProject.Arnold1963.AnalyticPhaseFunction.integral_centered_eq_zero {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) : ∫ (t : UnitAddTorus (Fin n)), f.torusValue p t - f.angleAverage p = 0