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]