LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Analytic.Inverse

`FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos` theorem FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F), 0 < p.radius → 0 < (p.rightInv i).radius This theorem states that if a formal multilinear series, denoted as 'p', has a positive radius of convergence, then the radius of convergence of its right inverse, denoted as '(p.rightInv i)', is also positive. This theorem applies to a formal multilinear series p between normed spaces E and F over a nontrivially normed field 𝕜, with 'i' being a continuous linear equivalence between E and F. More concisely: If `p` is a formal multilinear series with positive radius of convergence between normed spaces E and F over a nontrivially normed field, and `i` is a continuous linear equivalence between E and F, then the radius of convergence of `p.rightInv i` is positive.
`FormalMultilinearSeries.comp_rightInv` theorem FormalMultilinearSeries.comp_rightInv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F), p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i → p 0 = 0 → p.comp (p.rightInv i) = FormalMultilinearSeries.id 𝕜 F The theorem `FormalMultilinearSeries.comp_rightInv` states that for any non-trivially normed field `𝕜`, normed additive commutative groups `E` and `F` with respective normed spaces over `𝕜`, a formal multilinear series `p` from `E` to `F` and a continuous linear equivalence `i` from `E` to `F`, if the first term of the series `p` is the continuous multilinear embedding of `i`, and the constant term of `p` is zero, then the composition of `p` with its right inverse equals the identity formal multilinear series over `F`. This shows that the right inverse of a formal multilinear series indeed works as expected under certain conditions. More concisely: Given a non-trivially normed field `𝕜`, normed additive commutative groups `E` and `F` with respective normed spaces over `𝕜`, a formal multilinear series `p` from `E` to `F` with zero constant term, and a continuous linear equivalence `i` from `E` to `F` such that `p`'s first term is `i`, then `p` composed with `p`'s right inverse equals the identity formal multilinear series over `F`.
`FormalMultilinearSeries.leftInv_eq_rightInv` theorem FormalMultilinearSeries.leftInv_eq_rightInv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F), p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i → p.leftInv i = p.rightInv i This theorem states that for any non-trivially normed field 𝕜 and normed spaces E and F, given a formal multilinear series 'p' and a continuous linear equivalence 'i' between E and F, if the first term of series 'p' is the inverse of the continuous multilinear curry function applied to 'i', then the left and right inverses of 'p' are equal. This result is not immediately apparent from the definition of the inverses, but it is a consequence of the uniqueness of inverses coming from the fact that composition is associative on formal multilinear series. More concisely: For any non-trivially normed fields 𝕜 and normed spaces E and F, if there exists a continuous linear equivalence i between E and F such that the first term of the multilinear series p is the inverse of the curried i, then the left and right inverses of p are equal.
`FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1` theorem FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1 : ∀ (n : ℕ) (p : ℕ → ℝ), (∀ (k : ℕ), 0 ≤ p k) → ∀ {r a : ℝ}, 0 ≤ r → 0 ≤ a → ((Finset.Ico 2 (n + 1)).sum fun k => a ^ k * {c \| 1 < c.length}.toFinset.sum fun c => r ^ c.length * Finset.univ.prod fun j => p (c.blocksFun j)) ≤ (Finset.Ico 2 (n + 1)).sum fun j => r ^ j * ((Finset.Ico 1 n).sum fun k => a ^ k * p k) ^ j This theorem, named "FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1", states that for any natural number `n` and a sequence of non-negative real numbers `p : ℕ → ℝ`, and for any non-negative real numbers `r` and `a`, the sum over the finite set of integers from 2 to `n+1` (inclusive of 2 but exclusive of `n+1`) of the product of `a` to the power of `k` and the sum over all sequences `c` of length greater than 1 of `r` to the power of the length of `c` times the product of `p` applied to the elements of `c`, is less than or equal to the sum, over the same finite set of integers, of `r` to the power of `j` times the sum, over the finite set of integers from 1 to `n` (inclusive of 1, exclusive of `n`), of `a` to the power of `k` times `p(k)`, all raised to the power of `j`. In less formal terms, this theorem provides an upper bound for the sum of a certain sequence of terms. The terms in this sequence are each a product of a power of `a` times a sum over certain sequences `c`, where each term in the sum is a product of a power of `r` and a product involving `p` applied to elements of `c`. The upper bound is expressed as the sum of another sequence of terms, which involve powers of `r` and the sum of a different sequence involving powers of `a` and `p(k)`. More concisely: For natural number $n$ and non-negative real sequence $p$, and non-negative real numbers $r$ and $a$, the sum of products of powers of $a$ and sums of powers of $r$ and products of $p$ over certain indices, is bounded above by the sum of products of powers of $r$ and sums of powers of $a$ and $p(k)$ over different indices.
`FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2` theorem FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}, 2 ≤ n + 1 → ∀ (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) {r a C : ℝ}, 0 ≤ r → 0 ≤ a → 0 ≤ C → (∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n) → ((Finset.Ico 1 (n + 1)).sum fun k => a ^ k * ‖p.rightInv i k‖) ≤ ‖↑i.symm‖ * a + ‖↑i.symm‖ * C * (Finset.Ico 2 (n + 1)).sum fun k => (r * (Finset.Ico 1 n).sum fun j => a ^ j * ‖p.rightInv i j‖) ^ k This theorem, `FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2`, provides a technical lemma used to control the growth of coefficients of an inverse in a formal multilinear series. Specifically, it bounds the explicit expression for the sum `∑_{k a ^ k * ‖p.rightInv i k‖` is bounded above by `‖↑i.symm‖ * a + ‖↑i.symm‖ * C * (Finset.Ico 2 (n + 1)).sum fun k => (r * (Finset.Ico 1 n).sum fun j => a ^ j * ‖p.rightInv i j‖) ^ k`. More concisely: Given a formal multilinear series over a normed field with a nonnegative radius of convergence and assuming certain conditions, the norm of the sum of the products of coefficients and their inverse norms up to order `n+1` is bounded by a constant times the sum of the norms of the inverse coefficients up to order `n` raised to the power of `k` for `k` in the interval `[1, n+1]`, plus a constant times the sum of the norms of the `n-th` term scaled by the radius of convergence raised to the power of `n`.
`FormalMultilinearSeries.leftInv_comp` theorem FormalMultilinearSeries.leftInv_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F), p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i → (p.leftInv i).comp p = FormalMultilinearSeries.id 𝕜 E This theorem states that, for every nontrivially normed field `𝕜`, every normed additive commutative group `E`, every normed space over `𝕜` and `E`, every normed additive commutative group `F`, another normed space over `𝕜` and `F`, a formal multilinear series `p` that maps `E` to `F`, and a continuous linear equivalence `i` between `E` and `F`, if the first term of the formal multilinear series `p` is the continuous multilinear version of the inverse of `i`, then the composition of the left inverse of `p` (with respect to `i`) and `p` is the identity formal multilinear series on `E` over `𝕜`. Here, the identity formal multilinear series is defined such that all its coefficients are `0` except for `n=1` where it is the identity. More concisely: Given a nontrivially normed field `𝕜`, normed spaces `E` and `F` over `𝕜` with a continuous linear equivalence `i` between them, a formal multilinear series `p: E →ₗ[𝕜] F` with the first term being the inverse of `i` as a continuous multilinear map, then `(p ∘ (pⁱ₋¹)ₗ[𝕜]) = idₗ[𝕜]` on `E`, where `idₗ[𝕜]` is the identity formal multilinear series on `E` over `𝕜`.
`FormalMultilinearSeries.leftInv_removeZero` theorem FormalMultilinearSeries.leftInv_removeZero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F), p.removeZero.leftInv i = p.leftInv i This theorem states that the left inverse of a formal multilinear series does not depend on the zeroth coefficient. In other words, if we have a formal multilinear series `p` and an isomorphism `i` between normed vector spaces `E` and `F` over a nontrivial normed field `𝕜`, then removing the zeroth coefficient from `p` (i.e., `p.removeZero`) and calculating the left inverse gives the same result as directly calculating the left inverse of `p`. More concisely: Given a formal multilinear series `p` over a nontrivial normed field `𝕜`, an isomorphism `i` between normed vector spaces `E` and `F`, and assuming the left inverse `x` of `p` exists, then `x` is equal to the left inverse of `p.removeZero`.
`FormalMultilinearSeries.rightInv_removeZero` theorem FormalMultilinearSeries.rightInv_removeZero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F), p.removeZero.rightInv i = p.rightInv i This theorem states that the right inverse of a formal multilinear series over a nontrivially normed field remains unchanged when the zeroth coefficient of the series is removed. This is true for all series `(p : FormalMultilinearSeries 𝕜 E F)` where `𝕜` is the nontrivially normed field, `E` is a normed add commutative group space, and `F` is another normed add commutative group space, and `i : E ≃L[𝕜] F` is a continuous linear equivalence between `E` and `F`. More concisely: The right inverse of a formal multilinear series between two normed add commutative group spaces remains unchanged when removing its zeroth coefficient, under a continuous linear equivalence between the spaces.