Analytic dependence of Fourier coefficients and angle averages on action parameters, together with the centered perturbation and its uniform norm bound.

@[instance_reducible]

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

Normalized Haar measure for analytic dependence of Fourier coefficients on the action.

Equations

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

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

theorem KamProject.Arnold1963.analyticAt_fourierMonomial {n : ℕ} (k : FourierIndex n) (q : ComplexSpace n) : AnalyticAt ℂ (fourierMonomial k) q

theorem KamProject.Arnold1963.AnalyticPhaseFunction.fourierCoeff_eq_cubeIntegral_all {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (p : ComplexSpace n) (k : FourierIndex n) : f.fourierCoeff p k = unitCubeIntegral fun (t : RealSpace n) => f.toFun (p, scaledAngle t) * fourierMonomial (-k) (scaledAngle t)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.analyticOnNhd_fourierCoeff {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (k : FourierIndex n) : AnalyticOnNhd ℂ (fun (p : ComplexSpace n) => f.fourierCoeff p k) G

theorem KamProject.Arnold1963.AnalyticPhaseFunction.analyticOnNhd_angleAverage {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) : AnalyticOnNhd ℂ f.angleAverage G

theorem KamProject.Arnold1963.AnalyticPhaseFunction.analyticOnNhd_fourierTruncation {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) (N : ℝ) : AnalyticOnNhd ℂ (fun (z : ComplexPhaseSpace n) => fourierTruncation (f.fourierCoeff z.1) N z.2) (phaseDomain G ρ)

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

The angle average packaged as an analytic phase function independent of the angles.

Equations

• One or more equations did not get rendered due to their size.

theorem KamProject.Arnold1963.AnalyticPhaseFunction.uniformNorm_angleAverageFunction_le {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) : f.angleAverageFunction.uniformNorm ≤ f.uniformNorm

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

The phase function with its angle average removed.

Equations

• f.centered = f.sub f.angleAverageFunction

theorem KamProject.Arnold1963.AnalyticPhaseFunction.uniformNorm_centered_le {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) : f.centered.uniformNorm ≤ 2 * f.uniformNorm

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