PL1/ScalarRealification.lean

All source files · Download exact source

SHA-256: 1c948f25ccce706b2fb27f0b113079df764e051810a1445853fcef663156a19d

1import PL1.SingularConvolution23/-!4# Real scalar maps for the complex construction56The canonical real inclusion and real-part maps on Haar L1 intertwine probability7convolution. Consequently a singular convolution over any RCLike scalar field cannot8factor through a real Banach space with the reviewed Radon–Nikodym property.9-/1011noncomputable section12universe u1314open MeasureTheory15open scoped ENNReal Topology1617namespace PL1.ScalarRealification1819open Walsh2021variable (K : Type*) [RCLike K]2223/-- Pointwise inclusion of real L1 functions in scalar-valued L1. -/24def ofRealL1 : Lp ℝ 1 haar →L[ℝ] Lp K 1 haar :=25  (@RCLike.ofRealCLM K _).compLpL 1 haar2627/-- Pointwise real part on scalar-valued L1, as a real bounded linear map. -/28def reL1 : Lp K 1 haar →L[ℝ] Lp ℝ 1 haar :=29  (@RCLike.reCLM K _).compLpL 1 haar3031theorem coeFn_ofRealL1 (f : Lp ℝ 1 haar) :32    ofRealL1 K f =ᵐ[haar] fun x => (f x : K) :=33  (@RCLike.ofRealCLM K _).coeFn_compLpL f3435theorem coeFn_reL1 (f : Lp K 1 haar) :36    reL1 K f =ᵐ[haar] fun x => RCLike.re (f x) :=37  (@RCLike.reCLM K _).coeFn_compLpL f3839theorem reL1_ofRealL1 (f : Lp ℝ 1 haar) : reL1 K (ofRealL1 K f) = f := by40  apply Lp.ext41  filter_upwards [coeFn_reL1 K (ofRealL1 K f), coeFn_ofRealL1 K f] with x hr hc42  simp only [hr, hc, RCLike.ofReal_re]4344theorem ofRealL1_character (F : Finset ℕ) :45    ofRealL1 K (characterLp 1 F) = scalarCharacterLp K 1 F := by46  apply Lp.ext47  filter_upwards [coeFn_ofRealL1 K (characterLp 1 F), coeFn_characterLp 1 F,48    coeFn_scalarCharacterLp K 1 F] with x hc hr hk49  rw [hc, hr, hk]50  rfl5152theorem reL1_scalarCharacter (F : Finset ℕ) :53    reL1 K (scalarCharacterLp K 1 F) = characterLp 1 F := by54  rw [← ofRealL1_character K F, reL1_ofRealL1]5556/-- Taking real parts after scalar-valued convolution recovers real convolution on real inputs. -/57theorem reL1_convolution_ofRealL1 (ν : Measure Walsh.Group) [IsProbabilityMeasure ν] :58    (reL1 K).comp (((convolutionL1 (𝕜 := K) ν).restrictScalars ℝ).comp (ofRealL1 K)) =59      convolutionL1 (𝕜 := ℝ) ν := by60  apply ContinuousLinearMap.ext_on (dense_span_characterLp 1 (by norm_num))61  rintro x ⟨F, rfl⟩62  simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.coe_restrictScalars',63    ofRealL1_character, convolutionL1_scalarCharacter, convolutionL1_character]64  rw [← RCLike.real_smul_eq_coe_smul, map_smul, reL1_scalarCharacter]6566/-- A setwise density for scalar convolution on real input indicators would yield a67forbidden real density after taking real parts. -/68theorem no_setwise_density_of_null_carrier69    (ν : Measure Walsh.Group) [IsProbabilityMeasure ν] (N : Set Walsh.Group)70    (hmN : haar N = 0) (hνN : ν N ≠ 0) :71    ¬ ∃ b : Walsh.Group → Lp K 1 haar, Integrable b haar ∧72      ∀ A : Set Walsh.Group, MeasurableSet A →73        convolutionL1 ν (ofRealL1 K (RNPBridge.indicatorL1 haar A)) = ∫ x in A, b x ∂haar := by74  rintro ⟨b, hb, hrep⟩75  apply SingularConvolution.no_setwise_density_of_null_carrier ν N hmN hνN76  refine ⟨fun x => reL1 K (b x), (reL1 K).integrable_comp hb, ?_⟩77  intro A hA78  rw [(reL1 K).integral_comp_comm hb.integrableOn, ← hrep A hA]79  exact (congrArg (fun T : Lp ℝ 1 haar →L[ℝ] Lp ℝ 1 haar =>80    T (RNPBridge.indicatorL1 haar A)) (reL1_convolution_ofRealL1 K ν)).symm8182/-- Scalar-valued singular convolution cannot factor through any real RNP Banach space.83Only real inputs to the scalar convolution are needed for the obstruction. -/84theorem not_RNP_of_convolution_factorization85    (ν : Measure Walsh.Group) [IsProbabilityMeasure ν] (N : Set Walsh.Group)86    (hmN : haar N = 0) (hνN : ν N ≠ 0)87    {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]88    (S : Lp ℝ 1 haar →L[ℝ] E) (T : E →L[ℝ] Lp K 1 haar)89    (hfac : T.comp S = ((convolutionL1 (𝕜 := K) ν).restrictScalars ℝ).comp (ofRealL1 K)) :90    ¬ HasRadonNikodymProperty.{u, 0} E := by91  apply SingularConvolution.not_RNP_of_convolution_factorization ν N hmN hνN92    S ((reL1 K).comp T)93  rw [ContinuousLinearMap.comp_assoc, hfac]94  exact reL1_convolution_ofRealL1 K ν9596/-- A scalar-linear factorization also obstructs the RNP of the underlying real Banach space. -/97theorem not_RNP_of_scalar_convolution_factorization98    (ν : Measure Walsh.Group) [IsProbabilityMeasure ν] (N : Set Walsh.Group)99    (hmN : haar N = 0) (hνN : ν N ≠ 0)100    {E : Type u} [NormedAddCommGroup E] [NormedSpace K E] [NormedSpace ℝ E]101    [IsScalarTower ℝ K E] [CompleteSpace E]102    (S : Lp K 1 haar →L[K] E) (T : E →L[K] Lp K 1 haar)103    (hfac : T.comp S = convolutionL1 ν) : ¬ HasRadonNikodymProperty.{u, 0} E := by104  apply not_RNP_of_convolution_factorization K ν N hmN hνN105    ((S.restrictScalars ℝ).comp (ofRealL1 K)) (T.restrictScalars ℝ)106  ext1 f107  exact congrArg (fun L : Lp K 1 haar →L[K] Lp K 1 haar => L (ofRealL1 K f)) hfac108109end PL1.ScalarRealification110