Fourier reconstruction on shifted real tori inside the complex angle strip.

@[instance_reducible]

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

Normalized Haar measure for contour-shifted Fourier integration.

Equations

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

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

theorem KamProject.Arnold1963.fourierMonomial_add {n : ℕ} (k : FourierIndex n) (q z : ComplexSpace n) : fourierMonomial k (q + z) = fourierMonomial k q * fourierMonomial k z

theorem KamProject.Arnold1963.fourierMonomial_neg_mul {n : ℕ} (k : FourierIndex n) (q : ComplexSpace n) : fourierMonomial (-k) q * fourierMonomial k q = 1

theorem KamProject.Arnold1963.unitFourierWeight_eq_monomial {n : ℕ} (k : FourierIndex n) (q : ComplexSpace n) : unitFourierWeight k q = fourierMonomial (-k) ((angleScale n) q)

theorem KamProject.Arnold1963.angleScale_shift_split {n : ℕ} (y x : RealSpace n) : (angleScale n) (complexShift y x) = scaledAngle x + (angleScale n) (complexShift y 0)

theorem KamProject.Arnold1963.unitFourierWeight_shift_split {n : ℕ} (k : FourierIndex n) (y x : RealSpace n) : unitFourierWeight k (complexShift y x) = unitFourierWeight k (complexify x) * fourierMonomial (-k) ((angleScale n) (complexShift y 0))

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

Evaluation on a complex-shifted unit torus at a fixed action.

Equations

• f.shiftedTorusValue p y t = f.toFun (p, (KamProject.Arnold1963.angleScale n) (KamProject.Arnold1963.complexShift y (KamProject.Arnold1963.unitTorusRepr t)))

theorem KamProject.Arnold1963.AnalyticPhaseFunction.shiftedTorusValue_coe {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) (y : RealSpace n) (hy : ∀ (j : Fin n), |y j| ≤ ↑(normalizedWidth ρ)) (t : RealSpace n) : (f.shiftedTorusValue p y fun (j : Fin n) => ↑(t j)) = f.toFun (p, (angleScale n) (complexShift y t))

theorem KamProject.Arnold1963.AnalyticPhaseFunction.continuous_shiftedTorusValue {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) (y : RealSpace n) (hy : ∀ (j : Fin n), |y j| ≤ ↑(normalizedWidth ρ)) : Continuous (f.shiftedTorusValue p y)

noncomputable def KamProject.Arnold1963.AnalyticPhaseFunction.onShiftedTorus {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) (y : RealSpace n) (hy : ∀ (j : Fin n), |y j| ≤ ↑(normalizedWidth ρ)) : C(UnitAddTorus (Fin n), ℂ)

The continuous shifted-torus function used to move the Fourier integration contour.

Equations

• f.onShiftedTorus hp y hy = { toFun := f.shiftedTorusValue p y, continuous_toFun := ⋯ }

theorem KamProject.Arnold1963.AnalyticPhaseFunction.fourierCoeff_eq_shifted_unitCube {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) (k : FourierIndex n) (y : RealSpace n) (hy : ∀ (j : Fin n), |y j| ≤ ↑(normalizedWidth ρ)) : f.fourierCoeff p k = unitCubeIntegral fun (x : RealSpace n) => f.toFun (p, (angleScale n) (complexShift y x)) * unitFourierWeight k (complexShift y x)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.shiftedCoeff_eq_unitCube {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) (y : RealSpace n) (hy : ∀ (j : Fin n), |y j| ≤ ↑(normalizedWidth ρ)) (k : FourierIndex n) : UnitAddTorus.mFourierCoeff (f.shiftedTorusValue p y) k = unitCubeIntegral fun (x : RealSpace n) => f.toFun (p, (angleScale n) (complexShift y x)) * unitFourierWeight k (complexify x)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.shiftedCoeff_eq {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) (y : RealSpace n) (hy : ∀ (j : Fin n), |y j| ≤ ↑(normalizedWidth ρ)) (k : FourierIndex n) : UnitAddTorus.mFourierCoeff (f.shiftedTorusValue p y) k = f.fourierCoeff p k * fourierMonomial k ((angleScale n) (complexShift y 0))

theorem KamProject.Arnold1963.AnalyticPhaseFunction.hasSum_fourier_shifted {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (f : AnalyticPhaseFunction n G ρ) {p : ComplexSpace n} (hp : p ∈ G) (y : RealSpace n) (hy : ∀ (j : Fin n), |y j| ≤ ↑(normalizedWidth ρ)) {δ : ℝ} (hδ : 0 < δ) (hwidth : ‖imagPart ((angleScale n) (complexShift y 0))‖ ≤ ↑ρ - δ) (t : RealSpace n) : HasSum (fun (k : FourierIndex n) => f.fourierCoeff p k * fourierMonomial k ((angleScale n) (complexShift y t))) (f.toFun (p, (angleScale n) (complexShift y t)))