PL1/IntervalSubtype.lean

All source files · Download exact source

SHA-256: 45375de994d388627936d1b1801748ffa111bbda39fb012fefb866b68d11d34d

1import PL1.Definitions2import Mathlib.MeasureTheory.Constructions.UnitInterval3import Mathlib.Topology.Order.ProjIcc45/-! # The interval subtype and the reviewed restricted-measure L1 space -/67noncomputable section8open MeasureTheory Set9open scoped ENNReal unitInterval1011namespace PL1.IntervalSubtype1213def clamp : ℝ → unitInterval := Set.projIcc 0 1 zero_le_one1415theorem clamp_coe (x : unitInterval) : clamp (x : ℝ) = x :=16  Set.projIcc_of_mem zero_le_one x.property1718theorem measurePreserving_clamp :19    MeasurePreserving clamp intervalMeasure (volume : Measure unitInterval) where20  measurable := continuous_projIcc.measurable21  map_eq := by22    change Measure.map clamp (volume.restrict (Icc (0 : ℝ) 1)) = _23    rw [← unitInterval.measurePreserving_coe.map_eq,24      Measure.map_map (show Measurable clamp from continuous_projIcc.measurable)25        measurable_subtype_coe]26    have h : clamp ∘ ((↑) : unitInterval → ℝ) = id := funext clamp_coe27    rw [h, Measure.map_id]2829variable (K : Type*) [RCLike K]3031/-- Extend a subtype function using the interval clamp; values outside the interval are ignored. -/32def toInterval : Lp K 1 (volume : Measure unitInterval) →ₗᵢ[K] IntervalL1 K :=33  Lp.compMeasurePreservingₗᵢ K clamp measurePreserving_clamp3435/-- Restrict the actual real-domain L1 class to the interval subtype. -/36def fromInterval : IntervalL1 K →ₗᵢ[K] Lp K 1 (volume : Measure unitInterval) :=37  Lp.compMeasurePreservingₗᵢ K ((↑) : unitInterval → ℝ) unitInterval.measurePreserving_coe3839theorem toInterval_fromInterval (f : IntervalL1 K) :40    toInterval K (fromInterval K f) = f := by41  apply Lp.ext42  have hfrom := measurePreserving_clamp.quasiMeasurePreserving.ae_eq_comp43    (Lp.coeFn_compMeasurePreserving f unitInterval.measurePreserving_coe)44  filter_upwards [Lp.coeFn_compMeasurePreserving (fromInterval K f) measurePreserving_clamp,45    hfrom, ae_restrict_mem measurableSet_Icc] with x hto hf hx46  change toInterval K (fromInterval K f) x = _ at hto ⊢47  rw [hto]48  change fromInterval K f (clamp x) = f x49  change fromInterval K f (clamp x) = f (clamp x : ℝ) at hf50  rw [hf]51  rw [clamp, Set.projIcc_of_mem zero_le_one hx]5253/-- The actual isometric identification, oriented from subtype L1 to the reviewed IntervalL1. -/54def equiv : Lp K 1 (volume : Measure unitInterval) ≃ₗᵢ[K] IntervalL1 K :=55  LinearIsometryEquiv.ofSurjective (toInterval K)56    (fun f => ⟨fromInterval K f, toInterval_fromInterval K f⟩)5758theorem equiv_apply (f : Lp K 1 (volume : Measure unitInterval)) :59    equiv K f = toInterval K f := rfl6061end PL1.IntervalSubtype62