PL1/CompactRestriction.lean

All source files · Download exact source

SHA-256: e5431ff61cd8fe8fce96031af312f54a5bfddb541075995c665beb8205cfd79c

1import PL1.DunfordPettis2import PL1.LpInclusions34/-!5# Compact restriction and uniform approximation67This isolates the elementary compactness part of the L1 Dunford–Pettis8criterion. The uniform approximation hypothesis is explicit; in the concrete9application it is supplied by uniform integrability of weakly convergent L110sequences.11-/1213noncomputable section14open Filter15open scoped Topology1617namespace PL11819variable {𝕜 E F G : Type*} [RCLike 𝕜]20  [NormedAddCommGroup E] [NormedSpace 𝕜 E]21  [NormedAddCommGroup F] [NormedSpace 𝕜 F]22  [NormedAddCommGroup G] [NormedSpace 𝕜 G]2324def HasUniformBoundedApproximations (V : G →L[𝕜] E) (x : ℕ → E) : Prop :=25  ∀ ε > 0, ∃ M : ℝ, ∀ n, ∃ y : G, ‖y‖ ≤ M ∧ ‖x n - V y‖ < ε2627theorem totallyBounded_image_of_uniform_approximation28    (T : E →L[𝕜] F) (V : G →L[𝕜] E)29    (hTV : IsCompactOperator (T.comp V)) (x : ℕ → E)30    (hx : HasUniformBoundedApproximations V x) :31    TotallyBounded (Set.range (fun n => T (x n))) := by32  apply Metric.totallyBounded_iff.mpr33  intro ε hε34  have hδ : 0 < ε / (2 * (‖T‖ + 1)) := by positivity35  obtain ⟨M, hM⟩ := hx _ hδ36  obtain ⟨K, hK, hTK⟩ := hTV.image_subset_compact_of_bounded37    (Metric.isBounded_closedBall (x := (0 : G)) (r := M))38  obtain ⟨D, hD, hcover⟩ := Metric.totallyBounded_iff.mp hK.totallyBounded39    (ε / 2) (half_pos hε)40  refine ⟨D, hD, ?_⟩41  rintro z ⟨n, rfl⟩42  obtain ⟨y, hy, hxy⟩ := hM n43  have hyK : T (V y) ∈ K := hTK ⟨y, by simpa only [Metric.mem_closedBall,44    dist_zero_right] using hy, rfl⟩45  obtain ⟨w, hwD, hwy⟩ := Set.mem_iUnion₂.mp (hcover hyK)46  apply Set.mem_iUnion₂.mpr47  refine ⟨w, hwD, ?_⟩48  have hsmall : dist (T (x n)) (T (V y)) < ε / 2 := by49    rw [dist_eq_norm, ← map_sub]50    have hd := (lt_div_iff₀ (show 0 < 2 * (‖T‖ + 1) by positivity)).mp hxy51    have hb := T.le_opNorm (x n - V y)52    nlinarith [norm_nonneg (x n - V y)]53  exact (dist_triangle (T (x n)) (T (V y)) w).trans_lt54    (by have := Metric.mem_ball.mp hwy; linarith)5556/-- A compact restriction sends uniformly approximable weak sequences to norm57convergent sequences, by relative compactness and uniqueness of weak limits. -/58theorem weaklyConverges_image_of_compact_restriction [CompleteSpace F]59    (T : E →L[𝕜] F) (V : G →L[𝕜] E)60    (hTV : IsCompactOperator (T.comp V)) {x : ℕ → E} {a : E}61    (hx : WeaklyConverges 𝕜 E x a) (happrox : HasUniformBoundedApproximations V x) :62    Tendsto (fun n => T (x n)) atTop (𝓝 (T a)) :=63  (hx.map T).tendsto_of_totallyBounded64    (totallyBounded_image_of_uniform_approximation T V hTV x happrox)6566theorem isDunfordPettis_of_compact_restriction [CompleteSpace F]67    (T : E →L[𝕜] F) (V : G →L[𝕜] E)68    (hTV : IsCompactOperator (T.comp V))69    (happrox : ∀ (x : ℕ → E) (a : E), WeaklyConverges 𝕜 E x a →70      HasUniformBoundedApproximations V x) : IsDunfordPettis T :=71  fun x a hx => weaklyConverges_image_of_compact_restriction T V hTV hx (happrox x a hx)7273end PL174