Documentation

Carleson.Classical.Basic

source
theorem fourierCoeff_eq_fourierCoeff_of_aeeq {T : ℝ} [hT : Fact (0 < T)] {n : ℤ} {f g : AddCircle T → ℂ} (hf : MeasureTheory.AEStronglyMeasurable f AddCircle.haarAddCircle) (hg : MeasureTheory.AEStronglyMeasurable g AddCircle.haarAddCircle) (h : f =ᵐ[AddCircle.haarAddCircle] g) :
fourierCoeff f n = fourierCoeff g n
source
def partialFourierSum (N : ℕ) (f : ℝ → ℂ) (x : ℝ) :
ℂ
Equations
Instances For
    source
    def partialFourierSum' {T : ℝ} [hT : Fact (0 < T)] (N : ℕ) (f : AddCircle T → ℂ) :
    C(AddCircle T, ℂ)
    Equations
    Instances For
      source
      def partialFourierSumLp {T : ℝ} [hT : Fact (0 < T)] (p : ENNReal) [Fact (1 ≤ p)] (N : ℕ) (f : AddCircle T → ℂ) :
      ↥(MeasureTheory.Lp ℂ p AddCircle.haarAddCircle)
      Equations
      Instances For
        source
        theorem partialFourierSum_eq_partialFourierSum' [hT : Fact (0 < 2 * Real.pi)] (N : ℕ) (f : ℝ → ℂ) :
        AddCircle.liftIoc (2 * Real.pi) 0 (partialFourierSum N f) = ⇑(partialFourierSum' N (AddCircle.liftIoc (2 * Real.pi) 0 f))
        source
        theorem partialFourierSupLp_eq_partialFourierSupLp_of_aeeq {T : ℝ} [hT : Fact (0 < T)] {p : ENNReal} [Fact (1 ≤ p)] {N : ℕ} {f g : AddCircle T → ℂ} (hf : MeasureTheory.AEStronglyMeasurable f AddCircle.haarAddCircle) (hg : MeasureTheory.AEStronglyMeasurable g AddCircle.haarAddCircle) (h : f =ᵐ[AddCircle.haarAddCircle] g) :
        partialFourierSumLp p N f = partialFourierSumLp p N g
        source
        theorem partialFourierSum'_eq_partialFourierSumLp {T : ℝ} [hT : Fact (0 < T)] (p : ENNReal) [Fact (1 ≤ p)] (N : ℕ) (f : AddCircle T → ℂ) :
        partialFourierSumLp p N f = MeasureTheory.MemLp.toLp ⇑(partialFourierSum' N f) ⋯
        source
        theorem partialFourierSum_aeeq_partialFourierSumLp [hT : Fact (0 < 2 * Real.pi)] (p : ENNReal) [Fact (1 ≤ p)] (N : ℕ) (f : ℝ → ℂ) (h_mem_ℒp : MeasureTheory.MemLp (AddCircle.liftIoc (2 * Real.pi) 0 f) 2 AddCircle.haarAddCircle) :
        AddCircle.liftIoc (2 * Real.pi) 0 (partialFourierSum N f) =ᵐ[AddCircle.haarAddCircle] ↑↑(partialFourierSumLp p N ↑↑(MeasureTheory.MemLp.toLp (AddCircle.liftIoc (2 * Real.pi) 0 f) h_mem_ℒp))
        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)‖