PL1/IntrinsicWalsh.lean

All source files · Download exact source

SHA-256: 746adaa73169f0e68da714303c4a9545ccc7112ddeaa81e347e59ce064a65372

1import PL1.IntrinsicApproximations2import PL1.WalshExpectations34/-! # Actual contractive finite-dimensional approximations in the intrinsic norm -/56noncomputable section7open Filter MeasureTheory8open scoped Topology NNReal ENNReal910namespace PL1.Noise1112open IntrinsicGraph WalshExpectations ResolventEstimates1314variable (𝕜 : Type*) [RCLike 𝕜] (rates : ℕ → ℝ≥0)1516theorem expectation_analysis_commute (m n : ℕ) (f : Lp 𝕜 1 Walsh.haar) :17    expectationL1 𝕜 m ((dyadicSystem 𝕜 rates).analysis n f) =18      (dyadicSystem 𝕜 rates).analysis n (expectationL1 𝕜 m f) := by19  cases n with20  | zero => rfl21  | succ n =>22    change expectationL1 𝕜 m23      (((((dyadicRatio ^ (n + 1))⁻¹ : ℝ) : 𝕜)) •24        (f - resolventL1 𝕜 rates (dyadicTime (n + 1)) f)) = _25    rw [map_smul, map_sub]26    have hc := DFunLike.congr_fun27      (expectationL1_resolvent_commute 𝕜 m rates (dyadicTime (n + 1))) f28    change expectationL1 𝕜 m (resolventL1 𝕜 rates (dyadicTime (n + 1)) f) =29      resolventL1 𝕜 rates (dyadicTime (n + 1)) (expectationL1 𝕜 m f) at hc30    rw [hc]31    rfl3233/-- Finite-coordinate conditional expectation acting on the actual intrinsic graph. -/34def intrinsicExpectation (m : ℕ) :35    (dyadicSystem 𝕜 rates).IntrinsicSpace →L[𝕜] (dyadicSystem 𝕜 rates).IntrinsicSpace :=36  commutingLift (dyadicSystem 𝕜 rates).analysis rfl (expectationL1 𝕜 m)37    (expectation_analysis_commute 𝕜 rates m)3839@[simp] theorem evalZero_intrinsicExpectation (m : ℕ) (x : (dyadicSystem 𝕜 rates).IntrinsicSpace) :40    evalZero (dyadicSystem 𝕜 rates).analysis (intrinsicExpectation 𝕜 rates m x) =41      expectationL1 𝕜 m (evalZero (dyadicSystem 𝕜 rates).analysis x) :=42  evalZero_commutingLift _ _ _ _ _4344@[simp] theorem coord_intrinsicExpectation (m n : ℕ) (x : (dyadicSystem 𝕜 rates).IntrinsicSpace) :45    coord (dyadicSystem 𝕜 rates).analysis n (intrinsicExpectation 𝕜 rates m x) =46      expectationL1 𝕜 m (coord (dyadicSystem 𝕜 rates).analysis n x) :=47  coord_commutingLift _ _ _ _ _ _4849theorem norm_intrinsicExpectation_le (m : ℕ) : ‖intrinsicExpectation 𝕜 rates m‖ ≤ 1 :=50  (norm_commutingLift_le _ _ _ _).trans (norm_expectationL1_le_one 𝕜 m)5152theorem intrinsicExpectation_isProjection (m : ℕ) :53    IsProjection (intrinsicExpectation 𝕜 rates m) :=54  commutingLift_isProjection _ _ _ _ (expectationL1_idempotent 𝕜 m)5556instance intrinsicExpectation_range_finiteDimensional (m : ℕ) :57    FiniteDimensional 𝕜 (intrinsicExpectation 𝕜 rates m).range :=58  commutingLift_range_finiteDimensional _ _ _ _5960theorem intrinsicExpectation_comp_of_le (m n : ℕ) (hmn : m ≤ n) :61    (intrinsicExpectation 𝕜 rates m).comp (intrinsicExpectation 𝕜 rates n) =62      intrinsicExpectation 𝕜 rates m :=63  commutingLift_comp_eq_left _ _ _ _ _ _ (expectationL1_comp_of_le 𝕜 m n hmn)6465theorem tendsto_intrinsicExpectation (x : (dyadicSystem 𝕜 rates).IntrinsicSpace) :66    Tendsto (fun m => intrinsicExpectation 𝕜 rates m x) atTop (𝓝 x) :=67  commutingLift_tendsto _ _ (expectationL1 𝕜) (norm_expectationL1_le_one 𝕜)68    (expectation_analysis_commute 𝕜 rates) (tendsto_expectationL1 𝕜) x6970/-- One family of genuine contractive finite-rank projections converges to71the identity in precisely the inherited intrinsic norm, for every rate sequence. -/72theorem intrinsic_finite_dimensional_approximation :73    ∃ A : ℕ → (dyadicSystem 𝕜 rates).IntrinsicSpace →L[𝕜] (dyadicSystem 𝕜 rates).IntrinsicSpace,74      (∀ m, ‖A m‖ ≤ 1) ∧ (∀ m, IsProjection (A m)) ∧75      (∀ m, FiniteDimensional 𝕜 (A m).range) ∧76      (∀ m n, m ≤ n → (A m).comp (A n) = A m) ∧77      (∀ x, Tendsto (fun m => A m x) atTop (𝓝 x)) :=78  ⟨intrinsicExpectation 𝕜 rates, norm_intrinsicExpectation_le 𝕜 rates,79    intrinsicExpectation_isProjection 𝕜 rates, intrinsicExpectation_range_finiteDimensional 𝕜 rates,80    intrinsicExpectation_comp_of_le 𝕜 rates, tendsto_intrinsicExpectation 𝕜 rates⟩8182end PL1.Noise83