LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.NormedSpace.Banach

`ContinuousLinearMap.exists_preimage_norm_le` theorem ContinuousLinearMap.exists_preimage_norm_le : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomIsometric σ] [inst_4 : RingHomIsometric σ'] {E : Type u_3} [inst_5 : NormedAddCommGroup E] [inst_6 : NormedSpace 𝕜 E] {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜' F] (f : E →SL[σ] F) [inst_9 : CompleteSpace F] [inst_10 : CompleteSpace E], Function.Surjective ⇑f → ∃ C > 0, ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖ The theorem, known as the Banach Open Mapping Theorem, states that for any bounded linear map `f` from a Banach space `E` to another Banach space `F`, if `f` is surjective (i.e., every element in `F` is mapped from some element in `E`), then for any point `y` in `F`, there exists a point `x` in `E` such that `f` maps `x` to `y` and the norm of `x` is less than or equal to some positive constant `C` times the norm of `y`. Here, `𝕜` and `𝕜'` are nontrivial normed fields, `σ` and `σ'` are ring homomorphisms between these fields, and `E` and `F` are normed spaces over these fields. The theorem asserts that the same property holds in the context of complete normed spaces (Banach spaces). More concisely: Given a surjective bounded linear map `f` between Banach spaces `E` and `F` over nontrivial normed fields `𝕜` and `𝕜'`, there exists a constant `C` such that for all `y` in `F`, there exists `x` in `E` with `f(x) = y` and `\\|x\\| ≤ C \\|y\\|`.
`ContinuousLinearMap.isOpenMap` theorem ContinuousLinearMap.isOpenMap : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomIsometric σ] [inst_4 : RingHomIsometric σ'] {E : Type u_3} [inst_5 : NormedAddCommGroup E] [inst_6 : NormedSpace 𝕜 E] {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜' F] (f : E →SL[σ] F) [inst_9 : CompleteSpace F] [inst_10 : CompleteSpace E], Function.Surjective ⇑f → IsOpenMap ⇑f The Banach Open Mapping Theorem states that for any non-trivially normed field 𝕜, and any Banach spaces E and F (which are normed additive commutative groups and also normed spaces over 𝕜), a surjective continuous linear map from E to F is an open map. In other words, for such a map f, every open subset of E gets mapped to an open subset of F. The spaces E and F are required to be complete, meaning that every Cauchy sequence in these spaces converges to a limit in the space itself. More concisely: A surjective continuous linear map between two complete Banach spaces is an open mapping.
`LinearEquiv.continuous_symm` theorem LinearEquiv.continuous_symm : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] [inst_4 : RingHomIsometric σ] [inst_5 : RingHomIsometric σ'] {E : Type u_3} [inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace 𝕜 E] {F : Type u_4} [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜' F] [inst_10 : CompleteSpace F] [inst_11 : CompleteSpace E] (e : E ≃ₛₗ[σ] F), Continuous ⇑e → Continuous ⇑e.symm This theorem states that if we have a bounded linear map (which is a bijection) between two fully complete normed vector spaces over nontrivially normed fields, then the inverse of this map is also a bounded linear map (i.e., it's continuous). The map between the fields is assumed to be a ring homomorphism that preserves distances (i.e., is isometric). More concisely: If f : V₁ → V₂ is a bounded bijection between fully complete normed vector spaces over nontrivially normed fields, and F : K₁ → K₂ is a ring homomorphism and isometry between their fields, then the inverse map f⁻¹ is a bounded linear map from V₂ to V₁.
`LinearMap.continuous_of_isClosed_graph` theorem LinearMap.continuous_of_isClosed_graph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_5} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] (g : E →ₗ[𝕜] F), IsClosed ↑g.graph → Continuous ⇑g The Closed Graph Theorem states that for any linear map between two Banach spaces, if the graph of this map is closed, then the map is continuous. This theorem applies to a non-trivially normed field 𝕜 and two types E and F, both of which are normed additive commutative groups and also normed spaces over 𝕜 that are complete. It asserts that if g is a linear map from E to F and if the graph of g is closed, then the function g is continuous. More concisely: If $E$ and $F$ are Banach spaces over a completely normed field, and the graph of a linear map $g : E \rightarrow F$ is closed, then $g$ is continuous.
`LinearMap.continuous_of_seq_closed_graph` theorem LinearMap.continuous_of_seq_closed_graph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_5} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] (g : E →ₗ[𝕜] F), (∀ (u : ℕ → E) (x : E) (y : F), Filter.Tendsto u Filter.atTop (nhds x) → Filter.Tendsto (⇑g ∘ u) Filter.atTop (nhds y) → y = g x) → Continuous ⇑g This is a version of the closed graph theorem for Banach spaces. The theorem states that for a linear map `f` between two Banach spaces, the map `f` is continuous if and only if for any sequence `uₙ` that converges to `x`, if `f(uₙ)` converges to `y`, then `y = f(x)`. More formally, given a non-trivial normed field `𝕜` and normed additively commutative groups `E` and `F`, which are also normed spaces over `𝕜` and complete, a linear map `g : E →ₗ[𝕜] F` is continuous if for every sequence `u : ℕ → E` that tends to `x` in `E` and the sequence `f(uₙ)` tends to `y` in `F`, then `y = g x`. The theorem leverages the concept of limits (`Filter.Tendsto`), neighborhoods (`nhds`), and the limit towards infinity (`Filter.atTop`). More concisely: A linear map between two Banach spaces is continuous if and only if the image of every convergent sequence in the domain converges to the image of the limit in the codomain.
`ContinuousLinearMap.exists_approx_preimage_norm_le` theorem ContinuousLinearMap.exists_approx_preimage_norm_le : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomIsometric σ] [inst_4 : RingHomIsometric σ'] {E : Type u_3} [inst_5 : NormedAddCommGroup E] [inst_6 : NormedSpace 𝕜 E] {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜' F] (f : E →SL[σ] F) [inst_9 : CompleteSpace F], Function.Surjective ⇑f → ∃ C ≥ 0, ∀ (y : F), ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖ This theorem, which is the first step in the proof of the Banach open mapping theorem utilizing the completeness of `F`, states that given certain conditions on fields `𝕜` and `𝕜'` and normed spaces `E` and `F`, for any continuous linear mapping `f : E →SL[σ] F`, if function `f` is surjective, then there exists a constant `C` greater than or equal to 0 such that for every element `y` in `F`, there exists an element `x` in `E` satisfying two conditions: the distance between `f(x)` and `y` is less than or equal to one-half the norm of `y`, and the norm of `x` is less than or equal to `C` times the norm of `y`. In simpler terms, the image of any element in `F` can be very closely approximated by the image of an element in `E` whose norm is at most `C` times the norm of the original element. More concisely: Given a surjective continuous linear mapping between Banach spaces, there exists a constant such that for any element in the range space, there exists an element in the domain with distance less than half its norm and whose norm is less than or equal to the constant times the norm of the element in the range space.