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

PL1/SingularResolvents.lean

All source files · Download exact source

SHA-256: 49bc4f99a015396c2e35c5c1a69924a6fcbd264d01c728016400cbff0f1f9400

1import PL1.ConcreteResolvents2import PL1.SingularCarrier3import PL1.SingularConvolution4import PL1.ScalarRealification56/-! # Singular averaged resolvents and the actual intrinsic RNP obstruction -/78noncomputable section9open MeasureTheory ProbabilityTheory10open scoped NNReal ENNReal1112namespace PL1.Noise1314open Walsh Carrier ExponentialTime1516theorem resolventMeasure_carrier (rates : ℕ → ℝ≥0) {t : ℝ} (ht : 0 < t)17    (N : Set Walsh.Group) (hN : MeasurableSet N)18    (hnoise : ∀ u : ℝ≥0, measure rates u N = 1) : resolventMeasure rates t N = 1 := by19  let := isProbabilityMeasure_timeMeasure ht20  rw [resolventMeasure, Measure.bind_apply hN (kernel rates).aemeasurable]21  simp only [kernel_apply, hnoise, lintegral_one, measure_univ]2223theorem schur_resolvent_commonSet (t : PositiveTime) (d : ℕ) :24    resolventMeasure schurRates t (commonSet d) = 1 :=25  resolventMeasure_carrier schurRates t.property (commonSet d) (measurableSet_commonSet d)26    (fun u => noise_commonSet_eq_one u d)2728theorem constant_resolvent_commonSet (t : PositiveTime) (d : ℕ) :29    resolventMeasure constantRates t (commonSet d) = 1 :=30  resolventMeasure_carrier constantRates t.property (commonSet d) (measurableSet_commonSet d)31    (fun u => noise_constantRates_commonSet_eq_one u d)3233theorem schur_resolvent_singular (t : PositiveTime) :34    resolventMeasure schurRates t ⟂ₘ haar := by35  let := isProbabilityMeasure_resolventMeasure schurRates t.property36  refine ⟨(commonSet 0)ᶜ, (measurableSet_commonSet 0).compl, ?_, ?_⟩37  · rw [measure_compl (measurableSet_commonSet 0) (measure_ne_top _ _),38      measure_univ, schur_resolvent_commonSet, tsub_self]39  · simpa only [compl_compl] using haar_commonSet_eq_zero 04041theorem constant_resolvent_singular (t : PositiveTime) :42    resolventMeasure constantRates t ⟂ₘ haar := by43  let := isProbabilityMeasure_resolventMeasure constantRates t.property44  refine ⟨(commonSet 0)ᶜ, (measurableSet_commonSet 0).compl, ?_, ?_⟩45  · rw [measure_compl (measurableSet_commonSet 0) (measure_ne_top _ _),46      measure_univ, constant_resolvent_commonSet, tsub_self]47  · simpa only [compl_compl] using haar_commonSet_eq_zero 04849/-- A charged Haar-null carrier of the zeroth resolvent forces failure of the50full reviewed vector-measure RNP in the actual real intrinsic Banach space. -/51theorem intrinsic_not_RNP_of_resolvent_carrier (rates : ℕ → ℝ≥0)52    (N : Set Walsh.Group) (hmN : haar N = 0)53    (hνN : resolventMeasure rates (dyadicTime 0) N ≠ 0) :54    ¬ HasRadonNikodymProperty.{_, 0} (dyadicSystem ℝ rates).IntrinsicSpace := by55  let := isProbabilityMeasure_resolventMeasure rates (dyadicTime 0).property56  apply SingularConvolution.not_RNP_of_convolution_factorization57    (resolventMeasure rates (dyadicTime 0)) N hmN hνN58    ((dyadicSystem ℝ rates).column 0)59    (IntrinsicGraph.evalZero (dyadicSystem ℝ rates).analysis)60  apply ContinuousLinearMap.ext61  intro f62  rw [ContinuousLinearMap.comp_apply, DyadicSystem.evalZero_column]63  rfl6465theorem schur_intrinsic_not_RNP_real :66    ¬ HasRadonNikodymProperty.{_, 0} (dyadicSystem ℝ schurRates).IntrinsicSpace :=67  intrinsic_not_RNP_of_resolvent_carrier schurRates (commonSet 0)68    (haar_commonSet_eq_zero 0) (by rw [schur_resolvent_commonSet]; exact one_ne_zero)6970theorem constant_intrinsic_not_RNP_real :71    ¬ HasRadonNikodymProperty.{_, 0} (dyadicSystem ℝ constantRates).IntrinsicSpace :=72  intrinsic_not_RNP_of_resolvent_carrier constantRates (commonSet 0)73    (haar_commonSet_eq_zero 0) (by rw [constant_resolvent_commonSet]; exact one_ne_zero)7475theorem schur_projection_range_not_RNP_real :76    ¬ HasRadonNikodymProperty.{_, 0} (projection ℝ schurRates).range := by77  change ¬ HasRadonNikodymProperty.{_, 0} (dyadicSystem ℝ schurRates).projection.range78  rw [DyadicSystem.projection_range]79  exact schur_intrinsic_not_RNP_real8081theorem constant_projection_range_not_RNP_real :82    ¬ HasRadonNikodymProperty.{_, 0} (projection ℝ constantRates).range := by83  change ¬ HasRadonNikodymProperty.{_, 0} (dyadicSystem ℝ constantRates).projection.range84  rw [DyadicSystem.projection_range]85  exact constant_intrinsic_not_RNP_real8687/-- The same obstruction holds for the underlying real space of the scalar88construction, with exactly its inherited norm. -/89theorem intrinsic_not_RNP_of_resolvent_carrier_scalar (𝕜 : Type*) [RCLike 𝕜]90    (rates : ℕ → ℝ≥0) (N : Set Walsh.Group) (hmN : haar N = 0)91    (hνN : resolventMeasure rates (dyadicTime 0) N ≠ 0) :92    ¬ @HasRadonNikodymProperty.{_, 0}93      (UnderlyingReal 𝕜 (dyadicSystem 𝕜 rates).IntrinsicSpace)94      (inferInstanceAs (NormedAddCommGroup (dyadicSystem 𝕜 rates).IntrinsicSpace))95      (NormedSpace.restrictScalars ℝ 𝕜 (dyadicSystem 𝕜 rates).IntrinsicSpace) := by96  let : NormedSpace ℝ (dyadicSystem 𝕜 rates).IntrinsicSpace :=97    NormedSpace.restrictScalars ℝ 𝕜 (dyadicSystem 𝕜 rates).IntrinsicSpace98  let := IsScalarTower.restrictScalars ℝ 𝕜 (dyadicSystem 𝕜 rates).IntrinsicSpace99  let := isProbabilityMeasure_resolventMeasure rates (dyadicTime 0).property100  apply ScalarRealification.not_RNP_of_scalar_convolution_factorization 𝕜101    (resolventMeasure rates (dyadicTime 0)) N hmN hνN102    ((dyadicSystem 𝕜 rates).column 0)103    (IntrinsicGraph.evalZero (dyadicSystem 𝕜 rates).analysis)104  apply ContinuousLinearMap.ext105  intro f106  rw [ContinuousLinearMap.comp_apply, DyadicSystem.evalZero_column]107  rfl108109theorem schur_intrinsic_not_RNP (𝕜 : Type*) [RCLike 𝕜] :110    ¬ @HasRadonNikodymProperty.{_, 0}111      (UnderlyingReal 𝕜 (dyadicSystem 𝕜 schurRates).IntrinsicSpace)112      (inferInstanceAs (NormedAddCommGroup (dyadicSystem 𝕜 schurRates).IntrinsicSpace))113      (NormedSpace.restrictScalars ℝ 𝕜 (dyadicSystem 𝕜 schurRates).IntrinsicSpace) :=114  intrinsic_not_RNP_of_resolvent_carrier_scalar 𝕜 schurRates (commonSet 0)115    (haar_commonSet_eq_zero 0) (by rw [schur_resolvent_commonSet]; exact one_ne_zero)116117theorem constant_intrinsic_not_RNP (𝕜 : Type*) [RCLike 𝕜] :118    ¬ @HasRadonNikodymProperty.{_, 0}119      (UnderlyingReal 𝕜 (dyadicSystem 𝕜 constantRates).IntrinsicSpace)120      (inferInstanceAs (NormedAddCommGroup (dyadicSystem 𝕜 constantRates).IntrinsicSpace))121      (NormedSpace.restrictScalars ℝ 𝕜 (dyadicSystem 𝕜 constantRates).IntrinsicSpace) :=122  intrinsic_not_RNP_of_resolvent_carrier_scalar 𝕜 constantRates (commonSet 0)123    (haar_commonSet_eq_zero 0) (by rw [constant_resolvent_commonSet]; exact one_ne_zero)124125theorem schur_projection_range_not_RNP (𝕜 : Type*) [RCLike 𝕜] :126    ¬ @HasRadonNikodymProperty.{_, 0} (UnderlyingReal 𝕜 (projection 𝕜 schurRates).range)127      (inferInstanceAs (NormedAddCommGroup (projection 𝕜 schurRates).range))128      (NormedSpace.restrictScalars ℝ 𝕜 (projection 𝕜 schurRates).range) := by129  change ¬ @HasRadonNikodymProperty.{_, 0}130    ((dyadicSystem 𝕜 schurRates).projection.range)131    (inferInstanceAs (NormedAddCommGroup (dyadicSystem 𝕜 schurRates).projection.range))132    (NormedSpace.restrictScalars ℝ 𝕜 (dyadicSystem 𝕜 schurRates).projection.range)133  rw [DyadicSystem.projection_range]134  exact schur_intrinsic_not_RNP 𝕜135136theorem constant_projection_range_not_RNP (𝕜 : Type*) [RCLike 𝕜] :137    ¬ @HasRadonNikodymProperty.{_, 0} (UnderlyingReal 𝕜 (projection 𝕜 constantRates).range)138      (inferInstanceAs (NormedAddCommGroup (projection 𝕜 constantRates).range))139      (NormedSpace.restrictScalars ℝ 𝕜 (projection 𝕜 constantRates).range) := by140  change ¬ @HasRadonNikodymProperty.{_, 0}141    ((dyadicSystem 𝕜 constantRates).projection.range)142    (inferInstanceAs (NormedAddCommGroup (dyadicSystem 𝕜 constantRates).projection.range))143    (NormedSpace.restrictScalars ℝ 𝕜 (dyadicSystem 𝕜 constantRates).projection.range)144  rw [DyadicSystem.projection_range]145  exact constant_intrinsic_not_RNP 𝕜146147end PL1.Noise148