PL1/DyadicTrace.lean

All source files · Download exact source

SHA-256: cfe72c9871c6710289a28233b73e918e33b849f75fc4ef615535d9d817b3cb62

1import PL1.TraceBounds2import Mathlib.MeasureTheory.Function.Floor34/-! # Concrete dyadic traces on the reviewed interval L1 space56The dyadic index is clamped at the two ends. Thus the cells partition all of7the real line, while their restrictions to [0,1] are the usual dyadic intervals.8Outside values disappear in the reviewed restricted Lebesgue measure.9-/1011noncomputable section12set_option autoImplicit false13open MeasureTheory Filter14open scoped ENNReal BigOperators Topology1516namespace PL1.DyadicTrace1718theorem intervalMeasure_probability : IsProbabilityMeasure intervalMeasure := by19  constructor20  simp [intervalMeasure, Real.volume_Icc]2122attribute [local instance] intervalMeasure_probability2324def index (n : ℕ) (x : ℝ) : ℕ := min ⌊(2 : ℝ) ^ n * x⌋₊ (2 ^ n - 1)2526theorem measurable_index (n : ℕ) : Measurable (index n) :=27  (Nat.measurable_floor.comp (measurable_const.mul measurable_id)).min measurable_const2829theorem index_lt (n : ℕ) (x : ℝ) : index n x < 2 ^ n :=30  lt_of_le_of_lt (min_le_right _ _) (Nat.sub_lt (pow_pos (by decide) n) (by decide))3132def cell (n i : ℕ) : Set ℝ := {x | index n x = i}3334theorem measurableSet_cell (n i : ℕ) : MeasurableSet (cell n i) :=35  (measurable_index n) (measurableSet_singleton i)3637theorem pairwiseDisjoint_cell (n : ℕ) : Pairwise (fun i j => Disjoint (cell n i) (cell n j)) := by38  intro i j hij39  apply Set.disjoint_left.mpr40  intro x hxi hxj41  exact hij (hxi.symm.trans hxj)4243theorem cover_cell (n : ℕ) : (⋃ i ∈ Finset.range (2 ^ n), cell n i) = Set.univ := by44  ext x45  simp only [Set.mem_iUnion, Set.mem_univ, iff_true]46  exact ⟨index n x, Finset.mem_range.mpr (index_lt n x), rfl⟩4748variable {𝕜 : Type*} [RCLike 𝕜]4950/-- The canonical restriction of an interval L1 operator to interval L-infinity. -/51def restrictLinfty (R : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜) :52    Lp 𝕜 ∞ intervalMeasure →L[𝕜] IntervalL1 𝕜 :=53  R.comp (ProbabilityLp.inclusion intervalMeasure 1 ∞ le_top)5455def trace (n : ℕ) (R : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜) : 𝕜 :=56  TraceBounds.partitionTrace intervalMeasure (cell n) (measurableSet_cell n)57    (Finset.range (2 ^ n)) R5859theorem trace_eq (n : ℕ) (R : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜) :60    trace n R = ∑ i ∈ Finset.range (2 ^ n), ∫ x in cell n i,61      R (indicatorConstLp 1 (measurableSet_cell n i)62        (measure_ne_top intervalMeasure (cell n i)) (1 : 𝕜)) x ∂intervalMeasure :=63  TraceBounds.partitionTrace_eq _ _ _ _ _6465theorem norm_trace_le (n : ℕ) (R : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜) :66    ‖trace n R‖ ≤ ‖restrictLinfty R‖ :=67  TraceBounds.norm_partitionTrace_le _ _ _ _ (pairwiseDisjoint_cell n) _6869theorem trace_id (n : ℕ) : trace n (ContinuousLinearMap.id 𝕜 (IntervalL1 𝕜)) = 1 :=70  TraceBounds.partitionTrace_id _ _ _ _ (pairwiseDisjoint_cell n) (cover_cell n)7172theorem one_le_norm_id_sub (R : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜)73    (hR : Tendsto (fun n => trace n R) atTop (𝓝 0)) :74    1 ≤ ‖restrictLinfty (ContinuousLinearMap.id 𝕜 (IntervalL1 𝕜) - R)‖ :=75  TraceBounds.one_le_norm_id_sub_of_trace_tendsto_zero _ cell measurableSet_cell76    (fun n => Finset.range (2 ^ n)) pairwiseDisjoint_cell cover_cell R hR7778theorem trace_tendsto_zero_of_approximation (R : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜)79    (T : ℕ → IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜)80    (hT : ∀ m, Tendsto (fun n => trace n (T m)) atTop (𝓝 0))81    (happrox : Tendsto (fun m => ‖restrictLinfty (R - T m)‖) atTop (𝓝 0)) :82    Tendsto (fun n => trace n R) atTop (𝓝 0) :=83  TraceBounds.trace_tendsto_zero_of_approximation _ cell measurableSet_cell84    (fun n => Finset.range (2 ^ n)) pairwiseDisjoint_cell R T hT happrox8586end PL1.DyadicTrace87