controlled_prod_of_mem_closure_range

English

If a bounded homomorphism j with range in F has b in the closure of its range, then one can lift b via f to E with control constants C and ε, so f maps some a with j(a) = b up to a bounded norm by C+ε times the norm of a.

Русский

Пусть j: E→F гомоморфизм, диапазон которого ограничен; если b находится в замыкании диапазона j, то существует предобраз g в E с нормой ограниченной нормой C+ε.

LaTeX

$$$\\forall b\\in closure(j(Range)),\\exists a:\\mathbb{N}\\to E:\\ Tendsto (\\dots)\\ to nhds(b)\\text{ with bounded norms: } \\|j(a_0)/b\\|

Lean4

@[to_additive]
theorem controlled_prod_of_mem_closure_range {j : E →* F} {b : F} (hb : b ∈ closure (j.range : Set F)) {f : ℕ → ℝ}
    (b_pos : ∀ n, 0 < f n) :
    ∃ a : ℕ → E,
      Tendsto (fun n => ∏ i ∈ range (n + 1), j (a i)) atTop (𝓝 b) ∧
        ‖j (a 0) / b‖ < f 0 ∧ ∀ n, 0 < n → ‖j (a n)‖ < f n :=
  by
  obtain ⟨v, sum_v, v_in, hv₀, hv_pos⟩ := controlled_prod_of_mem_closure hb b_pos
  choose g hg using v_in
  exact ⟨g, by simpa [← hg] using sum_v, by simpa [hg 0] using hv₀, fun n hn => by simpa [hg] using hv_pos n hn⟩

Похожие утверждения