Documentation

Carleson.Classical.Basic

source
def partialFourierSum (N : ℕ) (f : ℝ → ℂ) (x : ℝ) :
ℂ
Equations
Instances For
    source
    @[simp]
    theorem fourierCoeffOn_mul {a b : ℝ} {hab : a < b} {f : ℝ → ℂ} {c : ℂ} {n : ℤ} :
    fourierCoeffOn hab (fun (x : ℝ) => c * f x) n = c * fourierCoeffOn hab f n
    source
    @[simp]
    theorem fourierCoeffOn_neg {a b : ℝ} {hab : a < b} {f : ℝ → ℂ} {n : ℤ} :
    fourierCoeffOn hab (-f) n = -fourierCoeffOn hab f n
    source
    @[simp]
    theorem fourierCoeffOn_add {a b : ℝ} {hab : a < b} {f g : ℝ → ℂ} {n : ℤ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hg : IntervalIntegrable g MeasureTheory.volume a b) :
    fourierCoeffOn hab (f + g) n = fourierCoeffOn hab f n + fourierCoeffOn hab g n
    source
    @[simp]
    theorem fourierCoeffOn_sub {a b : ℝ} {hab : a < b} {f g : ℝ → ℂ} {n : ℤ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hg : IntervalIntegrable g MeasureTheory.volume a b) :
    fourierCoeffOn hab (f - g) n = fourierCoeffOn hab f n - fourierCoeffOn hab g n
    source
    @[simp]
    theorem partialFourierSum_add {f g : ℝ → ℂ} {N : ℕ} (hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) (hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)) :
    partialFourierSum N (f + g) = partialFourierSum N f + partialFourierSum N g
    source
    @[simp]
    theorem partialFourierSum_sub {f g : ℝ → ℂ} {N : ℕ} (hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) (hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)) :
    partialFourierSum N (f - g) = partialFourierSum N f - partialFourierSum N g
    source
    @[simp]
    theorem partialFourierSum_mul {f : ℝ → ℂ} {a : ℂ} {N : ℕ} :
    (partialFourierSum N fun (x : ℝ) => a * f x) = fun (x : ℝ) => a * partialFourierSum N f x
    source
    theorem fourier_periodic {n : ℤ} :
    Function.Periodic (fun (x : ℝ) => (fourier n) ↑x) (2 * Real.pi)
    source
    theorem partialFourierSum_periodic {f : ℝ → ℂ} {N : ℕ} :
    Function.Periodic (partialFourierSum N f) (2 * Real.pi)
    source
    theorem Function.Periodic.uniformContinuous_of_continuous {f : ℝ → ℂ} {T : ℝ} (hT : 0 < T) (hp : Periodic f T) (hc : ContinuousOn f (Set.Icc (-T) (2 * T))) :
    UniformContinuous f
    source
    theorem fourier_uniformContinuous {n : ℤ} :
    UniformContinuous fun (x : ℝ) => (fourier n) ↑x
    source
    theorem partialFourierSum_uniformContinuous {f : ℝ → ℂ} {N : ℕ} :
    UniformContinuous (partialFourierSum N f)
    source
    theorem strictConvexOn_cos_Icc :
    StrictConvexOn ℝ (Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 2)) Real.cos
    source
    theorem lower_secant_bound_aux {η : ℝ} (ηpos : 0 < η) {x : ℝ} (le_abs_x : η ≤ x) (abs_x_le : x ≤ 2 * Real.pi - η) (x_le_pi : x ≤ Real.pi) (h : Real.pi / 2 < x) :
    2 / Real.pi * η ≤ ‖1 - Complex.exp (Complex.I * ↑x)‖
    source
    theorem lower_secant_bound' {η x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_le : |x| ≤ 2 * Real.pi - η) :
    2 / Real.pi * η ≤ ‖1 - Complex.exp (Complex.I * ↑x)‖
    source
    theorem lower_secant_bound {η x : ℝ} (xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)) (xAbs : η ≤ |x|) :
    η / 2 ≤ ‖1 - Complex.exp (Complex.I * ↑x)‖