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' {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_Lp : 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_Lp))
      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)‖