Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Golf a few proofs #20

Merged
merged 9 commits into from
Jun 7, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions Carleson/Carleson.lean
Original file line number Diff line number Diff line change
Expand Up @@ -68,10 +68,10 @@ theorem Int.le_ceil_iff (c : ℝ) (z : ℤ) : z ≤ ⌈c⌉ ↔ z - 1 < c := by
lemma mem_nonzeroS_iff {i : ℤ} {x : ℝ} (hx : 0 < x) (hD : 1 < D) :
i ∈ nonzeroS D x ↔ (D ^ i * x) ∈ Ioo (4 * D)⁻¹ 2⁻¹ := by
rw [Set.mem_Ioo, nonzeroS, Finset.mem_Icc]
simp [Int.floor_le_iff, Int.le_ceil_iff]
rw [← lt_div_iff hx, mul_comm D⁻¹, ← div_lt_div_iff hx (by positivity)]
rw [← Real.logb_inv, ← Real.logb_inv]
rw [div_inv_eq_mul, ← zpow_add_one₀ (by positivity)]
simp only [Int.floor_le_iff, neg_add_rev, Int.le_ceil_iff, lt_add_neg_iff_add_lt, sub_add_cancel,
mul_inv_rev]
rw [← lt_div_iff hx, mul_comm D⁻¹, ← div_lt_div_iff hx (by positivity), ← Real.logb_inv,
← Real.logb_inv, div_inv_eq_mul, ← zpow_add_one₀ (by positivity)]
simp_rw [← Real.rpow_intCast]
rw [Real.lt_logb_iff_rpow_lt hD (by positivity), Real.logb_lt_iff_lt_rpow hD (by positivity)]
simp [div_eq_mul_inv, mul_comm]
Expand Down
2 changes: 1 addition & 1 deletion Carleson/CoverByBalls.lean
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ lemma CoveredByBalls.zero_right : CoveredByBalls s n 0 ↔ s = ∅ := by
intro hs
have h21 : (∅ : Finset X).card ≤ n := by exact tsub_add_cancel_iff_le.mp rfl
have h22 : s ⊆ ⋃ x ∈ (∅ : Finset X), ball x 0 := by
simp
simp only [not_mem_empty, ball_zero, Set.iUnion_of_empty, Set.iUnion_empty]
exact Set.subset_empty_iff.mpr hs
exact ⟨(∅ : Finset X), h21, h22⟩
exact { mp := h1, mpr := h2 }
Expand Down
19 changes: 10 additions & 9 deletions Carleson/Theorem1_1/Approximation.lean
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ lemma uniformContinuous_iff_bounded [PseudoMetricSpace α] [PseudoMetricSpace β
. intro h ε εpos
obtain ⟨δ, δpos, _, hδ⟩ := h ε εpos
use δ

end section

/- TODO: might be generalized. -/
Expand All @@ -58,7 +59,7 @@ lemma closeSmoothApprox {f : ℝ → ℂ} (unicontf : UniformContinuous f) {ε :
apply ContDiffBump.dist_normed_convolution_le
. exact unicontf.continuous.aestronglyMeasurable
. intro y hy
simp at hy
simp only [Metric.mem_ball] at hy
exact (hδ hy).le

/- Slightly different version-/
Expand Down Expand Up @@ -89,7 +90,7 @@ lemma closeSmoothApproxPeriodic {f : ℝ → ℂ} (unicontf : UniformContinuous
apply ContDiffBump.dist_normed_convolution_le
. exact unicontf.continuous.aestronglyMeasurable
. intro y hy
simp at hy
simp only [Metric.mem_ball] at hy
exact (hδ hy).le

/- Inspired by mathlib : NNReal.summable_of_le-/
Expand Down Expand Up @@ -119,7 +120,7 @@ lemma summable_of_le_on_nonzero {f g : ℤ → ℝ} (hgpos : 0 ≤ g) (hgf : ∀
rw [f'def]
by_cases h : i = 0
. simp [h]
. simp [h]
. simp only [h, ↓reduceIte]
exact hgf i h
apply Real.summable_of_le hgpos this

Expand All @@ -132,7 +133,6 @@ lemma summable_of_le_on_nonzero {f g : ℤ → ℝ} (hgpos : 0 ≤ g) (hgf : ∀
rw [f'def]
simp [hb]


lemma continuous_bounded {f : ℝ → ℂ} (hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))) : ∃ C, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C := by
have interval_compact := (@isCompact_Icc ℝ _ _ _ 0 (2 * Real.pi))
have abs_f_continuousOn := Complex.continuous_abs.comp_continuousOn hf
Expand Down Expand Up @@ -172,7 +172,7 @@ lemma fourierCoeffOn_bound {f : ℝ → ℂ} (f_continuous : Continuous f) : ∃
_ = ∫ (x : ℝ) in (0 : ℝ)..(2 * Real.pi), ‖f x‖ := by
congr
ext x
simp
simp only [norm_mul, Complex.norm_eq_abs]
rw [mul_assoc, mul_comm Complex.I]
norm_cast
rw [Complex.abs_exp_ofReal_mul_I]
Expand Down Expand Up @@ -283,7 +283,8 @@ lemma int_sum_nat {β : Type} [AddCommGroup β] [TopologicalSpace β] [Continuou
rw [this, sum_insert, sum_insert, ih, ←add_assoc]
symm
rw [sum_range_succ, add_comm, ←add_assoc, add_comm]
simp
simp only [Nat.cast_add, Nat.cast_one, neg_add_rev, Int.reduceNeg, Nat.succ_eq_add_one,
Int.ofNat_eq_coe, add_right_inj]
rw [add_comm]
. simp
. norm_num
Expand Down Expand Up @@ -311,13 +312,13 @@ lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : Function.
have summable_maj : Summable maj := by
by_cases Ceq0 : C = 0
. rw [maj_def, Ceq0]
simp
simp only [one_div, mul_zero]
exact summable_zero
. rw [← summable_div_const_iff Ceq0]
convert Real.summable_one_div_int_pow.mpr one_lt_two using 1
rw [maj_def]
ext i
simp
simp only [one_div]
rw [mul_div_cancel_right₀]
exact Ceq0
rw [summable_congr @fourierCoeff_correspondence, ←summable_norm_iff]
Expand All @@ -343,7 +344,7 @@ lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : Function.
convert this.le using 2
congr 1
. rw [g_def]
simp
simp only [ContinuousMap.coe_mk]
rw [AddCircle.liftIco_coe_apply]
rw [zero_add]
exact hx
Expand Down
33 changes: 14 additions & 19 deletions Carleson/Theorem1_1/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -20,32 +20,31 @@ def partialFourierSum (f : ℝ → ℂ) (N : ℕ) : ℝ → ℂ := fun x ↦ ∑
@[simp]
lemma fourierCoeffOn_mul {a b : ℝ} {hab : a < b} {f: ℝ → ℂ} {c : ℂ} {n : ℤ} : fourierCoeffOn hab (fun x ↦ c * f x) n =
c * (fourierCoeffOn hab f n):= by
rw [fourierCoeffOn_eq_integral, fourierCoeffOn_eq_integral]
simp
rw [←mul_assoc, mul_comm c, mul_assoc _ c, mul_comm c, ←intervalIntegral.integral_mul_const]
simp only [fourierCoeffOn_eq_integral, one_div, fourier_apply, neg_smul, fourier_neg',
fourier_coe_apply', Complex.ofReal_sub, smul_eq_mul, Complex.real_smul, Complex.ofReal_inv]
rw [← mul_assoc, mul_comm c, mul_assoc _ c, mul_comm c, ← intervalIntegral.integral_mul_const]
congr
ext x
ring

@[simp]
lemma fourierCoeffOn_neg {a b : ℝ} {hab : a < b} {f: ℝ → ℂ} {n : ℤ} : fourierCoeffOn hab (-f) n =
- (fourierCoeffOn hab f n):= by
rw [fourierCoeffOn_eq_integral, fourierCoeffOn_eq_integral]
simp
- (fourierCoeffOn hab f n):= by simp [fourierCoeffOn_eq_integral, fourierCoeffOn_eq_integral]

@[simp]
lemma 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:= by
rw [fourierCoeffOn_eq_integral, fourierCoeffOn_eq_integral, fourierCoeffOn_eq_integral]
simp
rw [←mul_add, ←intervalIntegral.integral_add]
simp only [fourierCoeffOn_eq_integral, one_div, fourier_apply, neg_smul, fourier_neg',
fourier_coe_apply', Complex.ofReal_sub, Pi.add_apply, smul_eq_mul, Complex.real_smul,
Complex.ofReal_inv]
rw [← mul_add, ← intervalIntegral.integral_add]
congr
ext x
ring
. apply IntervalIntegrable.continuousOn_mul hf
. apply hf.continuousOn_mul
apply Continuous.continuousOn
continuity
. apply IntervalIntegrable.continuousOn_mul hg
. apply hg.continuousOn_mul
apply Continuous.continuousOn
continuity

Expand All @@ -58,16 +57,15 @@ lemma fourierCoeffOn_sub {a b : ℝ} {hab : a < b} {f g : ℝ → ℂ} {n : ℤ}
@[simp]
lemma partialFourierSum_add {f g : ℝ → ℂ} {N : ℕ} (hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) (hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)): partialFourierSum (f + g) N = partialFourierSum f N + partialFourierSum g N := by
ext x
simp
rw [partialFourierSum, partialFourierSum, partialFourierSum, ←sum_add_distrib]
simp [partialFourierSum, partialFourierSum, partialFourierSum, ← sum_add_distrib]
congr
ext n
rw [fourierCoeffOn_add hf hg, add_mul]

@[simp]
lemma partialFourierSum_sub {f g : ℝ → ℂ} {N : ℕ} (hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) (hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)): partialFourierSum (f - g) N = partialFourierSum f N - partialFourierSum g N := by
ext x
simp
simp only [Pi.sub_apply]
rw [partialFourierSum, partialFourierSum, partialFourierSum, ←sum_sub_distrib]
congr
ext n
Expand All @@ -82,9 +80,7 @@ lemma partialFourierSum_mul {f: ℝ → ℂ} {a : ℂ} {N : ℕ}: partialFourier
ext n
rw [fourierCoeffOn_mul, mul_assoc]

lemma fourier_periodic {n : ℤ} : Function.Periodic (fun (x : ℝ) ↦ fourier n (x : AddCircle (2 * Real.pi))) (2 * Real.pi) := by
intro x
simp
lemma fourier_periodic {n : ℤ} : Function.Periodic (fun (x : ℝ) ↦ fourier n (x : AddCircle (2 * Real.pi))) (2 * Real.pi) := by simp

lemma partialFourierSum_periodic {f : ℝ → ℂ} {N : ℕ} : Function.Periodic (partialFourierSum f N) (2 * Real.pi) := by
rw [Function.Periodic]
Expand All @@ -97,8 +93,7 @@ lemma partialFourierSum_periodic {f : ℝ → ℂ} {N : ℕ} : Function.Periodic

/-TODO: Add lemma Periodic.uniformContinuous_of_continuous. -/
lemma fourier_uniformContinuous {n : ℤ} : UniformContinuous (fun (x : ℝ) ↦ fourier n (x : AddCircle (2 * Real.pi))) := by
rw [fourier]
simp
simp [fourier]
--apply Complex.exp_mul_I_periodic.
sorry

Expand Down
5 changes: 1 addition & 4 deletions Carleson/Theorem1_1/Carleson_on_the_real_line.lean
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,11 @@ import Carleson.Theorem1_1.Basic
import Carleson.Theorem1_1.Hilbert_kernel
import Carleson.Theorem1_1.CarlesonOperatorReal


--import Mathlib.Tactic
import Mathlib.Analysis.Fourier.AddCircle
import Mathlib.MeasureTheory.Integral.IntervalIntegral
import Mathlib.Analysis.SpecialFunctions.Integrals


noncomputable section

--#lint
Expand Down Expand Up @@ -53,8 +51,7 @@ lemma h1 : 2 ∈ Set.Ioc 1 (2 : ℝ) := by simp
lemma h2 : Real.IsConjExponent 2 2 := by rw [Real.isConjExponent_iff_eq_conjExponent] <;> norm_num

lemma localOscillation_on_emptyset {X : Type} [PseudoMetricSpace X] {f g : C(X, ℂ)} : localOscillation ∅ f g = 0 := by
rw [localOscillation]
simp
simp [localOscillation]

lemma localOscillation_on_empty_ball {X : Type} [PseudoMetricSpace X] {x : X} {f g : C(X, ℂ)} {R : ℝ} (R_nonpos : R ≤ 0):
localOscillation (Metric.ball x R) f g = 0 := by
Expand Down
3 changes: 1 addition & 2 deletions Carleson/Theorem1_1/ClassicalCarleson.lean
Original file line number Diff line number Diff line change
Expand Up @@ -33,8 +33,7 @@ theorem classical_carleson {f : ℝ → ℂ}
have h_periodic : Function.Periodic h (2 * Real.pi) := Function.Periodic.sub periodic_f₀ periodicf
have h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε' := by
intro x _
rw [hdef]
simp
simp [hdef]
rw [←Complex.dist_eq, dist_comm, Complex.dist_eq]
exact hf₀ x

Expand Down
35 changes: 15 additions & 20 deletions Carleson/Theorem1_1/Dirichlet_kernel.lean
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@ open Complex

noncomputable section


def dirichletKernel (N : ℕ) : ℝ → ℂ := fun x ↦ ∑ n in Icc (-Int.ofNat ↑N) N, fourier n (x : AddCircle (2 * Real.pi))

def dirichletKernel' (N : ℕ) : ℝ → ℂ := fun x ↦ (exp (I * N * x) / (1 - exp (-I * x)) + exp (-I * N * x) / (1 - exp (I * x)))
Expand All @@ -34,37 +33,34 @@ lemma dirichletKernel_eq {N : ℕ} {x : ℝ} (h : cexp (I * x) ≠ 1) : dirichle
= cexp ((N + 1 / 2) * I * x) - cexp (-(N + 1 / 2) * I * x) := by
calc (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) * dirichletKernel N x
_ = ∑ n in Icc (-Int.ofNat N) ↑N, (cexp ((n + 1 / 2) * I * ↑x) - cexp ((n - 1 / 2) * I * ↑x)) := by
rw [dirichletKernel]
rw [mul_sum]
rw [dirichletKernel, mul_sum]
congr
ext n
simp
rw [sub_mul, ←exp_add, ←exp_add]
simp [sub_mul, ← exp_add, ← exp_add]
congr <;>
. ring_nf
congr 1
rw [mul_assoc, mul_assoc]
congr
rw [←mul_assoc, mul_comm, ←mul_assoc, inv_mul_cancel, one_mul]
rw [← mul_assoc, mul_comm, ← mul_assoc, inv_mul_cancel, one_mul]
norm_cast
exact Real.pi_pos.ne.symm
_ = ∑ n in Icc (-Int.ofNat N) ↑N, cexp ((n + 1 / 2) * I * ↑x) - ∑ n in Icc (-Int.ofNat N) ↑N, cexp ((n - 1 / 2) * I * ↑x) := by
rw [sum_sub_distrib]
_ = cexp ((N + 1 / 2) * I * x) - cexp (-(N + 1 / 2) * I * x) := by
rw [←sum_Ico_add_eq_sum_Icc, ←sum_Ioc_add_eq_sum_Icc, add_sub_add_comm]
rw [← sum_Ico_add_eq_sum_Icc, ← sum_Ioc_add_eq_sum_Icc, add_sub_add_comm]
symm
rw [←zero_add (cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x))]
rw [← zero_add (cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x))]
congr
symm
rw [sub_eq_zero]
conv => lhs; rw [←Int.add_sub_cancel (-Int.ofNat N) 1, sub_eq_add_neg, ←Int.add_sub_cancel (Nat.cast N) 1, sub_eq_add_neg, ←sum_Ico_add']
conv => lhs; rw [← Int.add_sub_cancel (-Int.ofNat N) 1, sub_eq_add_neg, ← Int.add_sub_cancel (Nat.cast N) 1, sub_eq_add_neg, ← sum_Ico_add']
congr
. ext n
rw [mem_Ico, mem_Ioc, Int.lt_iff_add_one_le, add_le_add_iff_right, ←mem_Icc, Int.lt_iff_add_one_le, ←mem_Icc]
rw [mem_Ico, mem_Ioc, Int.lt_iff_add_one_le, add_le_add_iff_right, ← mem_Icc, Int.lt_iff_add_one_le, ← mem_Icc]
. ext n
congr
simp
rw [add_assoc, sub_eq_add_neg]
simp [add_assoc, sub_eq_add_neg]
congr
norm_num
. rw [neg_add_rev, add_comm, Int.ofNat_eq_coe, Int.cast_neg, sub_eq_add_neg]
Expand All @@ -75,14 +71,14 @@ lemma dirichletKernel_eq {N : ℕ} {x : ℝ} (h : cexp (I * x) ≠ 1) : dirichle
rw [sub_eq_zero] at h
calc cexp (I * ↑x)
_ = cexp (1 / 2 * I * ↑x) * cexp (1 / 2 * I * ↑x) := by
rw [←exp_add]
rw [← exp_add]
congr
rw [mul_assoc, ←mul_add]
rw [mul_assoc, ← mul_add]
ring
_ = cexp (1 / 2 * I * ↑x) * cexp (-1 / 2 * I * ↑x) := by
congr
_ = 1 := by
rw [←exp_add]
rw [← exp_add]
ring_nf
exact exp_zero
rw [dirichletKernel']
Expand All @@ -94,14 +90,14 @@ lemma dirichletKernel_eq {N : ℕ} {x : ℝ} (h : cexp (I * x) ≠ 1) : dirichle
. contrapose! h
rwa [sub_eq_zero, neg_mul, exp_neg, eq_comm, inv_eq_one] at h
ring_nf
rw [←exp_add, ←exp_add, ←exp_add]
rw [← exp_add, ← exp_add, ← exp_add]
congr 2 <;> ring
. rw [mul_div]
apply eq_div_of_mul_eq
. contrapose! h
rwa [sub_eq_zero, eq_comm] at h
ring_nf
rw [←exp_add, ←exp_add, ←exp_add, neg_add_eq_sub]
rw [← exp_add, ← exp_add, ← exp_add, neg_add_eq_sub]
congr 2 <;> ring

lemma dirichletKernel'_eq_zero {N : ℕ} {x : ℝ} (h : cexp (I * x) = 1) : dirichletKernel' N x = 0 := by
Expand Down Expand Up @@ -163,15 +159,15 @@ lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {N : ℕ} {x :
ext n
rw [fourierCoeffOn_eq_integral, smul_mul_assoc]
_ = (1 / (2 * Real.pi)) * ∑ n in Icc (-Int.ofNat N) ↑N, ((∫ (y : ℝ) in (0 : ℝ)..2 * Real.pi, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by
rw [←smul_sum, real_smul, sub_zero]
rw [← smul_sum, real_smul, sub_zero]
norm_cast
_ = (1 / (2 * Real.pi)) * ∑ n in Icc (-Int.ofNat N) ↑N, ((∫ (y : ℝ) in (0 : ℝ)..2 * Real.pi, (fourier (-n) ↑y • f y) * (fourier n) ↑x)) := by
congr
ext n
symm
apply intervalIntegral.integral_mul_const
_ = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), ∑ n in Icc (-Int.ofNat N) ↑N, (fourier (-n)) y • f y * (fourier n) x := by
rw [←intervalIntegral.integral_finset_sum]
rw [← intervalIntegral.integral_finset_sum]
intro n _
apply IntervalIntegrable.mul_const
apply IntervalIntegrable.continuousOn_mul h fourier_uniformContinuous.continuous.continuousOn
Expand All @@ -194,7 +190,6 @@ lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {N : ℕ} {x :
field_simp
rw [mul_sub, sub_eq_neg_add]


lemma partialFourierSum_eq_conv_dirichletKernel' {f : ℝ → ℂ} {N : ℕ} {x : ℝ} (h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) :
partialFourierSum f N x = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel' N (x - y) := by
have : (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel' N (x - y) = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel N (x - y) := by
Expand Down
Loading
Loading