PL1/ConvolutionHypercontractivity.lean
All source files · Download exact source
SHA-256: df6a827c5e364a683f0a5c15a12db0133d5469b0ddc8ea4e577a7ebd65f1951d
1import PL1.LpInclusions2import PL1.ConvolutionL134/-! # Transfer a real convolution Lp-L2 bound to either scalar field56Positivity of the actual convolution kernel gives the same constant; no7complex tensorization premise is required.8-/910noncomputable section11open MeasureTheory12open scoped ENNReal1314namespace PL1.Walsh1516variable (K : Type*) [RCLike K] (p : ℝ≥0∞) [Fact (1 ≤ p)]1718def normLp (f : Lp K p haar) : Lp ℝ p haar :=19 lipschitzWith_one_norm.compLp norm_zero f2021omit [Fact (1 ≤ p)] in22theorem coeFn_normLp (f : Lp K p haar) : normLp K p f =ᵐ[haar] fun x => ‖f x‖ :=23 lipschitzWith_one_norm.coeFn_compLp norm_zero f2425omit [Fact (1 ≤ p)] in26theorem norm_normLp_le (f : Lp K p haar) : ‖normLp K p f‖ ≤ ‖f‖ := by27 simpa only [normLp, one_mul, NNReal.coe_one] using lipschitzWith_one_norm.norm_compLp_le norm_zero f2829variable (ν : Measure Group) [IsProbabilityMeasure ν]30 (H : Lp ℝ p haar →L[ℝ] Lp ℝ 2 haar)31 (hH : ∀ f, l2ToL1 (H f) = convolutionL1 ν32 (ProbabilityLp.inclusion haar 1 p (Fact.out : 1 ≤ p) f))3334include hH3536theorem norm_convolution_inclusion_le_real (f : Lp K p haar) :37 ∀ᵐ x ∂haar, ‖convolutionL1 ν38 (ProbabilityLp.inclusion haar 1 p (Fact.out : 1 ≤ p) f) x‖ ≤39 ‖H (normLp K p f) x‖ := by40 let g := ProbabilityLp.inclusion haar 1 p (Fact.out : 1 ≤ p) f41 let h := ProbabilityLp.inclusion haar 1 p (Fact.out : 1 ≤ p) (normLp K p f)42 have hnorm : h =ᵐ[haar] fun x => ‖g x‖ := by43 filter_upwards [ProbabilityLp.coeFn_inclusion haar 1 p (Fact.out : 1 ≤ p) f,44 ProbabilityLp.coeFn_inclusion haar 1 p (Fact.out : 1 ≤ p) (normLp K p f),45 coeFn_normLp K p f] with x hg hh hn46 exact hh.trans (hn.trans (congrArg norm hg).symm)47 have hconv := convolutionL1_ae_eq_integral_of_ae_eq ν hnorm48 have hHae : H (normLp K p f) =ᵐ[haar] convolutionL1 ν h := by49 exact (ProbabilityLp.coeFn_inclusion haar 1 2 (by norm_num) _).symm.trans50 (by rw [hH])51 filter_upwards [coeFn_convolutionL1 ν g, hconv, hHae] with x hx hh hHx52 rw [hx, hHx, hh]53 exact (norm_integral_le_integral_norm _).trans (le_abs_self _)5455theorem memLp_convolution_inclusion_two (f : Lp K p haar) :56 MemLp (convolutionL1 ν (ProbabilityLp.inclusion haar 1 p (Fact.out : 1 ≤ p) f)) 2 haar :=57 (Lp.memLp (H (normLp K p f))).mono58 (Lp.aestronglyMeasurable _) (norm_convolution_inclusion_le_real K p ν H hH f)5960def scalarLiftFun (f : Lp K p haar) : Lp K 2 haar :=61 (memLp_convolution_inclusion_two K p ν H hH f).toLp62 (convolutionL1 ν (ProbabilityLp.inclusion haar 1 p (Fact.out : 1 ≤ p) f))6364theorem coeFn_scalarLiftFun (f : Lp K p haar) :65 scalarLiftFun K p ν H hH f =ᵐ[haar]66 convolutionL1 ν (ProbabilityLp.inclusion haar 1 p (Fact.out : 1 ≤ p) f) :=67 MemLp.coeFn_toLp _6869theorem scalarLiftFun_add (f g : Lp K p haar) :70 scalarLiftFun K p ν H hH (f + g) =71 scalarLiftFun K p ν H hH f + scalarLiftFun K p ν H hH g := by72 let V := (convolutionL1 (𝕜 := K) ν).comp73 (ProbabilityLp.inclusion haar 1 p (Fact.out : 1 ≤ p))74 apply Lp.ext75 filter_upwards [coeFn_scalarLiftFun K p ν H hH (f + g),76 coeFn_scalarLiftFun K p ν H hH f, coeFn_scalarLiftFun K p ν H hH g,77 Lp.coeFn_add (V f) (V g),78 Lp.coeFn_add (scalarLiftFun K p ν H hH f) (scalarLiftFun K p ν H hH g)]79 with x hfg hf hg hv hl80 change scalarLiftFun K p ν H hH (f + g) x = _81 change scalarLiftFun K p ν H hH (f + g) x = V (f + g) x at hfg82 rw [hfg, map_add, hv, hl]83 simp only [Pi.add_apply, hf, hg]84 rfl8586theorem scalarLiftFun_smul (c : K) (f : Lp K p haar) :87 scalarLiftFun K p ν H hH (c • f) = c • scalarLiftFun K p ν H hH f := by88 let V := (convolutionL1 (𝕜 := K) ν).comp89 (ProbabilityLp.inclusion haar 1 p (Fact.out : 1 ≤ p))90 apply Lp.ext91 filter_upwards [coeFn_scalarLiftFun K p ν H hH (c • f),92 coeFn_scalarLiftFun K p ν H hH f, Lp.coeFn_smul c (V f),93 Lp.coeFn_smul c (scalarLiftFun K p ν H hH f)] with x hcf hf hv hl94 change scalarLiftFun K p ν H hH (c • f) x = V (c • f) x at hcf95 rw [hcf, map_smul, hv, hl]96 simp only [Pi.smul_apply, hf]97 rfl9899theorem norm_scalarLiftFun_le (f : Lp K p haar) :100 ‖scalarLiftFun K p ν H hH f‖ ≤ ‖H‖ * ‖f‖ := by101 calc102 _ ≤ ‖H (normLp K p f)‖ := by103 apply Lp.norm_le_norm_of_ae_le104 filter_upwards [coeFn_scalarLiftFun K p ν H hH f,105 norm_convolution_inclusion_le_real K p ν H hH f] with x hx hb106 simpa only [hx] using hb107 _ ≤ ‖H‖ * ‖normLp K p f‖ := H.le_opNorm _108 _ ≤ ‖H‖ * ‖f‖ := mul_le_mul_of_nonneg_left (norm_normLp_le K p f) (norm_nonneg _)109110/-- The complex (or real) convolution lift with the same bound as the real111lift, constructed on genuine equivalence classes. -/112def scalarLift : Lp K p haar →L[K] Lp K 2 haar :=113 LinearMap.mkContinuous114 { toFun := scalarLiftFun K p ν H hH115 map_add' := scalarLiftFun_add K p ν H hH116 map_smul' := scalarLiftFun_smul K p ν H hH }117 ‖H‖ (norm_scalarLiftFun_le K p ν H hH)118119theorem norm_scalarLift_le : ‖scalarLift K p ν H hH‖ ≤ ‖H‖ :=120 ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) (norm_scalarLiftFun_le K p ν H hH)121122theorem scalarLift_overlap (f : Lp K p haar) :123 l2ToL1 (scalarLift K p ν H hH f) =124 convolutionL1 ν (ProbabilityLp.inclusion haar 1 p (Fact.out : 1 ≤ p) f) := by125 apply Lp.ext126 exact (ProbabilityLp.coeFn_inclusion haar 1 2 (by norm_num) _).trans127 (coeFn_scalarLiftFun K p ν H hH f)128129end PL1.Walsh130