On complemented subspaces of L1[0,1]L_1[0,1]

PL1/IntrinsicRealParts.lean

All source files · Download exact source

SHA-256: 8f9e5f9835baf4406e876f8f5c3d7c01f68e4649647bf1dee3addfc385f2a6a1

1import PL1.ScalarRealification2import PL1.IntrinsicWalsh34/-! # Actual real and imaginary coordinates of the scalar intrinsic graph -/56noncomputable section7set_option backward.isDefEq.respectTransparency false8open MeasureTheory Filter9open scoped Topology ENNReal NNReal1011namespace PL1.IntrinsicRealParts12open Walsh Noise IntrinsicGraph ScalarRealification ResolventEstimates1314variable (K : Type*) [RCLike K]1516def scalarPart (T : K →L[ℝ] ℝ) : Lp K 1 haar →L[ℝ] Lp ℝ 1 haar :=17  T.compLpL 1 haar1819theorem scalarPart_convolution (T : K →L[ℝ] ℝ) (ν : Measure Walsh.Group)20    [IsProbabilityMeasure ν] (f : Lp K 1 haar) :21    scalarPart K T (convolutionL1 ν f) = convolutionL1 ν (scalarPart K T f) := by22  apply Lp.ext23  filter_upwards [T.coeFn_compLpL (convolutionL1 ν f), coeFn_convolutionL1 ν f,24    convolutionL1_ae_eq_integral_of_ae_eq ν (T.coeFn_compLpL f),25    (integrable_convolution_integrand ν f).prod_right_ae] with x hT hf hconv hint26  change (T.compLpL 1 haar (convolutionL1 ν f)) x = convolutionL1 ν (T.compLpL 1 haar f) x27  rw [hT, hf, hconv]28  exact (T.integral_comp_comm hint).symm2930theorem scalarPart_analysis (T : K →L[ℝ] ℝ) (rates : ℕ → ℝ≥0)31    (n : ℕ) (f : Lp K 1 haar) :32    scalarPart K T ((dyadicSystem K rates).analysis n f) =33      (dyadicSystem ℝ rates).analysis n (scalarPart K T f) := by34  cases n with35  | zero => rfl36  | succ n =>37    let := isProbabilityMeasure_resolventMeasure rates (dyadicTime (n + 1)).property38    change scalarPart K T ((((dyadicRatio ^ (n + 1))⁻¹ : ℝ) : K) •39      (f - resolventL1 K rates (dyadicTime (n + 1)) f)) = _40    rw [← RCLike.real_smul_eq_coe_smul, map_smul, map_sub]41    rw [show resolventL1 K rates (dyadicTime (n + 1)) =42      convolutionL1 (resolventMeasure rates (dyadicTime (n + 1))) from rfl,43      scalarPart_convolution]44    rfl4546theorem summable_norm_coords (rates : ℕ → ℝ≥0)47    (x : (dyadicSystem K rates).IntrinsicSpace) :48    Summable (fun n => ‖coord (dyadicSystem K rates).analysis n x‖) := by49  change Summable (fun n => ‖(x : lp (fun _ : ℕ => Lp K 1 haar) 1) n‖)50  simpa using (lp.memℓp (x : lp (fun _ : ℕ => Lp K 1 haar) 1)).summable51    (by norm_num : (0 : ℝ) < (1 : ℝ≥0∞).toReal)5253theorem summable_norm_parts (T : K →L[ℝ] ℝ) (rates : ℕ → ℝ≥0)54    (x : (dyadicSystem K rates).IntrinsicSpace) :55    Summable (fun n => ‖scalarPart K T (coord (dyadicSystem K rates).analysis n x)‖) := by56  have hs := summable_norm_coords K rates x57  exact Summable.of_nonneg_of_le (fun _ => norm_nonneg _)58    (fun n => (scalarPart K T).le_opNorm (coord (dyadicSystem K rates).analysis n x))59    (hs.mul_left ‖scalarPart K T‖)6061def partLinear (T : K →L[ℝ] ℝ) (rates : ℕ → ℝ≥0) :62    (dyadicSystem K rates).IntrinsicSpace →ₗ[ℝ] (dyadicSystem ℝ rates).IntrinsicSpace where63  toFun x := ⟨⟨fun n => scalarPart K T (coord (dyadicSystem K rates).analysis n x),64    memℓp_gen (by simpa using summable_norm_parts K T rates x)⟩, by65      intro n66      change scalarPart K T (coord (dyadicSystem K rates).analysis n x) = _67      rw [coord_eq, scalarPart_analysis]68      rfl⟩69  map_add' x y := by70    apply Subtype.ext71    apply lp.ext72    funext n73    change scalarPart K T (coord (dyadicSystem K rates).analysis n (x + y)) = _74    simp only [map_add]75    rfl76  map_smul' c x := by77    apply Subtype.ext78    apply lp.ext79    funext n80    simp only [RingHom.id_apply, Submodule.coe_smul, lp.coeFn_smul, Pi.smul_apply]81    change scalarPart K T (coord (dyadicSystem K rates).analysis n (c • x)) =82      c • scalarPart K T (coord (dyadicSystem K rates).analysis n x)83    have hm : coord (dyadicSystem K rates).analysis n (c • x) =84        c • coord (dyadicSystem K rates).analysis n x := by85      exact ((coord (dyadicSystem K rates).analysis n).restrictScalars ℝ).map_smul c x86    exact (congrArg (scalarPart K T) hm).trans (map_smul (scalarPart K T) c _)8788theorem coord_partLinear (T : K →L[ℝ] ℝ) (rates : ℕ → ℝ≥0)89    (n : ℕ) (x : (dyadicSystem K rates).IntrinsicSpace) :90    coord (dyadicSystem ℝ rates).analysis n (partLinear K T rates x) =91      scalarPart K T (coord (dyadicSystem K rates).analysis n x) := rfl9293theorem norm_partLinear_le (T : K →L[ℝ] ℝ) (rates : ℕ → ℝ≥0)94    (x : (dyadicSystem K rates).IntrinsicSpace) :95    ‖partLinear K T rates x‖ ≤ ‖scalarPart K T‖ * ‖x‖ := by96  rw [IntrinsicGraph.norm_eq_tsum, IntrinsicGraph.norm_eq_tsum, ← tsum_mul_left]97  exact Summable.tsum_le_tsum (fun n => (scalarPart K T).le_opNorm _)98    (summable_norm_parts K T rates x)99    ((summable_norm_coords K rates x).mul_left ‖scalarPart K T‖)100101def part (T : K →L[ℝ] ℝ) (rates : ℕ → ℝ≥0) :102    (dyadicSystem K rates).IntrinsicSpace →L[ℝ] (dyadicSystem ℝ rates).IntrinsicSpace :=103  (partLinear K T rates).mkContinuous ‖scalarPart K T‖ (norm_partLinear_le K T rates)104105def realPart (rates : ℕ → ℝ≥0) := part K (@RCLike.reCLM K _) rates106def imagPart (rates : ℕ → ℝ≥0) := part K (@RCLike.imCLM K _) rates107108def imL1 : Lp K 1 haar →L[ℝ] Lp ℝ 1 haar := scalarPart K (@RCLike.imCLM K _)109110theorem coeFn_imL1 (f : Lp K 1 haar) :111    imL1 K f =ᵐ[haar] fun x => RCLike.im (f x) :=112  (@RCLike.imCLM K _).coeFn_compLpL f113114@[simp] theorem coord_realPart (rates : ℕ → ℝ≥0) (n : ℕ)115    (x : (dyadicSystem K rates).IntrinsicSpace) :116    coord (dyadicSystem ℝ rates).analysis n (realPart K rates x) =117      reL1 K (coord (dyadicSystem K rates).analysis n x) := rfl118119@[simp] theorem coord_imagPart (rates : ℕ → ℝ≥0) (n : ℕ)120    (x : (dyadicSystem K rates).IntrinsicSpace) :121    coord (dyadicSystem ℝ rates).analysis n (imagPart K rates x) =122      imL1 K (coord (dyadicSystem K rates).analysis n x) := rfl123124theorem norm_ofRealL1_le (f : Lp ℝ 1 haar) : ‖ofRealL1 K f‖ ≤ ‖f‖ := by125  have h : ‖ofRealL1 K‖ ≤ 1 := by126    apply (ContinuousLinearMap.norm_compLpL_le (@RCLike.ofRealCLM K _)).trans127    apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one128    intro x129    simp only [RCLike.ofRealCLM_apply, RCLike.norm_ofReal, Real.norm_eq_abs, one_mul, le_refl]130  exact ((ofRealL1 K).le_opNorm f).trans131    (by simpa only [one_mul] using mul_le_mul_of_nonneg_right h (norm_nonneg f))132133theorem re_add_im (f : Lp K 1 haar) :134    ofRealL1 K (reL1 K f) + (RCLike.I : K) • ofRealL1 K (imL1 K f) = f := by135  apply Lp.ext136  filter_upwards [Lp.coeFn_add (ofRealL1 K (reL1 K f))137      ((RCLike.I : K) • ofRealL1 K (imL1 K f)),138    Lp.coeFn_smul (RCLike.I : K) (ofRealL1 K (imL1 K f)),139    coeFn_ofRealL1 K (reL1 K f), coeFn_ofRealL1 K (imL1 K f),140    coeFn_reL1 K f, coeFn_imL1 K f] with x ha hs hor hoi hr hi141  rw [ha]142  change ofRealL1 K (reL1 K f) x +143    ((RCLike.I : K) • ofRealL1 K (imL1 K f)) x = f x144  rw [hs, hor]145  change (reL1 K f x : K) + (RCLike.I : K) * ofRealL1 K (imL1 K f) x = _146  rw [hoi, hr, hi, mul_comm RCLike.I, RCLike.re_add_im]147148theorem norm_l1_le_parts (f : Lp K 1 haar) : ‖f‖ ≤ ‖reL1 K f‖ + ‖imL1 K f‖ := by149  have hI : ‖(RCLike.I : K)‖ ≤ 1 := by rw [RCLike.norm_I]; split_ifs <;> norm_num150  calc151    ‖f‖ = ‖ofRealL1 K (reL1 K f) + (RCLike.I : K) • ofRealL1 K (imL1 K f)‖ :=152      congrArg norm (re_add_im K f).symm153    _ ≤ ‖ofRealL1 K (reL1 K f)‖ + ‖(RCLike.I : K) • ofRealL1 K (imL1 K f)‖ := norm_add_le _ _154    _ ≤ ‖reL1 K f‖ + ‖imL1 K f‖ := by155      apply add_le_add (norm_ofRealL1_le K _)156      rw [norm_smul]157      exact (mul_le_mul_of_nonneg_right hI (norm_nonneg _)).trans158        (by simpa using norm_ofRealL1_le K (imL1 K f))159160/-- The scalar intrinsic norm is bounded by the sum of the two actual real161intrinsic norms. In particular the pair of real-part maps is injective. -/162theorem norm_le_parts (rates : ℕ → ℝ≥0) (x : (dyadicSystem K rates).IntrinsicSpace) :163    ‖x‖ ≤ ‖realPart K rates x‖ + ‖imagPart K rates x‖ := by164  rw [IntrinsicGraph.norm_eq_tsum, IntrinsicGraph.norm_eq_tsum,165    IntrinsicGraph.norm_eq_tsum]166  simp_rw [coord_realPart, coord_imagPart]167  change (∑' n, ‖coord (dyadicSystem K rates).analysis n x‖) ≤168    (∑' n, ‖scalarPart K (@RCLike.reCLM K _) (coord (dyadicSystem K rates).analysis n x)‖) +169    ∑' n, ‖scalarPart K (@RCLike.imCLM K _) (coord (dyadicSystem K rates).analysis n x)‖170  rw [← (summable_norm_parts K (@RCLike.reCLM K _) rates x).tsum_add171    (summable_norm_parts K (@RCLike.imCLM K _) rates x)]172  exact Summable.tsum_le_tsum (fun n => norm_l1_le_parts K _)173    (summable_norm_coords K rates x)174    ((summable_norm_parts K (@RCLike.reCLM K _) rates x).add175      (summable_norm_parts K (@RCLike.imCLM K _) rates x))176177theorem parts_injective (rates : ℕ → ℝ≥0) :178    Function.Injective (fun x : (dyadicSystem K rates).IntrinsicSpace =>179      (realPart K rates x, imagPart K rates x)) := by180  intro x y h181  apply sub_eq_zero.mp182  apply norm_eq_zero.mp183  have hbound := norm_le_parts K rates (x - y)184  have hr : realPart K rates x = realPart K rates y := congrArg Prod.fst h185  have hi : imagPart K rates x = imagPart K rates y := congrArg Prod.snd h186  rw [map_sub, map_sub, hr, hi,187    sub_self, sub_self, norm_zero, add_zero] at hbound188  exact le_antisymm hbound (norm_nonneg _)189190end PL1.IntrinsicRealParts191