Skip to content

Commit ffa63b5

Browse files
ldiederingfpvandoorn
ldiedering
and
fpvandoorn
authored
Translate spectral_projection_bound_lp to spectral_projection_bound (#252)
Proved `spectral_projection_bound`, a version of of Lemma 11.1.11 by translating the version `spectral_projection_bound_lp`. --------- Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
1 parent 1d13d8f commit ffa63b5

File tree

8 files changed

+191
-21
lines changed

8 files changed

+191
-21
lines changed

‎Carleson/Classical/Basic.lean‎

Lines changed: 77 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,20 +6,91 @@ import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
66
import Mathlib.Analysis.Convolution
77

88
import Carleson.Classical.Helper
9+
import Carleson.ToMathlib.Misc
10+
import Carleson.ToMathlib.Topology.Instances.AddCircle
11+
import Carleson.ToMathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
12+
import Carleson.ToMathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
913

10-
open Finset Real
14+
15+
open Finset Real MeasureTheory AddCircle
1116

1217
noncomputable section
1318

1419

20+
--TODO: I think the measurability assumptions might be unnecessary
21+
theorem fourierCoeff_eq_fourierCoeff_of_aeeq {T : ℝ} [hT : Fact (0 < T)] {n : ℤ} {f g : AddCircle T → ℂ}
22+
(hf : AEStronglyMeasurable f haarAddCircle) (hg : AEStronglyMeasurable g haarAddCircle)
23+
(h : f =ᵐ[haarAddCircle] g) : fourierCoeff f n = fourierCoeff g n := by
24+
unfold fourierCoeff
25+
apply integral_congr_ae
26+
change @DFunLike.coe C(AddCircle T, ℂ) (AddCircle T) (fun x ↦ ℂ) ContinuousMap.instFunLike (fourier (-n)) * f =ᶠ[ae haarAddCircle] @DFunLike.coe C(AddCircle T, ℂ) (AddCircle T) (fun x ↦ ℂ) ContinuousMap.instFunLike (fourier (-n)) * g
27+
have fourier_measurable : AEStronglyMeasurable (⇑(@fourier T (-n))) haarAddCircle := (ContinuousMap.measurable _).aestronglyMeasurable
28+
29+
rw [← AEEqFun.mk_eq_mk (hf := fourier_measurable.mul hf) (hg := fourier_measurable.mul hg),
30+
← AEEqFun.mk_mul_mk _ _ fourier_measurable hf, ← AEEqFun.mk_mul_mk _ _ fourier_measurable hg]
31+
congr 1
32+
rwa [AEEqFun.mk_eq_mk]
33+
34+
1535
def partialFourierSum (N : ℕ) (f : ℝ → ℂ) (x : ℝ) : ℂ := ∑ n ∈ Icc (-(N : ℤ)) N,
1636
fourierCoeffOn Real.two_pi_pos f n * fourier n (x : AddCircle (2 * π))
1737

18-
--TODO: Add an AddCircle version?
19-
/-
20-
def AddCircle.partialFourierSum' {T : ℝ} [hT : Fact (0 < T)] (N : ℕ) (f : AddCircle T → ℂ) (x : AddCircle T) : ℂ :=
21-
∑ n in Icc (-Int.ofNat ↑N) N, fourierCoeff f n * fourier n x
22-
-/
38+
def partialFourierSum' {T : ℝ} [hT : Fact (0 < T)] (N : ℕ) (f : AddCircle T → ℂ) : C(AddCircle T, ℂ) :=
39+
∑ n ∈ Finset.Icc (-Int.ofNat N) N, fourierCoeff f n • fourier n
40+
41+
def partialFourierSumLp {T : ℝ} [hT : Fact (0 < T)] (p : ENNReal) [Fact (1 ≤ p)] (N : ℕ) (f : AddCircle T → ℂ) : Lp ℂ p (@haarAddCircle T hT) :=
42+
∑ n ∈ Finset.Icc (-Int.ofNat N) N, fourierCoeff f n • fourierLp p n
43+
44+
45+
lemma partialFourierSum_eq_partialFourierSum' [hT : Fact (0 < 2 * Real.pi)] (N : ℕ) (f : ℝ → ℂ) :
46+
liftIoc (2 * Real.pi) 0 (partialFourierSum N f) = partialFourierSum' N (liftIoc (2 * Real.pi) 0 f) := by
47+
ext x
48+
unfold partialFourierSum partialFourierSum' liftIoc
49+
simp only [
50+
Function.comp_apply, Set.restrict_apply, Int.ofNat_eq_coe, ContinuousMap.coe_sum,
51+
ContinuousMap.coe_smul, Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
52+
congr
53+
ext n
54+
rw [← liftIoc, fourierCoeff_liftIoc_eq]
55+
congr 2
56+
. rw [zero_add (2 * Real.pi)]
57+
. rcases (eq_coe_Ioc x) with ⟨b, hb, rfl⟩
58+
rw [← zero_add (2 * Real.pi)] at hb
59+
rw [coe_eq_coe_iff_of_mem_Ioc (Subtype.coe_prop _) hb]
60+
have : (liftIoc (2 * Real.pi) 0 (fun x ↦ x)) b = (fun x ↦ x) b := liftIoc_coe_apply hb
61+
unfold liftIoc at this
62+
rw [Function.comp_apply, Set.restrict_apply] at this
63+
exact this
64+
65+
lemma partialFourierSupLp_eq_partialFourierSupLp_of_aeeq {T : ℝ} [hT : Fact (0 < T)] {p : ENNReal} [Fact (1 ≤ p)] {N : ℕ} {f g : AddCircle T → ℂ}
66+
(hf : AEStronglyMeasurable f haarAddCircle) (hg : AEStronglyMeasurable g haarAddCircle)
67+
(h : f =ᶠ[ae haarAddCircle] g) : partialFourierSumLp p N f = partialFourierSumLp p N g := by
68+
unfold partialFourierSumLp
69+
congr
70+
ext n : 1
71+
congr 1
72+
exact fourierCoeff_eq_fourierCoeff_of_aeeq hf hg h
73+
74+
75+
lemma partialFourierSum'_eq_partialFourierSumLp {T : ℝ} [hT : Fact (0 < T)] (p : ENNReal) [Fact (1 ≤ p)] (N : ℕ) (f : AddCircle T → ℂ) :
76+
partialFourierSumLp p N f = MemLp.toLp (partialFourierSum' N f) ((partialFourierSum' N f).MemLp haarAddCircle ℂ) := by
77+
unfold partialFourierSumLp partialFourierSum'
78+
unfold fourierLp
79+
simp_rw [ContinuousMap.coe_sum, ContinuousMap.coe_smul]
80+
rw [MemLp.toLp_sum _ (by intro n hn; apply MemLp.const_smul (ContinuousMap.MemLp haarAddCircle ℂ (fourier n)))]
81+
rw [Finset.univ_eq_attach]
82+
rw [← Finset.sum_attach]
83+
rfl
84+
85+
86+
lemma partialFourierSum_aeeq_partialFourierSumLp [hT : Fact (0 < 2 * Real.pi)] (p : ENNReal) [Fact (1 ≤ p)] (N : ℕ) (f : ℝ → ℂ) (h_mem_ℒp : MemLp (liftIoc (2 * Real.pi) 0 f) 2 haarAddCircle):
87+
liftIoc (2 * Real.pi) 0 (partialFourierSum N f) =ᶠ[ae haarAddCircle] ↑↑(partialFourierSumLp p N (MemLp.toLp (liftIoc (2 * Real.pi) 0 f) h_mem_ℒp)) := by
88+
rw [partialFourierSupLp_eq_partialFourierSupLp_of_aeeq (Lp.aestronglyMeasurable _) h_mem_ℒp.aestronglyMeasurable (MemLp.coeFn_toLp h_mem_ℒp)]
89+
rw [partialFourierSum'_eq_partialFourierSumLp, partialFourierSum_eq_partialFourierSum']
90+
symm
91+
apply MemLp.coeFn_toLp
92+
93+
2394

2495
local notation "S_" => partialFourierSum
2596

‎Carleson/Classical/HilbertStrongType.lean‎

Lines changed: 41 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -67,22 +67,56 @@ lemma partial_sum_selfadjoint {f g : ℝ → ℂ} {n : ℕ}
6767
∫ x in (0)..2 * π, conj (f x) * partialFourierSum n g x := by
6868
sorry
6969

70+
71+
--lemma eLpNorm_eq_norm {f : ℝ → ℂ} {p : ENNReal} (hf : MemLp f p) :
72+
-- ‖MemLp.toLp f hf‖ = eLpNorm f p := by
73+
-- sorry
74+
75+
theorem AddCircle.haarAddCircle_eq_smul_volume {T : ℝ} [hT : Fact (0 < T)] :
76+
(@haarAddCircle T _) = (ENNReal.ofReal T)⁻¹ • (volume : Measure (AddCircle T)) := by
77+
rw [volume_eq_smul_haarAddCircle, ← smul_assoc, smul_eq_mul, ENNReal.inv_mul_cancel (by simp [hT.out]) ENNReal.ofReal_ne_top, one_smul]
78+
7079
open AddCircle in
7180
/-- Lemma 11.1.11.
7281
The blueprint states this on `[-π, π]`, but I think we can consistently change this to `(0, 2π]`.
7382
-/
7483
-- todo: add lemma that relates `eLpNorm ((Ioc a b).indicator f)` to `∫ x in a..b, _`
75-
lemma spectral_projection_bound {f : ℝ → ℂ} {n : ℕ}
76-
(hmf : Measurable f) (hf : eLpNorm f ∞ < ∞) (periodic_f : f.Periodic (2 * π)) :
84+
lemma spectral_projection_bound {f : ℝ → ℂ} {n : ℕ} (hmf : Measurable f) :
7785
eLpNorm ((Ioc 0 (2 * π)).indicator (partialFourierSum n f)) 2 ≤
7886
eLpNorm ((Ioc 0 (2 * π)).indicator f) 2 := by
79-
-- Note: easiest proof might be by massaging the statement of `spectral_projection_bound_lp`
80-
-- into this
87+
-- Proof by massaging the statement of `spectral_projection_bound_lp` into this.
88+
by_cases hf_L2 : eLpNorm ((Ioc 0 (2 * π)).indicator f) 2 = ⊤
89+
. rw [hf_L2]
90+
exact OrderTop.le_top _
91+
push_neg at hf_L2
92+
rw [← lt_top_iff_ne_top] at hf_L2
8193
have : Fact (0 < 2 * π) := ⟨by positivity⟩
94+
have lift_MemLp : MemLp (liftIoc (2 * π) 0 f) 2 haarAddCircle := by
95+
unfold MemLp
96+
constructor
97+
. rw [haarAddCircle_eq_smul_volume]
98+
apply AEStronglyMeasurable.smul_measure
99+
exact hmf.aestronglyMeasurable.liftIoc (2 * π) 0
100+
. rw [haarAddCircle_eq_smul_volume, eLpNorm_smul_measure_of_ne_top (by trivial), eLpNorm_liftIoc _ _ hmf.aestronglyMeasurable, smul_eq_mul, zero_add]
101+
apply ENNReal.mul_lt_top _ hf_L2
102+
rw [← ENNReal.ofReal_inv_of_pos this.out]
103+
apply ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg ENNReal.ofReal_ne_top
82104
let F : Lp ℂ 2 haarAddCircle :=
83-
MemLp.toLp (AddCircle.liftIoc (2 * π) 0 f) sorry
84-
have := spectral_projection_bound_lp (N := n) F
85-
sorry
105+
MemLp.toLp (AddCircle.liftIoc (2 * π) 0 f) lift_MemLp
106+
107+
have lp_version := spectral_projection_bound_lp (N := n) F
108+
rw [Lp.norm_def, Lp.norm_def,
109+
ENNReal.toReal_le_toReal (Lp.eLpNorm_ne_top (partialFourierSumLp 2 n F)) (Lp.eLpNorm_ne_top F)] at lp_version
110+
111+
rw [← zero_add (2 * π), ← eLpNorm_liftIoc _ _ hmf.aestronglyMeasurable, ← eLpNorm_liftIoc _ _ partialFourierSum_uniformContinuous.continuous.aestronglyMeasurable, volume_eq_smul_haarAddCircle,
112+
eLpNorm_smul_measure_of_ne_top (by trivial), eLpNorm_smul_measure_of_ne_top (by trivial),
113+
smul_eq_mul, smul_eq_mul, ENNReal.mul_le_mul_left (by simp [Real.pi_pos]) (by simp)]
114+
have ae_eq_right : ↑↑F =ᶠ[ae haarAddCircle] liftIoc (2 * π) 0 f := MemLp.coeFn_toLp _
115+
have ae_eq_left : ↑↑(partialFourierSumLp 2 n F) =ᶠ[ae haarAddCircle] liftIoc (2 * π) 0 (partialFourierSum n f) := by
116+
exact Filter.EventuallyEq.symm (partialFourierSum_aeeq_partialFourierSumLp 2 n f lift_MemLp)
117+
rw [← eLpNorm_congr_ae ae_eq_right, ← eLpNorm_congr_ae ae_eq_left]
118+
exact lp_version
119+
86120

87121
/-- Lemma 11.3.1.
88122
The blueprint states this on `[-π, π]`, but I think we can consistently change this to `(0, 2π]`.

‎Carleson/Classical/SpectralProjectionBound.lean‎

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -21,14 +21,6 @@ lemma fourierCoeff_eq_innerProduct {T : ℝ} [hT : Fact (0 < T)] [h2 : Fact (1
2121
rw [← coe_fourierBasis, ← fourierBasis_repr]
2222
exact HilbertBasis.repr_apply_apply fourierBasis f n
2323

24-
25-
noncomputable section
26-
def partialFourierSumLp {T : ℝ} [hT : Fact (0 < T)] (p : ENNReal) [Fact (1 ≤ p)] (N : ℕ) (f : ↥(Lp ℂ 2 (@haarAddCircle T hT))) : Lp ℂ p (@haarAddCircle T hT) :=
27-
∑ n ∈ Finset.Icc (-Int.ofNat N) N, fourierCoeff f n • fourierLp p n
28-
29-
--TODO: add some lemma relating partialFourierSum and partialFourierSumLp
30-
31-
3224
lemma partialFourierSumL2_norm {T : ℝ} [hT : Fact (0 < T)] [h2 : Fact (1 ≤ (2 : ENNReal))] {f : ↥(Lp ℂ 2 haarAddCircle)} {N : ℕ} :
3325
‖partialFourierSumLp 2 N f‖ ^ 2 = ∑ n ∈ Finset.Icc (-Int.ofNat N) N, ‖@fourierCoeff T hT _ _ _ f n‖ ^ 2 := by
3426
calc ‖partialFourierSumLp 2 N f‖ ^ 2

‎Carleson/ToMathlib/MeasureTheory/Function/AEEqFun.lean‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
import Mathlib.MeasureTheory.Function.AEEqFun
2+
import Carleson.ToMathlib.Misc
3+
4+
open MeasureTheory Finset
5+
6+
--TODO: to mathlib
7+
theorem AEEqFun.mk_sum {α E ι : Type*} {m0 : MeasurableSpace α}
8+
{μ : Measure α} [inst : NormedAddCommGroup E] [DecidableEq ι] {s : Finset ι} {f : ι → α → E}
9+
(hf : ∀ i ∈ s, AEStronglyMeasurable (f i) μ) :
10+
AEEqFun.mk (∑ i ∈ s, f i) (Finset.aestronglyMeasurable_sum' s hf) =
11+
∑ i ∈ s.attach, AEEqFun.mk (f ↑i) (hf i (Finset.coe_mem i)) := by
12+
induction' s using Finset.induction_on with i s hi h
13+
. simp_rw [attach_empty, sum_empty]
14+
exact rfl
15+
simp_rw [sum_insert hi]
16+
rw [sum_attach_insert hi, ← AEEqFun.mk_add_mk, h fun i hi ↦ hf i (mem_insert_of_mem hi)]

‎Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
import Carleson.ToMathlib.Misc
2+
import Carleson.ToMathlib.MeasureTheory.Function.AEEqFun
3+
4+
open MeasureTheory
5+
6+
lemma MemLp.toLp_sum {α : Type*} {E : Type*} {m0 : MeasurableSpace α} {p : ENNReal}
7+
{μ : Measure α} [NormedAddCommGroup E] {ι : Type*} [DecidableEq ι] (s : Finset ι) {f : ι → α → E} (hf : ∀ i ∈ s, MemLp (f i) p μ) :
8+
MemLp.toLp (∑ i ∈ s, f i) (memLp_finset_sum' s hf) = ∑ i : ↑s, (MemLp.toLp (f i) (hf i (Finset.coe_mem i))) := by
9+
rw [Finset.univ_eq_attach]
10+
refine Lp.ext_iff.mpr ?_
11+
unfold MemLp.toLp
12+
rw [Subtype.val]
13+
rw [AddSubgroup.val_finset_sum]
14+
refine AEEqFun.ext_iff.mp ?_
15+
apply AEEqFun.mk_sum (fun i hi ↦ (hf i hi).aestronglyMeasurable)

‎Carleson/ToMathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
import Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
2+
3+
open MeasureTheory
4+
5+
lemma ContinuousMap.MemLp {α : Type*} {E : Type*} {m0 : MeasurableSpace α} {p : ENNReal} (μ : Measure α)
6+
[NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [CompactSpace α]
7+
[IsFiniteMeasure μ] (𝕜 : Type*) [Fact (1 ≤ p)] [NormedField 𝕜] [NormedSpace 𝕜 E] (f : C(α, E)) : MemLp f p μ := by
8+
have := Subtype.val_prop (ContinuousMap.toLp p μ 𝕜 f)
9+
have := Lp.mem_Lp_iff_memLp.mp this
10+
rw [ContinuousMap.coe_toLp, memLp_congr_ae (ContinuousMap.coeFn_toAEEqFun _ _)] at this
11+
exact this

‎Carleson/ToMathlib/Misc.lean‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -487,3 +487,16 @@ theorem ofReal_zpow {p : ℝ} (hp : 0 < p) (n : ℤ) :
487487
exact NNReal.coe_ne_zero.mp hp.ne.symm
488488

489489
end ENNReal
490+
491+
492+
--TODO: to mathlib
493+
@[to_additive (attr := simp)]
494+
theorem prod_attach_insert {α β : Type*} {s : Finset α} {a : α} [DecidableEq α] [CommMonoid β]
495+
{f : { i // i ∈ insert a s } → β} (ha : a ∉ s) :
496+
∏ x ∈ (insert a s).attach, f x =
497+
f ⟨a, Finset.mem_insert_self a s⟩ * ∏ x ∈ s.attach, f ⟨x, Finset.mem_insert_of_mem x.2⟩ := by
498+
rw [Finset.attach_insert, Finset.prod_insert, Finset.prod_image]
499+
· intros x hx y hy h
500+
ext
501+
simpa using h
502+
· simp [ha]

‎Carleson/ToMathlib/Topology/Instances/AddCircle.lean‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -65,4 +65,22 @@ theorem liftIco_eq_liftIoc : liftIco p a f = liftIoc p a' f :=
6565

6666
end Periodic
6767

68+
69+
/-- Ioc version of mathlib `coe_eq_coe_iff_of_mem_Ico` -/
70+
lemma coe_eq_coe_iff_of_mem_Ioc {𝕜 : Type*} [LinearOrderedAddCommGroup 𝕜] {p : 𝕜} [hp : Fact (0 < p)]
71+
{a : 𝕜} [Archimedean 𝕜] {x y : 𝕜} (hx : x ∈ Set.Ioc a (a + p)) (hy : y ∈ Set.Ioc a (a + p)) : (x : AddCircle p) = y ↔ x = y := by
72+
refine ⟨fun h => ?_, by tauto⟩
73+
suffices (⟨x, hx⟩ : Set.Ioc a (a + p)) = ⟨y, hy⟩ by exact Subtype.mk.inj this
74+
apply_fun equivIoc p a at h
75+
rw [← (equivIoc p a).right_inv ⟨x, hx⟩, ← (equivIoc p a).right_inv ⟨y, hy⟩]
76+
exact h
77+
78+
/-- Ioc version of mathlib `eq_coe_Ico` -/
79+
lemma eq_coe_Ioc {𝕜 : Type*} [LinearOrderedAddCommGroup 𝕜] {p : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜]
80+
(a : AddCircle p) : ∃ b ∈ Set.Ioc 0 p, ↑b = a := by
81+
let b := QuotientAddGroup.equivIocMod hp.out 0 a
82+
exact ⟨b.1, by simpa only [zero_add] using b.2,
83+
(QuotientAddGroup.equivIocMod hp.out 0).symm_apply_apply a⟩
84+
85+
6886
end AddCircle

0 commit comments

Comments
 (0)
⚡