Normally convergent Fourier series on narrower complex strips and reconstruction on real angles.
noncomputable def
KamProject.Arnold1963.fourierTermOnStrip
{n : ℕ}
(a : FourierIndex n → ℂ)
(σ : NNReal)
(k : FourierIndex n)
:
BoundedOnDomain (angleStrip n σ)
A bounded continuous Fourier summand on a closed complex angle strip.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
KamProject.Arnold1963.norm_fourierTermOnStrip_le_of_decay
{n : ℕ}
{a : FourierIndex n → ℂ}
{M ρ δ : ℝ}
{σ : NNReal}
(hM : 0 ≤ M)
(hσ : ↑σ ≤ ρ - δ)
(ha : ∀ (k : FourierIndex n), ‖a k‖ ≤ M * Real.exp (-(indexLength k * ρ)))
(k : FourierIndex n)
:
theorem
KamProject.Arnold1963.summable_fourierTerms_of_decay
{n : ℕ}
{a : FourierIndex n → ℂ}
{M ρ δ : ℝ}
{σ : NNReal}
(hM : 0 ≤ M)
(hδ : 0 < δ)
(hσ : ↑σ ≤ ρ - δ)
(ha : ∀ (k : FourierIndex n), ‖a k‖ ≤ M * Real.exp (-(indexLength k * ρ)))
:
Summable (fourierTermOnStrip a σ)
theorem
KamProject.Arnold1963.norm_tsum_fourierTerms_le_of_decay
{n : ℕ}
{a : FourierIndex n → ℂ}
{M ρ δ : ℝ}
{σ : NNReal}
(hM : 0 ≤ M)
(hδ : 0 < δ)
(hδ1 : δ ≤ 1)
(hσ : ↑σ ≤ ρ - δ)
(ha : ∀ (k : FourierIndex n), ‖a k‖ ≤ M * Real.exp (-(indexLength k * ρ)))
:
theorem
KamProject.Arnold1963.AnalyticPhaseFunction.hasSum_fourier_real_of_summable
{n : ℕ}
{G : Set (ComplexSpace n)}
{ρ : NNReal}
(f : AnalyticPhaseFunction n G ρ)
{p : ComplexSpace n}
(hp : p ∈ G)
(h : Summable (f.fourierCoeff p))
(t : RealSpace n)
:
HasSum (fun (k : FourierIndex n) => f.fourierCoeff p k * fourierMonomial k (scaledAngle t)) (f.toFun (p, scaledAngle t))
theorem
KamProject.Arnold1963.AnalyticPhaseFunction.summable_fourierCoeff_of_decay
{n : ℕ}
{G : Set (ComplexSpace n)}
{ρ : NNReal}
(f : AnalyticPhaseFunction n G ρ)
(p : ComplexSpace n)
{M : ℝ}
(hρ : 0 < ρ)
(h : ∀ (k : FourierIndex n), ‖f.fourierCoeff p k‖ ≤ M * Real.exp (-(indexLength k * ↑ρ)))
:
Summable (f.fourierCoeff p)