English
For a directed monotone family of subspaces whose supremum has a dense projection, the star-projection tends to the element itself.
Русский
Для направленной монотонной семьи подппространств, у которых верхняя граница имеет плотную проекцию, проекция-звезда стремится к самому элементу.
LaTeX
$$$(U_t)^{*} x \to x$ as t → ∞, given topological closure conditions$$
Lean4
/-- Given a monotone family `U` of complete submodules of `E` and a fixed `x : E`,
the orthogonal projection of `x` on `U i` tends to the orthogonal projection of `x` on
`(⨆ i, U i).topologicalClosure` along `atTop`. -/
theorem starProjection_tendsto_closure_iSup {ι : Type*} [Preorder ι] (U : ι → Submodule 𝕜 E)
[∀ i, (U i).HasOrthogonalProjection] [(⨆ i, U i).topologicalClosure.HasOrthogonalProjection] (hU : Monotone U)
(x : E) :
Filter.Tendsto (fun i => (U i).starProjection x) atTop (𝓝 ((⨆ i, U i).topologicalClosure.starProjection x)) :=
by
refine .of_neBot_imp fun h ↦ ?_
cases atTop_neBot_iff.mp h
let y := (⨆ i, U i).topologicalClosure.starProjection x
have proj_x : ∀ i, (U i).orthogonalProjection x = (U i).orthogonalProjection y := fun i =>
(orthogonalProjection_starProjection_of_le ((le_iSup U i).trans (iSup U).le_topologicalClosure) _).symm
suffices ∀ ε > 0, ∃ I, ∀ i ≥ I, ‖(U i).starProjection y - y‖ < ε by
simpa only [starProjection_apply, proj_x, NormedAddCommGroup.tendsto_atTop] using this
intro ε hε
obtain ⟨a, ha, hay⟩ : ∃ a ∈ ⨆ i, U i, dist y a < ε :=
by
have y_mem : y ∈ (⨆ i, U i).topologicalClosure := Submodule.coe_mem _
rw [← SetLike.mem_coe, Submodule.topologicalClosure_coe, Metric.mem_closure_iff] at y_mem
exact y_mem ε hε
rw [dist_eq_norm] at hay
obtain ⟨I, hI⟩ : ∃ I, a ∈ U I := by rwa [Submodule.mem_iSup_of_directed _ hU.directed_le] at ha
refine ⟨I, fun i (hi : I ≤ i) => ?_⟩
rw [norm_sub_rev, starProjection_minimal]
refine lt_of_le_of_lt ?_ hay
change _ ≤ ‖y - (⟨a, hU hi hI⟩ : U i)‖
exact ciInf_le ⟨0, Set.forall_mem_range.mpr fun _ => norm_nonneg _⟩ _
