PL1/MetricApproximation.lean

All source files · Download exact source

SHA-256: c016e3cef28c4ac540d32b5d654bc34047f23f896117f31b346b78481bf01b6d

1import PL1.IntrinsicWalshBlocks23/-! # Metric approximation in the actual intrinsic norm45Contractive finite-dimensional expectations approximate the identity uniformly6on each compact set. This is the metric approximation property, expressed7directly with bounded finite-rank operators and compact sets.8-/910noncomputable section11open Filter Set12open scoped Topology NNReal1314namespace PL11516variable {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]1718def HasMetricApproximationProperty (𝕜 E : Type*) [RCLike 𝕜]19    [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Prop :=20  ∀ K : Set E, IsCompact K → ∀ ε : ℝ, 0 < ε →21    ∃ T : E →L[𝕜] E, ‖T‖ ≤ 1 ∧ FiniteDimensional 𝕜 T.range ∧22      ∀ x ∈ K, ‖T x - x‖ < ε2324theorem contractive_strong_approximation_uniform_on_compact25    (T : ℕ → E →L[𝕜] E) (hT : ∀ n, ‖T n‖ ≤ 1)26    (hlim : ∀ x, Tendsto (fun n => T n x) atTop (𝓝 x))27    (K : Set E) (hK : IsCompact K) (ε : ℝ) (hε : 0 < ε) :28    ∀ᶠ n in atTop, ∀ x ∈ K, ‖T n x - x‖ < ε := by29  obtain ⟨s, _, hs, hcover⟩ := hK.finite_cover_balls (show 0 < ε / 4 by positivity)30  have hev : ∀ᶠ n in atTop, ∀ y ∈ s, ‖T n y - y‖ < ε / 2 := by31    apply hs.eventually_all.mpr32    intro y _33    have hy := (tendsto_iff_norm_sub_tendsto_zero.mp (hlim y)).eventually_lt_const34      (show 0 < ε / 2 by positivity)35    exact hy36  filter_upwards [hev] with n hn37  intro x hx38  obtain ⟨y, hy, hxy⟩ := mem_iUnion₂.mp (hcover hx)39  have hdist : ‖x - y‖ < ε / 4 := by simpa only [Metric.mem_ball, dist_eq_norm] using hxy40  have hbound : ‖T n x - T n y‖ ≤ ‖x - y‖ := by41    rw [← map_sub]42    exact ((T n).le_opNorm (x - y)).trans (by43      simpa only [one_mul] using mul_le_mul_of_nonneg_right (hT n) (norm_nonneg (x - y)))44  have hyx : ‖y - x‖ = ‖x - y‖ := norm_sub_rev _ _45  have htriangle : ‖T n x - x‖ ≤ ‖T n x - T n y‖ + ‖T n y - y‖ + ‖y - x‖ := by46    calc47      ‖T n x - x‖ = ‖(T n x - T n y) + (T n y - y) + (y - x)‖ := by congr 1; abel48      _ ≤ _ := (norm_add_le _ _).trans (add_le_add (norm_add_le _ _) le_rfl)49  have hmiddle := hn y hy50  linarith5152theorem hasMetricApproximationProperty_of_contractive_finiteDimensional_approximation53    (T : ℕ → E →L[𝕜] E) (hT : ∀ n, ‖T n‖ ≤ 1)54    (hfin : ∀ n, FiniteDimensional 𝕜 (T n).range)55    (hlim : ∀ x, Tendsto (fun n => T n x) atTop (𝓝 x)) :56    HasMetricApproximationProperty 𝕜 E := by57  intro K hK ε hε58  obtain ⟨n, hn⟩ := (contractive_strong_approximation_uniform_on_compact T hT hlim K hK ε hε).exists59  exact ⟨T n, hT n, hfin n, hn⟩6061namespace Noise6263theorem norm_intrinsicExpectation_eq_one (𝕜 : Type*) [RCLike 𝕜]64    (rates : ℕ → ℝ≥0) (m : ℕ) : ‖intrinsicExpectation 𝕜 rates m‖ = 1 := by65  apply le_antisymm (norm_intrinsicExpectation_le 𝕜 rates m)66  have hx : intrinsicCharacter 𝕜 rates ∅ ≠ 0 :=67    (linearIndependent_intrinsicCharacter 𝕜 rates).ne_zero ∅68  have hf : intrinsicExpectation 𝕜 rates m (intrinsicCharacter 𝕜 rates ∅) =69      intrinsicCharacter 𝕜 rates ∅ := by simp [intrinsicExpectation_character]70  have hn := (intrinsicExpectation 𝕜 rates m).le_opNorm (intrinsicCharacter 𝕜 rates ∅)71  rw [hf] at hn72  nlinarith [norm_pos_iff.mpr hx]7374theorem intrinsic_hasMetricApproximationProperty (𝕜 : Type*) [RCLike 𝕜] (rates : ℕ → ℝ≥0) :75    HasMetricApproximationProperty 𝕜 (dyadicSystem 𝕜 rates).IntrinsicSpace :=76  hasMetricApproximationProperty_of_contractive_finiteDimensional_approximation77    (intrinsicExpectation 𝕜 rates) (norm_intrinsicExpectation_le 𝕜 rates)78    (intrinsicExpectation_range_finiteDimensional 𝕜 rates) (tendsto_intrinsicExpectation 𝕜 rates)7980end Noise81end PL182