Documentation

Carleson.Classical.Basic

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

noncomputable def partialFourierSum' {T : ℝ} [hT : Fact (0 < T)] (N : ℕ) (f : AddCircle T → ℂ) :

C(AddCircle T, ℂ )

Equations

partialFourierSum' N f = ∑ n ∈ Finset.Icc (-Int.ofNat N) ↑N, fourierCoeff f n • fourier n

Instances For

theorem partialFourierSum'_comp_equivAddCircle {p q : ℝ} [hp : Fact (0 < p)] [hq : Fact (0 < q)] {f : AddCircle q → ℂ} {N : ℕ} {x : AddCircle q} :

(partialFourierSum' N fun (x : AddCircle p) => f ((AddCircle.equivAddCircle p q ⋯ ⋯) x)) ((AddCircle.equivAddCircle q p ⋯ ⋯) x) = (partialFourierSum' N f) x

noncomputable def partialFourierSumLp {T : ℝ} [hT : Fact (0 < T)] (p : ENNReal) [Fact (1 ≤ p)] (N : ℕ) (f : AddCircle T → ℂ) :

↥(MeasureTheory.Lp ℂ p AddCircle.haarAddCircle)

Equations

partialFourierSumLp p N f = ∑ n ∈ Finset.Icc (-Int.ofNat N) ↑N, fourierCoeff f n • fourierLp p n

Instances For

theorem instFactLtRealOfNatHMulPi_carleson :

Fact (0 < 2 * Real.pi)

theorem partialFourierSum_eq_partialFourierSum' (N : ℕ) (f : ℝ → ℂ) :

AddCircle.liftIoc (2 * Real.pi) 0 (partialFourierSum N f) = ⇑(partialFourierSum' N (AddCircle.liftIoc (2 * Real.pi) 0 f))

theorem partialFourierSum_eq_partialFourierSum'_apply (N : ℕ) (f : ℝ → ℂ) {x : AddCircle (2 * Real.pi)} :

AddCircle.liftIoc (2 * Real.pi) 0 (partialFourierSum N f) x = (partialFourierSum' N (AddCircle.liftIoc (2 * Real.pi) 0 f)) x

theorem partialFourierSum'_eq_partialFourierSum_apply (N : ℕ) (f : AddCircle (2 * Real.pi) → ℂ) {x : ℝ} (hx : x ∈ Set.Ioc 0 (2 * Real.pi)) :

(partialFourierSum' N f) ↑x = partialFourierSum N (fun (x : ℝ) => f ↑x) x

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

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) ⋯

theorem partialFourierSum_aeeq_partialFourierSumLp (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))

@[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

@[simp]

theorem fourierCoeffOn_neg {a b : ℝ} {hab : a < b} {f : ℝ → ℂ} {n : ℤ} :

fourierCoeffOn hab (-f) n = -fourierCoeffOn hab f n

@[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

@[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

@[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

@[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

@[simp]

theorem partialFourierSum_mul {f : ℝ → ℂ} {a : ℂ} {N : ℕ} :

(partialFourierSum N fun (x : ℝ) => a * f x) = fun (x : ℝ) => a * partialFourierSum N f x

theorem fourier_periodic {n : ℤ} :

Function.Periodic (fun (x : ℝ) => (fourier n) ↑x) (2 * Real.pi)

theorem partialFourierSum_periodic {f : ℝ → ℂ} {N : ℕ} :

Function.Periodic (partialFourierSum N f) (2 * Real.pi)

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

theorem fourier_uniformContinuous {n : ℤ} :

UniformContinuous fun (x : ℝ) => (fourier n) ↑x

theorem partialFourierSum_uniformContinuous {f : ℝ → ℂ} {N : ℕ} :

UniformContinuous (partialFourierSum N f)

theorem partialFourierSum_measurable {f : ℝ → ℂ} {N : ℕ} :

Measurable (partialFourierSum N f)

theorem strictConvexOn_cos_Icc :

StrictConvexOn ℝ (Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 2)) Real.cos

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)‖

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)‖

theorem lower_secant_bound {η x : ℝ} (xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)) (xAbs : η ≤ |x|) :

η / 2 ≤ ‖1 - Complex.exp (Complex.I * ↑x)‖