From 72d6a5dbc936a73dc3b06da189a668a4e417f732 Mon Sep 17 00:00:00 2001 From: madeve-unipi <56154049+madeve-unipi@users.noreply.github.com> Date: Mon, 22 Jul 2024 12:55:45 +0200 Subject: [PATCH 01/10] Three lines lemma on any strip from the Mathlib version on the unit strip (#38) Not sure this actually needs to be merged, but Hadamard.lean is a generalization of the Mathlib version of the three lines lemma to any vertical strip in the complex plane. --- BonnAnalysis/Hadamard.lean | 251 ++++++++++++++++++++++++ blueprint/src/chapter/interpolation.tex | 5 +- 2 files changed, 254 insertions(+), 2 deletions(-) create mode 100644 BonnAnalysis/Hadamard.lean diff --git a/BonnAnalysis/Hadamard.lean b/BonnAnalysis/Hadamard.lean new file mode 100644 index 0000000..fd20e79 --- /dev/null +++ b/BonnAnalysis/Hadamard.lean @@ -0,0 +1,251 @@ +import Mathlib.Analysis.Complex.Hadamard + +open Set Filter Function Complex Topology HadamardThreeLines + +lemma Real.sub_ne_zero_of_lt {a b : ℝ} (hab: a < b) : b - a ≠ 0 := by apply ne_of_gt; simp[hab] + +namespace Complex + +lemma DiffContOnCl.id {s: Set ℂ} : DiffContOnCl ℂ id s := + DiffContOnCl.mk differentiableOn_id continuousOn_id + +namespace HadamardThreeLines + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] + +/--An auxiliary function to prove the general statement of Hadamard's three lines theorem.-/ +def scale (f: ℂ → E) (l u : ℝ) : ℂ → E := fun z ↦ f (l + z • (u-l)) + +/--The transformation on ℂ that is used for `scale` maps the strip ``re ⁻¹' (l,u)`` + to the strip ``re ⁻¹' (0,1)``-/ +lemma scale_mapsto_dom {l u : ℝ} (hul: l Date: Sat, 27 Jul 2024 14:31:36 +0200 Subject: [PATCH 02/10] Enrich .gitignore (#45) --- .gitignore | 48 +++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 39 insertions(+), 9 deletions(-) diff --git a/.gitignore b/.gitignore index 143d724..8b796ca 100644 --- a/.gitignore +++ b/.gitignore @@ -1,14 +1,44 @@ -/build -/lake-packages -/.lake -/.cache +## macOS .DS_Store +## Lake +.lake/* +.cache/* +.devenv/* +.stfolder/* /lakefile.olean +/lake-packages/* +/build +## Blueprint +/blueprint/lean_decls +/blueprint/print/print.log +/blueprint/web/ +/blueprint/src/web.paux +/blueprint/src/web.bbl +/blueprint/print/ +## Docs +docs/_includes/sorries.md +## TeX *.aux -*.fdb_latexmk -*.fls +*.lof *.log +*.lot +*.fls +*.out +*.toc +*.fmt +*.fot +*.cb +*.cb2 +.*.lb +*.bbl +*.bcf +*.blg +*-blx.aux +*-blx.bib +*.run.xml +*.fdb_latexmk +*.synctex +*.synctex(busy) *.synctex.gz -# Lean blueprint -/blueprint/lean_decls -/blueprint/src/web.bbl \ No newline at end of file +*.synctex.gz(busy) +*.pdfsync From bd5dd48946a229a37f0833c997f4c921f5e7c900 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sat, 27 Jul 2024 14:32:22 +0200 Subject: [PATCH 03/10] Bump actions (#46) ## Changes - [x] Bump actions/cache from 3 to 4 - [x] Bump actions/upload-pages-artifact from 1 to 3 - [x] Bump actions/deploy-pages from 1 to 4 - [x] Bump actions/checkout from 2 to 4 ## Effects - Solved all warnings - Disk space usage seems to be reduced significantly (from 357 MB to just 19 MB), but I think it's nothing but a change in the variable displayed (from uncompressed to compressed size) --- .github/workflows/push.yml | 10 +++++----- .github/workflows/push_pr.yml | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 0605b24..ad15565 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -25,7 +25,7 @@ jobs: name: Build project steps: - name: Checkout project - uses: actions/checkout@v2 + uses: actions/checkout@v4 with: fetch-depth: 0 @@ -42,7 +42,7 @@ jobs: run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis - name: Cache mathlib documentation - uses: actions/cache@v3 + uses: actions/cache@v4 with: path: | .lake/build/doc/Init @@ -105,13 +105,13 @@ jobs: # path: docs/ - name: Upload docs & blueprint artifact to `docs/_site` - uses: actions/upload-pages-artifact@v1 + uses: actions/upload-pages-artifact@v3 with: path: docs/_site - name: Deploy to GitHub Pages id: deployment - uses: actions/deploy-pages@v1 + uses: actions/deploy-pages@v4 - name: Make sure the cache works - run: mv docs/docs .lake/build/doc \ No newline at end of file + run: mv docs/docs .lake/build/doc diff --git a/.github/workflows/push_pr.yml b/.github/workflows/push_pr.yml index 5990d43..5bc24dc 100644 --- a/.github/workflows/push_pr.yml +++ b/.github/workflows/push_pr.yml @@ -7,7 +7,7 @@ jobs: name: Build project steps: - name: Checkout project - uses: actions/checkout@v2 + uses: actions/checkout@v4 with: fetch-depth: 0 From ec564e98099c6ec6e16e35fc27641a28ad30d5b8 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 29 Jul 2024 16:50:20 +0200 Subject: [PATCH 04/10] Create dependabot (#49) Add GitHub action for automated dependency updates. --------- Co-authored-by: Floris van Doorn --- .github/dependabot.yml | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 .github/dependabot.yml diff --git a/.github/dependabot.yml b/.github/dependabot.yml new file mode 100644 index 0000000..4e43547 --- /dev/null +++ b/.github/dependabot.yml @@ -0,0 +1,9 @@ +version: 2 # Specifies the version of the Dependabot configuration file format + +updates: + # Configuration for dependency updates + - package-ecosystem: "github-actions" # Specifies the ecosystem to check for updates + directory: "/" # Specifies the directory to check for dependencies; "/" means the root directory + schedule: + # Check for updates to GitHub Actions every month + interval: "monthly" From ac837f98b1058e47d8b11bfc73669a5398673155 Mon Sep 17 00:00:00 2001 From: stefanalbrecht <147979832+sterecht@users.noreply.github.com> Date: Wed, 14 Aug 2024 15:02:50 +0200 Subject: [PATCH 05/10] Plancharel (#47) The proof of Plancharel's theorem is done, except for one theorem about convolutions that is missing from mathlib (which I didn't notice earlier) and a silly norm-cast lemma that I couldn't figure out. Unfortunately, I couldn't prove that L^1 intersected L^2 is a normed space. I don't understand why, but nothing I tried worked in instance : NormedSpace. This also means that I couldn't even state the following lemmas (The inclusion is DenseInducing, etc.) without throwing errors. I also updated the .tex file, so that the online version should have all the links and the dependency graph should display the progress correctly. (I did not test this, apart from making sure the LaTeX compiles.) --- BonnAnalysis/Plancherel.lean | 591 +++++++++++++++++++++++++-- blueprint/src/chapter/plancherel.tex | 99 +++-- 2 files changed, 628 insertions(+), 62 deletions(-) diff --git a/BonnAnalysis/Plancherel.lean b/BonnAnalysis/Plancherel.lean index 6484f46..1b8abe4 100644 --- a/BonnAnalysis/Plancherel.lean +++ b/BonnAnalysis/Plancherel.lean @@ -3,43 +3,542 @@ import Mathlib.Analysis.Fourier.Inversion import Mathlib.Analysis.Fourier.PoissonSummation import Mathlib.Analysis.Fourier.RiemannLebesgueLemma import BonnAnalysis.StrongType +import Mathlib.Analysis.Convolution noncomputable section -open FourierTransform MeasureTheory Real +open FourierTransform MeasureTheory Real Lp Memℒp Filter Complex Topology ComplexInnerProductSpace ComplexConjugate namespace MeasureTheory -variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] -/-- Part of **Plancherel theorem**: if `f` is in `L¹ ∩ L²` then its Fourier transform is also in -`L²`. -/ -theorem memℒp_fourierIntegral {f : V → E} (hf : Integrable f) (h2f : Memℒp f 2) : - Memℒp (𝓕 f) 2 := sorry -/-- Part of **Plancherel theorem**: if `f` is in `L¹ ∩ L²` then its inverse Fourier transform is -also in `L²`. -/ -theorem memℒp_fourierIntegralInv {f : V → E} (hf : Integrable f) (h2f : Memℒp f 2) : - Memℒp (𝓕⁻ f) 2 := sorry +-- The Fourier transform of conj f is the conjugate of the inverse Fourier transform +lemma fourier_conj {f : V → ℂ} : 𝓕 (conj f) = conj (𝓕 (f ∘ (fun x ↦ -x))) := by + unfold fourierIntegral VectorFourier.fourierIntegral + ext w + simp + rw [← integral_conj, ← integral_neg_eq_self] + apply congrArg (integral volume) + ext v + have : 𝐞 (-⟪v, w⟫_ℝ) • f (-v) = 𝐞 (-⟪v, w⟫_ℝ) * f (-v) := rfl + rw [this, starRingEnd_apply, starRingEnd_apply, star_mul'] + have : 𝐞 (-⟪-v, w⟫_ℝ) • star (f (-v)) = 𝐞 (-⟪-v, w⟫_ℝ) * star (f (-v)) := rfl + rw [this] + simp + left + unfold Real.fourierChar + simp [← Complex.exp_conj, Complex.exp_neg, inv_inv, conj_ofReal] + +-- The fourier transform of a convolution is the product of the individual Fourier transforms +lemma fourier_convolution {f g : V → ℂ} (hf : Integrable f volume) (hg : Integrable g volume) : + 𝓕 (convolution f g (ContinuousLinearMap.mul ℂ ℂ) volume) = (𝓕 f) * (𝓕 g) := by + unfold convolution fourierIntegral VectorFourier.fourierIntegral + simp + ext x + simp + symm + calc (∫ (v : V), 𝐞 (-⟪v, x⟫_ℝ) • f v) * ∫ (v : V), 𝐞 (-⟪v, x⟫_ℝ) • g v + _ = ∫ (v : V), 𝐞 (-⟪v, x⟫_ℝ) • f v * ∫ (w : V), 𝐞 (-⟪w, x⟫_ℝ) • g w := Eq.symm (integral_mul_right _ _) + _ = ∫ (v : V), 𝐞 (-⟪v, x⟫_ℝ) • f v * ∫ (w : V), 𝐞 (-⟪w - v,x⟫_ℝ) • g (w - v) := ?_ + _ = ∫ (v : V) (w : V), 𝐞 (-⟪v, x⟫_ℝ) * 𝐞 (-⟪w - v,x⟫_ℝ) * (f v * g (w - v)) := ?_ + _ = ∫ (v : V) (w : V), 𝐞 (-⟪w, x⟫_ℝ) * (f v * g (w - v)) := ?_ + _ = ∫ (w : V) (v : V), 𝐞 (-⟪w, x⟫_ℝ) * (f v * g (w - v)) := ?_ + _ = ∫ (w : V), 𝐞 (-⟪w, x⟫_ℝ) * ∫ (v : V), f v * g (w - v) := + congrArg (integral volume) <| (Set.eqOn_univ _ _).1 fun _ _ ↦ integral_mul_left _ _ + _ = ∫ (v : V), 𝐞 (-⟪v, x⟫_ℝ) • ∫ (t : V), f t * g (v - t) := rfl + · apply congrArg (integral volume) + ext v + simp + left + exact (@integral_sub_right_eq_self V ℂ _ _ _ volume _ _ _ (fun w ↦ 𝐞 (-⟪w,x⟫_ℝ) • g w) v).symm + · apply congrArg (integral volume) + ext v + rw [← integral_mul_left] + apply congrArg (integral volume) + ext w + have h1 : 𝐞 (-⟪v, x⟫_ℝ) • f v = 𝐞 (-⟪v, x⟫_ℝ) * f v := rfl + have h2 : 𝐞 (-⟪w - v, x⟫_ℝ) • g (w - v) = 𝐞 (-⟪w - v, x⟫_ℝ) * g (w - v) := rfl + rw [h1, h2] + ring + · apply congrArg (integral volume) + ext v + apply congrArg (integral volume) + ext w + apply mul_eq_mul_right_iff.2 + left + unfold Real.fourierChar + simp only [AddChar.coe_mk, mul_neg, coe_inv_unitSphere, expMapCircle_apply, ofReal_mul, ofReal_ofNat] + rw [← Complex.exp_add] + apply congrArg (cexp) + simp + have : ⟪w, x⟫_ℝ = ⟪v, x⟫_ℝ + ⟪w - v, x⟫_ℝ := by + rw [← InnerProductSpace.add_left, add_sub_cancel] + rw [this] + push_cast + ring + · apply integral_integral_swap + rw [integrable_prod_iff] + constructor + · simp + apply ae_of_all volume + intro v + have h : AEStronglyMeasurable (fun a ↦ f v * g (a - v)) volume := by + apply AEStronglyMeasurable.mul aestronglyMeasurable_const + apply AEStronglyMeasurable.comp_measurePreserving (Integrable.aestronglyMeasurable hg) + exact measurePreserving_sub_right volume v + apply (integrable_norm_iff ?_).1 + have : (∀ b, (fun a ↦ ‖(𝐞 (-⟪a,x⟫_ℝ) : ℂ) * (f v * g (a - v))‖) b = (fun a ↦ ‖f v * g (a - v)‖) b) := by + simp + apply (integrable_congr (ae_of_all volume this)).2 + apply (integrable_norm_iff h).2 + apply Integrable.const_mul + exact Integrable.comp_sub_right hg v + apply AEStronglyMeasurable.mul; swap; exact h + have : (fun y ↦ ↑(𝐞 (-⟪y, x⟫_ℝ))) = (Complex.exp ∘ ((- 2 * (π : ℂ) * I) • (fun y ↦ (⟪y, x⟫_ℝ : ℂ)))) := by + ext y + unfold Real.fourierChar + simp[Complex.exp_neg] + exact congrArg cexp (by ring) + rw [this] + apply aestronglyMeasurable_iff_aemeasurable.2 + apply Measurable.comp_aemeasurable Complex.measurable_exp + apply AEMeasurable.const_smul (Continuous.aemeasurable ?_) + have : (fun y ↦ (⟪y, x⟫_ℝ : ℂ)) = ((fun x ↦ (x : ℂ)) : ℝ → ℂ) ∘ ((fun y ↦ ⟪y, x⟫_ℝ) : V → ℝ) := by + ext y; simp + rw [this] + exact Continuous.comp continuous_ofReal (Continuous.inner continuous_id' continuous_const) + · simp + have : (fun x ↦ ∫ (y : V), Complex.abs (f x) * Complex.abs (g (y - x))) = (fun x ↦ ‖f x‖ * ∫ (y : V), Complex.abs (g y)) := by + ext x + rw [← integral_add_right_eq_self _ x] + simp + exact integral_mul_left (Complex.abs (f x)) fun a ↦ Complex.abs (g a) + rw [this] + apply Integrable.mul_const + apply (integrable_norm_iff ?_).2 + exact hf + exact Integrable.aestronglyMeasurable hf + · apply AEStronglyMeasurable.mul + have : AEStronglyMeasurable (fun a ↦ (𝐞 (-⟪a, x⟫_ℝ) : ℂ)) volume := by + unfold Real.fourierChar + simp + apply aestronglyMeasurable_iff_aemeasurable.2 + apply Measurable.comp_aemeasurable measurable_inv + apply Measurable.comp_aemeasurable Complex.measurable_exp + apply AEMeasurable.mul_const _ I + apply AEMeasurable.const_mul + apply Continuous.aemeasurable + have : (fun y ↦ (⟪y, x⟫_ℝ : ℂ)) = ((fun x ↦ (x : ℂ)) : ℝ → ℂ) ∘ ((fun y ↦ ⟪y, x⟫_ℝ) : V → ℝ) := by + ext y; simp + rw [this] + exact Continuous.comp continuous_ofReal (Continuous.inner continuous_id' continuous_const) + exact @AEStronglyMeasurable.snd V V _ _ volume volume _ _ _ _ this + apply AEStronglyMeasurable.mul + exact AEStronglyMeasurable.fst (Integrable.aestronglyMeasurable hf) + have : ((fun a : V × V ↦ g (a.2 - a.1)) = (fun a ↦ g (a.1 - a.2)) ∘ (fun a ↦ (a.2,a.1))) := by + ext a; simp + rw [this] + apply AEStronglyMeasurable.comp_measurePreserving _ (Measure.measurePreserving_swap) + apply AEStronglyMeasurable.comp_aemeasurable + apply AEStronglyMeasurable.mono_ac (quasiMeasurePreserving_sub_of_right_invariant volume volume).absolutelyContinuous + exact hg.1 + exact Measurable.aemeasurable measurable_sub + + +-- The function f ⋆ conj (f(-x)) which is used in Plancharel's theorem +-- We prove that it is continuous and integrable and calculate its Fourier transform +def selfConvolution (f : V → ℂ) := convolution f (conj (fun x ↦ f (-x))) (ContinuousLinearMap.mul ℂ ℂ) + +lemma integrable_selfConvolution {f : V → ℂ} (hf : Integrable f volume) : Integrable (selfConvolution f) volume := by + unfold selfConvolution + apply MeasureTheory.Integrable.integrable_convolution (ContinuousLinearMap.mul ℂ ℂ) hf + apply (integrable_norm_iff _).1 + · have : (fun a ↦ ‖(starRingEnd (V → ℂ)) (fun x ↦ f (-x)) a‖) = (fun a ↦ ‖f (-a)‖) := by + ext a; simp + rw [this] + apply (integrable_norm_iff _).2 + exact Integrable.comp_neg hf + rw [show (fun a ↦ f (-a)) = (f ∘ (fun a ↦ -a)) from by ext a; simp] + apply AEStronglyMeasurable.comp_aemeasurable + rw [Measure.map_neg_eq_self] + exact hf.aestronglyMeasurable + exact AEMeasurable.neg aemeasurable_id + · rw [show ((starRingEnd (V → ℂ)) fun x ↦ f (-x)) = ((starRingEnd ℂ) ∘ (fun x ↦ f (-x))) from ?_] + apply AEStronglyMeasurable.comp_aemeasurable + apply Continuous.aestronglyMeasurable + exact continuous_conj + rw [show (fun a ↦ f (-a)) = (f ∘ (fun a ↦ -a)) from by ext a; simp] + apply AEMeasurable.comp_aemeasurable + rw [Measure.map_neg_eq_self] + exact hf.aemeasurable + exact AEMeasurable.neg aemeasurable_id + ext x + simp + +/- This lemma follows easily from the following fact: + f ⋆ g is continuous if f ∈ L^p and g ∈ L^q with p,q conjugate. + This is listed as TODO in Mathlib.Analysis.Convolution -/ +lemma continuous_selfConvolution {f : V → ℂ} (hf : Memℒp f 2) : Continuous (selfConvolution f) := by + unfold selfConvolution + sorry + + +lemma fourier_selfConvolution {f : V → ℂ} (hf : Integrable f) : + 𝓕 (selfConvolution f) = fun x ↦ (‖𝓕 f x‖ : ℂ) ^ 2 := by + unfold selfConvolution + rw [fourier_convolution, fourier_conj] + ext x; simp + have : ((fun x ↦ f (-x)) ∘ fun x ↦ -x) = f := by ext x; simp + rw [this, mul_conj'] + simp + exact hf + apply (integrable_norm_iff ?_).1 + · have : (fun a ↦ ‖conj (fun x ↦ f (-x)) a‖) = (fun a ↦ ‖f (-a)‖) := by + ext a + simp + rw [this] + exact Integrable.norm (Integrable.comp_neg hf) + · apply aestronglyMeasurable_iff_aemeasurable.2 + apply Measurable.comp_aemeasurable (Continuous.measurable continuous_conj) + exact Integrable.aemeasurable (Integrable.comp_neg hf) + + +-- In the proofs we sometimes have to convert between ∫ and ∫⁻. This is surprisingly tricky, +-- the following two lemmas are helpful +lemma l2norm_bochnerIntegral {f : V → ℂ} (h2f : Memℒp f 2) : snorm f 2 volume = + ENNReal.ofReal ((∫ v : V, ‖f v‖ ^ 2) ^ ((1 : ℝ) / 2)) := by + unfold snorm; simp; unfold snorm'; simp + rw [← ENNReal.ofReal_rpow_of_nonneg] + apply congrArg (fun x ↦ (x ^ (2 : ℝ)⁻¹)) + rw [ofReal_integral_eq_lintegral_ofReal] + · apply congrArg (lintegral volume) + ext x + rw [ENNReal.ofReal_pow] + apply congrArg (fun x ↦ x ^ 2) + rw [← ofReal_norm_eq_coe_nnnorm] + simp + exact AbsoluteValue.nonneg Complex.abs (f x) + · rw [Integrable.eq_1]; constructor + · rw [show (fun v ↦ Complex.abs (f v) ^ 2) = (fun x ↦ x ^ 2) ∘ (fun v ↦ Complex.abs (f v)) from by ext v; simp] + apply aestronglyMeasurable_iff_aemeasurable.2 + apply Measurable.comp_aemeasurable + exact Measurable.pow_const (fun ⦃t⦄ a ↦ a) 2 + apply Measurable.comp_aemeasurable (Continuous.measurable Complex.continuous_abs) + exact aestronglyMeasurable_iff_aemeasurable.1 h2f.1 + · rw [hasFiniteIntegral_def] + rw [show (fun a ↦ (‖Complex.abs (f a) ^ 2‖₊ : ENNReal)) = (fun a ↦ (‖f a‖₊ ^ 2 : ENNReal)) from ?_] + have : snorm f 2 volume < ⊤ := h2f.2 + unfold snorm at this; simp at this; unfold snorm' at this; simp at this + have : ((∫⁻ (a : V), ↑‖f a‖₊ ^ 2) ^ (2 : ℝ)⁻¹) ^ (2 : ℝ) < ⊤ := by + rw [ENNReal.rpow_two] + exact ENNReal.pow_lt_top this 2 + rw [← ENNReal.rpow_mul] at this + simp at this + exact this + ext v + rw [← ofReal_norm_eq_coe_nnnorm, ← ofReal_norm_eq_coe_nnnorm, ← ENNReal.ofReal_pow] + simp + exact norm_nonneg (f v) + · apply ae_of_all volume; simp + · apply integral_nonneg + intro v + simp + · simp + + +lemma integrable_iff_memℒ2 {f : V → ℂ} : Memℒp f 2 ↔ + AEStronglyMeasurable f volume ∧ Integrable (fun v ↦ ‖f v‖ ^ 2) := by + constructor + intro h + constructor + exact h.1 + constructor + · apply aestronglyMeasurable_iff_aemeasurable.2 + rw [show (fun v ↦ ‖f v‖ ^ 2) = (fun v ↦ ‖v‖ ^ 2) ∘ f from by ext v; rfl] + apply Measurable.comp_aemeasurable _ (aestronglyMeasurable_iff_aemeasurable.1 h.1) + exact Continuous.measurable <| Continuous.comp (continuous_pow 2) (continuous_norm) + unfold HasFiniteIntegral + simp + rw [show ∫⁻ (a : V), ↑‖Complex.abs (f a)‖₊ ^ 2 = ∫⁻ (a : V), ↑‖f a‖₊ ^ (2 : ℝ) from ?_] + exact (snorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top (p := 2) (by simp) (by simp)).1 h.2 + apply congrArg (lintegral volume) + ext a + simp [← ofReal_norm_eq_coe_nnnorm] + intro h + constructor + exact h.1 + unfold Integrable HasFiniteIntegral at h + unfold snorm snorm'; simp + rw [show ∫⁻ (a : V), ↑‖(fun v ↦ ‖f v‖ ^ 2) a‖₊ = ∫⁻ (a : V), ↑‖f a‖₊ ^ 2 from ?_] at h + apply (ENNReal.rpow_lt_top_iff_of_pos (by simp)).2 h.2.2 + apply congrArg (lintegral volume) + ext a + simp [← ofReal_norm_eq_coe_nnnorm] + + + +lemma Complex.ofReal_integrable (f : V → ℝ) : Integrable (fun x ↦ f x) ↔ Integrable (fun x ↦ (f x : ℂ)) := by + constructor + exact Integrable.ofReal + intro h + have : Integrable (fun x ↦ (f x : ℂ).re) volume := MeasureTheory.Integrable.re h + simp at this + exact this + + +-- I really don't know why I can't show this, it should be easy. +lemma Complex.ofReal_integral (f : V → ℝ) : ∫ (v : V), f v = ∫ (v : V), (f v : ℂ) := by + by_cases h : Integrable (fun v ↦ f v) + · sorry + · simp [integral_undef h, integral_undef (fun k ↦ h ((ofReal_integrable f).2 k))] + + /-- **Plancherel theorem**: if `f` is in `L¹ ∩ L²` then its Fourier transform has the same `L²` norm as that of `f`. -/ -theorem snorm_fourierIntegral {f : V → E} (hf : Integrable f) (h2f : Memℒp f 2) : - snorm (𝓕 f) 2 volume = snorm f 2 volume := sorry +theorem snorm_fourierIntegral {f : V → ℂ} (hf : Integrable f) (h2f : Memℒp f 2) : + snorm (𝓕 f) 2 volume = snorm f 2 volume := by + have hpos : {c : ℝ | c > 0} ∈ atTop := by + simp only [gt_iff_lt, mem_atTop_sets, ge_iff_le, Set.mem_setOf_eq] + use 1; intro b h; linarith + have lim1 : Tendsto (fun (c : ℝ) ↦ ∫ v : V, cexp (-c⁻¹ * ‖v‖ ^ 2) * 𝓕 (selfConvolution f) v) atTop + (𝓝 (∫ v : V, ‖f v‖ ^ 2)) := by + have : (fun (c : ℝ) ↦ (∫ v : V, 𝓕 (fun w ↦ cexp (-c⁻¹ * ‖w‖ ^ 2)) v * (selfConvolution f v))) =ᶠ[atTop] (fun c ↦ ∫ v : V, cexp (-c⁻¹ * ‖v‖ ^ 2) * 𝓕 (selfConvolution f) v) := by + apply Filter.eventuallyEq_of_mem hpos + intro c hc + dsimp + unfold fourierIntegral + rw [show ∫ (v : V), VectorFourier.fourierIntegral 𝐞 volume (innerₗ V) (fun w ↦ cexp (-c⁻¹ * ↑‖w‖ ^ 2)) v * selfConvolution f v = + ∫ (v : V), (ContinuousLinearMap.mul ℂ ℂ) (VectorFourier.fourierIntegral 𝐞 volume (innerₗ V) (fun w ↦ cexp (-c⁻¹ * ↑‖w‖ ^ 2)) v) (selfConvolution f v) from ?_]; swap + · apply congrArg (integral volume) + simp + rw [VectorFourier.integral_bilin_fourierIntegral_eq_flip] + simp + · exact continuous_fourierChar + · simp + exact continuous_inner + · simpa using GaussianFourier.integrable_cexp_neg_mul_sq_norm_add (by simpa) 0 (0 : V) + · exact integrable_selfConvolution hf + apply Tendsto.congr' this + apply Tendsto.congr' (show ((fun (c : ℝ) ↦ ∫ v : V, ((π * c) ^ (FiniteDimensional.finrank ℝ V / 2 : ℂ) * cexp (-π ^ 2 * c * ‖0 - v‖^2)) * (selfConvolution f v)) =ᶠ[atTop] + (fun c ↦ ∫ v : V, 𝓕 (fun w ↦ cexp (-c⁻¹ * ‖w‖ ^ 2)) v * (selfConvolution f v))) from ?_); swap + · apply Filter.eventuallyEq_of_mem hpos + intro c hc + simp at hc + dsimp + apply congrArg (integral volume) + ext v + simp only [mul_eq_mul_right_iff] + left + rw [fourierIntegral_gaussian_innerProductSpace] + simp + constructor + ring_nf + simpa + have : ∫ v : V, (‖f v‖ : ℂ) ^ 2 = selfConvolution f 0 := by + unfold selfConvolution convolution + simp + apply congrArg (integral volume) + ext v + rw [mul_comm, ← Complex.normSq_eq_conj_mul_self, ← Complex.sq_abs] + simp + rw [this] + apply tendsto_integral_gaussian_smul' (integrable_selfConvolution hf) + exact Continuous.continuousAt (continuous_selfConvolution h2f) + have lim2 : Tendsto (fun (c : ℝ) ↦ ∫ v : V, cexp (- c⁻¹ * ‖v‖ ^ 2) * 𝓕 (selfConvolution f) v) atTop + (𝓝 (∫ v : V, ‖𝓕 f v‖ ^ 2)) := by + rw [fourier_selfConvolution hf] + by_cases hF : Integrable (fun x ↦ (‖𝓕 f x‖ ^ 2)) volume + · apply tendsto_integral_filter_of_dominated_convergence _ _ _ hF + apply ae_of_all volume + intro v + rw [show (‖𝓕 f v‖ ^ 2) = cexp (- (0 : ℝ) * ‖v‖ ^ 2) * (‖𝓕 f v‖ ^ 2) by simp] + apply (Tendsto.cexp _).smul_const + exact tendsto_inv_atTop_zero.ofReal.neg.mul_const _ + simp + use (1 : ℝ) + intro b hb + apply AEStronglyMeasurable.mul + apply Integrable.aestronglyMeasurable + have hb : 0 < (b : ℂ)⁻¹.re := by simpa using by linarith + simpa using GaussianFourier.integrable_cexp_neg_mul_sq_norm_add hb 0 (0 : V) + apply Integrable.aestronglyMeasurable + simp at hF + norm_cast + exact Integrable.ofReal hF + simp + use 1 + intro b hb + apply ae_of_all volume + intro v + rw [← one_mul (Complex.abs (𝓕 f v)), mul_pow, ← mul_assoc, show ((1 : ℝ) ^ 2 = 1) from by simp, mul_one] + apply mul_le_mul_of_nonneg_right + rw [Complex.abs_exp] + simp + apply Left.mul_nonneg + simpa using by linarith + rw [show ((‖v‖ : ℂ) ^ 2).re = ‖v‖ ^ 2 from by norm_cast] + exact sq_nonneg ‖v‖ + exact sq_nonneg (Complex.abs (𝓕 f v)) + · have : ¬Integrable (fun v ↦ (‖𝓕 f v‖ : ℂ) ^ 2) := by + norm_cast + intro h + rw [← Complex.ofReal_integrable] at h + exact hF h + rw [integral_undef this] + have : ∀ᶠ (c : ℝ) in atTop, ¬Integrable (fun v ↦ cexp (-↑c⁻¹ * (‖v‖ : ℂ) ^ 2) * (fun x ↦ (‖𝓕 f x‖ : ℂ) ^ 2) v) := by + by_contra h + simp at h + absurd this + sorry + have : ∀ᶠ (c : ℝ) in atTop, 0 = ∫ (v : V), cexp (-↑c⁻¹ * (‖v‖ : ℂ) ^ 2) * (fun x ↦ (‖𝓕 f x‖ : ℂ) ^ 2) v := by + simp + simp at this + obtain ⟨a, ha⟩ := this + use a + intro b hb + rw [integral_undef (ha b hb)] + apply Tendsto.congr' this + rw [tendsto_def] + intro s hs + simp + use 0 + intro _ _ + exact mem_of_mem_nhds hs + have hm : AEStronglyMeasurable (𝓕 f) := by + apply Continuous.aestronglyMeasurable + apply VectorFourier.fourierIntegral_continuous continuous_fourierChar + (by simp only [innerₗ_apply]; exact continuous_inner) hf + have : ∫ (v : V), (‖𝓕 f v‖ : ℂ) ^ 2 = ∫ (v : V), (‖f v‖ : ℂ) ^ 2 := tendsto_nhds_unique lim2 lim1 + have : ∫ (v : V), ‖𝓕 f v‖ ^ 2 = ∫ (v : V), ‖f v‖ ^ 2 := by + norm_cast at this + apply ofReal_inj.1 + rw [Complex.ofReal_integral, Complex.ofReal_integral, this] + rw [l2norm_bochnerIntegral h2f, l2norm_bochnerIntegral, this] + constructor; exact hm + by_cases H : snorm f 2 volume = 0 + · rw [snorm_eq_zero_iff] at H + have : ∀ w, (fun v ↦ 𝐞 (-⟪v, w⟫_ℝ) • f v) =ᶠ[ae volume] 0 := by + intro w + rw [eventuallyEq_iff_exists_mem] + rw [eventuallyEq_iff_exists_mem] at H + obtain ⟨s,hs,h⟩ := H + use s + constructor + exact hs + intro x hx + simp + rw [h hx] + simp + have : 𝓕 f = 0 := by + unfold fourierIntegral VectorFourier.fourierIntegral + ext w + simp + exact integral_eq_zero_of_ae (this w) + rw [this] + simp + exact hf.1 + simp + have : Memℒp (𝓕 f) 2 := by + apply integrable_iff_memℒ2.2 + constructor + exact hm + apply MeasureTheory.Integrable.of_integral_ne_zero + rw [this] + unfold snorm snorm' at H; simp at H + have : 0 < ∫⁻ (v : V), ‖f v‖₊ ^ 2 := by + apply lt_of_le_of_ne (zero_le _) (fun a ↦ H (id (Eq.symm a))) + have : 0 < ENNReal.ofReal (∫ (v : V), ‖f v‖ ^ 2) := by + rw [ofReal_integral_eq_lintegral_ofReal] + norm_cast at this + apply lt_of_lt_of_le this (le_of_eq _) + apply congrArg (lintegral volume) + ext v + simp [← ofReal_norm_eq_coe_nnnorm] + rw [ENNReal.ofReal_pow (AbsoluteValue.nonneg Complex.abs (f v))] + exact (integrable_iff_memℒ2.1 h2f).2 + apply ae_of_all + intro a + simp + rw [ENNReal.ofReal_pos] at this + exact Ne.symm (ne_of_lt this) + exact this.2 + + +/-- Part of **Plancherel theorem**: if `f` is in `L¹ ∩ L²` then its Fourier transform is +also in `L²`. -/ +theorem memℒp_fourierIntegral {f : V → ℂ} (hf : Integrable f) (h2f : Memℒp f 2) : + Memℒp (𝓕 f) 2 := by + unfold Memℒp; constructor + · apply Continuous.aestronglyMeasurable + exact VectorFourier.fourierIntegral_continuous continuous_fourierChar + (by simp only [innerₗ_apply]; exact continuous_inner) hf + · rw [snorm_fourierIntegral hf h2f] + exact h2f.2 + +/-- Part of **Plancherel theorem**: if `f` is in `L¹ ∩ L²` then its inverse Fourier transform is +also in `L²`. -/ +theorem memℒp_fourierIntegralInv {f : V → ℂ} (hf : Integrable f) (h2f : Memℒp f 2) : + Memℒp (𝓕⁻ f) 2 := by + rw [fourierIntegralInv_eq_fourierIntegral_comp_neg] + apply memℒp_fourierIntegral (Integrable.comp_neg hf) + apply Memℒp.comp_of_map + simpa + exact AEMeasurable.neg aemeasurable_id /-- **Plancherel theorem**: if `f` is in `L¹ ∩ L²` then its inverse Fourier transform has the same `L²` norm as that of `f`. -/ -theorem snorm_fourierIntegralInv {f : V → E} (hf : Integrable f) (h2f : Memℒp f 2) : - snorm (𝓕⁻ f) 2 volume = snorm f 2 volume := sorry +theorem snorm_fourierIntegralInv {f : V → ℂ} (hf : Integrable f) (h2f : Memℒp f 2) : + snorm (𝓕⁻ f) 2 volume = snorm f 2 volume := by + trans snorm (𝓕 f) 2 volume + · unfold snorm; simp; unfold snorm' + apply congrArg (fun x ↦ x ^ (1 / 2)) + trans ∫⁻ (a : V), ‖𝓕 f (-a)‖₊ ^ (2 : ℝ) + · apply lintegral_rw₁ _ id + apply Germ.coe_eq.1 (congrArg Germ.ofFun _) + ext a + rw [fourierIntegralInv_eq_fourierIntegral_neg] + · rw [← @lintegral_map' _ _ _ _ _ (fun x ↦ (‖𝓕 f x‖₊ : ENNReal) ^ 2) (fun x ↦ -x) _ (AEMeasurable.neg aemeasurable_id)] + simp; simp + have : (fun x ↦ (‖𝓕 f x‖₊ : ENNReal) ^ 2) = (fun x ↦ x ^ 2) ∘ (fun x ↦ (‖𝓕 f x‖₊ : ENNReal)) := by + ext x; simp + rw [this] + apply Measurable.comp_aemeasurable (Measurable.pow_const (fun ⦃t⦄ a ↦ a) 2) + have : (fun x ↦ (‖𝓕 f x‖₊ : ENNReal)) = (fun x ↦ (‖x‖₊ : ENNReal)) ∘ (fun x ↦ 𝓕 f x) := by + ext x; simp + rw [this] + exact Measurable.comp_aemeasurable (Continuous.measurable <| ENNReal.continuous_coe_iff.2 continuous_nnnorm) <| + AEStronglyMeasurable.aemeasurable (memℒp_fourierIntegral hf h2f).1 + · exact snorm_fourierIntegral hf h2f + + + +def L12 (V : Type*) [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] + [BorelSpace V] [FiniteDimensional ℝ V] : AddSubgroup (V →₂[volume] ℂ) where + carrier := {f | snorm f 1 volume < ⊤} + add_mem' := by + simp + intro a _ b _ h2a h2b + have h1a : Memℒp a 1 volume := mem_Lp_iff_memℒp.1 (mem_Lp_iff_snorm_lt_top.2 h2a) + have h1b : Memℒp b 1 volume := mem_Lp_iff_memℒp.1 (mem_Lp_iff_snorm_lt_top.2 h2b) + simp [snorm_congr_ae (AEEqFun.coeFn_add a b)] + apply lt_of_le_of_lt (snorm_add_le h1a.1 h1b.1 _) + exact ENNReal.add_lt_top.2 ⟨h2a, h2b⟩ + rfl + zero_mem' := by simp [snorm_congr_ae AEEqFun.coeFn_zero, snorm_zero] + neg_mem' := by simp[snorm_congr_ae (AEEqFun.coeFn_neg _)] + +instance : NormedAddCommGroup (L12 V) := AddSubgroup.normedAddCommGroup scoped[MeasureTheory] notation:25 α " →₁₂[" μ "] " E => ((α →₁[μ] E) ⊓ (α →₂[μ] E) : AddSubgroup (α →ₘ[μ] E)) - +/- /- Note: `AddSubgroup.normedAddCommGroup` is almost this, but not quite. -/ -instance : NormedAddCommGroup (V →₁₂[volume] E) := +instance : NormedAddCommGroup (V →₁₂[volume] ℂ) := AddGroupNorm.toNormedAddCommGroup { toFun := fun ⟨f,_⟩ ↦ ENNReal.toReal <| snorm f 2 volume map_zero' := by simp [snorm_congr_ae AEEqFun.coeFn_zero, snorm_zero] @@ -56,19 +555,63 @@ instance : NormedAddCommGroup (V →₁₂[volume] E) := ext apply ae_eq_trans <| (snorm_eq_zero_iff ((Lp.mem_Lp_iff_memℒp.1 hf).1) (by simp)).1 h apply ae_eq_trans (Lp.coeFn_zero E 2 volume).symm; rfl - } + }-/ +lemma memℒ12_iff {f : V → ℂ} (hf : Memℒp f 2 volume) : + (hf.toLp) ∈ L12 V ↔ Integrable f := by + constructor + · intro h + unfold L12 at h + simp at h + unfold Integrable + constructor + exact hf.1 + unfold HasFiniteIntegral + unfold snorm snorm' at h + simp at h + have : ∫⁻ (a : V), ‖f a‖₊ = ∫⁻ (a : V), ‖toLp f hf a‖₊ := by + sorry + rw [this] + exact h + · sorry + +lemma memL12_iff {f : V →₂[volume] ℂ} : f ∈ L12 V ↔ Integrable (↑f) := by + constructor + · intro h + apply (memℒ12_iff _).1 + rw [toLp_coeFn] + exact h + rw [← mem_Lp_iff_memℒp] + simp + · intro h + rw [← toLp_coeFn f, memℒ12_iff] + exact h + rw [← mem_Lp_iff_memℒp] + simp -instance : NormedSpace ℝ (V →₁₂[volume] E) := sorry +instance : NormedSpace ℝ (L12 V) where + smul := fun a f ↦ by + use a • f + sorry + one_smul := by + intro ⟨f, hf⟩ + sorry + mul_smul := sorry + smul_zero := sorry + smul_add := sorry + add_smul := sorry + zero_smul := sorry + norm_smul_le := sorry /- The Fourier integral as a continuous linear map `L^1(V, E) ∩ L^2(V, E) → L^2(V, E)`. -/ -def fourierIntegralL2OfL12Fun : (V →₁₂[volume] E) → (V →₂[volume] E) := - fun ⟨f,hf,hf2⟩ ↦ (memℒp_fourierIntegral (memℒp_one_iff_integrable.1 <| - Lp.mem_Lp_iff_memℒp.1 hf) (Lp.mem_Lp_iff_memℒp.1 hf2)).toLp <| 𝓕 f +def fourierIntegralL2OfL12Fun : (V →₁₂[volume] ℂ) → (V →₂[volume] ℂ) := sorry + --fun ⟨f,hf,hf2⟩ ↦ (memℒp_fourierIntegral (memℒp_one_iff_integrable.1 <| + -- Lp.mem_Lp_iff_memℒp.1 (by sorry)) (Lp.mem_Lp_iff_memℒp.1 hf2)).toLp <| 𝓕 f -def fourierIntegralL2OfL12 : (V →₁₂[volume] E) →L[ℝ] (V →₂[volume] E) := sorry +--def fourierIntegralL2OfL12 : (V →₁₂[volume] ℂ) →L[ℝ] (V →₂[volume] ℂ) := sorry /-have : IsBoundedLinearMap ℝ fourierIntegralL2OfL12Fun := { - map_add := sorry + map_add := by + intro f g map_smul := sorry bound := sorry } @@ -77,7 +620,7 @@ def fourierIntegralL2OfL12 : (V →₁₂[volume] E) →L[ℝ] (V →₂[volume] /- The Fourier integral as a continuous linear map `L^2(V, E) → L^2(V, E)`. -/ -def fourierIntegralL2 : (V →₂[volume] E) →L[ℝ] (V →₂[volume] E) := +def fourierIntegralL2 : (V →₂[volume] ℂ) →L[ℝ] (V →₂[volume] ℂ) := sorry end MeasureTheory diff --git a/blueprint/src/chapter/plancherel.tex b/blueprint/src/chapter/plancherel.tex index 34a7f68..a8b9acd 100644 --- a/blueprint/src/chapter/plancherel.tex +++ b/blueprint/src/chapter/plancherel.tex @@ -29,6 +29,10 @@ \section{Basic Properties of the Fourier Transform} Let $f\in L^1(V,E)$. Then its Fourier transform $\widehat f$ is well-defined and bounded. In particular, the Fourier transform defines a map $\mathcal F:L^1(V,E)\to L^\infty(V,E)$. \end{lemma} +\begin{proof} + \leanok + Omitted. +\end{proof} From now on assume that $V$ and $W$ are equipped with second-countable topologies such that $L$ is continuous. @@ -39,6 +43,10 @@ \section{Basic Properties of the Fourier Transform} \leanok Let $f\in L^1(V,E)$. Then $\widehat f$ is continuous. \end{lemma} +\begin{proof} + \leanok + Omitted. +\end{proof} \begin{lemma}[Multiplication formula] \label{lem:fourier-multiplication} @@ -48,38 +56,51 @@ \section{Basic Properties of the Fourier Transform} Let $f,g\in L^1(V,E)$. Then $$\int_WM(\widehat f(w),g(w))\,d\nu(w)=\int_VM(f(v),\widehat g(v))\,d\mu(v).$$ \end{lemma} +\begin{proof} + \leanok + Omitted. +\end{proof} \begin{lemma} \label{lem:fourier-prop} \uses{def:fourier-transform} - \lean{} - % \leanok -Let $f,g\in L^1(V,E)$, $t\in\R$ and $a,b\in\C$. The Fourier transform satisfies the following elementary properties: + \lean{VectorFourier.fourierIntegral_add, + Fourier.fourierIntegral_comp_add_right, + Fourier.fourierIntegral_smul_const, + MeasureTheory.fourier_conj, + MeasureTheory.fourier_convolution} + \leanok +Lef $f,g\in L^1(V,E)$, $t\in\R$ and $a,b\in\C$. The Fourier transform satisfies the following elementary properties: \begin{enumerate} \item[(i)] $\mathcal F(af+bg)=a\mathcal Ff+b\mathcal Fg$\hfill(Linearity) \item[(ii)] $\mathcal F(f(x-t)) = e^{-2\pi i ty}\mathcal F f(y)$\hfill (Shifting) \item[(iii)] $\mathcal F(f(tx)) = \frac1{|t|}\mathcal F f(\frac yt)$\hfill (Scaling) - \item[(iv)] $\mathcal F(\overline{f(x)}) = \overline{\mathcal Ff(-y)}$\hfill (Conjugation) + \item[(iv)] If $E$ admits a conjugation, then $\mathcal F(\overline{f(x)}) = \overline{\mathcal Ff(-y)}$\hfill (Conjugation) \item[(v)] Define the convolution of $f$ and $g$ w.r.t. a bilinear map $M:E\times E\to F$ as $$(f\ast_Mg)(w):=\int_VM(f(v),g(w-v))\,d\mu(v).$$ Then $\mathcal F(f\ast_M g) =M(\mathcal Ff,\mathcal Fg)$ \hfill (Convolution) \end{enumerate} \end{lemma} +\begin{proof} + \leanok + Omitted. +\end{proof} From now on, let $V$ be a finite-dimensional inner product space. We denote this product as ordinary multiplication, and the induced norm as $|\cdot|.$ We now study a family of functions which is useful for later proofs. \begin{lemma} \label{lem:fourier-gaussian} -\uses{def:fourier-transform, lem:fourier-prop} +\uses{def:fourier-transform} \lean{fourierIntegral_gaussian_innerProductSpace'} \leanok Let $x\in V$ and $\delta>0$. Define the \emph{modulated Gaussian} -$$u_{x,\delta}(y):V\to\C,\quad y\mapsto e^{-\pi|y|^2}e^{2\pi i x y}.$$ +$$u_{x,\delta}(y):V\to\C,\quad y\mapsto e^{-\delta\pi|y|^2}e^{2\pi i x y}.$$ Its Fourier transform (w.r.t. the inner product) is given by $$\widehat{u_{x,\delta}}(z)=\delta^{-n/2}e^{-\pi|x-y|^2/\delta}=:K_\delta(x-z).$$ \end{lemma} \begin{proof} + \uses{lem:fourier-prop} \leanok By choosing an orthonormal basis, wlog we may assume $V=\R^n$. First note $\widehat{u_{x,\delta}}(z-x)=\widehat{u_{0,\delta}}(z)$, so it is enough to consider $x=0$. @@ -100,9 +121,8 @@ \section{Basic Properties of the Fourier Transform} \begin{lemma} \label{lem:weierstrass-kernel} -% \uses{} % \lean{} -% \leanok +\leanok Let $K_\delta(v)=\delta^{-n/2}e^{-\pi|v|^2/\delta}$ as in \Cref{lem:fourier-gaussian}. This is a \emph{good kernel}, called the \emph{Weierstrass kernel}, satisfying @@ -113,7 +133,7 @@ \section{Basic Properties of the Fourier Transform} some constant $B$ independent of $\delta$. \end{lemma} \begin{proof} - % \leanok + \leanok By choosing an orthonormal basis, wlog we may assume $V=\R^n$. Then these are all straight-forward calculations: $$\int_{\R^n}e^{-\pi|x|^2/\delta}\,dx=\delta^{n/2}\int_{\R^n}e^{-\pi|x|^2}\,dx=\delta^{n/2}.$$ $$\int_{|x|>\eta}\delta^{-n/2}e^{-\pi|x|^2/\delta}\,dx=\int_{|x|>\eta/\delta^{1/2}}e^{-\pi|x|^2}\xrightarrow{\delta\to0}0.$$ @@ -129,15 +149,15 @@ \section{Basic Properties of the Fourier Transform} \begin{theorem} \label{thm:kernel-approximation} \uses{lem:weierstrass-kernel} -\lean{} -% \leanok +\lean{Real.tendsto_integral_gaussian_smul'} +\leanok Let $f:V\to E$ be integrable. Let $K_\delta$ be the Weierstrass kernel from \Cref{lem:weierstrass-kernel}, or indeed any family of functions satisfying the conditions of \Cref{lem:weierstrass-kernel}. Then $$(K_\delta\ast f)(x):=\int_V K_\delta(y)f(x-y)\,d\mu(y)\xrightarrow{\delta\to0}f(x)$$ in the $L^1$-norm. If $f$ is continuous, the convergence also holds pointwise. \end{theorem} \begin{proof} -% \leanok +\leanok Again we may assume $V=\R^n$. Consider the difference $$\Delta_\delta(x):=(K_\delta\ast f)(x)-f(x)= \int_{\R^n}(f(x-y)-f(x))K_\delta(y)\,dy.$$ We prove $L^1$-convergence first: Take $L^1$-norms and use Fubini's theorem to conclude @@ -172,16 +192,16 @@ \section{Basic Properties of the Fourier Transform} \begin{theorem}[Inversion formula] \label{thm:fourier-inversion} - \uses{thm:kernel-approximation, lem:fourier-multiplication} \lean{MeasureTheory.Integrable.fourier_inversion, Continuous.fourier_inversion} Let $f:V\to E$ be integrable and continuous. Assume $\widehat f$ is integrable as well. Then $$\mathcal F^{-1}\mathcal F f=f.$$ \leanok \end{theorem} \begin{proof} -\leanok -Apply the multiplication formula \Cref{lem:fourier-multiplication} to $u_{x,\delta}$ and $f$, and conclude with -\Cref{thm:kernel-approximation}. + \uses{thm:kernel-approximation, lem:fourier-multiplication} + \leanok + Apply the multiplication formula \Cref{lem:fourier-multiplication} to $u_{x,\delta}$ and $f$, and conclude with + \Cref{thm:kernel-approximation}. \end{proof} \begin{remark} @@ -191,33 +211,33 @@ \section{Basic Properties of the Fourier Transform} \begin{theorem}[Inversion formula, $L^1$-version] \label{thm:fourier-inversion-L1} - \uses{thm:kernel-approximation, lem:fourier-multiplication} \leanok Let $f\in L^1(V,E)$. If $\widehat f\in L^1(V,E)$, then $\mathcal F^{-1}\mathcal Ff=f$. \end{theorem} +\begin{proof} + \leanok + \uses{thm:kernel-approximation, lem:fourier-multiplication} + Similar to \Cref{thm:fourier-inversion}. +\end{proof} \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$} {Plancherel's Theorem and the Fourier Transform on L2}} -Again let $V$ be a finite-dimensional inner product space over $\R$ and let $E$ be a normed space over $\C$. -%TODO: The proof needs convolutions of functions into E. Is there another proof? Or assume E has products? +Let $(V,\cdot)$ be a finite-dimensional inner product space over $\R$ and let $(E,\langle\cdot,\cdot\rangle)$ be an inner product space over $\C$. + \begin{theorem}[Plancherel's Theorem] \label{thm:plancherel} - \uses{thm:kernel-approximation, lem:fourier-multiplication, lem:fourier-gaussian, lem:fourier-prop} - \lean{MeasureTheory.memℒp_fourierIntegral, MeasureTheory.snorm_fourierIntegral} % the full Lean name this corresponds to (can be a comma-separated list) - \leanok % the *statement* of the lemma is formalized + \lean{MeasureTheory.memℒp_fourierIntegral, MeasureTheory.snorm_fourierIntegral} + \leanok Suppose that $f : V \to E$ is in $L^1(V,E)\cap L^2(V,E)$ and let $\widehat{f}$ be the Fourier transform of $f$. Then $\widehat{f},\check{f}\in L^2(V,E)$ and \[\|\widehat{f}\|_{L^2} = \|f\|_{L^2}=\|\check f\|_{L^2}.\] Suppose that $f : V \to E$ is in $L^1(V,E)\cap L^2(V,E)$ and let $\widehat{f}$ be the Fourier transform of $f$. Then $\widehat{f},\check{f}\in L^2(V,E)$ and \[\|\widehat{f}\|_{L^2} = \|f\|_{L^2}=\|\check f\|_{L^2}.\] \end{theorem} \begin{proof} - % \leanok % uncomment if the lemma has been proven - %Let $(e_i)_{i\in I}$ be a normalized basis of E. This choice defines a conjugation on $E$: Let $E_\R$ be - %the $\R$-span of the $e_i$, then $E\cong E_\R\otimes_\R\C$ and we can conjugate on the second factor. - %We denote this conjugation by $e\mapsto\overline e$. - Let $g(x)=\overline{f(-x)}$ and apply the multiplication formula \Cref{lem:fourier-multiplication} + \uses{thm:kernel-approximation, lem:fourier-multiplication, lem:fourier-gaussian, lem:fourier-prop} + Let $g(x)=f(-x)$ and apply the multiplication formula \Cref{lem:fourier-multiplication} to $f\ast g$ and $u_{0,\delta}$: $$\int_V\widehat{f\ast g}\cdot u_{0,\delta}(x)\,dx=\int_V(f\ast g)(x)K_\delta(-x)\,dx - \overset{\delta\to0}\to(f\ast g)(0)=\int_Vf(x)\overline{f(x)}\,dx=\| f\|_2^2$$ by \Cref{thm:kernel-approximation}. + \overset{\delta\to0}\to(f\ast g)(0)=\int_V \langle f(x),f(x)\rangle\,dx=\| f\|_2^2$$ by \Cref{thm:kernel-approximation}. On the other hand, by \Cref{lem:fourier-prop} the left hand side simplifies to $$\int_V|\widehat f(x)|^2e^{-\delta\pi|x|^2}\,dx\xrightarrow{\delta\to0}\|\widehat f\|_2^2$$ by dominated convergence. @@ -228,9 +248,9 @@ \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$ such that $f_n\xrightarrow[L^2]{}f$. Such sequences exist: \begin{lemma} \label{lem:L12-dense} - %\uses{MeasureTheory.Memℒp.exists_hasCompactSupport_snorm_sub_le} + %\uses{MeasureTheory.Memℒp.exists_hasCompactSupport_snorm_sub_le, Mathlib.MeasureTheory.Function.SimpleFuncDenseLp} \lean{} - % \leanok + %\leanok $L^1(V,E)\cap L^2(V,E)$ is dense in $L^2(V,E)$. \end{lemma} \begin{proof} @@ -242,7 +262,7 @@ \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$ Let $f\in L^2(V,E)$. Plancherel's theorem lets us now approximate a potential $\widehat f$: \begin{lemma} \label{lem:fourier12-cauchy} - \uses{lem:L12-dense, thm:plancherel, lem:fourier-prop} + \uses{lem:L12-dense,} \lean{} % \leanok Let $f\in L^2(V,E)$ and $(f_n)_n\subset L^1(V,E)\cap L^2(V,E)$ a sequence with $f_n\xrightarrow[L^2]{}f$. Then $(\widehat f_n)_n$ is a Cauchy sequence, @@ -250,6 +270,7 @@ \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$ \end{lemma} \begin{proof} % \leanok + \uses{thm:plancherel, lem:fourier-prop} $$\|\widehat f_n-\widehat f_m\|_2=\|\widehat{f_n-f_m}\|_2\overset{\text{Plancherel}}=\|f_n-f_m\|_2$$ goes to $0$ for $n,m$ large, as $(f_n)_n$ is convergent, hence Cauchy. Since $L^2(V,E)$ is complete, $(\widehat f_n)_n$ converges. \end{proof} @@ -263,7 +284,7 @@ \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$ \end{definition} \begin{lemma} \label{lem:fourier2-welldef} - \uses{def:fourier-L2, lem:fourier12-cauchy, thm:plancherel} + \uses{def:fourier-L2, lem:fourier12-cauchy} \lean{} % \leanok This is well-defined: By \Cref{lem:fourier12-cauchy}, the limit exists. Further it does not depend @@ -272,6 +293,7 @@ \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$ \end{lemma} \begin{proof} % \leanok + \uses{thm:plancherel} Let $(g_n)_n$ be another sequence approximating $f$. Then $$\|\widehat f_n-\widehat g_n\|_2=\|f_n-g_n\|\leq\|f_n-f\|+\|g_n-g\|\to0.$$ If $f\in L^1(V,E)\cap L^2(V,E)$, we can choose the constant sequence $(f_n)_n=(f)_n$. @@ -288,13 +310,14 @@ \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$ \begin{corollary} \label{thm:fourier2-properties} - \uses{def:fourier-L2, def:invFourier-L2, thm:plancherel, thm:fourier-inversion, lem:fourier-prop} + \uses{def:fourier-L2, def:invFourier-L2, lem:fourier2-welldef} \lean{} % \leanok Plancherel's Theorem, the inversion formula, and the properties of \Cref{lem:fourier-prop} hold for the Fourier transform on $L^2(V,E)$ as well. \end{corollary} \begin{proof} + \uses{thm:plancherel, thm:fourier-inversion, lem:fourier-prop} % \leanok All of these follow immediately from the definition and the observation, that all operations (norms, sums, conjugation, $\ldots$) are continuous. For example, let $f\in L^2(V,E)$ and take an approximating sequence $(f_n)_n$ as before. Then @@ -304,14 +327,14 @@ \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$ \begin{corollary} \label{thm:fourier-is-l2-linear} - \uses{thm:fourier2-properties} % the (list of) LaTeX labels of the lemmas that are used for this result - \lean{MeasureTheory.fourierIntegralL2} % the full Lean name this corresponds to (can be a comma-separated list) - \leanok % the *statement* of the lemma is formalized + \uses{def:fourier-L2, lem:fourier2-welldef} + \lean{MeasureTheory.fourierIntegralL2} + \leanok The Fourier transform induces a continuous linear map $L^2(V,E) \to L^2(V,E)$. \end{corollary} \begin{proof} - % \uses{} % Put any results used in the proof but not in the statement here + \uses{thm:fourier2-properties} % \leanok % uncomment if the lemma has been proven This follows immediately from \Cref{thm:fourier2-properties}: Linearity from the $L^2$-version of \Cref{lem:fourier-prop}, and continuity and well-definedness from the $L^2$-version of Plancherel's theorem. -\end{proof} \ No newline at end of file +\end{proof} From ec4a4106e77ce4118af620f4fb0a33877661adfb Mon Sep 17 00:00:00 2001 From: madeve-unipi <56154049+madeve-unipi@users.noreply.github.com> Date: Wed, 14 Aug 2024 15:03:34 +0200 Subject: [PATCH 06/10] speed up some proofs; some changes (#48) As in the final seminar, I sped up a few proofs, but many are still quite slow even by replacing all `simp`s by `simp only`s. Some typeclass inferences are slow and I don't really know how to deal with them. In the final theorems, it looked like we were only really considering the product as a bilinear function, so I did the same for `toDual_{li}` and fixed a sorry. --- BonnAnalysis/Dual.lean | 264 ++++++++++++++++++++++++++++++----------- 1 file changed, 193 insertions(+), 71 deletions(-) diff --git a/BonnAnalysis/Dual.lean b/BonnAnalysis/Dual.lean index 8633c7b..f222eaf 100644 --- a/BonnAnalysis/Dual.lean +++ b/BonnAnalysis/Dual.lean @@ -7,6 +7,12 @@ import Mathlib.Analysis.NormedSpace.LinearIsometry import Mathlib.MeasureTheory.Integral.Bochner import Mathlib.Data.Real.Sign + +set_option linter.setOption false +set_option trace.profiler true +set_option profiler true + + /-! We show that the dual space of `L^p` for `1 ≤ p < ∞`. See [Stein-Shakarchi, Functional Analysis, section 1.4] -/ @@ -107,9 +113,9 @@ lemma toNNReal {p q : ℝ≥0∞} (hp : p ≠ ∞) (hq : q ≠ ∞) (hpq : p.IsC lemma mul_eq_add (hpq : p.IsConjExponent q) : p * q = p + q := by induction p - . simp [hpq.right_ne_zero] + . simp only [ne_eq, hpq.right_ne_zero, not_false_eq_true, top_mul, top_add] induction q - . simp [hpq.left_ne_zero] + . simp only [ne_eq, hpq.left_ne_zero, not_false_eq_true, mul_top, add_top] norm_cast exact hpq.toNNReal coe_ne_top coe_ne_top |>.mul_eq_add @@ -152,13 +158,14 @@ lemma _root_.ENNReal.lintegral_mul_le_one_top (μ : Measure α) {f g : α → rw [Filter.eventually_iff, ← Filter.exists_mem_subset_iff] use {a | g a ≤ essSup g μ} rw [← Filter.eventually_iff] - exact ⟨ae_le_essSup _, by simp; intro _ ha; exact ENNReal.mul_left_mono ha⟩ + exact ⟨ae_le_essSup _, by simp only [Pi.mul_apply, Set.setOf_subset_setOf]; intro _ ha; exact ENNReal.mul_left_mono ha⟩ _ = (∫⁻ (a : α), f a ∂μ) * (essSup g μ) := by rw [lintegral_mul_const'' _ hf] lemma _root_.ENNReal.lintegral_norm_mul_le_one_top (μ : Measure α) {f : α → E₁} {g : α → E₂} (hf : AEMeasurable f μ) : ∫⁻ a, ‖f a‖₊ * ‖g a‖₊ ∂μ ≤ snorm f 1 μ * snorm g ⊤ μ := by - simp [snorm, snorm', snormEssSup] + simp only [snorm, one_ne_zero, ↓reduceIte, one_ne_top, snorm', one_toReal, rpow_one, ne_eq, + not_false_eq_true, div_self, top_ne_zero, snormEssSup] exact lintegral_mul_le_one_top _ hf.ennnorm theorem lintegral_mul_le (hpq : p.IsConjExponent q) (μ : Measure α) {f : α → E₁} {g : α → E₂} @@ -198,7 +205,12 @@ theorem integrable_bilin (hpq : p.IsConjExponent q) (μ : Measure α) {f : α end IsConjExponent lemma toNNReal_eq_toNNreal_of_toReal (x : ℝ≥0∞) : - x.toReal.toNNReal = x.toNNReal := by aesop + x.toReal.toNNReal = x.toNNReal := by + rename_i inst inst_1 inst_2 _ inst_4 inst_5 _ inst_7 inst_8 _ inst_10 inst_11 _ inst_13 + _ inst_15 _ inst_17 _ inst_19 _ + ext1 + simp_all only [coe_toNNReal', toReal_nonneg, max_eq_left] + apply Eq.refl lemma rpow_of_to_ENNReal_of_NNReal_ne_top (x : ℝ≥0) (y : ℝ) (hynneg : y ≥ 0) : (x : ℝ≥0∞) ^ y ≠ ∞ := by aesop @@ -323,7 +335,7 @@ lemma q_div_p_add_one : q / p + 1 = q := by lemma q_div_p_add_one' (hqᵢ : q ≠ ∞) : q.toReal / p.toReal + 1 = q.toReal := by calc _ = (q / p).toReal + 1 := by rw [toReal_div] - _ = (q / p + 1).toReal := by rw [toReal_add]; simp; exact q_div_p_ne_top hqᵢ; simp + _ = (q / p + 1).toReal := by rw [toReal_add]; simp only [one_toReal]; exact q_div_p_ne_top hqᵢ; simp _ = q.toReal := by rw [q_div_p_add_one] lemma q_div_p_add_one'' (hqᵢ : q ≠ ∞) : q.toReal / p.toReal = q.toReal - 1 := by @@ -337,12 +349,14 @@ open Memℒp section BasicFunctions +--Inference of Module takes 130ms, but I don't get this message every time. Same for other theorems in the file theorem snorm'_mul_const {p : ℝ} (hp : p > 0) (f : α → ℝ) (c : ℝ) : snorm' (fun x => f x * c) p μ = (snorm' f p μ) * ‖c‖₊ := by - unfold snorm'; dsimp only; simp_all + unfold snorm'; dsimp only; simp_all only [gt_iff_lt, nnnorm_mul, ENNReal.coe_mul, one_div] by_cases hc : c = 0 - . simp_all[hc, p_ne_zero'] + . simp_all only [_root_.nnnorm_zero, ENNReal.coe_zero, mul_zero, zero_rpow_of_pos, + lintegral_const, zero_mul, inv_pos] conv => pattern (_ * _) ^ _ @@ -352,17 +366,20 @@ theorem snorm'_mul_const {p : ℝ} (hp : p > 0) (f : α → ℝ) (c : ℝ) : apply coe_ne_top rw[lintegral_mul_const'] - case neg.hr => simp_all + case neg.hr => simp_all only [ne_eq, rpow_eq_top_iff, ENNReal.coe_eq_zero, nnnorm_eq_zero, + false_and, coe_ne_top, and_true, or_self, not_false_eq_true] by_cases hf : ∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ = ∞ - . rw[hf]; simp_all + . rw[hf]; simp_all only [ne_eq, ENNReal.rpow_eq_zero_iff, ENNReal.coe_eq_zero, nnnorm_eq_zero, + and_true, coe_ne_top, false_and, or_self, not_false_eq_true, top_mul, inv_pos, top_rpow_of_pos] rw[ENNReal.mul_rpow_of_ne_top hf] - case neg.hy => simp_all; + case neg.hy => simp_all only [ne_eq, rpow_eq_top_iff, ENNReal.coe_eq_zero, nnnorm_eq_zero, + false_and, coe_ne_top, and_true, or_self, not_false_eq_true]; congr apply ENNReal.rpow_rpow_inv - linarith + exact ne_of_gt hp theorem nnnorm_toReal_eq_abs (x : ℝ) : ‖x‖₊.toReal = |x| := by rw [coe_nnnorm, norm_eq_abs] @@ -400,7 +417,7 @@ theorem abs_of_sign (x) : |Real.sign x| = if x = 0 then 0 else 1 := by simp [h₁, h₂] . by_cases h₂ : x = 0 . simp [h₁, h₂] - . have h₃ : 0 < x := by apply lt_of_le_of_ne; simp at h₁; exact h₁; symm; exact h₂ + . have h₃ : 0 < x := by apply lt_of_le_of_ne; simp only [not_lt] at h₁; exact h₁; symm; exact h₂ simp [h₁, h₂, h₃] @[simp] theorem nnnorm_of_sign (x) : ‖Real.sign x‖₊ = if x = 0 then 0 else 1 := by @@ -490,7 +507,8 @@ theorem integral_mul_le (hpq : p.IsConjExponent q) (μ : Measure α) {f : Lp E rw [integral_norm_eq_lintegral_nnnorm this] have : (‖L‖₊ * (snorm f p μ) * (snorm g q μ)).toReal = ‖L‖ * ‖f‖ * ‖g‖ := by - calc _ = ‖L‖₊.toReal * (snorm f p μ).toReal * (snorm g q μ).toReal := by simp + calc _ = ‖L‖₊.toReal * (snorm f p μ).toReal * (snorm g q μ).toReal := by simp only [toReal_mul, + coe_toReal, coe_nnnorm] _ = ‖L‖ * ‖f‖ * ‖g‖ := by congr rw [←this] @@ -514,12 +532,13 @@ theorem lint_conj_q_lt_top'_mul_self (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} : ∫⁻ (x : α), (conj_q_lt_top' g x).toNNReal * (g x).toNNReal ∂μ = ‖g‖₊ ^ q.toReal := by unfold conj_q_lt_top' unfold ENNReal.rpow' + -- Isn't this false e.g. if the function only has negative values the lhs is 0??? I'm confused conv => lhs congr . rfl . intro x - simp + dsimp congr . congr rw[mul_comm, Real.toNNReal_mul, ENNReal.toNNReal_eq_toNNreal_of_toReal] @@ -530,7 +549,26 @@ theorem lint_conj_q_lt_top'_mul_self (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} . apply toReal_nonneg . rfl - sorry + have hq' : q ≠ 0 := by { + symm + apply ne_of_lt + calc + 0 < 1 := by norm_num + _ ≤ q := hq.out + } + simp only [ENNReal.coe_mul, nnnorm_coe_ennreal, snorm, hq', ↓reduceIte, hqᵢ] + rw[← MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_snorm'] + · apply MeasureTheory.lintegral_congr_ae + filter_upwards with x + sorry --not true? + · apply lt_of_le_of_ne + · simp + · symm + rw[ENNReal.toReal_ne_zero] + simp[hq', hqᵢ] + + + theorem int_conj_q_lt_top'_mul_self (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} : ‖∫ (x : α), (conj_q_lt_top' g) x * g x ∂μ‖ = ‖g‖ ^ q.toReal := by @@ -545,7 +583,28 @@ theorem int_conj_q_lt_top'_mul_self (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} rw[←nnnorm_toReal_eq_abs] rfl - sorry + have hq' : q ≠ 0 := by { + symm + apply ne_of_lt + calc + 0 < 1 := by norm_num + _ ≤ q := hq.out + } + + rw[MeasureTheory.Lp.norm_def] + simp only [ENNReal.rpow_eq_pow, coe_nnnorm, norm_eq_abs, snorm, hq', ↓reduceIte, hqᵢ] + have : (snorm' (↑↑g) q.toReal μ).toReal ^ q.toReal = ((snorm' (↑↑g) q.toReal μ) ^ q.toReal).toReal := by{ + sorry + } + + rw[this, ← MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_snorm'] + · sorry + · apply lt_of_le_of_ne + · simp + · symm + rw[ENNReal.toReal_ne_zero] + simp[hq', hqᵢ] + @[measurability] theorem conj_q_lt_top'_aemeasurable (g : Lp ℝ q μ) @@ -599,20 +658,20 @@ theorem snorm'_of_conj_q_lt_top' (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) conv => lhs pattern _ ^ _ - rw[nnnorm_mul, ENNReal.coe_mul, (ENNReal.mul_rpow_of_nonneg _ _ p_ge_zero')] + rw [nnnorm_mul, ENNReal.coe_mul, (ENNReal.mul_rpow_of_nonneg _ _ p_ge_zero')] congr rfl - rw[ENNReal.coe_rpow_of_nonneg _ p_ge_zero'] + rw [ENNReal.coe_rpow_of_nonneg _ p_ge_zero'] congr - rw[←Real.toNNReal_eq_nnnorm_of_nonneg toReal_nonneg] - rw[toNNReal_eq_toNNreal_of_toReal, ENNReal.toNNReal_rpow] + rw [←Real.toNNReal_eq_nnnorm_of_nonneg toReal_nonneg] + rw [toNNReal_eq_toNNreal_of_toReal, ENNReal.toNNReal_rpow] congr dsimp [ENNReal.rpow] - rw[←ENNReal.rpow_mul] + rw [←ENNReal.rpow_mul] congr rfl - rw[sub_mul (c := p.toReal), one_mul, mul_comm, ←p_add_q' hqᵢ] - simp + rw [sub_mul (c := p.toReal), one_mul, mul_comm, ←p_add_q' hqᵢ] + rw [add_comm, add_sub_assoc, sub_self, add_zero] rfl conv => @@ -620,21 +679,22 @@ theorem snorm'_of_conj_q_lt_top' (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) pattern _*_ congr - . rw[rpow_of_nnnorm_of_sign _ _ p_gt_zero'] + . rw [rpow_of_nnnorm_of_sign _ _ p_gt_zero'] rfl - . rw[ENNReal.coe_toNNReal] + . rw [ENNReal.coe_toNNReal] rfl apply ENNReal.rpow_of_to_ENNReal_of_NNReal_ne_top _ _ q_ge_zero' apply lintegral_congr_ae apply ae_iff.mpr - simp_all + simp_all only [ne_eq, ite_mul, _root_.nnnorm_zero, ENNReal.coe_zero, zero_mul, one_mul, + ite_eq_right_iff, Classical.not_imp] conv => lhs pattern _ ^ _ - rw[ENNReal.zero_rpow_of_pos (q_gt_zero' hqᵢ)] + rw [ENNReal.zero_rpow_of_pos (q_gt_zero' hqᵢ)] rfl simp @@ -652,7 +712,7 @@ theorem snorm_of_conj_q_lt_top' (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) theorem Memℒp_conj_q_lt_top' (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) : Memℒp (conj_q_lt_top' g) p μ := by constructor . measurability - . rw[snorm_of_conj_q_lt_top' hqᵢ g] + . rw [snorm_of_conj_q_lt_top' hqᵢ g] exact ENNReal.rpow_lt_top_of_nonneg (q_sub_one_nneg' (p := p) hqᵢ) (snorm_ne_top g) def conj_q_lt_top (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) : Lp ℝ p μ := @@ -668,7 +728,7 @@ theorem snorm_of_conj_q_lt_top (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) @[simp] theorem norm_of_conj_q_lt_top (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) : ‖conj_q_lt_top (p := p) hqᵢ g‖ = ‖g‖ ^ (q.toReal - 1) := by - rw[norm_def, norm_def, ENNReal.toReal_rpow] + rw [norm_def, norm_def, ENNReal.toReal_rpow] congr exact snorm_of_conj_q_lt_top (p := p) hqᵢ g @@ -693,7 +753,8 @@ theorem normalized_conj_q_lt_top'_ae_measurable (g : Lp ℝ q μ) theorem normalized_conj_q_lt_top'_aestrongly_measurable (g : Lp ℝ q μ) : AEStronglyMeasurable (normalized_conj_q_lt_top' g) μ := by unfold normalized_conj_q_lt_top' - exact (aestronglyMeasurable_iff_aemeasurable (μ := μ)).mpr (normalized_conj_q_lt_top'_ae_measurable g) + exact (aestronglyMeasurable_iff_aemeasurable (μ := μ)).mpr + (normalized_conj_q_lt_top'_ae_measurable g) @[simp] theorem snorm'_normalized_conj_q_lt_top' {g : Lp ℝ q μ} (hqᵢ : q ≠ ∞) (hg : ‖g‖₊ ≠ 0) @@ -795,14 +856,15 @@ theorem snorm_eq_sup_q_gt_top (g : Lp ℝ q μ) (hqᵢ : q ≠ ∞) : . use ‖g‖ intro x hx rcases hx with ⟨f, hf, rfl⟩ - dsimp at hf + dsimp only [Set.mem_setOf_eq] at hf dsimp only calc _ ≤ ∫ x, ‖f x * g x‖ ∂μ := by apply norm_integral_le_integral_norm - _ = ∫ x, ‖(mul ℝ ℝ) (f x) (g x)‖ ∂μ := by simp + _ = ∫ x, ‖(mul ℝ ℝ) (f x) (g x)‖ ∂μ := by simp only [norm_mul, norm_eq_abs, + mul_apply'] _ ≤ ‖(mul ℝ ℝ)‖ * ‖f‖ * ‖g‖ := by apply integral_mul_le; exact hpq.out - _ = ‖f‖ * ‖g‖ := by simp + _ = ‖f‖ * ‖g‖ := by simp only [opNorm_mul, one_mul] _ ≤ 1 * ‖g‖ := by gcongr - _ = ‖g‖ := by simp + _ = ‖g‖ := by simp only [one_mul] . use normalized_conj_q_lt_top (p := p) hqᵢ (?_ : ‖g‖₊ ≠ 0) swap; sorry constructor @@ -814,21 +876,21 @@ theorem snorm_eq_sup_q_gt_top (g : Lp ℝ q μ) (hqᵢ : q ≠ ∞) : . apply Real.sSup_le; swap; apply norm_nonneg intro x hx rcases hx with ⟨f, hf, rfl⟩ - simp at hf; dsimp only + simp only [Set.mem_setOf_eq] at hf; dsimp only calc _ ≤ ∫ x, ‖f x * g x‖ ∂μ := by apply norm_integral_le_integral_norm _ = ∫ x, ‖(mul ℝ ℝ) (f x) (g x)‖ ∂μ := by simp only [norm_mul, norm_eq_abs, mul_apply'] _ ≤ ‖(mul ℝ ℝ)‖ * ‖f‖ * ‖g‖ := by apply integral_mul_le; exact hpq.out - _ = ‖f‖ * ‖g‖ := by rw[opNorm_mul, one_mul] + _ = ‖f‖ * ‖g‖ := by rw [opNorm_mul, one_mul] _ ≤ 1 * ‖g‖ := by gcongr - _ = ‖g‖ := by rw[one_mul] + _ = ‖g‖ := by rw [one_mul] variable (p q μ) in theorem snorm_eq_sup_abs (hμ : SigmaFinite μ) (g : Lp ℝ q μ): ‖g‖ = sSup ((fun f => ‖∫ x, (f x) * (g x) ∂μ‖) '' {(f : Lp ℝ p μ) | ‖f‖ ≤ 1}) := by by_cases hqᵢ : q ≠ ⊤; swap - . simp at hqᵢ + . simp only [ne_eq, Decidable.not_not] at hqᵢ have hp₁ : p = 1 := by { rw [left_eq_one_iff, ← hqᵢ] exact hpq.out @@ -837,6 +899,8 @@ theorem snorm_eq_sup_abs (hμ : SigmaFinite μ) (g : Lp ℝ q μ): sorry . sorry + +-- The following def takes 3.2 seconds /- The map sending `g` to `f ↦ ∫ x, L (g x) (f x) ∂μ` induces a map on `L^q` into `Lp E₂ p μ →L[ℝ] E₃`. Generally we will take `E₃ = ℝ`. -/ variable (p μ) in @@ -848,25 +912,25 @@ def toDual (g : Lp E₁ q μ) : Lp E₂ p μ →L[ℝ] E₃ := by{ exact { map_add := by{ intro f₁ f₂ - simp [F] + simp only [AddSubmonoid.coe_add, AddSubgroup.coe_toAddSubmonoid, F] rw [← integral_add] · apply integral_congr_ae filter_upwards [coeFn_add f₁ f₂] with a ha norm_cast rw [ha] - simp + simp only [Pi.add_apply, map_add] · exact ENNReal.IsConjExponent.integrable_bilin L hpq.out.symm μ (Lp.memℒp g) (Lp.memℒp f₁) · exact ENNReal.IsConjExponent.integrable_bilin L hpq.out.symm μ (Lp.memℒp g) (Lp.memℒp f₂) } map_smul := by{ intro m f - simp [F] + simp only [F] rw [← integral_smul] apply integral_congr_ae filter_upwards [coeFn_smul m f] with a ha rw [ha] - simp + simp only [Pi.smul_apply, LinearMapClass.map_smul] } bound := by{ @@ -878,7 +942,7 @@ def toDual (g : Lp E₁ q μ) : Lp E₂ p μ →L[ℝ] E₃ := by{ calc ‖F f‖ ≤ M * ‖f‖ := hM f _ ≤ 1 * ‖f‖ := by apply mul_le_mul_of_nonneg_right; linarith apply norm_nonneg - . simp at hM_le_zero; use M + . simp only [not_le] at hM_le_zero; use M simp only [F] use ‖L‖ * ‖g‖ @@ -894,82 +958,140 @@ def toDual (g : Lp E₁ q μ) : Lp E₂ p μ →L[ℝ] E₃ := by{ apply IsBoundedLinearMap.toContinuousLinearMap this } + + +-- NOTE: SO ARE WE JUST TAKING L TO BE THE PRODUCT FROM NOW ON? +-- The assumptions making L' into the product were added previously, I added hμ + +--3 seconds. Half a second wasted on typeclass inferences + +variable (L' : ℝ →L[ℝ] ℝ →L[ℝ] ℝ) (L'mul : ∀ x y, L' x y = x * y) (L'norm_one : ‖L'‖ = 1) + (hμ: SigmaFinite μ) (f : Lp ℝ p μ) (g : Lp ℝ q μ) (N:ℝ) (Nnneg: N ≥ 0) in +lemma toDual_bound (hbound: ∀ (x : ↥(Lp ℝ p μ)), ‖(toDual p μ L' g) x‖ ≤ N * ‖x‖ ) : ‖g‖ ≤ N := by{ + rw[snorm_eq_sup_abs p q μ hμ g] + apply csSup_le + · apply Set.Nonempty.image + use 0 + simp only [Set.mem_setOf_eq, _root_.norm_zero, zero_le_one] + · intro x hx + obtain ⟨f, hf₁, hf₂⟩ := hx + simp only [Set.mem_setOf_eq] at hf₁ + simp only [norm_eq_abs] at hf₂ + specialize hbound f + rw[← hf₂] + have : (toDual p μ L' g) f = ∫ (x : α), L' (g x) (f x) ∂μ := rfl + rw[this] at hbound + conv in f _ * g _ => rw[mul_comm] + simp_rw[L'mul] at hbound + calc + |∫ (x : α), g x * f x ∂μ| ≤ N * ‖f‖ := hbound + _ ≤ N := by nth_rewrite 2 [← mul_one N]; gcongr +} + +--2.6 seconds +variable (L' : ℝ →L[ℝ] ℝ →L[ℝ] ℝ) (L'norm_one : ‖L'‖ = 1) + (f : Lp ℝ p μ) (g : Lp ℝ q μ) in +lemma toDual_norm : ‖(toDual p μ L' g) f‖ ≤ ‖g‖ * ‖f‖ := by{ + calc ‖(toDual p μ L' g) f‖ ≤ ∫ x, ‖L' (g x) (f x)‖ ∂μ := by apply norm_integral_le_integral_norm + _ ≤ ‖L'‖ * ‖g‖ * ‖f‖ := by apply integral_mul_le L' hpq.out.symm + _ = ‖g‖ * ‖f‖ := by simp only [L'norm_one, one_mul] +} + +-- Lots of things take lots of time here, even the `simp only`s + /- The map sending `g` to `f ↦ ∫ x, (f x) * (g x) ∂μ` is a linear isometry. -/ -variable (L' : ℝ →L[ℝ] ℝ →L[ℝ] ℝ) (L'mul : ∀ x y, L' x y = x * y) (L'norm_one : ‖L'‖ = 1) in +variable (L' : ℝ →L[ℝ] ℝ →L[ℝ] ℝ) (L'mul : ∀ x y, L' x y = x * y) (L'norm_one : ‖L'‖ = 1) + (hμ: SigmaFinite μ) in def toDualₗᵢ' : Lp ℝ q μ →ₗᵢ[ℝ] Lp ℝ p μ →L[ℝ] ℝ where toFun := toDual _ _ L' map_add':= by{ intro g₁ g₂ - simp [toDual, IsBoundedLinearMap.toContinuousLinearMap, IsBoundedLinearMap.toLinearMap] + simp only [toDual, IsBoundedLinearMap.toContinuousLinearMap, IsBoundedLinearMap.toLinearMap, + AddSubmonoid.coe_add, AddSubgroup.coe_toAddSubmonoid] ext f - simp + simp only [coe_mk', IsLinearMap.mk'_apply, add_apply] rw [← integral_add] · apply integral_congr_ae filter_upwards [coeFn_add g₁ g₂] with a ha norm_cast rw [ha] - simp + simp only [Pi.add_apply, map_add, add_apply] · exact ENNReal.IsConjExponent.integrable_bilin L' hpq.out.symm μ (Lp.memℒp g₁) (Lp.memℒp f) · exact ENNReal.IsConjExponent.integrable_bilin L' hpq.out.symm μ (Lp.memℒp g₂) (Lp.memℒp f) } map_smul':= by{ intro m g - simp [toDual, IsBoundedLinearMap.toContinuousLinearMap, IsBoundedLinearMap.toLinearMap] + simp only [toDual, IsBoundedLinearMap.toContinuousLinearMap, IsBoundedLinearMap.toLinearMap, + RingHom.id_apply] ext f - simp + simp only [coe_mk', IsLinearMap.mk'_apply, coe_smul', Pi.smul_apply, smul_eq_mul] rw [← integral_mul_left] -- mul vs smul apply integral_congr_ae filter_upwards [coeFn_smul m g] with a ha rw [ha] - simp [L'mul]; ring + simp only [Pi.smul_apply, smul_eq_mul, L'mul]; ring } norm_map' := by { intro g - conv_lhs => simp [Norm.norm] + conv_lhs => simp [Norm.norm] -- is this simp okay or is there a risk this gets converted to something else if simp rules change? How do we deal with simps in conv? apply ContinuousLinearMap.opNorm_eq_of_bounds - . simp + . simp only [norm_nonneg] . intro f - calc ‖(toDual p μ L' g) f‖ ≤ ∫ x, ‖L' (g x) (f x)‖ ∂μ := by apply norm_integral_le_integral_norm - _ ≤ ‖L'‖ * ‖g‖ * ‖f‖ := by apply integral_mul_le L' hpq.out.symm - _ = ‖g‖ * ‖f‖ := by simp [L'norm_one] - _ = _ := by aesop + apply toDual_norm + exact L'norm_one . intro N Nnneg intro hbound - sorry + apply toDual_bound L' L'mul hμ g N Nnneg hbound } -/- The map sending `g` to `f ↦ ∫ x, L (f x) (g x) ∂μ` is a linear isometry. -/ -variable (p q μ) in -def toDualₗᵢ : Lp E₁ q μ →ₗᵢ[ℝ] Lp E₂ p μ →L[ℝ] E₃ where - toFun := toDual _ _ L +--See above. 5.6 seconds +-- I AM ADDING THE SAME HYPOTHESES AS ABOVE DOWN HERE. Namely, every space becomes ℝ and any bilinear map becomes a product +/- The map sending `g` to `f ↦ ∫ x, (f x) * (g x) ∂μ` is a linear isometry. -/ +variable (p q μ) (L' : ℝ →L[ℝ] ℝ →L[ℝ] ℝ) (L'mul : ∀ x y, L' x y = x * y) (L'norm_one : ‖L'‖ = 1) + (hμ: SigmaFinite μ) in +def toDualₗᵢ : Lp ℝ q μ →ₗᵢ[ℝ] Lp ℝ p μ →L[ℝ] ℝ where + + toFun := toDual _ _ L' map_add':= by{ intro g₁ g₂ - simp [toDual, IsBoundedLinearMap.toContinuousLinearMap, IsBoundedLinearMap.toLinearMap] + simp only [toDual, IsBoundedLinearMap.toContinuousLinearMap, IsBoundedLinearMap.toLinearMap, + AddSubmonoid.coe_add, AddSubgroup.coe_toAddSubmonoid] ext f - simp + simp only [coe_mk', IsLinearMap.mk'_apply, add_apply] rw [← integral_add] · apply integral_congr_ae filter_upwards [coeFn_add g₁ g₂] with a ha norm_cast rw [ha] - simp - · exact ENNReal.IsConjExponent.integrable_bilin L hpq.out.symm μ (Lp.memℒp g₁) (Lp.memℒp f) - · exact ENNReal.IsConjExponent.integrable_bilin L hpq.out.symm μ (Lp.memℒp g₂) (Lp.memℒp f) + simp only [Pi.add_apply, map_add, add_apply] + · exact ENNReal.IsConjExponent.integrable_bilin L' hpq.out.symm μ (Lp.memℒp g₁) (Lp.memℒp f) + · exact ENNReal.IsConjExponent.integrable_bilin L' hpq.out.symm μ (Lp.memℒp g₂) (Lp.memℒp f) } map_smul':= by{ intro m g - simp [toDual, IsBoundedLinearMap.toContinuousLinearMap, IsBoundedLinearMap.toLinearMap] + simp only [toDual, IsBoundedLinearMap.toContinuousLinearMap, IsBoundedLinearMap.toLinearMap, + RingHom.id_apply] ext f - simp + simp only [coe_mk', IsLinearMap.mk'_apply, coe_smul', Pi.smul_apply] rw [← integral_smul] apply integral_congr_ae filter_upwards [coeFn_smul m g] with a ha rw [ha] - simp + simp only [Pi.smul_apply, smul_eq_mul, L'mul, mul_assoc] } norm_map' := by { - sorry + intro g + simp only [LinearMap.coe_mk, AddHom.coe_mk] + conv_lhs => simp[Norm.norm] + apply ContinuousLinearMap.opNorm_eq_of_bounds + · simp only [norm_nonneg] + · intro f + apply toDual_norm + exact L'norm_one + · intro N Nnneg + intro hbound + apply toDual_bound L' L'mul hμ g N Nnneg hbound } /- The map sending `g` to `f ↦ ∫ x, L (f x) (g x) ∂μ` is a linear isometric equivalence. -/ From 8b60e48b7d1153275f1f298dbea5a92232dca710 Mon Sep 17 00:00:00 2001 From: Kunhong Du <43747297+KunhongDu@users.noreply.github.com> Date: Wed, 14 Aug 2024 15:06:20 +0200 Subject: [PATCH 07/10] Prove prop 6.13 [Folland] (#51) Proved prop 6.13 [Folland], finite case and infinite case. Also shortened some long lines. --- BonnAnalysis/ComplexInterpolation.lean | 383 ++++++++++++++++++------ blueprint/src/chapter/interpolation.tex | 62 +++- 2 files changed, 349 insertions(+), 96 deletions(-) diff --git a/BonnAnalysis/ComplexInterpolation.lean b/BonnAnalysis/ComplexInterpolation.lean index 32c74e4..00c88fb 100644 --- a/BonnAnalysis/ComplexInterpolation.lean +++ b/BonnAnalysis/ComplexInterpolation.lean @@ -945,45 +945,43 @@ theorem DiffContOnCl.norm_le_pow_mul_pow {a b : ℝ} {f : ℂ → ℂ} (hab: a rwa [← snorm_congr_ae hf.ae_eq_mk] + _ = sSup {snorm (f * (g.1 : α → ℂ)) 1 μ | g : Lp.simpleLe1 ℂ q μ} := by + congr; ext + have (g : Lp.simpleLe1 ℂ q μ) : snorm (f * (g.1 : α → ℂ)) 1 μ + = snorm (hf.mk * (g.1 : α → ℂ)) 1 μ := + snorm_congr_ae <| Filter.EventuallyEq.mul hf.ae_eq_mk (EventuallyEq.refl _ _) + simp [this] + + +open Set in +lemma snormEssSup_eq_sSup_snorm [SigmaFinite μ] (f : α → ℂ) (hf : Measurable f) +(hf' : sSup {x |∃ g : SimpleFunc α ℂ, snorm g 1 μ ≤ 1 ∧ +x = snorm (f * (g : α → ℂ)) 1 μ} < ⊤): +snormEssSup f μ = sSup {x |∃ g : SimpleFunc α ℂ, snorm g 1 μ ≤ 1 +∧ x = snorm (f * (g : α → ℂ)) 1 μ} := by + apply le_antisymm ?_ + . apply sSup_le + intro s ⟨g, hg₁, hg₂⟩ + rw [hg₂, mul_comm] + simp [snorm, snorm'] + apply le_trans (lintegral_norm_mul_le_one_top _ (by measurability)) + apply mul_le_of_le_one_of_le hg₁ (by simp [snorm]) + . set M := sSup {x |∃ g : SimpleFunc α ℂ, snorm g 1 μ ≤ 1 ∧ + x = snorm (f * (g : α → ℂ)) 1 μ} + apply essSup_le_of_ae_le + simp only [EventuallyLE, eventually_iff, mem_ae_iff] + by_contra h + + have aux1 : ∃ B : Set α, MeasurableSet B ∧ B ⊆ {x | ‖f x‖₊ ≤ M}ᶜ ∧ 0 < μ B ∧ μ B < ⊤ := by + apply Measure.exists_subset_measure_lt_top (MeasurableSet.compl _) ((ne_eq _ _) ▸ h).bot_lt + convert hf.ennnorm measurableSet_Iic + rcases aux1 with ⟨B, hB⟩ + + let g : SimpleFunc α ℂ := { + toFun := B.indicator (fun _ ↦ ((μ B)⁻¹.toReal : ℂ)) + measurableSet_fiber' := by + intro x + simp [indicator_preimage] + rcases eq_or_ne x ((μ B)⁻¹.toReal : ℂ) with (H | H) + simp [H] + apply MeasurableSet.ite hB.1 (by simp only [MeasurableSet.univ, M]) + apply measurableSet_preimage measurable_zero (MeasurableSet.singleton _) + apply MeasurableSet.ite hB.1 _ (measurableSet_preimage measurable_zero + (MeasurableSet.singleton _)) + rw [preimage_const_of_not_mem] + apply MeasurableSet.empty + rw [mem_singleton_iff] + exact H.symm + finite_range' := by + have : range (B.indicator fun _ ↦ ((μ B)⁻¹.toReal : ℂ)) + ⊆ {0, ((μ B)⁻¹.toReal : ℂ)} := by + intro x + rw [Set.mem_range_indicator] + simp + rintro (h | h) + exact Or.intro_left _ h.1 + exact Or.intro_right _ h.2.symm + apply Set.Finite.subset _ this + simp only [finite_singleton, Finite.insert] + } + + have aux_μB : (μ B)⁻¹ = ‖(μ B)⁻¹.toReal‖₊ := by + have : (μ B)⁻¹ < ⊤ := by simp [hB.2.2.1] + generalize (μ B)⁻¹ = y at this -- better solution??? + cases y + simp only [lt_self_iff_false] at this + simp only [coe_toReal, nnnorm_eq] + + have : ¬ (M < snorm (f * (g : α → ℂ)) 1 μ) := by + simp + apply le_sSup + use g + constructor + simp [snorm, snorm', lintegral_indicator_const] + have : ∫⁻ (a : α), (B.indicator (fun _ ↦ (μ B)⁻¹) a) ∂ μ ≤ 1 := by + rw [lintegral_indicator_const hB.1, + ENNReal.inv_mul_cancel hB.2.2.1.ne.symm hB.2.2.2.ne] + convert this + rename α => x + by_cases hx : x ∈ B + simp [indicator_of_mem hx, aux_μB.symm] + simp [indicator_of_not_mem hx] + rfl + + apply this + calc M = ∫⁻ _ in B, (μ B)⁻¹ * M ∂ μ := by { + rw [setLIntegral_const, mul_assoc, mul_comm M, ← mul_assoc, + ENNReal.inv_mul_cancel hB.2.2.1.ne.symm hB.2.2.2.ne, one_mul] + } + _ < ∫⁻ x in B, (μ B)⁻¹ * ‖f x‖₊ ∂ μ := by + apply setLIntegral_strict_mono hB.1 hB.2.2.1.ne.symm (hf.ennnorm.const_mul _) + rw [setLIntegral_const] + apply mul_ne_top (mul_ne_top (ENNReal.inv_ne_top.mpr + hB.2.2.1.ne.symm) hf'.ne) hB.2.2.2.ne + apply eventually_of_forall + intro x hx + rw [ENNReal.mul_lt_mul_left (ENNReal.inv_ne_zero.mpr hB.2.2.2.ne) + (ENNReal.inv_ne_top.mpr hB.2.2.1.ne.symm)] + convert hB.2.1 hx + simp only [mem_compl_iff, mem_setOf_eq, not_le] + _ = ∫⁻ x : α, B.indicator (fun a ↦ ‖f a‖₊ * ‖(fun _ ↦ ((μ B)⁻¹.toReal : ℂ)) a‖₊) x ∂μ := by + rw [lintegral_indicator _ hB.1] + simp [mul_comm] + congr with x; congr + _ = snorm (f * B.indicator fun _ ↦ ((μ B)⁻¹.toReal : ℂ)) 1 μ := by + simp [snorm, snorm'] + congr with x + by_cases hx : x ∈ B + simp only [indicator_of_mem hx, nnnorm_real] + simp only [indicator_of_not_mem hx, nnnorm_zero, ENNReal.coe_zero, mul_zero] + +lemma snormEssSup_eq_sSup_snorm' [SigmaFinite μ] (f : α → ℂ) (hf : AEMeasurable f μ) +(hf' : sSup {x |∃ g : SimpleFunc α ℂ, snorm g 1 μ ≤ 1 ∧ +x = snorm (f * (g : α → ℂ)) 1 μ} < ⊤): +snormEssSup f μ = sSup {x |∃ g : SimpleFunc α ℂ, snorm g 1 μ ≤ 1 +∧ x = snorm (f * (g : α → ℂ)) 1 μ} := by + + have aux1 {g : α → ℂ} : snorm (f * g) 1 μ = snorm (hf.mk * g) 1 μ := by + rw [snorm_congr_ae] + apply EventuallyEq.mul hf.ae_eq_mk EventuallyEq.rfl + + have : sSup {x |∃ g : SimpleFunc α ℂ, snorm g 1 μ ≤ 1 ∧ + x = snorm (hf.mk * (g : α → ℂ)) 1 μ} = sSup {x |∃ g : SimpleFunc α ℂ, snorm g 1 μ ≤ 1 + ∧ x = snorm (f * (g : α → ℂ)) 1 μ} := by + congr with x; simp + constructor + . rintro ⟨g, hg⟩; use g; rw [aux1]; exact hg --- need better solution + . rintro ⟨g, hg⟩; use g; rw [← aux1]; exact hg + + calc snormEssSup f μ = snormEssSup hf.mk μ := snormEssSup_congr_ae hf.ae_eq_mk + _ = sSup {x |∃ g : SimpleFunc α ℂ, snorm g 1 μ ≤ 1 ∧ x + = snorm (hf.mk * (g : α → ℂ)) 1 μ} := by + apply snormEssSup_eq_sSup_snorm hf.mk hf.measurable_mk + . rwa [this] + _ = sSup {x |∃ g : SimpleFunc α ℂ, snorm g 1 μ ≤ 1 ∧ + x = snorm (f * (g : α → ℂ)) 1 μ} := this + + end MeasureTheory end @@ -1110,7 +1282,8 @@ x ^ (y + z) = x ^ y * x ^ z := by simp only [hx0, coe_zero, add_pos hy hz, zero_rpow_of_pos, hy, hz, mul_zero] apply ENNReal.rpow_add <;> simp [hx0'] -lemma ENNReal.essSup_const_rpow (f : α → ℝ≥0∞) {r : ℝ} (hr : 0 < r) : (essSup f μ) ^ r = essSup (fun x ↦ (f x) ^ r) μ := +lemma ENNReal.essSup_const_rpow (f : α → ℝ≥0∞) {r : ℝ} (hr : 0 < r) : +(essSup f μ) ^ r = essSup (fun x ↦ (f x) ^ r) μ := OrderIso.essSup_apply (g := ENNReal.orderIsoRpow r hr) _ _ def InSegment.toIsConjugateExponent (p₀ p₁ p : ℝ≥0∞) (t s : ℝ≥0) (hp₀ : 0 < p₀) @@ -1119,16 +1292,26 @@ def InSegment.toIsConjugateExponent (p₀ p₁ p : ℝ≥0∞) (t s : ℝ≥0) Real.IsConjExponent (p₀⁻¹ * (s : ℝ≥0∞) * p).toReal ⁻¹ (p₁⁻¹ * (t : ℝ≥0∞) * p).toReal ⁻¹ where one_lt := by --- [one_lt_inv (a := (p₀⁻¹ * ↑s * p).toReal)] does not work ha?? - rw [lt_inv zero_lt_one (ENNReal.toReal_pos (mul_ne_zero (mul_ne_zero (ENNReal.inv_ne_zero.mpr (LT.lt.ne_top hp₀₁)) (by rwa [ENNReal.coe_ne_zero])) hp0') (ENNReal.mul_ne_top (ENNReal.mul_ne_top (ENNReal.inv_ne_top.mpr hp₀.ne.symm) ENNReal.coe_ne_top) hpt')), mul_comm p₀⁻¹] + rw [lt_inv zero_lt_one (ENNReal.toReal_pos (mul_ne_zero (mul_ne_zero (ENNReal.inv_ne_zero.mpr + (LT.lt.ne_top hp₀₁)) (by rwa [ENNReal.coe_ne_zero])) hp0') (ENNReal.mul_ne_top + (ENNReal.mul_ne_top (ENNReal.inv_ne_top.mpr hp₀.ne.symm) ENNReal.coe_ne_top) hpt')), + mul_comm p₀⁻¹] apply_fun (fun x ↦ x * p) at hp rw [add_mul, ENNReal.inv_mul_cancel hp0' hpt'] at hp - calc (↑s * p₀⁻¹ * p).toReal < (↑s * p₀⁻¹ * p + ↑t * p₁⁻¹ * p).toReal := ENNReal.toReal_strict_mono (hp ▸ one_ne_top) <| ENNReal.lt_add_right ((ENNReal.add_ne_top (b := ↑t * p₁⁻¹ * p)).mp (hp ▸ one_ne_top)).1 (mul_ne_zero (mul_ne_zero (by rwa [ENNReal.coe_ne_zero]) (by rwa [ENNReal.inv_ne_zero])) hp0') + calc (↑s * p₀⁻¹ * p).toReal < (↑s * p₀⁻¹ * p + ↑t * p₁⁻¹ * p).toReal := + ENNReal.toReal_strict_mono (hp ▸ one_ne_top) <| ENNReal.lt_add_right ( + (ENNReal.add_ne_top (b := ↑t * p₁⁻¹ * p)).mp (hp ▸ one_ne_top)).1 ( + mul_ne_zero (mul_ne_zero (by rwa [ENNReal.coe_ne_zero]) (by rwa [ENNReal.inv_ne_zero])) hp0') _ = 1⁻¹ := by simp [hp] inv_add_inv_conj := by - rw [inv_inv, inv_inv, ← ENNReal.toReal_add (ENNReal.mul_ne_top (ENNReal.mul_ne_top (ENNReal.inv_ne_top.mpr hp₀.ne.symm) ENNReal.coe_ne_top) hpt') (ENNReal.mul_ne_top (ENNReal.mul_ne_top (ENNReal.inv_ne_top.mpr hp₁.ne.symm) ENNReal.coe_ne_top) hpt'), ← ENNReal.one_toReal] + rw [inv_inv, inv_inv, ← ENNReal.toReal_add (ENNReal.mul_ne_top (ENNReal.mul_ne_top ( + ENNReal.inv_ne_top.mpr hp₀.ne.symm) ENNReal.coe_ne_top) hpt') (ENNReal.mul_ne_top ( + ENNReal.mul_ne_top (ENNReal.inv_ne_top.mpr hp₁.ne.symm) ENNReal.coe_ne_top) hpt'), + ← ENNReal.one_toReal] congr apply_fun (fun x ↦ x * p) at hp - rwa [add_mul, ENNReal.inv_mul_cancel hp0' hpt', mul_comm (ofNNReal s), mul_comm (ofNNReal t)] at hp + rwa [add_mul, ENNReal.inv_mul_cancel hp0' hpt', + mul_comm (ofNNReal s), mul_comm (ofNNReal t)] at hp lemma lintegral_mul_le_segment_exponent_aux {p₀ p₁ p : ℝ≥0∞} {t s : ℝ≥0} (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀₁ : p₀ < p₁) (hp : p⁻¹ = s / p₀ + t / p₁) @@ -1136,7 +1319,9 @@ lemma lintegral_mul_le_segment_exponent_aux {p₀ p₁ p : ℝ≥0∞} {t s : ∫⁻ (a : α), ↑‖f a‖₊ ^ (↑s * p.toReal) * ↑‖f a‖₊ ^ (↑t * p.toReal) ∂μ ≤ snorm (↑f) p₀ μ ^ (↑s * p.toReal) * snorm (↑f) p₁ μ ^ (↑t * p.toReal) := by rw [eq_comm] at hp + rw [eq_comm] at hp rcases eq_or_ne p ⊤ with hpt | hpt' + symm at hp simp [hpt, add_eq_zero, hs0', ht0'] at hp exact False.elim <| ne_top_of_lt hp₀₁ hp.1 @@ -1146,7 +1331,7 @@ lemma lintegral_mul_le_segment_exponent_aux {p₀ p₁ p : ℝ≥0∞} {t s : simp only [hp₁t, div_top, add_zero] at hp apply_fun (fun x ↦ x * p₀) at hp rw [ENNReal.div_mul_cancel hp₀.ne.symm (ne_top_of_lt hp₀₁)] at hp - have hp_aux : s * p = p₀ := by rw [hp, mul_assoc, mul_comm p₀, ← mul_assoc, + have hp_aux : s * p = p₀ := by rw [← hp, mul_assoc, mul_comm p₀, ← mul_assoc, ENNReal.inv_mul_cancel hp0' hpt', one_mul] apply le_trans (lintegral_mul_le_one_top _ (AEMeasurable.pow_const hf.ennnorm _)) (le_of_eq _) @@ -1154,33 +1339,41 @@ lemma lintegral_mul_le_segment_exponent_aux {p₀ p₁ p : ℝ≥0∞} {t s : rw [← ENNReal.rpow_mul, ← ENNReal.rpow_one (∫⁻ (a : α), ↑‖f a‖₊ ^ (↑s * p.toReal) ∂μ)] congr; ext; congr simp only [← hp_aux, toReal_mul, coe_toReal] -- lemma? to rw - simp only [← hp_aux, toReal_mul, coe_toReal, mul_inv_rev, mul_assoc p.toReal⁻¹, ← mul_assoc, inv_mul_cancel (by rwa [NNReal.coe_ne_zero]), one_mul, + simp only [← hp_aux, toReal_mul, coe_toReal, mul_inv_rev, mul_assoc p.toReal⁻¹, + ← mul_assoc, inv_mul_cancel (by rwa [NNReal.coe_ne_zero]), one_mul, inv_mul_cancel (ENNReal.toReal_ne_zero.mpr ⟨hp0', hpt'⟩)] apply (ENNReal.essSup_const_rpow _ ?_).symm - exact Real.mul_pos (lt_of_le_of_ne (NNReal.coe_nonneg t) (NNReal.coe_ne_zero.mpr ht0').symm) (ENNReal.toReal_pos hp0' hpt') + exact Real.mul_pos (lt_of_le_of_ne (NNReal.coe_nonneg t) (NNReal.coe_ne_zero.mpr ht0').symm) + (ENNReal.toReal_pos hp0' hpt') simp only [snorm, (ne_of_lt hp₀).symm, ↓reduceIte, LT.lt.ne_top hp₀₁, snorm', one_div, (ne_of_lt hp₁).symm, hp₁t', ge_iff_le] - apply le_trans (ENNReal.lintegral_mul_le_Lp_mul_Lq μ (by apply InSegment.toIsConjugateExponent p₀ p₁ p t s; repeat assumption) (AEMeasurable.pow_const hf.ennnorm _) (AEMeasurable.pow_const hf.ennnorm _)) (le_of_eq _) - + apply le_trans (ENNReal.lintegral_mul_le_Lp_mul_Lq μ + (InSegment.toIsConjugateExponent p₀ p₁ p t s hp₀ hp₁ hp₀₁ hp.symm hp0' ht0' hs0' hpt' hp₁t') + (AEMeasurable.pow_const hf.ennnorm _) (AEMeasurable.pow_const hf.ennnorm _)) (le_of_eq _) simp only [← ENNReal.rpow_mul] congr simp only [toReal_mul, coe_toReal, mul_inv_rev] - rw [toReal_inv, inv_inv, ← mul_assoc, ← mul_assoc, mul_comm _ p.toReal, mul_assoc p.toReal, mul_comm s.toReal, ← mul_assoc, mul_assoc _ s.toReal, - mul_inv_cancel (ENNReal.toReal_ne_zero.mpr ⟨hp0', hpt'⟩), mul_inv_cancel (by rwa [NNReal.coe_ne_zero]), one_mul, one_mul] + rw [toReal_inv, inv_inv, ← mul_assoc, ← mul_assoc, mul_comm _ p.toReal, + mul_assoc p.toReal, mul_comm s.toReal, ← mul_assoc, mul_assoc _ s.toReal, + mul_inv_cancel (ENNReal.toReal_ne_zero.mpr ⟨hp0', hpt'⟩), mul_inv_cancel + (by rwa [NNReal.coe_ne_zero]), one_mul, one_mul] rotate_left 1 simp only [toReal_mul, coe_toReal, mul_inv_rev] - rw [toReal_inv, inv_inv, ← mul_assoc, ← mul_assoc, mul_comm _ p.toReal, mul_assoc p.toReal, mul_comm t.toReal, ← mul_assoc, mul_assoc _ t.toReal, - mul_inv_cancel (ENNReal.toReal_ne_zero.mpr ⟨hp0', hpt'⟩), mul_inv_cancel (by rwa [NNReal.coe_ne_zero]), one_mul, one_mul] + rw [toReal_inv, inv_inv, ← mul_assoc, ← mul_assoc, mul_comm _ p.toReal, + mul_assoc p.toReal, mul_comm t.toReal, ← mul_assoc, mul_assoc _ t.toReal, + mul_inv_cancel (ENNReal.toReal_ne_zero.mpr ⟨hp0', hpt'⟩), mul_inv_cancel + (by rwa [NNReal.coe_ne_zero]), one_mul, one_mul] repeat' simp [← mul_assoc, ENNReal.toReal_inv] -lemma lintegral_mul_le_segment_exponent {p₀ p₁ p : ℝ≥0∞} {s t : ℝ≥0} (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀₁ : p₀ < p₁) (hp : p⁻¹ = s / p₀ + t / p₁) (hst : s + t = 1) -(f : α → E) (hf : AEMeasurable f μ) +lemma lintegral_mul_le_segment_exponent {p₀ p₁ p : ℝ≥0∞} {s t : ℝ≥0} +(hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀₁ : p₀ < p₁) (hp : p⁻¹ = s / p₀ + t / p₁) +(hst : s + t = 1) (f : α → E) (hf : AEMeasurable f μ) : snorm f p μ ≤ (snorm f p₀ μ) ^ (s : ℝ) * (snorm f p₁ μ) ^ (t : ℝ) := by rw [eq_comm] at hp have hp0' : p ≠ 0 := by @@ -1205,11 +1398,14 @@ lemma lintegral_mul_le_segment_exponent {p₀ p₁ p : ℝ≥0∞} {s t : ℝ≥ . simp [hpt, add_eq_zero, hs0', ht0'] at hp exact False.elim <| ne_top_of_lt hp₀₁ hp.1 - . calc snorm f p μ = (∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ) ^ p.toReal⁻¹ := by simp [snorm, hp0', hpt', snorm'] + . calc snorm f p μ = (∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ) ^ p.toReal⁻¹ := by + {simp [snorm, hp0', hpt', snorm']} _ = (∫⁻ (a : α), ↑‖f a‖₊ ^ (s * p.toReal) * ↑‖f a‖₊ ^ (t * p.toReal) ∂μ) ^ p.toReal⁻¹ := by congr; ext - rw [← ENNReal.rpow_add_of_pos (s * p.toReal) (t * p.toReal) ?_ ?_, ← add_mul, ← NNReal.coe_add, hst, NNReal.coe_one, one_mul] - <;> apply Real.mul_pos (lt_of_le_of_ne (NNReal.coe_nonneg _) (NNReal.coe_ne_zero.mpr (by assumption)).symm) (ENNReal.toReal_pos hp0' hpt') + rw [← ENNReal.rpow_add_of_pos (s * p.toReal) (t * p.toReal) ?_ ?_, ← add_mul, + ← NNReal.coe_add, hst, NNReal.coe_one, one_mul] + <;> apply Real.mul_pos (lt_of_le_of_ne (NNReal.coe_nonneg _) + (NNReal.coe_ne_zero.mpr (by assumption)).symm) (ENNReal.toReal_pos hp0' hpt') _ ≤ ((snorm f p₀ μ) ^ (s * p.toReal) * (snorm f p₁ μ) ^ (t * p.toReal)) ^ p.toReal⁻¹ := by gcongr rw [eq_comm] at hp @@ -1227,12 +1423,14 @@ theorem exists_lnorm_le_of_subadditive_of_lbounded {p₀ p₁ q₀ q₁ : ℝ≥ (T : (α → E₁) →ₗ[ℂ] β → E₂) (h₀T : HasStrongType T p₀ q₀ μ ν M₀) (h₁T : HasStrongType T p₁ q₁ μ ν M₁) - {θ η : ℝ≥0} (hθη : θ + η = 1) + {θ η : ℝ≥0} (hθη : θ + η = 1) (hθ : 0 < θ) (hη : 0 < η) + -- when θ = 0 it is trivial should discard this assumtption later {p q : ℝ≥0∞} (hp : p⁻¹ = θ / p₀ + η / p₁) (hq : q⁻¹ = θ / q₀ + η / q₁) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) : HasStrongType T p q μ ν (M₀ ^ (θ : ℝ) * M₁ ^ (η : ℝ)) := by rcases eq_or_ne p₀ p₁ with (hp₀₁ | hp₀₁) - . simp only [hp₀₁, ← ENNReal.add_div, ← ENNReal.coe_add, hθη, ENNReal.coe_one, one_div, inv_inj] at hp + . simp only [hp₀₁, ← ENNReal.add_div, ← ENNReal.coe_add, hθη, ENNReal.coe_one, + one_div, inv_inj] at hp intro f hf have aesm := (h₀T f (by rwa [hp₀₁, ← hp])).1 constructor @@ -1242,9 +1440,12 @@ theorem exists_lnorm_le_of_subadditive_of_lbounded {p₀ p₁ q₀ q₁ : ℝ≥ exact lintegral_mul_le_segment_exponent hq₀ hq₁ hq₀₁ hq hθη _ aesm.aemeasurable rcases lt_or_eq_of_le hq₀₁ with hq₀₁ | hq₀₁ rw [mul_comm] - apply lintegral_mul_le_segment_exponent hq₁ hq₀ hq₀₁ (by rwa [add_comm]) (by rwa [add_comm]) _ aesm.aemeasurable - simp only [hq₀₁, ← ENNReal.add_div, ← ENNReal.coe_add, hθη, ENNReal.coe_one, one_div, inv_inj] at hq - rw [hq₀₁, ← hq, ← ENNReal.rpow_add_of_nonneg _ _ (by norm_num) (by norm_num), ← NNReal.coe_add, hθη, NNReal.coe_one, ENNReal.rpow_one] + apply lintegral_mul_le_segment_exponent hq₁ hq₀ hq₀₁ (by rwa [add_comm]) + (by rwa [add_comm]) _ aesm.aemeasurable + simp only [hq₀₁, ← ENNReal.add_div, ← ENNReal.coe_add, hθη, ENNReal.coe_one, + one_div, inv_inj] at hq + rw [hq₀₁, ← hq, ← ENNReal.rpow_add_of_nonneg _ _ (by norm_num) + (by norm_num), ← NNReal.coe_add, hθη, NNReal.coe_one, ENNReal.rpow_one] } _ ≤ (M₀ * snorm f p μ) ^ (θ : ℝ) * (M₁ * snorm f p μ) ^ (η : ℝ) := by gcongr @@ -1253,5 +1454,11 @@ theorem exists_lnorm_le_of_subadditive_of_lbounded {p₀ p₁ q₀ q₁ : ℝ≥ rw [hp] at * apply (h₁T f hf).2 _ = ↑(M₀ ^ (θ : ℝ) * M₁ ^ (η : ℝ)) * snorm f p μ := by - rw [ENNReal.mul_rpow_of_nonneg _ _ (by norm_num), ENNReal.mul_rpow_of_nonneg _ _ (by norm_num), ← mul_assoc, mul_assoc ((M₀ : ℝ≥0∞) ^ (θ : ℝ)), mul_comm _ ((M₁ : ℝ≥0∞) ^ (η : ℝ)), ← mul_assoc, mul_assoc, ← ENNReal.rpow_add_of_nonneg _ _ (by norm_num) (by norm_num), ← NNReal.coe_add, hθη, NNReal.coe_one, ENNReal.rpow_one, coe_mul, ENNReal.coe_rpow_of_ne_zero hM₀.ne.symm, ENNReal.coe_rpow_of_ne_zero hM₁.ne.symm] - . sorry + rw [ENNReal.mul_rpow_of_nonneg _ _ (by norm_num), + ENNReal.mul_rpow_of_nonneg _ _ (by norm_num), + ← mul_assoc, mul_assoc ((M₀ : ℝ≥0∞) ^ (θ : ℝ)), mul_comm _ ((M₁ : ℝ≥0∞) ^ (η : ℝ)), + ← mul_assoc, mul_assoc, ← ENNReal.rpow_add_of_nonneg _ _ (by norm_num) (by norm_num), + ← NNReal.coe_add, hθη, NNReal.coe_one, ENNReal.rpow_one, + coe_mul, ENNReal.coe_rpow_of_ne_zero hM₀.ne.symm, + ENNReal.coe_rpow_of_ne_zero hM₁.ne.symm] + . sorry diff --git a/blueprint/src/chapter/interpolation.tex b/blueprint/src/chapter/interpolation.tex index 764e48c..90d41d0 100644 --- a/blueprint/src/chapter/interpolation.tex +++ b/blueprint/src/chapter/interpolation.tex @@ -95,20 +95,66 @@ \section{Rietz-Thorin's Interpolation Theorem} \begin{lemma} - \label{lem:lp_of_sup_norm} + \label{lem:snorm_eq_sSup_snorm} %\uses{} - %\lean{} - %\leanok - Let $p$ and $q$ be conjugate exponents and let $g$ be integrable on all sets of finite measure. If - \[ \sup_{||f||_{L^p} \leq 1, \ f \text{ simple}} \left| \int fg \right| = M < \infty \] - then $g$ is in $L^q$ and $||g||_{L^q} = M$. + \lean{MeasureTheory.snorm_eq_sSup_snorm} + \leanok + Let $p$ and $q$ be real conjugate exponents. Let $f$ be measurable. Then + \[ \|f\|_{L^q} = \sup_{\|g\|_{L^p} \leq 1, \ g \text{ simple}} \| fg \|_{L^1}.\] + + In particular, if the right hand side formula is finite, $f\in L^q$. \end{lemma} \begin{proof} % \uses{} % Put any results used in the proof but not in the statement here - % \leanok % uncomment if the lemma has been proven - Details to be filled later. + \leanok % uncomment if the lemma has been proven + That $$\sup_{\|g\|_{L^p} \leq 1, \ g \text{ simple}} \| fg \|_{L^1} \le \|f\|_{L^q}$$ + follows from Hölder's inequality. + + The other direction is trivial when $\|f\|_{L^q}=0$. Suppose $\|f\|_{L^q}\ne 0$. + Set $$g = \cfrac{|f|^{p-1}}{\|f\|_{L^p}^{p-1}}.$$ + Then $\|g\|_{L^p} = 1$. + \begin{align*} + \|f\|_{L^q} &= \| fg \|_{L^1} \\ + &= \sup_{n \in \mathbb N} \| fg_n \|_{L^1} \tag{1}\\ + &\le \sup_{\|g\|_{L^p} \leq 1, \ g \text{ simple}} \| fg \|_{L^1} \tag{2} + \end{align*} + + In (1) and (2), $g_n$ is a monotone sequence of simple function approximating $g$ from below, + whose existence is basic real analysis. \end{proof} +\begin{lemma} + \label{lem:snormEssSup_eq_sSup_snorm} + %\uses{} + \lean{MeasureTheory.snormEssSup_eq_sSup_snorm} + \leanok + Let $f$ be measurable and the measure $\mu$ be $\sigma$-finite. Then + \[ \|f\|_{L^\infty} = \sup_{\|g\|_{L^1} \leq 1, \ g \text{ simple}} \| fg \|_{L^1}.\] +\end{lemma} + +\begin{proof} + \leanok + That $$\sup_{\|g\|_{L^1} \leq 1, \ g \text{ simple}} \| fg \|_{L^1} \le \|f\|_{L^\infty}$$ + follows from Hölder's inequality. + + Suppose $M:= \sup_{\|g\|_{L^1} \leq 1, \ g \text{ simple}} \| fg \|_{L^1} < \|f\|_{L^\infty}$. + Then $\{x | |f(x)| \ge M \}$ has positive measure. Since $\mu$ is $\sigma$-finite, we have a subset $B \subset \{x | |f(x)| \ge M \}$ with finite positive measure + by \href{https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/Typeclasses.html#MeasureTheory.Measure.exists_subset_measure_lt_top}{a classical lemma.} Now set + $$h := \mu(B)^{-1} \chi_B.$$ + Then we have + \begin{align*} + M &= \int_B \mu (B)^{-1} M d\mu \\ + &< \int_B \mu (B) |f| d\mu \\ + &= \|fh\|_{L^1}. + \end{align*} + But $\|h\|=1$ and $h$ is simple, so $\|fh\|_{L^1} \le M$, contradiction. + +\end{proof} + + + + + \begin{comment} (Note: This is used by Stein-Shakarchi to prove the dual of $L^p$ is $L^q$, so it may be already formalized by the time we get to this point?)\\\\ From 646d268876c1b9d8d7889fa20a50d8e818f00d0a Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 14 Aug 2024 13:27:38 +0000 Subject: [PATCH 08/10] Golf `Hadamard.lean` (#44) --- BonnAnalysis/Hadamard.lean | 87 +++++++++++++++----------------------- 1 file changed, 33 insertions(+), 54 deletions(-) diff --git a/BonnAnalysis/Hadamard.lean b/BonnAnalysis/Hadamard.lean index fd20e79..df8906a 100644 --- a/BonnAnalysis/Hadamard.lean +++ b/BonnAnalysis/Hadamard.lean @@ -2,7 +2,7 @@ import Mathlib.Analysis.Complex.Hadamard open Set Filter Function Complex Topology HadamardThreeLines -lemma Real.sub_ne_zero_of_lt {a b : ℝ} (hab: a < b) : b - a ≠ 0 := by apply ne_of_gt; simp[hab] +lemma Real.sub_ne_zero_of_lt {a b : ℝ} (hab: a < b) : b - a ≠ 0 := by apply ne_of_gt; simp [hab] namespace Complex @@ -61,26 +61,21 @@ lemma scale_mem_strip {z : ℂ} {l u : ℝ} (hul: l < u) (hz: z ∈ verticalClos div_self (Real.sub_ne_zero_of_lt hul), ← div_eq_mul_one_div] constructor · gcongr - · apply le_of_lt; simp [hul] + · exact le_of_lt (sub_pos.mpr hul) · exact hz.1 · rw [← sub_le_sub_iff_right (l / (u-l)), add_sub_assoc, sub_self, add_zero, div_sub_div_same, - div_le_one (by simp[hul]), sub_le_sub_iff_right l] + div_le_one (by simp [hul]), sub_le_sub_iff_right l] exact hz.2 } /-- The function `scale f l u` is `diffContOnCl`. -/ lemma scale_diffContOnCl {f: ℂ → E} {l u : ℝ} (hul: l < u) (hd : DiffContOnCl ℂ f (verticalStrip l u)) : DiffContOnCl ℂ (scale f l u) - (verticalStrip 0 1) := by{ - unfold scale - apply DiffContOnCl.comp (s:= verticalStrip l u) hd - · apply DiffContOnCl.const_add - apply DiffContOnCl.smul_const - apply DiffContOnCl.id - · rw [MapsTo] - intro z hz - exact scale_mapsto_dom hul hz -} + (verticalStrip 0 1) := by + apply DiffContOnCl.comp (s:= verticalStrip l u) hd (DiffContOnCl.const_add + (DiffContOnCl.smul_const DiffContOnCl.id _) _) _ + rw [MapsTo] + exact fun z hz ↦ scale_mapsto_dom hul hz /-- The norm of the function `scale f l u` is bounded above on the closed strip `re⁻¹' [0, 1]`-/ lemma scale_bddAbove {f: ℂ → E} {l u : ℝ} (hul: l< u) @@ -106,8 +101,7 @@ lemma scale_bddAbove {f: ℂ → E} {l u : ℝ} (hul: l< u) lemma scale_bound_left {f: ℂ → E} {l u a : ℝ} (ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a) : ∀ z ∈ re ⁻¹' {0}, ‖scale f l u z‖ ≤ a := by{ simp only [mem_preimage, mem_singleton_iff, scale, smul_eq_mul] - intro z hz - exact ha (↑l + z * (↑u - ↑l)) (by simp[hz]) + exact fun z hz ↦ ha (↑l + z * (↑u - ↑l)) (by simp [hz]) } /--A bound to the norm of `f` on the line `z.re=u` induces a bound to the norm of `scale f l u z` @@ -115,8 +109,7 @@ lemma scale_bound_left {f: ℂ → E} {l u a : ℝ} (ha : ∀ z ∈ re ⁻¹' {l lemma scale_bound_right {f: ℂ → E} {l u b : ℝ} (hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b) : ∀ z ∈ re ⁻¹' {1}, ‖scale f l u z‖ ≤ b := by{ simp only [scale, mem_preimage, mem_singleton_iff, smul_eq_mul] - intro z hz - exact hb (↑l + z * (↑u - ↑l)) (by simp[hz]) + exact fun z hz ↦ hb (↑l + z * (↑u - ↑l)) (by simp [hz]) } /--A technical lemma needed in the proof-/ @@ -129,14 +122,11 @@ lemma fun_arg_eq {l u: ℝ} (hul: l < u) (z: ℂ) : /--Another technical lemma needed in the proof-/ lemma bound_exp_eq {l u: ℝ} (hul : l < u) (z:ℂ) : - (z / (↑u - ↑l)).re - ((l:ℂ) / (↑u - ↑l)).re = (z.re - l) / (u - l) := by{ + (z / (↑u - ↑l)).re - ((l:ℂ) / (↑u - ↑l)).re = (z.re - l) / (u - l) := by norm_cast rw [Complex.div_re, Complex.normSq_ofReal, Complex.ofReal_re, Complex.ofReal_im, mul_div_assoc, - div_mul_eq_div_div_swap, div_self (by norm_cast; exact Real.sub_ne_zero_of_lt hul), - ← div_eq_mul_one_div] - simp only [mul_zero, zero_div, add_zero] - rw [← div_sub_div_same] -} + div_mul_eq_div_div_swap, div_self (by exact_mod_cast Real.sub_ne_zero_of_lt hul), + ← div_eq_mul_one_div, mul_zero, zero_div, add_zero, ← div_sub_div_same] /--The correct generalization of `interpStrip` to produce bounds in the general case-/ noncomputable def interpStrip' (f: ℂ → E) (l u : ℝ) (z : ℂ) : ℂ := @@ -148,45 +138,39 @@ noncomputable def interpStrip' (f: ℂ → E) (l u : ℝ) (z : ℂ) : ℂ := /--The supremum of the norm of `scale f l u` on the line `z.re = 0` is the same as the supremum of `f` on the line `z.re=l`.-/ lemma sSupNormIm_scale_left (f: ℂ → E) {l u : ℝ} (hul: l < u) : - sSupNormIm (scale f l u) 0 = sSupNormIm f l := by{ + sSupNormIm (scale f l u) 0 = sSupNormIm f l := by simp_rw [sSupNormIm, image_comp] - have : scale f l u '' (re ⁻¹' {0}) = f '' (re ⁻¹' {l}) := by{ + have : scale f l u '' (re ⁻¹' {0}) = f '' (re ⁻¹' {l}) := by ext e simp only [scale, smul_eq_mul, mem_image, mem_preimage, mem_singleton_iff] - constructor - · intro h - obtain ⟨z, hz₁, hz₂⟩ := h + refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ + · obtain ⟨z, hz₁, hz₂⟩ := h use ↑l + z * (↑u - ↑l) simp [hz₁, hz₂] - · intro h - obtain ⟨z, hz₁, hz₂⟩ := h + · obtain ⟨z, hz₁, hz₂⟩ := h use ((z-l)/(u-l)) constructor · norm_cast rw [Complex.div_re, Complex.normSq_ofReal, Complex.ofReal_re] - simp[hz₁] - · rw [div_mul_comm, div_self (by norm_cast; exact Real.sub_ne_zero_of_lt hul)] + simp [hz₁] + · rw [div_mul_comm, div_self (by exact_mod_cast Real.sub_ne_zero_of_lt hul)] simp [hz₂] - } rw [this] -} /--The supremum of the norm of `scale f l u` on the line `z.re = 1` is the same as the supremum of `f` on the line `z.re=u`.-/ lemma sSupNormIm_scale_right (f: ℂ → E) {l u : ℝ} (hul: l < u) : - sSupNormIm (scale f l u) 1 = sSupNormIm f u := by{ + sSupNormIm (scale f l u) 1 = sSupNormIm f u := by simp_rw [sSupNormIm, image_comp] - have : scale f l u '' (re ⁻¹' {1}) = f '' (re ⁻¹' {u}) := by{ + have : scale f l u '' (re ⁻¹' {1}) = f '' (re ⁻¹' {u}) := by ext e simp only [scale, smul_eq_mul, mem_image, mem_preimage, mem_singleton_iff] - constructor - · intro h - obtain ⟨z, hz₁, hz₂⟩ := h + refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ + · obtain ⟨z, hz₁, hz₂⟩ := h use ↑l + z * (↑u - ↑l) simp only [add_re, ofReal_re, mul_re, hz₁, sub_re, one_mul, sub_im, ofReal_im, sub_self, mul_zero, sub_zero, add_sub_cancel, hz₂, and_self] - · intro h - obtain ⟨z, hz₁, hz₂⟩ := h + · obtain ⟨z, hz₁, hz₂⟩ := h use ((z-l)/(u-l)) constructor · norm_cast @@ -194,21 +178,17 @@ lemma sSupNormIm_scale_right (f: ℂ → E) {l u : ℝ} (hul: l < u) : simp only [sub_re, hz₁, ofReal_re, sub_im, ofReal_im, sub_zero, ofReal_sub, sub_self, mul_zero, zero_div, add_zero] rw [div_mul_eq_div_div_swap, mul_div_assoc, - div_self (by norm_cast; exact Real.sub_ne_zero_of_lt hul), - mul_one, div_self (by norm_cast; exact Real.sub_ne_zero_of_lt hul)] - · rw [div_mul_comm, div_self (by norm_cast; exact Real.sub_ne_zero_of_lt hul)] + div_self (by exact_mod_cast Real.sub_ne_zero_of_lt hul), + mul_one, div_self (by exact_mod_cast Real.sub_ne_zero_of_lt hul)] + · rw [div_mul_comm, div_self (by exact_mod_cast Real.sub_ne_zero_of_lt hul)] simp only [one_mul, add_sub_cancel, hz₂] - } rw [this] -} /--A technical lemma relating the bounds given by the three lines lemma on a general strip to the bounds for its scaled version on the strip ``re ⁻¹' [0,1]` to the bounds on a general strip.-/ lemma interpStrip_scale (f: ℂ → E) {l u : ℝ} (hul: l < u) (z : ℂ) : interpStrip (scale f l u) - ((z - ↑l) / (↑u - ↑l)) = interpStrip' f l u z := by{ - simp only [interpStrip, interpStrip'] - simp_rw [sSupNormIm_scale_left f hul, sSupNormIm_scale_right f hul] -} + ((z - ↑l) / (↑u - ↑l)) = interpStrip' f l u z := by + rw [interpStrip, interpStrip', sSupNormIm_scale_left f hul, sSupNormIm_scale_right f hul] /-- **Hadamard three-line theorem**: If `f` is a bounded function, continuous on the @@ -222,8 +202,8 @@ lemma norm_le_interpStrip_of_mem {l u : ℝ} (hul: l < u) {f : ℂ → E} {z : ‖f z‖ ≤ ‖interpStrip' f l u z‖ := by{ have hgoal := norm_le_interpStrip_of_mem_verticalClosedStrip (scale f l u) (scale_mem_strip hul hz) (scale_diffContOnCl hul hd) (scale_bddAbove hul hB) - simp only [scale, smul_eq_mul, norm_eq_abs] at hgoal - rw [fun_arg_eq hul, div_sub_div_same, interpStrip_scale f hul z] at hgoal + rw [scale, smul_eq_mul, norm_eq_abs, fun_arg_eq hul, div_sub_div_same, + interpStrip_scale f hul z] at hgoal exact hgoal } @@ -242,8 +222,7 @@ lemma norm_le_interp_of_mem' {f : ℂ → E} {z : ℂ} {a b l u : ℝ} (hul: l < have hgoal := norm_le_interp_of_mem_verticalClosedStrip' (scale f l u) (scale_mem_strip hul hz) (scale_diffContOnCl hul hd) (scale_bddAbove hul hB) (scale_bound_left ha) (scale_bound_right hb) - simp only [scale, smul_eq_mul, sub_re] at hgoal - rw [fun_arg_eq hul, bound_exp_eq hul] at hgoal + rw [scale, smul_eq_mul, sub_re, fun_arg_eq hul, bound_exp_eq hul] at hgoal exact hgoal } From 76c2f66555379eb9b3601b84a5ae53dfba8fe1d5 Mon Sep 17 00:00:00 2001 From: Tim Lichtnau Date: Wed, 14 Aug 2024 15:39:16 +0200 Subject: [PATCH 09/10] Distributions (#50) Unfortunately, there is still missing: - Distributions commute with Integration - convolution of Distribution with test function is not only continuous but actually smooth --- BonnAnalysis/ConvergingSequences.lean | 192 +++++++ BonnAnalysis/ConvolutionTendsToUniformly.lean | 386 +++++++++++++ BonnAnalysis/Distributions.lean | 338 +++++++++++ BonnAnalysis/DistributionsExamples.lean | 530 ++++++++++++++++++ BonnAnalysis/DistributionsOfVEndo.lean | 494 ++++++++++++++++ BonnAnalysis/UniformConvergenceSequences.lean | 73 +++ 6 files changed, 2013 insertions(+) create mode 100644 BonnAnalysis/ConvergingSequences.lean create mode 100644 BonnAnalysis/ConvolutionTendsToUniformly.lean create mode 100644 BonnAnalysis/Distributions.lean create mode 100644 BonnAnalysis/DistributionsExamples.lean create mode 100644 BonnAnalysis/DistributionsOfVEndo.lean create mode 100644 BonnAnalysis/UniformConvergenceSequences.lean diff --git a/BonnAnalysis/ConvergingSequences.lean b/BonnAnalysis/ConvergingSequences.lean new file mode 100644 index 0000000..8fbd70b --- /dev/null +++ b/BonnAnalysis/ConvergingSequences.lean @@ -0,0 +1,192 @@ +import Mathlib.Topology.Sequences +import Mathlib.Topology.Defs.Filter +import Mathlib.Topology.Order +import Mathlib.Order.Filter.Basic +import Mathlib.Tactic.FunProp +-- import Mathlib.Order +-- noncomputable section + +--open FourierTransform MeasureTheory Real + + +namespace MeasureTheory + +universe u v +open Order Set Filter +open Filter +open scoped Topology + +set_option checkBinderAnnotations false +class SubSequence {X : Type u} (a : ℕ → X) where + φ : ℕ → ℕ + hφ : StrictMono φ +--open SubSequence +--@[coe] def coeSubS {X : Type u} {a : ℕ → X} (σ : SubSequence a): ℕ → X := a ∘ σ.φ -- how to not automatically coerce everywhere? +instance {X : Type u} {a : ℕ → X} : CoeFun (SubSequence a) (fun _ => ℕ → X) where + coe σ := a ∘ σ.φ -- how to not automatically coerce everywhere? +--instance {X Y : Type u} {f : X → Y} {a : ℕ → X} : Coe (SubSequence a) (SubSequence (f ∘ a)) where +-- coe σ := ⟨ σ.φ , σ.hφ⟩ +lemma bndOnStrictMono {φ : ℕ → ℕ} (hφ : StrictMono φ) {a : ℕ} : ¬ (φ a < a) := by + intro ass + induction' a with n hn + · exact Nat.not_succ_le_zero (φ 0) ass + · apply hn + have : φ (n + 1) ≤ n := Nat.le_of_lt_succ ass + apply LE.le.trans_lt' this + apply hφ + exact lt_add_one n +lemma subsequencePreservesTop {φ : ℕ → ℕ} + (hφ : StrictMono φ) : map φ atTop ≤ atTop := by + rw [le_def] + intro U hU + simp at hU + obtain ⟨ a , ha⟩ := hU + have : ∃ a' , φ a' ≥ a := by + by_contra ass + push_neg at ass + specialize ass a + apply bndOnStrictMono hφ ass + simp only [mem_map, mem_atTop_sets, ge_iff_le, mem_preimage] + + use this.choose + intro b hb + apply ha + trans + exact this.choose_spec + apply StrictMono.monotone hφ hb + +lemma subSeqConverges' {X : Type u} {ι : Type v} {q : Filter ι}{p : Filter X} {a : ι → X} + {φ : ι → ι} + (hφ : map φ q ≤ q) (pf : Tendsto a q p) : + Tendsto (a ∘ φ) q p := by + intro U hU + rw [tendsto_def] at pf + specialize pf U hU + rw [mem_map] + exact hφ pf +lemma subSeqConverges {X : Type u} {p : Filter X} {a : ℕ → X} + (pf : Tendsto a atTop p) (a' : SubSequence a) : + Tendsto a' atTop p := subSeqConverges' (subsequencePreservesTop a'.hφ) pf + +class ConvergingSequences (X : Type u) where + seq : (ℕ → X) × X → Prop + seq_cnst : ∀ x : X , seq (fun _ => x , x ) + seq_sub : ∀ {a x} , seq ( a, x) → ∀ a' : SubSequence a , seq (a' , x) + + +variable {X : Type u} [ConvergingSequences X] +--notation (priority := high) P "[" A "]" => obj_over (P:=P.1.hom) A +open ConvergingSequences +scoped notation a " ⟶ " x => seq (a , x) +@[simp] def nbh (x : X) : Filter X := by + use {Y | ∀ a , (a ⟶ x) → Y ∈ map a atTop} + · simp + · simp only [mem_map, mem_atTop_sets, ge_iff_le, mem_preimage, mem_setOf_eq] ; + intro Y Z + intro ass hYZ b (hb : b ⟶ x) + specialize ass b hb + obtain ⟨ a , ha⟩ := ass + use a + intro i hi + apply hYZ + exact ha i hi + · intro Y Z hY hZ + intro a ha + rw [inter_mem_iff] + constructor + apply hY a ha + apply hZ a ha + -- def IsSeqClosed (s : Set X) : Prop := ∀ ⦃x : ℕ → X⦄ ⦃p : X⦄, (∀ n, x n ∈ s) ∧ seq (x , p) → p ∈ s + +instance fromSeq : TopologicalSpace X := .mkOfNhds nbh + +lemma tendsToNbh {x : X} (a : ℕ → X) (ha : a ⟶ x) : Tendsto a atTop (nbh x) := by + intro N hN + apply hN + exact ha +lemma nbhdCofinalIn𝓝 {x : X} {U} (hU : U ∈ 𝓝 x) : ∃ V ∈ nbh x , V ⊆ U := by + rw [@mem_nhds_iff] at hU + obtain ⟨ V , hV ⟩ := hU + use V + constructor + · apply hV.2.1 + exact hV.2.2 + · exact hV.1 +lemma tendsTo𝓝 {x : X} (a : ℕ → X) (ha : a ⟶ x) : Tendsto a atTop (𝓝 x) := by +intro U hU +obtain ⟨ V , hV ⟩ := nbhdCofinalIn𝓝 hU +apply mem_of_superset ; swap +· exact hV.2 +· apply hV.1 + exact ha + +lemma subSeqCnstrction {a : ℕ → X} {Y : Set (X)} (as : Y ∉ map a atTop) : + ∃ (a' : SubSequence a) , ∀ n , a' n ∉ Y := by + simp at as + let φ : ℕ → ℕ := by + intro n + induction n with + | zero => exact (as 0).choose + | succ _ φn => exact ((as (Nat.succ φn)).choose) + use ⟨ φ , by + intro n b + induction b with + | zero => simp + | succ b hb => + intro as' + have : φ n ≤ φ b := by + by_cases h : n = b + · rw [h] ; + · exact le_of_lt (hb <| Nat.lt_of_le_of_ne (Nat.le_of_lt_succ as') h) + exact Nat.lt_of_le_of_lt this (as (Nat.succ (φ b))).choose_spec.1 + ⟩ + intro n + simp + induction n with + | zero => exact (as 0).choose_spec.2 + | succ n _ => exact ((as (Nat.succ (φ n))).choose_spec.2) + +lemma seqInNhd {a : ℕ → X} {N : Set X} (hN : N ∈ map a atTop) : ∃ n , a n ∈ N := by + simp at hN + use hN.choose + apply hN.choose_spec + exact le_rfl + +lemma important (x : X) (N : Set X) (p : N ∈ 𝓝 x) : N ∈ nbh x := by + rw [mem_nhds_iff] at p + + + + obtain ⟨ U , ⟨ q , r , p⟩ ⟩ := p + exact mem_of_superset (r x p) q +@[fun_prop] structure SeqContinuous' {Y : Type v} [TopologicalSpace Y] (f : X → Y) : Prop where + seqCont :∀ {x} {a : X} , (x ⟶ a) → Tendsto (f ∘ x) atTop (𝓝 (f a)) + +open SeqContinuous' +@[fun_prop] structure SeqContinuousStrongly {Y : Type v} [ConvergingSequences Y] (f : X → Y) : Prop where + seqCont :∀ {x} {a : X} , (x ⟶ a) → (f ∘ x) ⟶ (f a) +@[fun_prop] lemma continuous_of_SeqContinuous {Y : Type v} [TopologicalSpace Y] {f : X → Y} + (hf : SeqContinuous' f) : Continuous f := by + apply continuous_iff_isClosed.mpr + intro C hC + rw [← @isOpen_compl_iff] + intro x hx a ha + by_contra φ + obtain ⟨ a' , ha' ⟩ := subSeqCnstrction φ + simp at ha' + apply hx + have hC : IsSeqClosed C := IsClosed.isSeqClosed hC + + apply hC + · exact ha' + · intro N hN + have main : map ((f ∘ a) ∘ a'.φ) atTop ≤ map (f ∘ a) atTop := by calc + map ((f ∘ a) ∘ a'.φ) atTop = map (f ∘ a) (map (a'.φ) atTop) := by rw [← Filter.map_compose] ; rfl + _ ≤ map (f ∘ a) atTop := by apply map_mono ; apply subsequencePreservesTop ; exact a'.hφ + apply main + exact hf.seqCont ha hN; +lemma SeqContinuous'OfStrongly {Y : Type v} [ConvergingSequences Y] (f : X → Y) (hf : SeqContinuousStrongly f) : SeqContinuous' f := by + constructor + intro α a hx + apply tendsTo𝓝 + apply hf.seqCont hx diff --git a/BonnAnalysis/ConvolutionTendsToUniformly.lean b/BonnAnalysis/ConvolutionTendsToUniformly.lean new file mode 100644 index 0000000..b5fd101 --- /dev/null +++ b/BonnAnalysis/ConvolutionTendsToUniformly.lean @@ -0,0 +1,386 @@ +import Mathlib.Topology.Sequences +import Mathlib.Topology.Defs.Filter +import Mathlib.Topology.Order +import Mathlib.Topology.Algebra.ContinuousAffineMap +import Mathlib.Order.Filter.Basic +import Mathlib.Init.Function +import BonnAnalysis.ConvergingSequences +import Mathlib.Geometry.Manifold.Instances.Real +import Mathlib.Topology.UniformSpace.UniformConvergence +import Mathlib.Data.Set.Pointwise.Basic +import BonnAnalysis.UniformConvergenceSequences +import BonnAnalysis.Distributions +import BonnAnalysis.DistributionsOfVEndo +import Mathlib + +import Mathlib.Analysis.Convolution +--import Mathlib.Analysis.InnerProductSpace +-- import Mathlib.Order +-- noncomputable section +--open FourierTransform MeasureTheory Real + + +namespace MeasureTheory +open MeasureTheory +open scoped Pointwise +universe v w u u' v' -- u' is assumed to be ≤ u +open Order Set + +open scoped Classical +open NNReal Topology +open Filter + +open scoped Topology +open TopologicalSpace +noncomputable section +open Function +open Convolution + +variable {V : Type u} + [MeasureSpace V] + [NormedAddCommGroup V] [NormedSpace ℝ V] --[ProperSpace V] + [MeasureTheory.Measure.IsAddHaarMeasure (volume : Measure V)] [BorelSpace V] {Ω : Opens V} [T2Space V] [SecondCountableTopology V] [LocallyCompactSpace V] + [BorelSpace V] + {k' : Type u'} [NormedAddCommGroup k'] [NormedSpace ℝ k'] + {L : ℝ →L[ℝ ] k' →L[ℝ] k'} + {φ : 𝓓F ℝ V}-- {ψ0 : V → k'} {ψ0' : V → k'} + +lemma TendstoUniformly_iff_uniformZeroSeq.{l} {k : Type l} [UniformSpace k] [AddGroup k] [UniformAddGroup k] {φ : ℕ → V → k} {φ₀ : V → k} : TendstoUniformly φ φ₀ atTop ↔ TendstoUniformly (fun n => φ n - φ₀) 0 atTop := by + constructor + · intro hφ + rw [show (0 = φ₀ - φ₀) from (by simp)] + apply TendstoUniformly.sub hφ + rw [← tendstoUniformlyOn_univ] + apply CnstSeqTendstoUniformlyOn + · intro hφ + rw [show (φ = (fun n => φ n - φ₀ + φ₀)) from (by simp)] + -- rw [show (φ₀ = 0 + φ₀) from (by simp)] + have : TendstoUniformly (fun n ↦ (φ n - φ₀) + φ₀) ( 0 + φ₀) atTop := by + apply TendstoUniformly.add hφ ; + · rw [← tendstoUniformlyOn_univ] + apply CnstSeqTendstoUniformlyOn φ₀ atTop ; + rw [show 0 + φ₀ = φ₀ from (by simp)] at this + exact this + +lemma convolutionWithConstFunc {φ : V → ℝ} (c : ℝ) : (φ ⋆ (fun _ => c)) = fun _ => (∫ v , φ v) * c := by + unfold convolution + ext x + symm ; + trans (∫ (v : V), c* (φ v) ) + · symm ; rw [mul_comm] ; exact (integral_smul c φ) + · simp only [smul_eq_mul, ContinuousLinearMap.lsmul_apply] ; simp_rw [mul_comm] ; + +lemma zeroSeqUniformly {a : ℕ → (V → k')} {α : ℕ → V → ENNReal} {C : ℝ≥0} + (ha : ∀ n x , ‖ a n x‖ ≤ (α n x).toReal * C ) + (hα : TendstoUniformly (fun n x => (α n x).toReal) 0 atTop) : TendstoUniformly a 0 atTop := by + + rw [ TendstoUniformly_iff_uniformZeroSeq] + rw [Metric.tendstoUniformly_iff] at hα + simp_rw [ eventually_atTop ] at hα + simp_rw [ ← tendstoUniformlyOn_univ , SeminormedAddGroup.tendstoUniformlyOn_zero, eventually_atTop ] + intro ε hε + + by_cases h : C = 0 + · use 0 ; intro b _ ; + intro x _ + apply LE.le.trans_lt + · simp ; exact ha b x + · have : ‖(α b x).toReal‖ * C < ε := by + rw [h] ; + simp + exact hε + rw [show ‖(α b x).toReal‖ = (α b x).toReal from NNReal.norm_eq _] at this + exact this + · let ε' : ℝ := ε / C + -- have hε' : ε' > 0 ∧ + have hC : 0 < C := pos_iff_ne_zero.mpr h + obtain ⟨ m , hm ⟩ := hα ε' (by apply (div_pos_iff_of_pos_right ?_).mpr ; exact hε ; exact hC ) + use m + + intro b hb x _ + specialize hm b hb x + apply LE.le.trans_lt + · simp ; exact ha b x + · rw [show (ε = ε' * C ) from ?_] + · apply (mul_lt_mul_right ?_ ).mpr + simp only [Pi.zero_apply, dist_zero_left, Real.norm_eq_abs, ENNReal.abs_toReal] at hm + exact hm + exact hC + · refine Eq.symm (IsUnit.div_mul_cancel ?q _) + exact (Ne.isUnit (coe_ne_zero.mpr h)) +lemma EssSupNormSub {φ : ℕ → V → k'} {φ₀ : V → k' } (hφ : TendstoUniformly φ φ₀ atTop) : + ∀ ε > 0 , ∃ a, ∀ n ≥ a, || fun x => (φ n) x - φ₀ x ||_∞.toReal < ε := by + have : ∀ ε > 0 , ∃ a, ∀ n ≥ a, ∀ x ∈ univ , ‖((φ n) - φ₀) x‖ < ε := by + simp_rw [← eventually_atTop ] + + + have : TendstoUniformly (fun n => (φ n) - φ₀) 0 atTop := by apply TendstoUniformly_iff_uniformZeroSeq.mp hφ + + apply SeminormedAddGroup.tendstoUniformlyOn_zero.mp (tendstoUniformlyOn_univ.mpr this) + intro ε hε + obtain ⟨ a , ha ⟩ := this (ε / 2) (half_pos hε ) -- hε + use a + intro n hn + have foo {ε} {ψ : V → k'} (hε : ε ≥ 0) (p : ∀ x ∈ univ , ‖ ψ x‖ < ε) : || ψ ||_∞.toReal ≤ ε := by + have : || ψ ||_∞ ≤ ENNReal.ofReal ε := by + apply MeasureTheory.snormEssSup_le_of_ae_bound (C:=ε) + apply ae_of_all volume + intro a + apply le_of_lt + exact p a trivial + refine ENNReal.toReal_le_of_le_ofReal hε this + apply LE.le.trans_lt + · exact foo (ε := ε / 2) (ψ := fun x => (φ n x) - φ₀ x) (le_of_lt (half_pos hε)) (ha n hn) + · exact div_two_lt_of_pos hε + +-------------------------------------------------------- + + +@[continuity] lemma ContCompactSupp.continuous (ψ0 : ContCompactSupp ℝ V k' ) : Continuous ψ0 := by apply ContDiff.continuous (𝕜:=ℝ ) ; exact ψ0.smooth + +lemma convOfCtsCmpctSupportExists {φ : LocallyIntegrableFunction V} (ψ : ContCompactSupp ℝ V k') : ConvolutionExists φ.f ψ L := by + intro x ; + apply HasCompactSupport.convolutionExists_right -- HasCompactSupport.convolutionExistsAt + exact ψ.hsupp -- --HasCompactSupport.convolution φ.fHasCmpctSupport + exact φ.hf -- exact testFunctionIsLocallyIntegrable V φ + exact ψ.continuous + + + +lemma norm_convolution_le {x} {φ : 𝓓F ℝ V} (ψ0 : ContCompactSupp ℝ V k' ) : ‖ (φ ⋆[L] ψ0) x‖ ≤ ‖L‖ * ( (fun x => ‖ φ x‖) ⋆ (fun x => ‖ ψ0 x‖) ) x := by + unfold convolution + have {x y : V} : ‖ L (φ x) (ψ0 y)‖ ≤ ‖L‖ * ‖ φ x‖ * ‖ ψ0 y‖ := by + trans ‖ L (φ x)‖ * ‖ ψ0 y‖ + · apply ContinuousLinearMap.le_opNorm + · gcongr ; apply ContinuousLinearMap.le_opNorm + calc + ‖ (φ ⋆[L] ψ0) x‖ ≤ (∫⁻ (a : V), ENNReal.ofReal ‖ L (φ a) (ψ0 (x - a))‖).toReal := by apply MeasureTheory.norm_integral_le_lintegral_norm + _ ≤ (∫⁻ (t : V), ENNReal.ofReal (‖L‖ * ‖φ t‖ * ‖ψ0 (x-t)‖)).toReal := ?_ -- simp_rw [norm_mul] + _ = ∫ (t : V), ‖L‖ • (‖φ t‖ * ‖ψ0 (x-t)‖) := ?_ + _ = ‖L‖ • ∫ (t : V), ‖φ t‖ * ‖ψ0 (x-t)‖ := by apply integral_smul + --∫ (t : V), ‖φ t‖ * ‖ψ0 (x-t)‖ = ∫ (t : V), ((ContinuousLinearMap.lsmul ℝ ℝ) ((fun x ↦ ‖φ x‖) t)) ((fun x ↦ ‖ψ0 x‖) (x - t)) := by rfl + · gcongr ; + · rw [← lt_top_iff_ne_top] ; + apply MeasureTheory.Integrable.lintegral_lt_top + + apply Continuous.integrable_of_hasCompactSupport + have : Continuous φ.f := φ.continuous + have : Continuous ψ0.f := ψ0.continuous + continuity + apply HasCompactSupport.mul_right --(f:= fun _ => ‖L‖ ) + apply HasCompactSupport.mul_left + apply HasCompactSupport.norm + exact φ.hsupp + + + + + · exact this + · rw [← MeasureTheory.integral_toReal] + · congr ; ext a ; simp only [smul_eq_mul] ; + rw [mul_assoc , ENNReal.toReal_ofReal_eq_iff] ; + apply mul_nonneg ; + · apply ContinuousLinearMap.opNorm_nonneg + · apply mul_nonneg ; + · apply norm_nonneg + · apply norm_nonneg -- exact norm_nonneg _ + · apply AEMeasurable.ennreal_ofReal ; -- I DONT KNOW HOW TO FIX THIS, because k' is not a measurable space in general (we want things like V →L[ℝ] ℝ) -- apply AEMeasurable.norm ; apply AEMeasurable.mul ; + · + apply AEMeasurable.mul + · apply AEMeasurable.mul ; + · measurability ; + · + apply AEMeasurable.norm + apply Continuous.aemeasurable + apply ContDiff.continuous (𝕜:=ℝ ) (φ.smooth) ; + + + + + · apply Continuous.aemeasurable + apply Continuous.norm + + continuity + + + · apply ae_of_all + intro _ + exact ENNReal.ofReal_lt_top + + + +open ContinuousLinearMap +variable {G : Type* } {x : G} [MeasureSpace G] {μ : Measure G} + [AddGroup G] [ MeasurableAdd₂ G] [ SigmaFinite μ] [ MeasurableNeg G] [ μ.IsAddLeftInvariant] + + + +theorem convolution_mono_right_ae {f g g' : G → ℝ} (hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ) + (hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ) (hf : ∀ x, 0 ≤ f x) (hg : ∀ᵐ (x : G) ∂μ, g x ≤ g' x) : + (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x := by + apply integral_mono_ae hfg hfg' + simp only [lsmul_apply, Algebra.id.smul_eq_mul] + unfold EventuallyLE + + have hg : {t | g (x - t) ≤ g' (x-t)} ∈ ae μ := by + have : {t | g (x - t) ≤ g' (x-t)} = (fun t => x - t) ⁻¹' {t | g t ≤ g' t} := by rfl -- ext t ; simp ; constructor ; intro h ; use x - t; exact ⟨ h , simp ⟩ ; intro h ; obtain ⟨ x' , hx' ⟩ := h ; rw [show x = x' + t from ?_] ; exact hx'.1 + rw [this] + rw [ae_iff] at hg + rw [mem_ae_iff ,← Set.preimage_compl] + apply MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null + apply MeasureTheory.quasiMeasurePreserving_sub_left + exact hg + + + + have {x t} : g (x - t) ≤ g' (x-t) → f t * g (x - t) ≤ f t * g' (x-t) := by + intro h + apply mul_le_mul_of_nonneg_left h (hf _) + rw [Filter.eventually_iff] + + -- have hg : {x | g (x - t) ≤ g' (x-t)} ∈ ae μ + + apply sets_of_superset + · + exact hg + · intro t ht ; apply this ht + -- simp_rw [ ] + + -- intro t +lemma convolution_mono_right_of_nonneg_ae {f g g' : G → ℝ} (hfg' : ConvolutionExistsAt f g' x (ContinuousLinearMap.lsmul ℝ ℝ) μ) + (hf : ∀ (x : G), 0 ≤ f x) (hg : ∀ᵐ (x : G) ∂ μ, g x ≤ g' x) (hg' : ∀ (x : G), 0 ≤ g' x) : + (f ⋆[ContinuousLinearMap.lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[ContinuousLinearMap.lsmul ℝ ℝ, μ] g') x := + by + by_cases H : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ + · exact convolution_mono_right_ae H hfg' hf hg + have : (f ⋆[lsmul ℝ ℝ, μ] g) x = 0 := integral_undef H + rw [this] + exact integral_nonneg fun y => mul_nonneg (hf y) (hg' (x - y)) +variable {ψ : ℕ → ContCompactSupp ℝ V k'} {ψ0 : ContCompactSupp ℝ V k'} (hψ : ψ ⟶ ψ0) --TendstoUniformly (fun n => (ψ n)) ψ0 atTop) (KhK : ∃ K : Set V , IsCompact K ∧ ∀ n , tsupport (ψ n) ⊆ K) + +lemma ConvWithIsUniformContinuous + : + TendstoUniformly (β := k') (fun n => (φ.f ⋆[L] (ψ n))) ((φ.f ⋆[L] ψ0)) atTop := by + apply TendstoUniformly_iff_uniformZeroSeq.mpr + --exact UniformContinuous.comp_tendstoUniformly (g:= fun ψ => φ.f ⋆ ψ) ?_ ?_ + rw [show (fun n ↦ φ.f ⋆[L] ψ n - φ.f ⋆[L] ψ0) = fun n ↦ φ.f ⋆[L] (ψ n - ψ0) from ?_] ; swap + · ext1 n ; + rw [show (ψ n - ψ0).f = ((ψ n).f + (((-1 : ℝ) • ψ0).f)) from ?_] + ext x + + rw [ConvolutionExistsAt.distrib_add, sub_eq_add_neg] + simp only [Pi.add_apply, Pi.neg_apply, add_right_inj] + apply congrFun (a:=x) + trans (-1 : ℝ) • (φ.f ⋆[L] ψ0); swap + · symm ; exact convolution_smul + · ext x ; simp only [Pi.smul_apply, smul_eq_mul, neg_mul, one_mul, neg_smul, one_smul] + · apply convOfCtsCmpctSupportExists (φ := (φ : LocallyIntegrableFunction V)) + · apply convOfCtsCmpctSupportExists (φ := (φ : LocallyIntegrableFunction V)) + · simp only [instAddCommGroupContCompactSupp, instNegContCompactSupp, + instSMulContCompactSupp] ; ext x ; simp only [Pi.sub_apply, Pi.add_apply, Pi.neg_apply] ; simp ; apply sub_eq_add_neg (a := (ψ n) x) (b:= ψ0 x) + · let C : ℝ≥0 := ⟨ ‖L‖ * ∫ v , ‖ φ v‖ , by apply mul_nonneg ; apply ContinuousLinearMap.opNorm_nonneg ; apply integral_nonneg ; intro _ ; apply norm_nonneg ⟩ + have : ∀ n x , ‖ (φ.f ⋆[L] (ψ n - ψ0)) x‖ ≤ || ψ n - ψ0 ||_∞.toReal * C.1 := by + intro n x + + calc + ‖ (φ.f ⋆[L] (ψ n - ψ0)) x‖ ≤ ‖L‖ * ((fun x => ‖φ.f x‖) ⋆ (fun x => ‖ (ψ n - ψ0) x‖ )) x := norm_convolution_le (φ := φ) (ψ0 := ψ n - ψ0) + _ ≤ ‖L‖ * ((fun x => ‖φ.f x‖) ⋆ (fun _ => || ψ n - ψ0 ||_∞.toReal )) x := ?_ + _ = ‖L‖ * ((∫ v , ‖ φ v‖) * || ψ n - ψ0 ||_∞.toReal) := by apply congrArg ; apply congrFun ; apply convolutionWithConstFunc + _ ≤ || ψ n - ψ0 ||_∞.toReal * (‖L‖ * ∫ v , ‖ φ v‖) := by rw [← mul_assoc , mul_comm] + + gcongr + apply convolution_mono_right_of_nonneg_ae + · apply HasCompactSupport.convolutionExists_left_of_continuous_right ; + · refine (hasCompactSupport_comp_left (g:= fun x => ‖x‖) (f:= φ.f) ?_).mpr ?_ ; + · intro _ ; exact norm_eq_zero ; + · exact φ.hsupp + · rw [← MeasureTheory.locallyIntegrableOn_univ] ; apply MeasureTheory.LocallyIntegrableOn.norm ; rw [MeasureTheory.locallyIntegrableOn_univ] ; apply testFunctionIsLocallyIntegrable -- apply testFunctionIsLocallyIntegrable + · apply continuous_const ; + · intro x ; apply norm_nonneg ; + · have {x} : ‖(ψ n - ψ0) x‖ ≤ || ψ n - ψ0 ||_∞.toReal ↔ ENNReal.ofReal ‖(ψ n - ψ0) x‖ ≤ || ψ n - ψ0 ||_∞ := by + symm + apply ENNReal.ofReal_le_iff_le_toReal + rw [← lt_top_iff_ne_top] + apply EssSupTestFunction + simp_rw [this] + simp_rw [ofReal_norm_eq_coe_nnnorm] + apply ae_le_snormEssSup (f:=(ψ n - ψ0)) + · intro _ ; apply ENNReal.toReal_nonneg + apply zeroSeqUniformly this + rw [← tendstoUniformlyOn_univ] + apply Filter.Tendsto.tendstoUniformlyOn_const + apply NormedAddCommGroup.tendsto_nhds_zero.mpr + have {x : ENNReal} : ‖x.toReal‖ = x.toReal := NNReal.norm_eq _ + simp_rw [ eventually_atTop , this, ccs_sub] + apply EssSupNormSub (φ := fun n => (ψ n).f) (φ₀:= ψ0.f) + apply (zeroCase _ ).mp (hψ.2 0) + +lemma fderiv_convolution (ψ0 : ContCompactSupp ℝ V k') {φ : LocallyIntegrableFunction V} : + fderiv ℝ (φ.f ⋆[L] ψ0) = φ.f ⋆[ContinuousLinearMap.precompR V L] (fderiv ℝ ψ0) := by + ext1 x + apply HasFDerivAt.fderiv + apply HasCompactSupport.hasFDerivAt_convolution_right ; + exact ψ0.hsupp + exact φ.hf + + exact ContDiff.of_le (𝕜 := ℝ) (f:= ψ0) ψ0.smooth (OrderTop.le_top 1) + + +open ContinuousMultilinearMap + +variable +{k' : Type u} [NormedAddCommGroup k'] [NormedSpace ℝ k'] + {V : Type u} + [MeasureSpace V] + [NormedAddCommGroup V] [NormedSpace ℝ V] --[ProperSpace V] + [MeasureTheory.Measure.IsAddHaarMeasure (volume : Measure V)] [BorelSpace V] [T2Space V] [SecondCountableTopology V] [LocallyCompactSpace V] + [BorelSpace V] + + {L : ℝ →L[ℝ ] k' →L[ℝ] k'} + {φ : 𝓓F ℝ V} {ψ : ℕ → ContCompactSupp ℝ V k'} (ψ0 : ContCompactSupp ℝ V k' ) + (hψ : ψ ⟶ ψ0) + +-- def T : Type max 1 u u' := V →L[ℝ] k' +--#check : Type max 1 u u' +theorem iteratedDerivConv + {φ : 𝓓F ℝ V} {l : ℕ} + : + TendstoUniformly (fun n => iteratedFDeriv ℝ (l) (φ.f ⋆[L] (ψ n))) (iteratedFDeriv ℝ (l) (φ.f ⋆[L] ψ0)) atTop := by + + + induction' l with l hl generalizing k' ψ ψ0 hψ L + · apply (zeroCase _).mpr ; apply ConvWithIsUniformContinuous hψ + · have {ψ0} : iteratedFDeriv ℝ (l+1) (φ.f ⋆[L] (ψ0)) = + fun z => (iteratedFDeriv ℝ (l) (fderiv ℝ (φ.f ⋆[L] (ψ0))) z).uncurryRight := by ext1 z ; exact iteratedFDeriv_succ_eq_comp_right + + have {ψ0 : ContCompactSupp ℝ V k'} : iteratedFDeriv ℝ (l+1) (φ.f ⋆[L] (ψ0.f)) = + fun z => (iteratedFDeriv ℝ (l) (φ ⋆[ContinuousLinearMap.precompR V L] (fderivCCS ψ0).f) z).uncurryRight := by + rw [this] ; + simp_rw [fderiv_convolution (φ := (φ : LocallyIntegrableFunction V)) (ψ0 := ψ0)] ; + + rfl + -- have _ : := ⟨ hψ0 , + -- by apply ContCompactLimit (ψ := ψ) hψ KhK ⟩ + simp_rw [this ] + + have moin : TendstoUniformly + (fun n ↦ (iteratedFDeriv ℝ l (φ.f ⋆[ContinuousLinearMap.precompR V L, volume] fderiv ℝ (ψ n)))) + (iteratedFDeriv ℝ l (φ.f ⋆[ContinuousLinearMap.precompR V L, volume] ( fderivCCS ψ0 ).f)) atTop := by + apply hl (k' := (V →L[ℝ] k' )) (ψ := fun n => fderivCCS (ψ n)) (L := ContinuousLinearMap.precompR V L) + · apply SeqContinuousStronglyFderivCCS.seqCont + exact hψ + + + refine UniformContinuous.comp_tendstoUniformly (g:= (continuousMultilinearCurryRightEquiv' ℝ l V k')) ?_ moin + exact Isometry.uniformContinuous (continuousMultilinearCurryRightEquiv' ℝ l V k').isometry + +-- variable (ψ : V → k') +-- def ContCompactLimit : HasCompactSupport ψ := by + +-- obtain ⟨ K , hK ⟩ := hψ.1 +-- apply IsCompact.of_isClosed_subset ; +-- · exact hK.1 +-- · exact isClosed_tsupport ψ0 +-- · apply KcontainsSuppOfLimit' +-- intro p +-- refine TendstoUniformly.tendsto_at ((zeroCase _ ).mp (hψ.2 0)) hK diff --git a/BonnAnalysis/Distributions.lean b/BonnAnalysis/Distributions.lean new file mode 100644 index 0000000..75cf514 --- /dev/null +++ b/BonnAnalysis/Distributions.lean @@ -0,0 +1,338 @@ +import Mathlib.Topology.Sequences +import Mathlib.Topology.Defs.Filter +import Mathlib.Topology.Order +import Mathlib.Order.Filter.Basic +import BonnAnalysis.ConvergingSequences +import Mathlib.Geometry.Manifold.Instances.Real +import Mathlib.Topology.UniformSpace.UniformConvergence + +import BonnAnalysis.UniformConvergenceSequences +import Mathlib +--import Mathlib.Analysis.InnerProductSpace +-- import Mathlib.Order +-- noncomputable section +--open FourierTransform MeasureTheory Real + +-- set_option profiler true +namespace MeasureTheory +open MeasureTheory +universe u v u' +open Order Set Filter +open Filter +open scoped Classical +open NNReal Topology + + +open scoped Topology +open TopologicalSpace +noncomputable section + +variable + (k : Type v) [NontriviallyNormedField k] --{ΩisOpen : IsOpen Ω} + (V : Type u) [NormedAddCommGroup V] [NormedSpace k V] +/- +structure HasCompactSupportIn (φ : V → k) : Prop where + hasCmpctSprt : HasCompactSupport φ + sprtinΩ : tsupport φ ⊆ Ω + -/ +--Set.EqOn +variable (k' : Type u') [NormedAddCommGroup k'] [NormedSpace k k'] -- [MulZeroClass k'] +@[ext] structure ContCompactSupp where + f : V → k' + smooth : ContDiff k ⊤ f + hsupp : HasCompactSupport f +instance : CoeFun (ContCompactSupp k V k') (fun _ => V → k') where + coe σ := σ.f +@[simp] instance : Zero (ContCompactSupp k V k' ) where + zero := ⟨ + 0 , + by apply contDiff_const , + by rw [hasCompactSupport_def, Function.support_zero' , closure_empty] ; exact isCompact_empty ⟩ +@[simp] instance : Add (ContCompactSupp k V k' ) where + add := fun φ ψ => + ⟨φ.f + ψ.f , + ContDiff.add φ.smooth ψ.smooth, + HasCompactSupport.add φ.hsupp ψ.hsupp ⟩ +lemma neg_tsupport {φ : ContCompactSupp k V k'} : tsupport (-φ.f) = tsupport (φ.f) := by + unfold tsupport ; apply congrArg ; apply Function.support_neg +@[simp] instance : Neg (ContCompactSupp k V k' ) where + neg := fun φ => ⟨ -φ.f , + ContDiff.neg φ.smooth , by + unfold HasCompactSupport ; rw [neg_tsupport] ; exact φ.hsupp ; ⟩ +@[simp] instance : AddCommGroup (ContCompactSupp k V k' ) where + add_assoc := fun φ ψ τ => by ext x ; apply add_assoc + zero_add := fun φ => by ext x ; apply zero_add + add_zero := fun φ => by ext x ; apply add_zero + nsmul := nsmulRec + add_comm := fun φ ψ => by ext x ; apply add_comm + + zsmul := zsmulRec + add_left_neg := fun φ => by ext x;apply add_left_neg +@[simp] instance : SMul k (ContCompactSupp k V k' ) where + smul := fun l φ => ⟨ fun x => l • φ.f x , + ContDiff.smul contDiff_const φ.smooth , + + HasCompactSupport.smul_left φ.hsupp ⟩ +@[simp] lemma ccs_add {φ ψ : ContCompactSupp k V k'} : (φ + ψ).f = φ.f + ψ.f := by + rfl +@[simp] lemma ccs_sub {φ ψ : ContCompactSupp k V k'} : (φ - ψ).f = φ.f - ψ.f := by + rw [sub_eq_add_neg , show φ.f - ψ.f = φ.f + (-ψ).f from ?_] ; + rfl + simp only [instNegContCompactSupp] + rw [sub_eq_add_neg] +instance : Module k (ContCompactSupp k V k') where + + one_smul := fun φ => by ext x ; exact one_smul k (φ x) + mul_smul := fun l l' φ => by ext x ; exact mul_smul l l' (φ x) + smul_zero := fun a => by ext ; exact smul_zero a + smul_add := fun a φ φ' => by ext x; exact smul_add a (φ x) (φ' x) + add_smul := fun a b φ => by ext x; exact add_smul a b (φ x) + zero_smul := fun φ => by ext x; exact zero_smul k (φ x) +------- +variable + --{ΩisOpen : IsOpen Ω} + {V : Type u} [NormedAddCommGroup V] [NormedSpace k V] (Ω : Opens V) +@[ext] structure 𝓓 where + + φ : ContCompactSupp k V k + + sprtinΩ : tsupport φ ⊆ Ω + +instance : CoeFun (𝓓 k Ω) (fun _ => V → k) where + coe σ := σ.φ.f +------- Historical reasons +variable {V : Type u} [NormedAddCommGroup V] [NormedSpace k V] {Ω : Opens V} {φ : 𝓓 k Ω} +lemma 𝓓.φIsSmooth : ContDiff k ⊤ φ.φ := φ.φ.smooth --⊤ φ +lemma 𝓓.φHasCmpctSupport : HasCompactSupport φ.φ := φ.φ.hsupp + +instance : ConvergingSequences (ContCompactSupp k V k') where + seq := fun (a , x) => + (∃ K : Set V , IsCompact K ∧ ∀ n , tsupport (a n).f ⊆ K) ∧ + ∀ l : ℕ , TendstoUniformly + (fun n => iteratedFDeriv k l (a n).f) + (iteratedFDeriv k l x.f) atTop + seq_cnst := fun x => by + let A : Set (V ) := @tsupport _ _ ⟨ 0 ⟩ _ x.f --- weird + constructor + · use A + constructor + · exact x.hsupp + · intro n + exact subset_rfl + · intro l + rw [← tendstoUniformlyOn_univ ] + + apply CnstSeqTendstoUniformlyOn + seq_sub := fun {a} {x} p a' => by + obtain ⟨⟨ K , ⟨ hK1 , hK2 ⟩ ⟩ , conv ⟩ := p + constructor + · use K + constructor + · exact hK1 + · intro n + apply hK2 + · intro l + --let da' : SubSequence (fun n => iteratedFDeriv k l (a n)) := + rw [← tendstoUniformlyOn_univ ] + exact SubSeqConvergesUniformly ( tendstoUniformlyOn_univ.mpr (conv l)) ⟨ a'.φ , a'.hφ ⟩ + + +---------- +variable {V : Type u} [NormedAddCommGroup V] [NormedSpace k V] (Ω : Opens V) +@[simp] instance : Zero (𝓓 k Ω ) where + zero := ⟨ + ⟨0 , + by apply contDiff_const , + by rw [hasCompactSupport_def, Function.support_zero' , closure_empty] ; exact isCompact_empty ⟩, + by unfold tsupport ; rw [show Function.support 0 = ∅ from Function.support_zero] ; rw [closure_empty] ; apply empty_subset ⟩ +@[simp] instance : Add (𝓓 k Ω ) where + add := fun φ ψ => + ⟨φ.φ + ψ.φ + , by + trans (tsupport (φ.φ) ∪ tsupport ψ.φ) ; + apply closure_minimal + · trans + · apply Function.support_add ; + · apply Set.union_subset_union + · trans ; exact subset_tsupport _ ; exact fun _ a ↦ a + · trans ; exact subset_tsupport _ ; exact fun _ => id + · apply IsClosed.union ; apply isClosed_tsupport ; apply isClosed_tsupport + · apply union_subset_iff.mpr ; constructor + · exact φ.sprtinΩ + · exact ψ.sprtinΩ ⟩ +@[simp] instance : Neg (𝓓 k Ω ) where + neg := fun φ => ⟨ - φ.φ , by rw [show tsupport (-φ.φ).f = tsupport φ.φ.f from neg_tsupport (φ := φ.φ)] ; exact φ.sprtinΩ ⟩ +@[simp] instance : AddCommGroup (𝓓 k Ω ) where + add_assoc := fun φ ψ τ => by ext x ; apply add_assoc + zero_add := fun φ => by ext x ; apply zero_add + add_zero := fun φ => by ext x ; apply add_zero + nsmul := nsmulRec + add_comm := fun φ ψ => by ext x ; apply add_comm + + zsmul := zsmulRec + add_left_neg := fun φ => by ext x;apply add_left_neg + --'neg', 'zsmul', 'add_left_neg' +@[simp] instance : SMul k (𝓓 k Ω ) where + smul := fun l φ => ⟨ l • φ.φ , + by + trans ; + · exact tsupport_smul_subset_right (fun _=> l) (φ.φ) ; + · exact φ.sprtinΩ ⟩ +instance : Module k (𝓓 k Ω) where + + one_smul := fun φ => by ext x ; exact one_smul k (φ x) + mul_smul := fun l l' φ => by ext x ; exact mul_smul l l' (φ x) + smul_zero := fun a => by ext ; exact smul_zero a + smul_add := fun a φ φ' => by ext x; exact smul_add a (φ x) (φ' x) + add_smul := fun a b φ => by ext x; exact add_smul a b (φ x) + zero_smul := fun φ => by ext x; exact zero_smul k (φ x) +-- theorem tendsto_const_nhds {α : Type u} {β : Type v} [TopologicalSpace α] {a : α} {f : Filter β} : +-- Filter.Tendsto (fun x => a) f (nhds a) +open Uniformity +universe w x +instance : ConvergingSequences (𝓓 k Ω) where + seq := fun (a , x) => (fun n=> (a n).φ) ⟶ x.φ + + seq_sub := fun {a} {x} p a' => ConvergingSequences.seq_sub p ⟨ a'.φ , a'.hφ ⟩ + seq_cnst := fun p => ConvergingSequences.seq_cnst p.φ + +def 𝓓' := (𝓓 k Ω ) →L[k] k + +instance : CoeFun (𝓓' k Ω ) (fun _ => (𝓓 k Ω) → k ) where + coe σ := σ.toFun +instance : ConvergingSequences (𝓓' k Ω ) where + seq := fun AT => ∀ φ : 𝓓 k Ω , Tendsto (fun n => (AT.1 n) φ ) atTop (𝓝 (AT.2 φ)) + seq_cnst := fun T φ => by apply tendsto_const_nhds + seq_sub := fun hAT A' φ => subSeqConverges (hAT φ) ⟨ _ , A'.hφ ⟩ +lemma diffAt (φ : ContCompactSupp k V k') {x : V} : DifferentiableAt k φ x := by + have := ContDiff.differentiable φ.smooth (OrderTop.le_top 1) + apply Differentiable.differentiableAt this + + + +lemma zeroCase {k' : Type u'} [NormedAddCommGroup k'] [NormedSpace k k'] {φ : ℕ → (V → k')} {φ0 : V → k'} : + (TendstoUniformly (fun n ↦ iteratedFDeriv k 0 (φ n)) (iteratedFDeriv k 0 φ0) atTop) ↔ + TendstoUniformly (fun n => (φ n) ) (φ0) atTop := by + + rw [iteratedFDeriv_zero_eq_comp] + have myrw : (fun n ↦ iteratedFDeriv k 0 (φ n)) = fun n ↦ (⇑(continuousMultilinearCurryFin0 k V k').symm ∘ (φ n)) := by + ext1 n + rw [iteratedFDeriv_zero_eq_comp] + rw [myrw] + constructor + · apply UniformContinuous.comp_tendstoUniformly (g:=⇑(continuousMultilinearCurryFin0 k V k')) ?_ + apply Isometry.uniformContinuous + apply LinearIsometryEquiv.isometry + · apply UniformContinuous.comp_tendstoUniformly (g:=⇑(continuousMultilinearCurryFin0 k V k').symm) ?_ + apply Isometry.uniformContinuous + apply LinearIsometryEquiv.isometry +lemma seqImpliesConvergence {φ : ℕ → (𝓓 k Ω )} {φ0 : 𝓓 k Ω} (hφ : φ ⟶ φ0) {x : V} : + Tendsto (fun n => (φ n).φ x) atTop (𝓝 (φ0 x)):= by + apply TendstoUniformly.tendsto_at ; + apply (zeroCase k).mp + exact hφ.2 0 + + +lemma KcontainsSuppOfLimit' {k : Type* } [TopologicalSpace k] [T2Space k] [Zero k] {α : ℕ → V → k} {φ : V → k } (hφ : ∀ p , Tendsto (fun n => α n p) atTop (𝓝 (φ p)) ) + {K : Set V} (hK : IsCompact K ∧ (∀ n , tsupport (α n) ⊆ K)) : tsupport φ ⊆ K :=by + + · apply closure_minimal ; swap + · exact IsCompact.isClosed hK.1 + · apply Set.compl_subset_compl.mp + intro p hp + simp + + apply tendsto_nhds_unique (f:= fun n => (α n) p) (l:=atTop) + + exact hφ _ + have : (fun n => (α n) p) = (fun n => 0) := by + ext1 n ; + have : Function.support (α n) ⊆ K := by + trans tsupport (α n) ; + exact subset_tsupport (α n) ; + exact hK.2 n + exact Function.nmem_support.mp (Set.compl_subset_compl.mpr this hp) + rw [this] + apply tendsto_const_nhds +lemma KcontainsSuppOfLimit {α : ℕ → 𝓓 k Ω} {φ : 𝓓 k Ω } (hφ : α ⟶ φ) + {K : Set V} (hK : IsCompact K ∧ (∀ n , tsupport (α n).φ ⊆ K)) : tsupport φ.φ ⊆ K :=by + apply KcontainsSuppOfLimit' + apply seqImpliesConvergence + exact hφ + exact hK + +lemma testFunctionIsBnd (ψ : ContCompactSupp k V k') : ∃ C, ∀ (x : V), ‖ψ x‖ ≤ C := by + apply Continuous.bounded_above_of_compact_support ; apply ContDiff.continuous (𝕜:=k ) (ψ.smooth) ; + exact ψ.hsupp +notation "|| " f " ||_∞" => MeasureTheory.snormEssSup f volume + +lemma EssSupTestFunction [MeasureSpace V] (φ : ContCompactSupp k V k') : || φ.f ||_∞ < ⊤ := by + obtain ⟨ C , hC ⟩ := testFunctionIsBnd (ψ := φ) + apply MeasureTheory.snormEssSup_lt_top_of_ae_nnnorm_bound ; swap + · exact ‖ C ‖₊ + apply ae_of_all + intro x + · have : ‖φ.f x‖ ≤ ‖C‖ := by + trans + · exact hC x ; + · apply le_abs_self + exact this + + + + + + + + + + +variable (k : Type v) [NontriviallyNormedField k] + {X : Type w} [ConvergingSequences X] [AddCommMonoid X] [Module k X] + {M : Type* } [TopologicalSpace M] [AddCommGroup M] [Module k M] + +class IsSeqCtsLinearMap (f : X → M) where + isAdd : ∀ x y, f (x + y) = f x + f y -- we write this out because X might not be a normed space + isMul : ∀ (c : k) (x), f (c • x) = c • f x + isSeqCts : SeqContinuous' f +open IsSeqCtsLinearMap + +@[simp] def mk (T : X → M) (hT : IsSeqCtsLinearMap k T) : X →L[k] M := by + -- (hT2 : IsLinearMap k T) (hT : SeqContinuous' T) := by + use ⟨ ⟨ T ,hT.isAdd ⟩ , hT.isMul ⟩ + apply continuous_of_SeqContinuous hT.isSeqCts +lemma SeqContinuous'OfContinuous (T : X →L[k] M) : SeqContinuous' T := by + constructor + intro x x0 hx + apply Continuous.seqContinuous + exact T.cont + apply tendsTo𝓝 + exact hx +def Full (V : Type u) [TopologicalSpace V] : Opens V := ⟨ univ , isOpen_univ ⟩ + +abbrev 𝓓F (k : Type v) (V : Type u) [NontriviallyNormedField k] + [NormedAddCommGroup V] [NormedSpace k V] := ContCompactSupp k V k +abbrev 𝓓'F (k : Type v) (V : Type u) [NontriviallyNormedField k] + [NormedAddCommGroup V] [NormedSpace k V] := 𝓓F k V →L[k] k + + + +variable (V : Type u) [MeasureSpace V] [NormedAddCommGroup V] [NormedSpace ℝ V] [T2Space V] + [MeasureSpace V] [OpensMeasurableSpace V] {Ω : Opens V} [OpensMeasurableSpace V] [IsFiniteMeasureOnCompacts (volume (α := V))] --[IsFiniteMeasureOnCompacts (volume V)] +structure LocallyIntegrableFunction where + f : V → ℝ + hf : MeasureTheory.LocallyIntegrable f + +lemma testFunctionIsLocallyIntegrable + (φ : 𝓓F ℝ V ) : MeasureTheory.LocallyIntegrable φ := by + apply MeasureTheory.Integrable.locallyIntegrable + apply Continuous.integrable_of_hasCompactSupport + exact ContDiff.continuous (𝕜:=ℝ) φ.smooth + exact φ.hsupp +instance : Coe ( 𝓓F ℝ V) (LocallyIntegrableFunction V) where + coe φ := ⟨ φ.f , testFunctionIsLocallyIntegrable V φ ⟩ + + + +instance : CoeFun (LocallyIntegrableFunction V) (fun _ => V → ℝ) where + coe σ := σ.f diff --git a/BonnAnalysis/DistributionsExamples.lean b/BonnAnalysis/DistributionsExamples.lean new file mode 100644 index 0000000..ceeb16c --- /dev/null +++ b/BonnAnalysis/DistributionsExamples.lean @@ -0,0 +1,530 @@ +import Mathlib.Topology.Sequences +import Mathlib.Topology.Defs.Filter +import Mathlib.Topology.Order +import Mathlib.Topology.Algebra.ContinuousAffineMap +import Mathlib.Order.Filter.Basic +import Mathlib.Init.Function +import BonnAnalysis.ConvergingSequences +import Mathlib.Geometry.Manifold.Instances.Real +import Mathlib.Topology.UniformSpace.UniformConvergence +import Mathlib.Data.Set.Pointwise.Basic +import BonnAnalysis.UniformConvergenceSequences +import BonnAnalysis.Distributions +import BonnAnalysis.DistributionsOfVEndo +import BonnAnalysis.ConvolutionTendsToUniformly +import Mathlib + +import Mathlib.Analysis.Convolution +--import Mathlib.Analysis.InnerProductSpace +-- import Mathlib.Order +-- noncomputable section +--open FourierTransform MeasureTheory Real + + +namespace MeasureTheory +open MeasureTheory +open scoped Pointwise +universe u v w +open Order Set + +open scoped Classical +open NNReal Topology +open Filter + +open scoped Topology +open TopologicalSpace +noncomputable section +open Function + + +-- notation:67 ψ "ʳ" => ψʳ + + + -- + + +--rw [Metric.tendstoUniformly_iff] +---------- the rest deals with real numbers +/- +Unfortunately I have some universe issues and have to assume V lives in 0.th universe +-/ +variable (V : Type) [MeasureSpace V] [NormedAddCommGroup V] [NormedSpace ℝ V] [T2Space V] [BorelSpace V] + [MeasureSpace V] [OpensMeasurableSpace V] {Ω : Opens V} [OpensMeasurableSpace V] [IsFiniteMeasureOnCompacts (volume (α := V))] --[IsFiniteMeasureOnCompacts (volume V)] +@[simp] def intSm' (φ : V → 𝓓F ℝ V) : V → ℝ := fun y => ∫ x , φ x y + +@[simp] def intSm (φ : V → 𝓓F ℝ V) (hφ : HasCompactSupport (fun y x => φ x y)) (hcontφ : ContDiff ℝ ⊤ (intSm' V φ)) : 𝓓F ℝ V := by + use intSm' V φ + · apply IsCompact.of_isClosed_subset + · exact hφ + · apply isClosed_tsupport + apply closure_minimal + trans ; swap + · apply subset_tsupport + · rw [← Set.compl_subset_compl] + intro x hx + simp only [intSm' , mem_compl_iff, mem_support, ne_eq, Decidable.not_not] at hx + simp only [intSm' , mem_compl_iff, mem_support, ne_eq, Decidable.not_not] + rw [hx] + simp only [integral_zero'] + apply isClosed_tsupport + + + +-- ContinuousLinearMap.integral_comp_comm PROBLEM: 𝓓F ℝ V is not NormedAddGroup so we cant apply +-- probably some smoothness condition on φ is missing anyway really Ccinfty(Ω × Ω ) needed? +lemma FcommWithIntegrals (φ : V → 𝓓F ℝ V) (hφ : HasCompactSupport (fun x y => φ y x)) (T : 𝓓'F ℝ V) (hcontφ : ContDiff ℝ ⊤ (intSm' V φ)) : + T (intSm V φ hφ hcontφ) = ∫ x : V , T (φ x) := by + symm + sorry + + + + +lemma convOfTestFunctionsExists [BorelSpace V] {φ ψ : 𝓓F ℝ V} : ConvolutionExists φ.f ψ.f (ContinuousLinearMap.lsmul ℝ ℝ) := + convOfCtsCmpctSupportExists (φ := (φ : LocallyIntegrableFunction V)) (ψ := ψ) + +open MeasureSpace + +variable {V : Type} [MeasureSpace V] + [NormedAddCommGroup V] [NormedSpace ℝ V] [ProperSpace V] [MeasureTheory.Measure.IsAddHaarMeasure (volume : Measure V)] [BorelSpace V] {Ω : Opens V} [T2Space V] [SecondCountableTopology V] [LocallyCompactSpace V] + + + + + + +/- +The next lemma look similar as zeroSeqUniformly and are proven similarly. If I have time I try to generalize. +-/ +-- lemma zeroSeq' {R : Type*} [AddCommGroup R] [TopologicalSpace R] [TopologicalAddGroup R] [SeminormedAddGroup R] [Module ℝ R] +-- {a : ℕ → R} {α : ℕ → R} {C : ℝ≥0} +-- (ha : ∀ n , ‖ a n‖ ≤ C * ‖ α n‖ ) +-- (hα : ∀ ε > 0 , ∃ a, ∀ n ≥ a, ‖ α n‖ < ε) : Tendsto a atTop (𝓝 0) := by + +lemma zeroSeq {a : ℕ → ℝ} {α : ℕ → ENNReal} {C : ℝ≥0} + (ha : ∀ n , ‖ a n‖ ≤ (α n).toReal * C ) + (hα : ∀ ε > 0 , ∃ a, ∀ n ≥ a, (α n).toReal < ε) : Tendsto a atTop (𝓝 0) := by + rw [← tendsto_sub_nhds_zero_iff] + simp_rw [ NormedAddCommGroup.tendsto_nhds_zero, eventually_atTop ] + intro ε hε + + by_cases h : C = 0 + · use 0 ; intro b _ ; + apply LE.le.trans_lt + · simp ; exact ha b + · have : ‖(α b).toReal‖ * C < ε := by + rw [h] ; + simp + exact hε + rw [show ‖(α b).toReal‖ = (α b).toReal from NNReal.norm_eq _] at this + exact this + · let ε' : ℝ := ε / C + -- have hε' : ε' > 0 ∧ + have hC : 0 < C := pos_iff_ne_zero.mpr h + obtain ⟨ m , hm ⟩ := hα ε' (by apply (div_pos_iff_of_pos_right ?_).mpr ; exact hε ; exact hC ) + use m + + intro b hb + specialize hm b hb + apply LE.le.trans_lt + · simp ; exact ha b + · rw [show (ε = ε' * C ) from ?_] + · apply (mul_lt_mul_right ?_ ).mpr + + exact hm + exact hC + · refine Eq.symm (IsUnit.div_mul_cancel ?q _) + exact (Ne.isUnit (coe_ne_zero.mpr h)) + + +lemma shouldExist {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + (f : E' → E) [MeasureSpace E'] (K : Set E') (hK1 : MeasurableSet K) (hK : support f ⊆ K) + : ∫ (x : E' ) , f x = ∫ (x : E') in K , f x := by symm ; rw [← MeasureTheory.integral_indicator _] ; congr ; rw [Set.indicator_eq_self] ; exact hK ; exact hK1 + +lemma testFunctionMeasurable {φ : 𝓓 ℝ Ω} : AEStronglyMeasurable φ.φ volume := by apply Continuous.aestronglyMeasurable ; apply ContDiff.continuous (𝕜:=ℝ ) (φ.φIsSmooth) +@[simp] def Λ (f : LocallyIntegrableFunction V) : 𝓓' ℝ Ω := by + have fIsIntegrableOnK {K : Set V} (hK : IsCompact K) := LocallyIntegrable.integrableOn_isCompact f.hf hK + have fIsIntegrableOnK' {K : Set V} (hK : IsCompact K) : ∫⁻ (a : V) in K, ↑‖f.f a‖₊ ≠ ⊤ := by apply LT.lt.ne_top ; exact (fIsIntegrableOnK hK).2 + have integrable {ψ : 𝓓 ℝ Ω} : Integrable (fun v ↦ ψ v * f.f v) volume := by + let K := tsupport ψ + + have hf : ((fun v ↦ ψ v * f.f v ) = fun v => ψ v * K.indicator f.f v ) := by + have hsψ : support ψ ⊆ K := subset_tsupport ψ.φ + nth_rw 2 [← Set.indicator_eq_self.mpr hsψ] + rw [← Set.indicator_mul] + refine Eq.symm ( Set.indicator_eq_self.mpr ?_) + trans + · refine Function.support_mul_subset_left _ _ + · exact hsψ + rw [hf] + apply MeasureTheory.Integrable.bdd_mul + · have hK := ψ.φHasCmpctSupport ; + rw [MeasureTheory.integrable_indicator_iff] ; + apply fIsIntegrableOnK ; + · exact hK ; + · apply IsCompact.measurableSet ; + exact hK + · exact testFunctionMeasurable (φ := ψ) + + apply testFunctionIsBnd + + apply mk ; swap + · exact fun φ => ∫ v , φ v * f v + · constructor + · intro φ ψ ; rw [← integral_add] ; + · congr ; + ext v ; + apply add_mul ; + · apply integrable ; + · apply integrable ; + + · intro c φ ; symm ; rw [← integral_smul] ; congr ; ext v ; simp ; rw [← mul_assoc] ; congr ; + · constructor + intro φ φ₀ hφ + obtain ⟨ K , hK ⟩ := hφ.1 + + + have {a b : ℝ } : ENNReal.ofReal (‖ a‖ * ‖b‖) = ↑(‖a‖₊ * ‖b‖₊) := by + calc + ENNReal.ofReal (‖ a‖ * ‖b‖) = ENNReal.ofReal (‖ a * b‖) := by congr ; rw [← norm_mul] + _ = ↑(‖ a * b‖₊) := by exact ofReal_norm_eq_coe_nnnorm (a * b) + _ = ↑(‖a‖₊ * ‖b‖₊) := by congr ; exact nnnorm_mul a b + + have mainArg : ∀ n , + ‖ (∫ (v : V), (φ n).φ v * f.f v) - ∫ (v : V), φ₀.φ v * f.f v ‖₊ + ≤ ENNReal.toReal (|| (φ n).φ - φ₀.φ ||_∞) * ENNReal.toReal (∫⁻ (v : V) in K, ‖ (f v) ‖₊ ) := by + intro n + + have fIsMeasureable : AEMeasurable fun a ↦ ENNReal.ofNNReal ‖f.f a‖₊ := by + refine AEMeasurable.ennnorm ?hf + have : MeasureTheory.AEStronglyMeasurable f.f := by apply LocallyIntegrable.aestronglyMeasurable ; exact f.hf + measurability + + + have supportφ₀ := KcontainsSuppOfLimit ℝ Ω hφ hK + have someArg : (support fun x => ((φ n).φ - φ₀.φ) x * f.f x ) ⊆ K := by + rw [Function.support_mul ((φ n).φ - φ₀.φ) (f.f)] + trans + · exact inter_subset_left + rw [← Set.union_self K] + trans + · apply Function.support_sub + · apply Set.union_subset_union + · trans ; exact subset_tsupport _ ; exact hK.2 n + · trans ; exact subset_tsupport _ ; exact supportφ₀ + have someOtherArg : (∫⁻ (v : V) in K , ‖ ((φ n).φ -φ₀.φ) v ‖₊ * ‖ f.f v ‖₊ ).toReal ≤ + (∫⁻ (v : V) in K , || ((φ n).φ -φ₀.φ) ||_∞ * ‖ f.f v ‖₊ ).toReal := by + have : || (φ n).φ - φ₀.φ ||_∞ ≠ ⊤ := by apply LT.lt.ne_top ; apply LE.le.trans_lt ; apply MeasureTheory.snormEssSup_add_le ; apply WithTop.add_lt_top.mpr ; constructor ; exact EssSupTestFunction ℝ _ (φ n).φ; exact EssSupTestFunction _ _ (-φ₀).φ + apply ENNReal.toReal_mono ; + · apply LT.lt.ne_top ; rw [MeasureTheory.lintegral_const_mul''] ; apply WithTop.mul_lt_top ; exact this ; exact fIsIntegrableOnK' hK.1 ; apply AEMeasurable.restrict ; exact fIsMeasureable + · apply MeasureTheory.lintegral_mono_ae ; + --rw + have {a : V} (ha : ‖ ((φ n).φ -φ₀.φ) a‖₊ ≤ || ((φ n).φ -φ₀.φ) ||_∞ ) : + ↑‖((φ n).φ - φ₀.φ) a‖₊ * ↑‖f.f a‖₊ ≤ || (φ n).φ - φ₀.φ ||_∞ * ↑‖f.f a‖₊ := by + calc + _ = ENNReal.ofNNReal (‖((φ n).φ - φ₀.φ) a‖₊ * ‖f.f a‖₊ ) := by rfl + _ ≤ ENNReal.ofNNReal ( || ((φ n).φ -φ₀.φ) ||_∞.toNNReal * ‖f.f a‖₊ ) := by apply ENNReal.coe_mono ; apply mul_le_mul_right' ; refine ENNReal.toNNReal_mono ?_ ha ; exact this + _ = ( (ENNReal.ofNNReal || ((φ n).φ -φ₀.φ) ||_∞.toNNReal) * ‖f.f a‖₊ ) := by apply ENNReal.coe_mul + _ = _ := by congr; apply ENNReal.coe_toNNReal ; exact this + rw [Filter.eventually_iff] + apply sets_of_superset + · apply MeasureTheory.ae_le_snormEssSup (f:=((φ n).φ -φ₀.φ)) + · intro x hx + apply this + trans + · exact hx + · apply MeasureTheory.snormEssSup_mono_measure + apply Measure.absolutelyContinuous_of_le + trans ; swap + · apply le_of_eq + have : volume (α := V) = volume.restrict univ := Eq.symm Measure.restrict_univ + rw [this] + · apply Measure.restrict_mono + exact fun _ _ ↦ trivial + exact le_of_eq rfl + calc + ‖ (∫ (v : V), (φ n).φ v * f.f v) - ∫ (v : V), φ₀.φ v * f.f v‖ + = ‖ ∫ (v : V) , (φ n).φ v * f.f v - φ₀.φ v * f.f v‖ := by congr ; rw [← MeasureTheory.integral_sub] ; exact integrable ; exact integrable + _ = ‖ ∫ (v : V) , ((φ n).φ v -φ₀.φ v) * f.f v‖ := by congr ; ext1 v ; symm ; exact (sub_smul ((φ n).φ v) (φ₀.φ v) (f.f v) ) + _ = ‖ ∫ (v : V) in K , (((φ n).φ -φ₀.φ) * f.f) v‖ := by apply congrArg ; apply shouldExist (fun v => ((φ n).φ -φ₀.φ) v * f.f v ) K ; exact IsCompact.measurableSet hK.1 ; exact someArg + _ ≤ (∫⁻ (v : V) in K , ENNReal.ofReal ‖ (((φ n).φ -φ₀.φ) v) * f.f v‖ ).toReal := by apply MeasureTheory.norm_integral_le_lintegral_norm (((φ n).φ -φ₀.φ).f * f.f ) + _ = (∫⁻ (v : V) in K , ‖ ((φ n).φ -φ₀.φ) v ‖₊ * ‖ f.f v ‖₊ ).toReal := by congr ; ext v ; simp_rw [norm_mul] ; trans ; swap ; apply ENNReal.coe_mul ; exact this + _ ≤ (∫⁻ (v : V) in K , || ((φ n).φ -φ₀.φ) ||_∞ * ‖ f.f v ‖₊).toReal := by exact someOtherArg + _ = ((|| ((φ n).φ -φ₀.φ) ||_∞) * (∫⁻ (v : V) in K , ‖ f.f v ‖₊ )).toReal := by congr ; apply MeasureTheory.lintegral_const_mul'' (|| ((φ n).φ -φ₀.φ) ||_∞) ; apply AEMeasurable.restrict ; exact fIsMeasureable + _ = (|| ((φ n).φ -φ₀.φ) ||_∞).toReal * (∫⁻ (v : V) in K , ‖ f.f v ‖₊ ).toReal := by rw [ENNReal.toReal_mul] + + have : TendstoUniformly (fun n => (φ n).φ ) φ₀.φ atTop := by apply (zeroCase _).mp (hφ.2 0) ; + -- + + rw [← tendsto_sub_nhds_zero_iff] + exact zeroSeq mainArg (EssSupNormSub this) + + +open Convolution + +@[simp] def shift (x : V) : 𝓓F ℝ V →L[ℝ] 𝓓F ℝ V := fromEndoOfV (shift' ℝ x) (shiftIsProper ℝ x) +--lemma tsupportShift {v : V} {ψ : 𝓓F ℝ V} : tsupport (shift v ψ) ⊆ {x - v | x : tsupport ψ } := by +theorem integral_congr {f g : V → ℝ} (p : ∀ x , f x = g x) : ∫ x , f x = ∫ x , g x := by congr ; ext x ; exact p x + +@[simp] def convWith ( φ : 𝓓F ℝ V) : (𝓓F ℝ V) →L[ℝ] 𝓓F ℝ V := by + apply mk ℝ ; swap + intro ψ + use φ ⋆ ψ + --rw [← contDiffOn_univ] ; + · apply HasCompactSupport.contDiff_convolution_right + · exact ψ.hsupp + · exact (testFunctionIsLocallyIntegrable V φ) + · exact ψ.smooth + · apply HasCompactSupport.convolution + · exact φ.hsupp + · exact ψ.hsupp + + · constructor + · intro ψ₁ ψ₂ ; ext z ; simp ; apply ConvolutionExistsAt.distrib_add ; exact convOfTestFunctionsExists V z ; exact convOfTestFunctionsExists V z --help + · intro c ψ ; ext z ; simp ; exact congrFun (convolution_smul (𝕜 := ℝ ) (F:= ℝ ) (G:= V) (f:=φ.f) (g:= ψ.f) ) z + · constructor + intro ψ ψ0 hψ + apply tendsTo𝓝 + constructor + · obtain ⟨ K , hK⟩ := hψ.1 + use tsupport (φ) + K + constructor + · apply add_compact_subsets + exact φ.hsupp + exact hK.1 + + · intro n + have : tsupport (φ.f ⋆ (ψ n).f) ⊆ tsupport φ.f + tsupport (ψ n).f := by + apply tsupport_convolution_subset + exact φ.hsupp + exact (ψ n).hsupp + trans + · exact this + · apply add_subset_add_left + exact hK.2 n + + + + · intro l + induction' l with l _ -- ψ ψ0 hψ -- + · simp + apply (zeroCase _).mpr + exact ConvWithIsUniformContinuous hψ -- ((zeroCase ℝ ).mp (hψ.2 0)) + · apply iteratedDerivConv + · exact hψ + + +notation:67 φ " 𝓓⋆ " ψ => convWith φ ψ +open ContinuousLinearMap + +notation:67 T " °⋆ " φ => convWith (φʳ) ** T +example (φ : 𝓓F ℝ V ) (T : 𝓓'F ℝ V ) : ∀ ψ, (T °⋆ φ) ψ = T ( φʳ 𝓓⋆ ψ) := fun _ => rfl +lemma convAsLambda (φ ψ : 𝓓F ℝ V) : (φ 𝓓⋆ ψ) = fun x => Λ (Ω:= Full V ) (φ : LocallyIntegrableFunction V) ⟨ shift x (ψʳ) , fun _ _ => trivial⟩ := by + simp + unfold convolution + simp_rw [mul_comm] + + + ext x ; + simp only [ContinuousLinearMap.lsmul_apply, smul_eq_mul] + congr + ext v + rw [neg_add_eq_sub] + + + + +-- def smoothFuncForConv (ψ : 𝓓F ℝ V ) : (𝓓F ℝ V) := +open Measure.IsAddHaarMeasure +-- example [MeasureTheory.Measure.IsAddHaarMeasure (volume (α := V))]: Measure.IsNegInvariant (volume (α := V)) := by exact? +lemma shift_comm_fderiv {ψ : 𝓓F ℝ V} {v : V} {l : ℕ} : + iteratedFDeriv ℝ l (shift v ψ) = (iteratedFDeriv ℝ l ψ) ∘ (shift' (k := ℝ) v) := by + trans iteratedFDeriv ℝ l (ψ ∘ shift' ℝ v) + · rfl + · ext1 x ; apply ContinuousAffineMap.iteratedFDeriv_comp_right +theorem shiftIsContinuous {ζ : 𝓓F ℝ V} : Continuous (fun v => shift v ζ) := by + apply SeqContinuous.continuous + intro x x0 hx + apply tendsTo𝓝 + constructor + have : ∃ K' : Set V , IsCompact K' ∧ ∀ n , x n ∈ K' := by + have :∃ R > 0, ∀ (m n : ℕ), dist (x m) (x n) < R := by apply cauchySeq_bdd ; apply Filter.Tendsto.cauchySeq ; exact hx + obtain ⟨ r , hr⟩ := this + use Metric.closedBall (x 0) r + constructor + · exact isCompact_closedBall (x 0) r + · intro n ; simp ; apply le_of_lt ; apply hr.2 + + + obtain ⟨ K' , hK' ⟩ := this + use K' + tsupport ζ + constructor + apply add_compact_subsets ; exact hK'.1 ; exact ζ.hsupp + intro n + trans + · exact supportfromEndoOfV (Φ := shift' ℝ (x n)) ζ + · rw [show ⇑(shift' ℝ (x n)) ⁻¹' tsupport ζ.f = {x n} + tsupport ζ.f from ?_] + apply Set.add_subset_add_right + refine singleton_subset_iff.mpr ?_ + exact hK'.2 n + ext y ; + rw [Set.singleton_add] + constructor + · intro hy + simp at hy + simp + rw [neg_add_eq_sub] + exact hy + · intro hy + obtain ⟨ z , hz ⟩ := hy + simp only [shift', ContinuousAffineMap.coe_mk, AffineMap.coe_mk, mem_preimage] + rw [show y - x n = z from ?_] + exact hz.1 + rw [← hz.2] + simp only [add_sub_cancel_left] + intro l + have : (fun n ↦ iteratedFDeriv ℝ l (((fun v ↦ (shift v ζ) ) ∘ x) n).f) = + (fun n ↦ iteratedFDeriv ℝ l ζ ∘ shift' ℝ (x n)) + := by + trans (fun n ↦ iteratedFDeriv ℝ l ( shift (x n) ζ )) + · rfl + · ext1 n ; rw [shift_comm_fderiv] + rw [this] + rw [shift_comm_fderiv] + + + apply UniformContinuous.comp_tendstoUniformly + · apply HasCompactSupport.uniformContinuous_of_continuous ; + · apply HasCompactSupport.iteratedFDeriv + exact ζ.hsupp + · apply ContDiff.continuous_iteratedFDeriv ( OrderTop.le_top _) (ζ.smooth) + + · rw [Metric.tendstoUniformly_iff] + have {x_1 } {b} : dist (x_1 - x0 + x b) x_1 = ‖ (x b) - x0‖ := by + rw [dist_eq_norm] ; apply congrArg ; rw[ sub_eq_neg_add , + show -x_1 + (x_1 - x0 + x b) = (-x_1 + x_1) + (- x0 + x b) from ?_ , ← sub_eq_neg_add,← sub_eq_neg_add ] ; + trans 0 + (x b - x0) ; swap + · rw [zero_add] ; -- , add_assoc , ← add_ssoc ] ; + · congr ; exact sub_eq_zero_of_eq rfl + rw [add_assoc] + apply congrArg + rw [← add_assoc] + rw [sub_eq_add_neg x_1 x0] + simp + simp_rw [this] + have : ∀ (ε : ℝ), 0 < ε → ∃ a, ∀ (b : ℕ), a ≤ b → ‖(x b) - x0‖ < ε := by + rw [← tendsto_sub_nhds_zero_iff] at hx + simp_rw [ NormedAddCommGroup.tendsto_nhds_zero, eventually_atTop ] at hx + exact hx + intro ε hε + obtain ⟨ a , ha ⟩ := this ε hε + use a + intro b hb _ + exact ha b hb + + + + +def convolutionAsFunction (T : 𝓓'F ℝ V ) (ψ : 𝓓F ℝ V ) : LocallyIntegrableFunction V := by + let ψ'f := fun x =>T (shift x (ψʳ)) + use ψ'f + apply Continuous.locallyIntegrable ; + rw [show ψ'f = T ∘ (fun v => shift v (ψʳ)) from rfl] ; + apply Continuous.comp T.cont ; + apply shiftIsContinuous +notation T " *f " ψ => convolutionAsFunction T ψ + +theorem convolutionProp (ψ : 𝓓F ℝ V ) (T : 𝓓'F ℝ V ) {φ : 𝓓 ℝ (Full V)} : (T °⋆ ψ) φ.φ = (Λ (Ω := Full V) (T *f ψ)) φ := by + + symm + trans + have : Λ (T *f ψ) φ = ∫ x , φ x * T (shift x (ψʳ)) := by + congr ; + exact this + trans + · apply integral_congr + intro x + symm + exact T.map_smul (φ.φ x) _ + + · let biφ : V → 𝓓F ℝ V := fun x => φ x • (shift x (ψʳ)) + + have biφcalc {x y : V} := calc + biφ x y = φ x * ψ (- (y - x)) := by rfl + _ = φ x * (ψ (x-y)) := by rw [neg_sub ] + have sub_compact : IsCompact (tsupport φ.φ - tsupport ψ.f) := + sub_compact_subsets (φ.φ.hsupp) (ψ.hsupp) + have hbiφ : HasCompactSupport (fun x y => biφ y x) := by + apply IsCompact.of_isClosed_subset + exact sub_compact + apply isClosed_tsupport + have : (fun y x => biφ x y) = (fun y => φ.φ.f * (shift y ψ ) ) := by ext y x ; exact biφcalc + simp_rw [this] + apply closure_minimal ; swap + · apply IsCompact.isClosed ; exact sub_compact + · trans (support φ) - (support ψ) ; swap + · apply sub_subset_sub + · apply subset_tsupport + · apply subset_tsupport + · intro y hy + simp only [instAddCommGroup𝓓, fromEndoOfV, mk, ContinuousLinearMap.coe_mk', + LinearMap.coe_mk, AddHom.coe_mk, mem_support, ne_eq] at hy + have hy := Function.support_nonempty_iff (f:= φ.φ.f * ((shift y ψ).f)).mpr hy + obtain ⟨ x , hx ⟩ := hy + have hx1 : x ∈ support φ.φ := by apply support_mul_subset_left ; exact hx + have hx2 : x ∈ support (shift y ψ) := by apply support_mul_subset_right ; exact hx -- + constructor + constructor + exact hx1 + use x - y + constructor + · exact hx2 + · simp only [sub_sub_cancel] + have : intSm' V biφ = (ψʳ 𝓓⋆ φ.φ) := by + ext y + trans ; swap + · exact (congrFun (convAsLambda ( ψʳ) (φ.φ )) y).symm + · simp + symm + rw [← MeasureTheory.integral_sub_left_eq_self _ _ y ] + congr + ext x + simp only [neg_sub, sub_add_cancel] + symm + exact biφcalc + have cd : ContDiff ℝ ⊤ (intSm' V biφ) := by + rw [this] + apply ContCompactSupp.smooth + + trans T (intSm V biφ hbiφ cd) + · symm ; + have := FcommWithIntegrals V biφ hbiφ T cd + exact this + · simp only [instAddCommGroup𝓓, instNeg𝓓, intSm, AddHom.toFun_eq_coe, + LinearMap.coe_toAddHom, ContinuousLinearMap.coe_coe, convWith, mk, reflection, + fromEndoOfV, reflection', coe_toContinuousAffineMap, coe_mk', LinearMap.coe_mk, + AddHom.coe_mk, coe_comp', Function.comp_apply] + congr + + +theorem convolution𝓓'IsSmooth (ψ : 𝓓F ℝ V ) (T : 𝓓'F ℝ V ) : ContDiff ℝ ⊤ (T *f ψ) := by + -- have SeqContℕψ' : Tendsto (ψ'f ∘ x) atTop (𝓝 (ψ'f x0)) := by + -- apply (SeqContinuous'OfContinuous ℝ T).seqCont + + + + /- Idea how to get smoothness from here: + Induction. + As For every ψ we find ψ' s.th. T °⋆ ψ = Λ ψ' , we find a function ∂ψ' such that T °⋆ ∂ ψ = Λ ∂ψ' + One can show Then + ∂ Λ ψ' = ∂ (T °* ψ) = T °⋆ ∂ ψ = Λ ∂ψ' + If the weak derivative of a continuous function is continuous then the function was continuously differentiable. + -/ + + + + + + sorry +-- #lint diff --git a/BonnAnalysis/DistributionsOfVEndo.lean b/BonnAnalysis/DistributionsOfVEndo.lean new file mode 100644 index 0000000..f286564 --- /dev/null +++ b/BonnAnalysis/DistributionsOfVEndo.lean @@ -0,0 +1,494 @@ +import Mathlib.Topology.Sequences +import Mathlib.Topology.Defs.Filter +import Mathlib.Topology.Order +import Mathlib.Topology.Algebra.ContinuousAffineMap +import Mathlib.Order.Filter.Basic +import Mathlib.Init.Function +import BonnAnalysis.ConvergingSequences +import Mathlib.Geometry.Manifold.Instances.Real +import Mathlib.Topology.UniformSpace.UniformConvergence +import Mathlib.Data.Set.Pointwise.Basic +import BonnAnalysis.UniformConvergenceSequences +import BonnAnalysis.Distributions +import Mathlib + +import Mathlib.Analysis.Convolution +--import Mathlib.Analysis.InnerProductSpace +-- import Mathlib.Order +-- noncomputable section +--open FourierTransform MeasureTheory Real + + +namespace MeasureTheory +open MeasureTheory +open scoped Pointwise +universe u v w u' u'' +open Order Set + +open scoped Classical +open NNReal Topology +open Filter + +open scoped Topology +open TopologicalSpace +noncomputable section +open Function + +variable (k : Type v) [NontriviallyNormedField k] + +open ContinuousLinearEquiv + +variable {V : Type u} [MeasurableSpace V] [NormedAddCommGroup V] [NormedSpace k V] +@[simp] def reflection' : V →ᴬ[k] V := (ContinuousLinearMap.neg.neg (ContinuousLinearMap.id k V)).toContinuousAffineMap +@[simp] def shift' (x : V) : V →ᴬ[k] V := by + apply ContinuousAffineMap.mk ; swap ; + refine AffineMap.mk (fun y => y - x ) (LinearMap.id (R:=k) (M:=V)) ?_ + intro p v ; simp ; exact add_sub_assoc v p x + apply Continuous.sub + exact continuous_id' + exact continuous_const +lemma properNessOfHomeo {X : Type*} {Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] + (e : ContinuousMap X Y) (f : ContinuousMap Y X) (hf : ∀ x , (f ∘ e) x = x) (hf2 : ∀ x , e ( f x) = x): + IsProperMap e := Homeomorph.isProperMap (by use ⟨ e , f , hf , hf2⟩ ; continuity ; continuity) + +lemma reflectionIsProper : IsProperMap (reflection' k : V → V) := + + by + have : ∀ (x : V), (⇑(reflection' k).toContinuousMap ∘ ⇑(reflection' k).toContinuousMap) x = x := by + intro x ; simp only [reflection', ContinuousAffineMap.toContinuousMap_coe, + ContinuousMap.coe_coe, ContinuousLinearMap.coe_toContinuousAffineMap, comp_apply, + ContinuousLinearMap.neg_apply, ContinuousLinearMap.coe_id', id_eq, _root_.map_neg, neg_neg] + apply properNessOfHomeo (reflection' k).toContinuousMap (reflection' k).toContinuousMap + exact this + exact this + +instance shiftIsProper (v : V) : IsProperMap ((shift' k v) : V → V) := by + + apply properNessOfHomeo (shift' k v).toContinuousMap (shift' k (-v)).toContinuousMap + · intro x ; simp only [shift', sub_neg_eq_add, ContinuousAffineMap.toContinuousMap_coe, + ContinuousMap.coe_coe, ContinuousAffineMap.coe_mk, AffineMap.coe_mk, comp_apply, + sub_add_cancel] + · intro x ; simp only [shift', ContinuousAffineMap.toContinuousMap_coe, sub_neg_eq_add, + ContinuousMap.coe_coe, ContinuousAffineMap.coe_mk, AffineMap.coe_mk, add_sub_cancel_right] + +variable {V : Type u} {k : Type v} [NontriviallyNormedField k] + [MeasurableSpace V] [NormedAddCommGroup V] [NormedSpace k V] {Ω : Opens V} + + +variable (W : Type* ) [NormedAddCommGroup W] [NormedSpace k W] + +@[simp] def ev_cts (v : V) {W : Type* } [NormedAddCommGroup W] [NormedSpace k W] : + (V →L[k] W) →L[k] W := ContinuousLinearMap.apply _ _ v + + +-- open LinearMap + + + + + +open 𝓓 +lemma supportfromEndoOfV (Φ : V →ᴬ[k] V) (ψ : 𝓓F k V) : tsupport (ψ ∘ Φ) ⊆ Φ ⁻¹' (tsupport ψ ) := by + + have ( A : Set V ) : closure (Φ ⁻¹' (A)) ⊆ Φ ⁻¹' (closure A) := by + apply Continuous.closure_preimage_subset + apply Φ.cont + apply this (ψ ⁻¹' {x | x ≠ 0}) +lemma tsupport_comp_subset {M N α : Type*} [TopologicalSpace α ] [TopologicalSpace M] [TopologicalSpace N] [Zero M] [Zero N] {g : M → N} (hg : g 0 = 0) (f : α → M) : + tsupport (g ∘ f) ⊆ tsupport f := by + apply closure_minimal + · trans support f + · apply support_comp_subset ; exact hg + · exact subset_tsupport f + · exact isClosed_tsupport f +open Convolution + +section CommGroup +lemma add_compact_subsets {G : Type*} [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {A B : Set G} (hA : IsCompact A) (hB : IsCompact B) + : IsCompact (A + B ) := by + let plus : G × G → G := fun p => p.1 + p.2 + have check : plus '' (A ×ˢ B) = A + B := add_image_prod + rw [← check] + apply IsCompact.image + exact IsCompact.prod hA hB + + exact continuous_add +lemma sub_compact_subsets {G : Type*} [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {A B : Set G} (hA : IsCompact A) (hB : IsCompact B) + : IsCompact (A - B ) := by + let plus : G × G → G := fun p => p.1 - p.2 + have check : plus '' (A ×ˢ B) = A - B := sub_image_prod + rw [← check] + apply IsCompact.image + exact IsCompact.prod hA hB + + exact continuous_sub + -- use that images of compact subsets under + : G x G → G are compact. +lemma tsupport_convolution_subset {𝕜 : Type*}[NontriviallyNormedField 𝕜] {G : Type*} [MeasurableSpace G] (μ : Measure G) {E : Type*} {E' : Type*} {F : Type*} + [NormedAddCommGroup F] [NormedAddCommGroup E] [NormedAddCommGroup E'] + [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] [NormedSpace ℝ F] + [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] + (L : E →L[𝕜] E' →L[𝕜] F) {f : G → E} {g : G → E'} (hf : HasCompactSupport f) (hg : HasCompactSupport g) : tsupport (f ⋆[L, μ] g) ⊆ tsupport f + tsupport g:=by + apply closure_minimal + · trans support f + support g + · apply support_convolution_subset + · have a1 := subset_tsupport (f) + have a2 := subset_tsupport g + exact add_subset_add a1 a2 + · have : IsCompact ( tsupport f + tsupport g) := by + apply add_compact_subsets + exact hf + exact hg + -- maybe use that compact subsets of metrizable spaces are closed? + exact IsCompact.isClosed this + +-- lemma affineAsUnderlyingLinearTransition {Φ : V →ᴬ[k] V} {v : V} : Φ v = (Φ.linear v) + Φ 0 := by rw [show Φ v = Φ (v + 0) from by simp only [add_zero]] ; apply Φ.map_vadd' +-- def precompmyΦ (Φ : V →ᴬ[k] V) (l : ℕ) : (V [×l]→L[k] k) →L[k] (V [×l]→L[k] k) := ContinuousMultilinearMap.compContinuousLinearMapL fun _ ↦ Φ.contLinear +def precompmyΦ (Φ : V →ᴬ[k] V) (l : ℕ) : (V [×l]→L[k] k) →L[k] (V [×l]→L[k] k) := ContinuousMultilinearMap.compContinuousLinearMapL (fun _ ↦ Φ.contLinear) +--(W : Type* ) [NormedAddCommGroup W] [NormedSpace k W] +lemma affineAsUnderlyingLinearTransition {Φ : V →ᴬ[k] V} {v : V} : Φ v = (Φ.linear v) + Φ 0 := by rw [show Φ v = Φ (v + 0) from by simp only [add_zero]] ; apply Φ.map_vadd' +-- lemma fderiv_iteratedFDeriv' +lemma fDerivTransition (v x : V) (φ0 : V → W) (hφ0 : ContDiff k ⊤ φ0): + fderiv k (φ0.comp (shift' k v)) (x) = fderiv k φ0 (x - v) := by + rw [fderiv.comp ] -- , AffineMap.deriv (shift' k v)] + · have : (fderiv k (⇑(shift' k v)) x) = ContinuousLinearMap.id k V := by + calc + fderiv k (⇑(shift' k v)) x = fderiv k ((fun x => x) - (fun _ => v)) x := by congr + _ = fderiv k (id) x - fderiv k (fun _ => v) x := by apply fderiv_sub ; exact differentiableAt_id' ; apply differentiableAt_const + _ = _ := by rw [fderiv_id ,fderiv_const] ; simp only [Pi.zero_apply, sub_zero] + rw [this] + simp only [shift', ContinuousAffineMap.coe_mk, AffineMap.coe_mk, ContinuousLinearMap.comp_id] + · apply Differentiable.differentiableAt + exact ContDiff.differentiable hφ0 (OrderTop.le_top 1) + · apply Differentiable.differentiableAt + apply ContDiff.differentiable ; swap + · exact OrderTop.le_top _ + · exact ContinuousAffineMap.contDiff (𝕜 := k) (shift' k v) + +lemma iteratedFDerivTransition (v x : V) (l) (φ0 : 𝓓F k V) : -- V[×ℓ]→L[ k ] k) (l : ℕ) :{ℓ : ℕ } + iteratedFDeriv k (l) (φ0.f.comp (shift' k v)) (x) = iteratedFDeriv k l φ0 (x - v) := by + + induction' l with l hl generalizing x -- φ0 ℓ + · simp ; ext z ; rw [iteratedFDeriv_zero_apply , iteratedFDeriv_zero_apply] ; apply congrArg ; rfl + + · have {ψ : V → k} {l}: (fun f => f.uncurryLeft) ∘ (fderiv k (iteratedFDeriv k l ψ)) = + iteratedFDeriv k (l + 1) ψ := by + symm ; + rw [fderiv_iteratedFDeriv] ; + congr + + rw [← this] + symm ; + rw [← this] + simp only [Nat.succ_eq_add_one, comp_apply, shift', ContinuousAffineMap.coe_mk, + AffineMap.coe_mk] + + ext1 m + simp + apply congrFun + apply congrArg + apply congrFun + apply congrArg + let ψ := iteratedFDeriv k l φ0 + have : fderiv k (ψ.comp (shift' k v)) (x) = fderiv k ψ (x - v) := by + apply fDerivTransition + apply ContDiff.iteratedFDeriv_right + exact φ0.smooth + apply OrderTop.le_top + rw [← this] + congr + ext1 r + simp + exact Eq.symm (hl r) + + + + + + + +-- This is a version of iteratedFDeriv_comp_right for continuous affine maps. +theorem ContinuousAffineMap.iteratedFDeriv_comp_right {l} {φ0 : 𝓓F k V} (Φ : V →ᴬ[k] V) {x} : (iteratedFDeriv k l (φ0 ∘ Φ)) x = + (precompmyΦ Φ l) (iteratedFDeriv k l (φ0) (Φ x) ) := by + let φ0' : V → k := (φ0.f ).comp ((shift' k (- Φ 0))) + have : φ0 ∘ Φ = φ0' ∘ Φ.contLinear := by + ext x ; simp only [φ0',Function.comp_apply, + shift', sub_neg_eq_add, ContinuousAffineMap.coe_mk, AffineMap.coe_mk, + ContinuousAffineMap.coe_contLinear] ; congr ; apply affineAsUnderlyingLinearTransition + rw [this] + ext1 y + rw [ContinuousLinearMap.iteratedFDeriv_comp_right (i:=l) (Φ.contLinear) ?_ _ (OrderTop.le_top _)] + · have sth : ((iteratedFDeriv k l φ0' (Φ.contLinear x)).compContinuousLinearMap fun _ ↦ Φ.contLinear) = + ⇑(precompmyΦ Φ l) (iteratedFDeriv k l φ0' (Φ.contLinear x)) := by unfold precompmyΦ ; rw [ContinuousMultilinearMap.compContinuousLinearMapL_apply] + rw [sth] + simp + apply congrFun + apply congrArg + apply congrArg + rw [affineAsUnderlyingLinearTransition] + rw [show Φ.linear x + Φ 0 = Φ.linear x - (- Φ 0) from ?_] + rw [iteratedFDerivTransition] + + simp only [sub_neg_eq_add] + · have : ContDiff k ⊤ ⇑(shift' k (-Φ 0)) := by apply ContinuousAffineMap.contDiff + + refine ContDiff.comp φ0.smooth (this) + + +theorem chainRule {l} {φ0 : 𝓓F k V} (Φ : V →ᴬ[k] V) : (iteratedFDeriv k l (φ0 ∘ Φ)) = + (precompmyΦ Φ l ∘ (iteratedFDeriv k l (φ0) ∘ Φ )) := by ext1 x ; exact ContinuousAffineMap.iteratedFDeriv_comp_right Φ + +@[simp] def fromEndoOfV (Φ : V →ᴬ[k] V) (hΦ : IsProperMap (Φ : V → V)): 𝓓F k V →L[k] 𝓓F k V := by + + apply mk ; swap + · intro ψ + exact ⟨ ψ ∘ Φ , + ContDiff.comp ψ.smooth (ContinuousAffineMap.contDiff Φ ) , by + apply IsCompact.of_isClosed_subset ; swap + exact isClosed_tsupport (ψ.f ∘ Φ) + swap + · exact supportfromEndoOfV (k:=k) Φ ψ + · apply IsProperMap.isCompact_preimage + apply (hΦ) + exact (ψ.hsupp) ⟩ + + --ψ.fHasCmpctSupport + · constructor + · intro φ ψ + ext x + rfl + · intro c φ + ext x + rfl + · constructor + intro φ φ0 hφ + obtain ⟨ ⟨ K , hK⟩ ,hφ ⟩ := hφ + apply tendsTo𝓝 + constructor + · use Φ ⁻¹' K + constructor + · apply IsProperMap.isCompact_preimage + apply hΦ + exact hK.1 + · intro n + trans + · exact supportfromEndoOfV (k:=k) Φ (φ n) + · apply Set.monotone_preimage + exact hK.2 n + + · intro l + -- apply TendstoUniformly.comp + + + + + + + have : (fun n => iteratedFDeriv k l ((φ n).f ∘ Φ) ) = (fun n => precompmyΦ Φ l ∘ iteratedFDeriv k l (φ n).f ∘ Φ ) := by + ext1 n + apply chainRule + have : TendstoUniformly (fun n => iteratedFDeriv k l (φ n ∘ Φ) ) (iteratedFDeriv k l (φ0 ∘ Φ)) atTop := by + rw [chainRule (φ0 := φ0)] + rw [this] + apply UniformContinuous.comp_tendstoUniformly (g:= precompmyΦ Φ l) + · apply ContinuousLinearMap.uniformContinuous -- apply UniformFun.postcomp_uniformContinuous , uniform Inducing? + · apply TendstoUniformly.comp + exact hφ l + exact this + + + +def δ : 𝓓' k Ω := mk k (fun φ => φ 0) (by + constructor + · intro x y ; rfl + · intro c x ; rfl + · constructor + intro x a hx + apply TendstoUniformly.tendsto_at + have := hx.2 0 + apply (zeroCase k).mp + assumption + ) +lemma testfunctionIsDiffAt {φ : 𝓓F k V} (x : V) : DifferentiableAt k (φ) x := by + apply ContDiffAt.differentiableAt + · apply contDiff_iff_contDiffAt.mp + exact φ.smooth + · exact OrderTop.le_top 1 +variable {V : Type u} [NontriviallyNormedField k] [NormedAddCommGroup V] + [NormedSpace k V] + {k' : Type u'} [NormedAddCommGroup k'] [NormedSpace k k'] + {k'' : Type u''} [NormedAddCommGroup k''] [NormedSpace k k''] + (e : k' →L[k] k'') {Ω : Opens V} + +lemma obs' {φ : V → k'} : tsupport (fun x => fderiv k φ x ) ⊆ tsupport (φ) := by -- ⊆ tsupport (fun x => fderiv k φ) := + exact tsupport_fderiv_subset k (f:= φ) +lemma obs {φ : ContCompactSupp k V k'} : tsupport (e ∘ φ.f) ⊆ tsupport (φ) := by -- ⊆ tsupport (fun x => fderiv k φ) := + · apply tsupport_comp_subset (ContinuousLinearMap.map_zero e) (f:=φ) + + +@[simp] def postCCSMap : ContCompactSupp k V k' → ContCompactSupp k V k'' := fun φ => ⟨ e ∘ φ.f + , by apply ContDiff.comp ; apply ContinuousLinearMap.contDiff ; exact φ.smooth , + by + apply IsCompact.of_isClosed_subset (φ.hsupp) + exact isClosed_tsupport _ + exact obs e + ⟩ +lemma SeqContinuousStronglypostCCSMap : SeqContinuousStrongly (postCCSMap (V:=V) e) := by + constructor + intro α a hx + constructor + · obtain ⟨ K , hK ⟩ := hx.1 + use K + constructor + · exact hK.1 + · intro n + trans (tsupport (α n).f) + · exact obs e + · exact hK.2 n + · intro l + have : TendstoUniformly (fun n ↦ iteratedFDeriv k (l) (α n).f) (iteratedFDeriv k (l) (a).f) atTop := hx.2 (l) + let precomp_e : (V[×l]→L[k] k') →L[k] (V[×l]→L[k] k'') :=ContinuousLinearMap.compContinuousMultilinearMapL k (fun _ => V) k' k'' e + have hxg (ψ : ContCompactSupp k V k') : iteratedFDeriv k l (postCCSMap e ψ).f = precomp_e ∘ iteratedFDeriv k (l) (ψ).f := by + simp only [postCCSMap] + ext1 x + rw [ContinuousLinearMap.iteratedFDeriv_comp_left] + + · rfl + · exact ψ.smooth + · apply OrderTop.le_top + + rw [hxg] + have hxg : (fun (n : ℕ) => iteratedFDeriv k l (((postCCSMap e) ∘ α ) n).f) = + fun (n : ℕ) => precomp_e ∘ (iteratedFDeriv k (l) (α n).f) := by + ext1 n + exact hxg (α n) + + + rw [hxg] + + --rw [← tendstoUniformlyOn_univ ] at this + --rw [← tendstoUniformlyOn_univ ] + + refine UniformContinuous.comp_tendstoUniformly ?_ this + apply ContinuousLinearMap.uniformContinuous + +@[simp] def postCCS : ContCompactSupp k V k' →L[k] ContCompactSupp k V k'' := by + + let f : ContCompactSupp k V k' → ContCompactSupp k V k'' := postCCSMap e + apply mk ; swap + · exact f + · constructor + · intro φ ψ + ext x + simp only [ f, postCCSMap, instAddCommGroupContCompactSupp, instAddContCompactSupp, + instZeroContCompactSupp, instNegContCompactSupp, ccs_add, map_comp_add, Pi.add_apply, + comp_apply] + · intro c φ + ext x + simp + apply LinearMap.map_smul + · apply SeqContinuous'OfStrongly + exact (SeqContinuousStronglypostCCSMap e) + +@[simp] def fderivCCS : (ContCompactSupp k V k') →ₗ[k] ContCompactSupp k V (V →L[k] k') := by + let map : (ContCompactSupp k V k') → ContCompactSupp k V (V →L[k] k') := fun φ => by + use fderiv k φ.f + · have dfh : ContDiff k ⊤ (fun x => fderiv k φ.f x) := (contDiff_top_iff_fderiv.mp (φ.smooth )).2 + exact dfh + -- have evvh : ContDiff k ⊤ (ContinuousLinearMap.apply k k' v ) := by apply ContinuousLinearMap.contDiff + + -- apply ContDiff.comp evvh dfh + + + · apply IsCompact.of_isClosed_subset (φ.hsupp) + exact isClosed_tsupport _ + exact obs' + apply LinearMap.mk ; swap + use map + + · intro x y ; ext1 ; simp only [map] ; + ext1 z + apply fderiv_add + apply diffAt + apply diffAt + · intro c x ; + ext1 ; simp only [map] ; + ext1 z + simp + + apply fderiv_const_smul + apply diffAt +lemma SeqContinuousStronglyFderivCCS : SeqContinuousStrongly + (fderivCCS : ContCompactSupp k V (k') → ContCompactSupp k V (V →L[k] k') ) := by + + + constructor + intro φ φ0 hφ + constructor + · obtain ⟨ K , hK⟩ := hφ.1 + use K + constructor + · exact hK.1 + · intro n + trans ; swap + · exact hK.2 n + · apply obs' + · intro l + have {φ : ContCompactSupp k V k'} : (iteratedFDeriv k l ((fderivCCS φ) ).f) = fun z => (iteratedFDeriv k (l+1) ((φ).f) z).curryRight:= by + ext z x + rw [iteratedFDeriv_succ_eq_comp_right] + simp only [fderivCCS, Nat.succ_eq_add_one, comp_apply, + ContinuousMultilinearMap.curryRight_apply, continuousMultilinearCurryRightEquiv_apply', + Fin.init_snoc, Fin.snoc_last] + congr + + + rw [this] + have : (fun n ↦ iteratedFDeriv k l ((fderivCCS ∘ φ) n).f) = fun n ↦ fun z => (iteratedFDeriv k (l+1) ((φ n).f) z).curryRight := by + ext1 n ; + exact this + rw [this] + have := (hφ.2 (l+1)) + refine UniformContinuous.comp_tendstoUniformly (g:=(fun f => f.curryRight)) ?_ this + exact Isometry.uniformContinuous (continuousMultilinearCurryRightEquiv' k l V k').symm.isometry + +@[simp] def fderivCCSAt (v : V) : (ContCompactSupp k V k') →ₗ[k] ContCompactSupp k V k' := ((postCCS (ev_cts v)).toLinearMap).comp (fderivCCS) + +lemma obsOLD' {v : V} {φ : V → k'} : tsupport (fun x => fderiv k φ x v) ⊆ tsupport (φ) := by -- ⊆ tsupport (fun x => fderiv k φ) := + trans ; swap + · exact tsupport_fderiv_subset k (f:= φ) + · apply tsupport_comp_subset rfl (g := fun f => f v) (f:=fderiv k φ) +lemma obsOLD {v : V} {φ : ContCompactSupp k V k'} : tsupport (fun x => (fderivCCSAt v φ).f x) ⊆ tsupport (φ) := by -- ⊆ tsupport (fun x => fderiv k φ) := + + apply obsOLD' +def fderiv𝓓 (v : V) : (𝓓 k Ω) →L[k] 𝓓 k Ω := by + let f : 𝓓 k Ω → 𝓓 k Ω := fun φ => ⟨ fderivCCSAt v φ.φ , by + trans + · exact obsOLD + · exact φ.sprtinΩ ⟩ + apply mk ; swap + · exact f + · constructor + · intro φ ψ ; ext1 ; apply LinearMap.map_add + · intro φ ψ ; ext1 ; apply LinearMap.map_smul + · apply SeqContinuous'OfStrongly + constructor + + intro α a hx + + --apply tendsTo𝓝 + have : (fun n => (α n).φ) ⟶ a.φ := hx + apply (SeqContinuousStronglypostCCSMap (V:=V) (k' := V →L[k] k) (k'' := k) (ev_cts v)).seqCont + apply SeqContinuousStronglyFderivCCS.seqCont hx + + + + + + +notation A "**" T => T ∘L A +example (v : V) (φ : 𝓓 k Ω ) (T : 𝓓' k Ω ): (fderiv𝓓 v ** T) φ = T (fderiv𝓓 v φ) := by rfl + + + +@[simp] def reflection : 𝓓F k V →L[k] (𝓓F k V) := fromEndoOfV (reflection' k) (reflectionIsProper _) +postfix:200 "ʳ" => reflection diff --git a/BonnAnalysis/UniformConvergenceSequences.lean b/BonnAnalysis/UniformConvergenceSequences.lean new file mode 100644 index 0000000..de7195c --- /dev/null +++ b/BonnAnalysis/UniformConvergenceSequences.lean @@ -0,0 +1,73 @@ +import Mathlib.Topology.Sequences +import Mathlib.Topology.Defs.Filter +import Mathlib.Topology.Order +import Mathlib.Order.Filter.Basic +import BonnAnalysis.ConvergingSequences +import Mathlib.Geometry.Manifold.Instances.Real +import Mathlib.Topology.UniformSpace.UniformConvergence +import Mathlib + + +namespace MeasureTheory +open MeasureTheory +universe u v x w +open Order Set Filter +open Filter + + +lemma CnstSeqTendstoUniformlyOn {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] + (f : α → β) (p : Filter ι) (s : Set α) : TendstoUniformlyOn (fun n => f) f p s := by + unfold TendstoUniformlyOn + simp + intro u hu + have : True = ∀ x ∈ s , (f x , f x) ∈ u := by rw [eq_true_eq_id] ; simp ; intro x _ ; apply refl_mem_uniformity hu + rw [← this] + simp +lemma SubSeqConvergesUniformly' {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] + {f : α → β} {p : Filter ι} {s : Set α} {φ : ι → ι} + (hφ : map φ p ≤ p) {F : ι → α → β} (hF : TendstoUniformlyOn F f p s) + : TendstoUniformlyOn (F ∘ φ) f p s := by + rw [tendstoUniformlyOn_iff_tendsto] + rw [tendstoUniformlyOn_iff_tendsto] at hF + let φ' : ι × α → ι × α := fun (x , y) => (φ x , y) + have hφ' : map φ' (p ×ˢ 𝓟 s) ≤ (p ×ˢ 𝓟 s) := by + rw [le_def] + intro q hq + rw [mem_map] + rw[mem_prod_iff] + rw [mem_prod_iff] at hq + obtain ⟨ t₁ , ht₁ , t₂ , ht₂ , ht ⟩ := hq + use φ ⁻¹' t₁ + constructor + · exact hφ ht₁ + · use t₂ + constructor + · exact ht₂ + · trans φ' ⁻¹' (t₁ ×ˢ t₂) + · apply subset_rfl + · exact fun ⦃a⦄ x ↦ ht x + exact subSeqConverges' hφ' hF + -- + lemma SubSeqConvergesUniformly {α : Type u} {β : Type v} [UniformSpace β] + {f : α → β} {s : Set α} + {F : ℕ → α → β} (hF : TendstoUniformlyOn F f atTop s) + (F' : SubSequence F) + : TendstoUniformlyOn F' f atTop s := + SubSeqConvergesUniformly' (subsequencePreservesTop F'.hφ) hF + + + +lemma UniformContPresUniformConvergence {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [TopologicalSpace α] [UniformSpace β] [UniformSpace γ] + {f : α → β} {p : Filter ι} {s : Set α} {F : ι → α → β} (hF : TendstoUniformlyOn F f p s) + (g : β → γ) (hg : UniformContinuous g) : TendstoUniformlyOn (fun n => g ∘ F n) (g ∘ f) p s := by + intro u hu + have := hg hu + let v := hF _ this + exact v + + + + + + + --rw [tendstoUniformlyOn_iff_tendsto] From c19ce17ff990acb9e81f5e06fbc18f588cd00e13 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 14 Aug 2024 15:41:41 +0200 Subject: [PATCH 10/10] mk_all and remove options --- BonnAnalysis.lean | 7 +++++++ BonnAnalysis/Dual.lean | 6 ------ 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/BonnAnalysis.lean b/BonnAnalysis.lean index a3ff7b2..c34c78c 100644 --- a/BonnAnalysis.lean +++ b/BonnAnalysis.lean @@ -1,8 +1,15 @@ import BonnAnalysis.ComplexInterpolation +import BonnAnalysis.ConvergingSequences +import BonnAnalysis.ConvolutionTendsToUniformly +import BonnAnalysis.Distributions +import BonnAnalysis.DistributionsExamples +import BonnAnalysis.DistributionsOfVEndo import BonnAnalysis.Dual import BonnAnalysis.Examples +import BonnAnalysis.Hadamard import BonnAnalysis.LorentzSpace import BonnAnalysis.Plancherel import BonnAnalysis.RealInterpolation import BonnAnalysis.StrongType import BonnAnalysis.Test +import BonnAnalysis.UniformConvergenceSequences diff --git a/BonnAnalysis/Dual.lean b/BonnAnalysis/Dual.lean index f222eaf..5466de6 100644 --- a/BonnAnalysis/Dual.lean +++ b/BonnAnalysis/Dual.lean @@ -7,12 +7,6 @@ import Mathlib.Analysis.NormedSpace.LinearIsometry import Mathlib.MeasureTheory.Integral.Bochner import Mathlib.Data.Real.Sign - -set_option linter.setOption false -set_option trace.profiler true -set_option profiler true - - /-! We show that the dual space of `L^p` for `1 ≤ p < ∞`. See [Stein-Shakarchi, Functional Analysis, section 1.4] -/