PL1/IntervalWalsh.lean

All source files · Download exact source

SHA-256: 74f0448ad39714f927eb61e1dd4b6fab5968d6c7e81ad68faa1f9bb893663139

1import PL1.IntervalRetraction2import PL1.IntervalSubtype3import PL1.ProjectionRetract45/-!6# Actual interval transport for the Walsh ell1 ambient space78The maps are constructed through the explicit geometric probability model,9a measurable interval sampler, and its regular conditional distribution.10The resulting interval projection does not need an assumed ambient isomorphism.11-/1213noncomputable section14open MeasureTheory15open scoped ENNReal1617namespace PL1.IntervalWalsh1819variable (𝕜 : Type*) [RCLike 𝕜]2021/-- Concrete isometric embedding of the Walsh ell1 ambient space in interval L1. -/22def walshSumEmbedding : L1Sum (Lp 𝕜 1 Walsh.haar) →ₗᵢ[𝕜] IntervalL1 𝕜 :=23  (IntervalSubtype.equiv 𝕜).toLinearIsometry.comp24    ((IntervalRetraction.pullback (IntervalModel.probabilityMeasure Walsh.haar)).comp25      IntervalModel.walshSumProbabilityEquiv.toLinearIsometry)2627/-- Concrete averaging retraction from interval L1 to the Walsh ell1 ambient space. -/28def walshSumRetraction : IntervalL1 𝕜 →L[𝕜] L1Sum (Lp 𝕜 1 Walsh.haar) :=29  IntervalModel.walshSumProbabilityEquiv.symm.toContinuousLinearEquiv.toContinuousLinearMap.comp30    ((IntervalRetraction.retraction (IntervalModel.probabilityMeasure Walsh.haar)).comp31      (IntervalSubtype.equiv 𝕜).symm.toContinuousLinearEquiv.toContinuousLinearMap)3233@[simp] theorem walshSumRetraction_embedding (x : L1Sum (Lp 𝕜 1 Walsh.haar)) :34    walshSumRetraction 𝕜 (walshSumEmbedding 𝕜 x) = x := by35  change IntervalModel.walshSumProbabilityEquiv.symm36    (IntervalRetraction.retraction (IntervalModel.probabilityMeasure Walsh.haar)37      ((IntervalSubtype.equiv 𝕜).symm ((IntervalSubtype.equiv 𝕜)38        (IntervalRetraction.pullback (IntervalModel.probabilityMeasure Walsh.haar)39          (IntervalModel.walshSumProbabilityEquiv x))))) = x40  rw [LinearIsometryEquiv.symm_apply_apply, IntervalRetraction.retraction_pullback,41    LinearIsometryEquiv.symm_apply_apply]4243theorem norm_walshSumRetraction_le : ‖walshSumRetraction 𝕜‖ ≤ 1 := by44  apply ContinuousLinearMap.opNorm_le_bound _ (by norm_num)45  intro x46  change ‖IntervalModel.walshSumProbabilityEquiv.symm47    (IntervalRetraction.retraction (IntervalModel.probabilityMeasure Walsh.haar)48      ((IntervalSubtype.equiv 𝕜).symm x))‖ ≤ 1 * ‖x‖49  rw [LinearIsometryEquiv.norm_map, one_mul]50  calc51    _ ≤ ‖IntervalRetraction.retraction (𝕜 := 𝕜) (IntervalModel.probabilityMeasure Walsh.haar)‖ *52        ‖(IntervalSubtype.equiv 𝕜).symm x‖ := ContinuousLinearMap.le_opNorm _ _53    _ ≤ 1 * ‖(IntervalSubtype.equiv 𝕜).symm x‖ :=54      mul_le_mul_of_nonneg_right (IntervalRetraction.norm_retraction_le _) (norm_nonneg _)55    _ = ‖x‖ := by rw [one_mul, LinearIsometryEquiv.norm_map]5657/-- The concrete contractive retract needed to transport either actual projection58onto the reviewed interval L1 space, over both real and complex scalars. -/59def walshSumContractiveRetract :60    ContractiveRetract 𝕜 (L1Sum (Lp 𝕜 1 Walsh.haar)) (IntervalL1 𝕜) where61  embedding := walshSumEmbedding 𝕜62  retraction := walshSumRetraction 𝕜63  left_inv := walshSumRetraction_embedding 𝕜64  norm_retraction_le := norm_walshSumRetraction_le 𝕜6566end PL1.IntervalWalsh6768