PL1/RademacherEmbedding.lean
All source files · Download exact source
SHA-256: c5bbddae3bc3974131c9ea9b236faef5a436f75f7a37f184c9e74a937e9f1ac8
1import PL1.LpInclusions2import PL1.Definitions3import Mathlib.Analysis.Normed.Operator.Banach4import Mathlib.Tactic.Ring5import Mathlib.Tactic.LinearCombination67/-!8# The first Walsh chaos in Haar L1910This module develops the concrete Rademacher map and its finite-sum moment11estimates. Constants in the embedding estimate need not be optimal.12-/1314noncomputable section15set_option maxHeartbeats 100000016open MeasureTheory17open scoped ENNReal BigOperators Topology1819namespace PL1.Walsh2021private theorem continuous_integrable (f : C(Group, ℝ)) : Integrable f haar :=22 f.continuous.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace f)2324/-- Haar expectation on continuous real functions, as a linear map. -/25def expectation : C(Group, ℝ) →ₗ[ℝ] ℝ where26 toFun f := ∫ x, f x ∂haar27 map_add' f g := integral_add (continuous_integrable f) (continuous_integrable g)28 map_smul' c f := integral_smul c f2930@[simp] theorem expectation_one : expectation 1 = 1 := by31 simp [expectation]3233@[simp] theorem expectation_const_mul (c : ℝ) (f : C(Group, ℝ)) :34 expectation (ContinuousMap.const Group c * f) = c * expectation f :=35 integral_const_mul c f3637@[simp] theorem expectation_const (c : ℝ) : expectation (ContinuousMap.const Group c) = c := by38 simp [expectation]3940/-- A finite Rademacher polynomial, as an actual continuous function on the sign group. -/41def rademacherPolynomial (s : Finset ℕ) (a : ℕ → ℝ) : C(Group, ℝ) :=42 ∑ j ∈ s, ContinuousMap.const Group (a j) * characterContinuous {j}4344@[simp] theorem rademacherPolynomial_empty (a : ℕ → ℝ) :45 rademacherPolynomial ∅ a = 0 := by simp [rademacherPolynomial]4647theorem rademacherPolynomial_insert {j : ℕ} {s : Finset ℕ} (hj : j ∉ s) (a : ℕ → ℝ) :48 rademacherPolynomial (insert j s) a =49 ContinuousMap.const Group (a j) * characterContinuous {j} + rademacherPolynomial s a := by50 simp only [rademacherPolynomial, Finset.sum_insert hj]5152theorem character_flip_of_not_mem {s : Finset ℕ} {j : ℕ} (hj : j ∉ s) :53 character s (flip j) = 1 := by54 apply Finset.prod_eq_one55 intro i hi56 have hij : i ≠ j := fun h => hj (h ▸ hi)57 simp [flip, Function.update_of_ne hij, signValue]5859theorem rademacherPolynomial_flip {s : Finset ℕ} {j : ℕ} (hj : j ∉ s)60 (a : ℕ → ℝ) (x : Group) :61 rademacherPolynomial s a (flip j * x) = rademacherPolynomial s a x := by62 simp only [rademacherPolynomial, ContinuousMap.sum_apply, ContinuousMap.mul_apply,63 ContinuousMap.const_apply, characterContinuous]64 apply Finset.sum_congr rfl65 intro i hi66 have hji : j ∉ ({i} : Finset ℕ) := by67 simpa only [Finset.mem_singleton] using (fun h : j = i => hj (h ▸ hi))68 simp only [ContinuousMap.coe_mk, character_mul, character_flip_of_not_mem hji, one_mul]6970/-- An odd factor in a fresh Rademacher coordinate has zero Haar expectation. -/71theorem expectation_rademacher_odd {s : Finset ℕ} {j : ℕ} (hj : j ∉ s)72 (a : ℕ → ℝ) (k : ℕ) :73 expectation (rademacherPolynomial s a ^ k * characterContinuous {j}) = 0 := by74 apply integral_eq_zero_of_mul_left_eq_neg (g := flip j)75 intro x76 change rademacherPolynomial s a (flip j * x) ^ k * character {j} (flip j * x) =77 -(rademacherPolynomial s a x ^ k * character {j} x)78 rw [rademacherPolynomial_flip hj, character_mul,79 character_flip_of_mem (Finset.mem_singleton_self j)]80 ring8182private theorem rademacherPolynomial_square {s : Finset ℕ} {j : ℕ} (hj : j ∉ s)83 (a : ℕ → ℝ) :84 rademacherPolynomial (insert j s) a ^ 2 =85 rademacherPolynomial s a ^ 2 +86 ContinuousMap.const Group (2 * a j) * (rademacherPolynomial s a * characterContinuous {j}) +87 ContinuousMap.const Group (a j ^ 2) := by88 ext x89 rw [rademacherPolynomial_insert hj]90 change (a j * character {j} x + rademacherPolynomial s a x) ^ 2 =91 rademacherPolynomial s a x ^ 2 + 2 * a j *92 (rademacherPolynomial s a x * character {j} x) + a j ^ 293 have hr : character {j} x ^ 2 = 1 := by94 simpa only [pow_two] using character_mul_self {j} x95 nlinarith [sq_nonneg (a j)]9697/-- The exact second moment of a finite real Rademacher polynomial. -/98theorem expectation_rademacher_square (s : Finset ℕ) (a : ℕ → ℝ) :99 expectation (rademacherPolynomial s a ^ 2) = ∑ j ∈ s, a j ^ 2 := by100 induction s using Finset.induction_on with101 | empty => simp102 | @insert j s hj ih =>103 rw [rademacherPolynomial_square hj, map_add, map_add,104 expectation_const_mul, expectation_const, ih]105 have ho := expectation_rademacher_odd hj a 1106 simp only [pow_one] at ho107 rw [ho]108 simp [Finset.sum_insert hj, add_comm]109110private theorem rademacherPolynomial_fourth {s : Finset ℕ} {j : ℕ} (hj : j ∉ s)111 (a : ℕ → ℝ) :112 rademacherPolynomial (insert j s) a ^ 4 =113 rademacherPolynomial s a ^ 4 +114 ContinuousMap.const Group (4 * a j) * (rademacherPolynomial s a ^ 3 * characterContinuous {j}) +115 ContinuousMap.const Group (6 * a j ^ 2) * (rademacherPolynomial s a ^ 2) +116 ContinuousMap.const Group (4 * a j ^ 3) * (rademacherPolynomial s a * characterContinuous {j}) +117 ContinuousMap.const Group (a j ^ 4) := by118 ext x119 rw [rademacherPolynomial_insert hj]120 change (a j * character {j} x + rademacherPolynomial s a x) ^ 4 =121 rademacherPolynomial s a x ^ 4 + 4 * a j *122 (rademacherPolynomial s a x ^ 3 * character {j} x) +123 6 * a j ^ 2 * rademacherPolynomial s a x ^ 2 +124 4 * a j ^ 3 * (rademacherPolynomial s a x * character {j} x) + a j ^ 4125 have hr : character {j} x ^ 2 = 1 := by126 simpa only [pow_two] using character_mul_self {j} x127 rcases sq_eq_one_iff.mp hr with hr | hr <;> rw [hr] <;> ring128129/-- The exact fourth moment, including its negative diagonal correction. -/130theorem expectation_rademacher_fourth (s : Finset ℕ) (a : ℕ → ℝ) :131 expectation (rademacherPolynomial s a ^ 4) =132 3 * (∑ j ∈ s, a j ^ 2) ^ 2 - 2 * ∑ j ∈ s, a j ^ 4 := by133 induction s using Finset.induction_on with134 | empty => simp135 | @insert j s hj ih =>136 rw [rademacherPolynomial_fourth hj]137 simp only [map_add, expectation_const_mul, expectation_const,138 expectation_rademacher_odd hj a 3, expectation_rademacher_square, ih]139 have ho := expectation_rademacher_odd hj a 1140 simp only [pow_one] at ho141 rw [ho]142 simp only [Finset.sum_insert hj]143 ring144145theorem expectation_rademacher_fourth_le (s : Finset ℕ) (a : ℕ → ℝ) :146 expectation (rademacherPolynomial s a ^ 4) ≤ 3 * (∑ j ∈ s, a j ^ 2) ^ 2 := by147 rw [expectation_rademacher_fourth]148 have h : 0 ≤ ∑ j ∈ s, a j ^ 4 := Finset.sum_nonneg (fun j _ => by positivity)149 linarith150151private theorem quartic_lower_bound (A u : ℝ) (hA : 0 ≤ A) (hu : 0 ≤ u) :152 A * u ^ 2 ≤ 4 * A * Real.sqrt A * u + (1 / 16 : ℝ) * u ^ 4 := by153 have hr := Real.sqrt_nonneg A154 have hr2 := Real.sq_sqrt hA155 by_cases h : u ≤ 4 * Real.sqrt A156 · have hm := mul_le_mul_of_nonneg_left h (mul_nonneg hA hu)157 nlinarith [pow_nonneg hu 4]158 · have hle : 4 * Real.sqrt A ≤ u := (lt_of_not_ge h).le159 have hs := (sq_le_sq₀ (by positivity : 0 ≤ 4 * Real.sqrt A) hu).mpr hle160 have hm := mul_le_mul_of_nonneg_right hs (sq_nonneg u)161 nlinarith [mul_nonneg (mul_nonneg hA hr) hu]162163/-- An elementary moment interpolation bound, with a nonoptimal but convenient constant.164The proof uses a pointwise quartic inequality instead of fractional-exponent Hölder. -/165theorem sqrt_secondMoment_le_eight_firstMoment (f : C(Group, ℝ)) (A : ℝ) (hA : 0 ≤ A)166 (h2 : expectation (f ^ 2) = A) (h4 : expectation (f ^ 4) ≤ 6 * A ^ 2) :167 Real.sqrt A ≤ 8 * ∫ x, ‖f x‖ ∂haar := by168 let af : C(Group, ℝ) := ⟨fun x => |f x|, f.continuous.abs⟩169 have habs : expectation af = ∫ x, ‖f x‖ ∂haar := by rfl170 have hnonneg : 0 ≤ expectation af := integral_nonneg (fun x => abs_nonneg (f x))171 have hint : expectation (ContinuousMap.const Group A * f ^ 2) ≤172 expectation (ContinuousMap.const Group (4 * A * Real.sqrt A) * af +173 ContinuousMap.const Group (1 / 16 : ℝ) * f ^ 4) := by174 apply integral_mono (continuous_integrable _) (continuous_integrable _)175 intro x176 change A * f x ^ 2 ≤ 4 * A * Real.sqrt A * |f x| + (1 / 16 : ℝ) * f x ^ 4177 have h := quartic_lower_bound A |f x| hA (abs_nonneg _)178 simpa only [sq_abs, (show Even (4 : ℕ) from ⟨2, rfl⟩).pow_abs] using h179 simp only [map_add, expectation_const_mul, h2] at hint180 rw [← habs]181 by_cases hAz : A = 0182 · simpa [hAz] using mul_nonneg (by norm_num : (0 : ℝ) ≤ 8) hnonneg183 · have hAp : 0 < A := lt_of_le_of_ne hA (Ne.symm hAz)184 have hrp : 0 < Real.sqrt A := Real.sqrt_pos.mpr hAp185 by_contra hbad186 have hL : expectation af < Real.sqrt A / 8 := by linarith187 have hm := mul_lt_mul_of_pos_left hL (by positivity : 0 < 4 * A * Real.sqrt A)188 have heq : (4 * A * Real.sqrt A) * (Real.sqrt A / 8) = A ^ 2 / 2 := by189 calc190 _ = A * (Real.sqrt A ^ 2) / 2 := by ring191 _ = _ := by rw [Real.sq_sqrt hA]; ring192 rw [heq] at hm193 nlinarith [sq_pos_of_pos hAp]194195theorem rademacher_firstMoment_lower (s : Finset ℕ) (a : ℕ → ℝ) :196 Real.sqrt (∑ j ∈ s, a j ^ 2) ≤197 8 * ∫ x, ‖rademacherPolynomial s a x‖ ∂haar := by198 apply sqrt_secondMoment_le_eight_firstMoment _ _199 (Finset.sum_nonneg (fun j _ => sq_nonneg _)) (expectation_rademacher_square s a)200 exact (expectation_rademacher_fourth_le s a).trans (by nlinarith [sq_nonneg (∑ j ∈ s, a j ^ 2)])201202section RademacherMap203204variable (𝕜 : Type*) [RCLike 𝕜]205206theorem orthonormal_rademacherL2 :207 Orthonormal 𝕜 (fun j : ℕ => scalarCharacterLp 𝕜 2 {j}) :=208 (orthonormal_scalarCharacterL2 𝕜).comp (fun j : ℕ => ({j} : Finset ℕ))209 (fun _i _j h => Finset.singleton_injective h)210211/-- The Rademacher series defines an isometry from actual scalar ell2 into Haar L2. -/212def rademacherL2 : Ell2 𝕜 →ₗᵢ[𝕜] Lp 𝕜 2 haar :=213 (orthonormal_rademacherL2 𝕜).orthogonalFamily.linearIsometry214215theorem rademacherL2_single (j : ℕ) (a : 𝕜) :216 rademacherL2 𝕜 (lp.single 2 j a) = a • scalarCharacterLp 𝕜 2 {j} := by217 exact (orthonormal_rademacherL2 𝕜).orthogonalFamily.linearIsometry_apply_single a218219/-- The concrete first-chaos map into Haar L1. -/220def rademacherL1 : Ell2 𝕜 →L[𝕜] Lp 𝕜 1 haar :=221 l2ToL1.comp (rademacherL2 𝕜).toContinuousLinearMap222223theorem rademacherL1_single (j : ℕ) (a : 𝕜) :224 rademacherL1 𝕜 (lp.single 2 j a) = a • scalarCharacterLp 𝕜 1 {j} := by225 change l2ToL1 (rademacherL2 𝕜 (lp.single 2 j a)) = _226 rw [rademacherL2_single, map_smul, l2ToL1_scalarCharacter]227228theorem norm_rademacherL1_le (a : Ell2 𝕜) : ‖rademacherL1 𝕜 a‖ ≤ ‖a‖ := by229 have h := ProbabilityLp.norm_inclusionFun_le haar 1 2 (by norm_num) (rademacherL2 𝕜 a)230 change ‖rademacherL1 𝕜 a‖ ≤ ‖rademacherL2 𝕜 a‖ at h231 simpa only [LinearIsometry.norm_map] using h232233end RademacherMap234235theorem scalarCharacterLp_real (p : ℝ≥0∞) (F : Finset ℕ) :236 scalarCharacterLp ℝ p F = characterLp p F := by237 apply Lp.ext238 exact (coeFn_scalarCharacterLp ℝ p F).trans (coeFn_characterLp p F).symm239240theorem rademacherL1_real_sum (s : Finset ℕ) (a : ℕ → ℝ) :241 rademacherL1 ℝ (∑ j ∈ s, lp.single 2 j (a j)) =242 ContinuousMap.toLp 1 haar ℝ (rademacherPolynomial s a) := by243 simp only [map_sum, rademacherL1_single, scalarCharacterLp_real,244 rademacherPolynomial]245 apply Finset.sum_congr rfl246 intro j hj247 have heq : ContinuousMap.const Group (a j) * characterContinuous {j} =248 a j • characterContinuous {j} := by ext x; rfl249 rw [heq, map_smul, toLp_characterContinuous]250251theorem norm_rademacherL1_real_sum (s : Finset ℕ) (a : ℕ → ℝ) :252 ‖rademacherL1 ℝ (∑ j ∈ s, lp.single 2 j (a j))‖ =253 ∫ x, ‖rademacherPolynomial s a x‖ ∂haar := by254 rw [rademacherL1_real_sum, L1.norm_eq_integral_norm]255 exact integral_congr_ae ((ContinuousMap.coeFn_toLp haar256 (rademacherPolynomial s a)).fun_comp norm)257258theorem norm_ell2_real_sum (s : Finset ℕ) (a : ℕ → ℝ) :259 ‖∑ j ∈ s, lp.single 2 j (a j)‖ = Real.sqrt (∑ j ∈ s, a j ^ 2) := by260 have h := lp.norm_sum_single (E := fun _ : ℕ => ℝ) (p := 2) (by norm_num) a s261 norm_num [Real.rpow_natCast, Real.norm_eq_abs, sq_abs] at h262 rw [← h, Real.sqrt_sq (norm_nonneg _)]263264theorem rademacherL1_real_sum_lower (s : Finset ℕ) (a : ℕ → ℝ) :265 ‖∑ j ∈ s, lp.single 2 j (a j)‖ ≤266 8 * ‖rademacherL1 ℝ (∑ j ∈ s, lp.single 2 j (a j))‖ := by267 rw [norm_ell2_real_sum, norm_rademacherL1_real_sum]268 exact rademacher_firstMoment_lower s a269270theorem rademacherL1_real_lower (a : Ell2 ℝ) :271 ‖a‖ ≤ 8 * ‖rademacherL1 ℝ a‖ := by272 have hsum := lp.hasSum_single (p := 2) (by norm_num) a273 exact le_of_tendsto_of_tendsto' hsum.norm274 ((((rademacherL1 ℝ).continuous.tendsto a).comp hsum).norm.const_mul 8)275 (fun s => rademacherL1_real_sum_lower s a)276277theorem rademacherL1_real_antilipschitz : AntilipschitzWith 8 (rademacherL1 ℝ) :=278 (rademacherL1 ℝ).antilipschitz_of_bound rademacherL1_real_lower279280theorem rademacherL1_real_injective : Function.Injective (rademacherL1 ℝ) :=281 rademacherL1_real_antilipschitz.injective282283theorem rademacherL1_real_isClosed_range : IsClosed (Set.range (rademacherL1 ℝ)) :=284 rademacherL1_real_antilipschitz.isClosed_range (rademacherL1 ℝ).uniformContinuous285286/-- The genuine Hilbert space ell2 is continuously linearly isomorphic to the287closed first Walsh chaos in Haar L1. -/288def rademacherL1_real_equivRange : Ell2 ℝ ≃L[ℝ] (rademacherL1 ℝ).range :=289 (rademacherL1 ℝ).equivRange rademacherL1_real_injective rademacherL1_real_isClosed_range290291theorem haarL1_contains_ell2_real : ContainsIsomorphicCopy ℝ (Ell2 ℝ) (Lp ℝ 1 haar) :=292 ⟨(rademacherL1 ℝ).range, rademacherL1_real_isClosed_range, ⟨rademacherL1_real_equivRange⟩⟩293294section ScalarEmbedding295296variable (𝕜 : Type*) [RCLike 𝕜]297298def scalarRademacherPolynomial (s : Finset ℕ) (a : ℕ → 𝕜) : C(Group, 𝕜) :=299 ∑ j ∈ s, a j • scalarCharacterContinuous 𝕜 {j}300301theorem re_scalarRademacherPolynomial (s : Finset ℕ) (a : ℕ → 𝕜) (x : Group) :302 RCLike.re (scalarRademacherPolynomial 𝕜 s a x) =303 rademacherPolynomial s (fun j => RCLike.re (a j)) x := by304 simp [scalarRademacherPolynomial, rademacherPolynomial, scalarCharacterContinuous,305 scalarCharacter, characterContinuous, RCLike.mul_re]306307theorem im_scalarRademacherPolynomial (s : Finset ℕ) (a : ℕ → 𝕜) (x : Group) :308 RCLike.im (scalarRademacherPolynomial 𝕜 s a x) =309 rademacherPolynomial s (fun j => RCLike.im (a j)) x := by310 simp [scalarRademacherPolynomial, rademacherPolynomial, scalarCharacterContinuous,311 scalarCharacter, characterContinuous, RCLike.mul_im]312313theorem rademacherL1_sum (s : Finset ℕ) (a : ℕ → 𝕜) :314 rademacherL1 𝕜 (∑ j ∈ s, lp.single 2 j (a j)) =315 ContinuousMap.toLp 1 haar 𝕜 (scalarRademacherPolynomial 𝕜 s a) := by316 simp only [map_sum, rademacherL1_single, scalarRademacherPolynomial, map_smul,317 toLp_scalarCharacterContinuous]318319theorem norm_rademacherL1_sum (s : Finset ℕ) (a : ℕ → 𝕜) :320 ‖rademacherL1 𝕜 (∑ j ∈ s, lp.single 2 j (a j))‖ =321 ∫ x, ‖scalarRademacherPolynomial 𝕜 s a x‖ ∂haar := by322 rw [rademacherL1_sum, L1.norm_eq_integral_norm]323 exact integral_congr_ae ((ContinuousMap.coeFn_toLp haar324 (scalarRademacherPolynomial 𝕜 s a)).fun_comp norm)325326theorem norm_ell2_sum_le_re_add_im (s : Finset ℕ) (a : ℕ → 𝕜) :327 ‖∑ j ∈ s, lp.single 2 j (a j)‖ ≤328 Real.sqrt (∑ j ∈ s, RCLike.re (a j) ^ 2) +329 Real.sqrt (∑ j ∈ s, RCLike.im (a j) ^ 2) := by330 have h := lp.norm_sum_single (E := fun _ : ℕ => 𝕜) (p := 2) (by norm_num) a s331 norm_num only [ENNReal.toReal_ofNat, Real.rpow_two] at h332 have hsplit : (∑ j ∈ s, ‖a j‖ ^ (2 : ℕ)) =333 (∑ j ∈ s, RCLike.re (a j) ^ 2) + (∑ j ∈ s, RCLike.im (a j) ^ 2) := by334 rw [← Finset.sum_add_distrib]335 apply Finset.sum_congr rfl336 intro j hj337 simpa only [sq] using (RCLike.norm_sq_eq_def (z := a j))338 rw [hsplit] at h339 have hr := Real.sq_sqrt (Finset.sum_nonneg (fun j (_ : j ∈ s) => sq_nonneg (RCLike.re (a j))))340 have hi := Real.sq_sqrt (Finset.sum_nonneg (fun j (_ : j ∈ s) => sq_nonneg (RCLike.im (a j))))341 have hr0 := Real.sqrt_nonneg (∑ j ∈ s, RCLike.re (a j) ^ 2)342 have hi0 := Real.sqrt_nonneg (∑ j ∈ s, RCLike.im (a j) ^ 2)343 nlinarith [norm_nonneg (∑ j ∈ s, lp.single 2 j (a j)), mul_nonneg hr0 hi0]344345theorem rademacherL1_sum_lower (s : Finset ℕ) (a : ℕ → 𝕜) :346 ‖∑ j ∈ s, lp.single 2 j (a j)‖ ≤347 16 * ‖rademacherL1 𝕜 (∑ j ∈ s, lp.single 2 j (a j))‖ := by348 rw [norm_rademacherL1_sum]349 have hint : Integrable (fun x => ‖scalarRademacherPolynomial 𝕜 s a x‖) haar :=350 (scalarRademacherPolynomial 𝕜 s a).continuous.norm.integrable_of_hasCompactSupport351 (HasCompactSupport.of_compactSpace _)352 have hre : (∫ x, ‖rademacherPolynomial s (fun j => RCLike.re (a j)) x‖ ∂haar) ≤353 ∫ x, ‖scalarRademacherPolynomial 𝕜 s a x‖ ∂haar := by354 apply integral_mono (continuous_integrable _).norm hint355 intro x356 change ‖rademacherPolynomial s (fun j => RCLike.re (a j)) x‖ ≤ _357 rw [← re_scalarRademacherPolynomial 𝕜 s a x]358 exact RCLike.norm_re_le_norm _359 have him : (∫ x, ‖rademacherPolynomial s (fun j => RCLike.im (a j)) x‖ ∂haar) ≤360 ∫ x, ‖scalarRademacherPolynomial 𝕜 s a x‖ ∂haar := by361 apply integral_mono (continuous_integrable _).norm hint362 intro x363 change ‖rademacherPolynomial s (fun j => RCLike.im (a j)) x‖ ≤ _364 rw [← im_scalarRademacherPolynomial 𝕜 s a x]365 exact RCLike.norm_im_le_norm _366 have hr := rademacher_firstMoment_lower s (fun j => RCLike.re (a j))367 have hi := rademacher_firstMoment_lower s (fun j => RCLike.im (a j))368 have hn := norm_ell2_sum_le_re_add_im 𝕜 s a369 linarith370371/-- A uniform first-chaos lower bound covering both real and complex scalars. -/372theorem rademacherL1_lower (a : Ell2 𝕜) :373 ‖a‖ ≤ 16 * ‖rademacherL1 𝕜 a‖ := by374 have hsum := lp.hasSum_single (p := 2) (by norm_num) a375 exact le_of_tendsto_of_tendsto' hsum.norm376 ((((rademacherL1 𝕜).continuous.tendsto a).comp hsum).norm.const_mul 16)377 (fun s => rademacherL1_sum_lower 𝕜 s a)378379theorem rademacherL1_antilipschitz : AntilipschitzWith 16 (rademacherL1 𝕜) :=380 (rademacherL1 𝕜).antilipschitz_of_bound (rademacherL1_lower 𝕜)381382theorem rademacherL1_injective : Function.Injective (rademacherL1 𝕜) :=383 (rademacherL1_antilipschitz 𝕜).injective384385theorem rademacherL1_isClosed_range : IsClosed (Set.range (rademacherL1 𝕜)) :=386 (rademacherL1_antilipschitz 𝕜).isClosed_range (rademacherL1 𝕜).uniformContinuous387388def rademacherL1_equivRange : Ell2 𝕜 ≃L[𝕜] (rademacherL1 𝕜).range :=389 (rademacherL1 𝕜).equivRange (rademacherL1_injective 𝕜) (rademacherL1_isClosed_range 𝕜)390391theorem haarL1_contains_ell2 : ContainsIsomorphicCopy 𝕜 (Ell2 𝕜) (Lp 𝕜 1 haar) :=392 ⟨(rademacherL1 𝕜).range, rademacherL1_isClosed_range 𝕜, ⟨rademacherL1_equivRange 𝕜⟩⟩393394/-- A common eigenvalue on coordinate Rademacher functions extends to the whole395closed first chaos by norm convergence of the ell2 series. -/396theorem rademacherL1_eigen (S : Lp 𝕜 1 haar →L[𝕜] Lp 𝕜 1 haar) (c : 𝕜)397 (hS : ∀ j, S (scalarCharacterLp 𝕜 1 {j}) = c • scalarCharacterLp 𝕜 1 {j})398 (a : Ell2 𝕜) : S (rademacherL1 𝕜 a) = c • rademacherL1 𝕜 a := by399 have hs := lp.hasSum_single (p := 2) (by norm_num) a400 have hleft := (S.comp (rademacherL1 𝕜)).hasSum hs401 have hright := (c • rademacherL1 𝕜).hasSum hs402 apply hleft.unique403 convert hright using 1404 · ext j405 simp only [ContinuousLinearMap.comp_apply, rademacherL1_single,406 smul_apply, map_smul, hS, smul_smul]407 rw [mul_comm]408 · rfl409410end ScalarEmbedding411412end PL1.Walsh413414