From 8e3b53b8c47cb84b9db093c7c1c7efba6a5bdf10 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Sat, 28 Sep 2024 07:48:11 +0000 Subject: [PATCH] feat: the inverse of an analytic partial homeo is also analytic (#17170) We already have the results for the inverse of formal multilinear series, so this PR is mostly just extending our API. However, this showed that our API is suboptimal (notably with respect to the choice of constant coefficients in inverses of formal multilinear series), so we also tweak the definitions of `FormalMultilinearSeries.id` and `FormalMultilinearSeries.leftInv/rightInv` to make them more usable. Co-authored-by: Johan Commelin --- Mathlib/Analysis/Analytic/Basic.lean | 7 + Mathlib/Analysis/Analytic/Composition.lean | 90 +++-- Mathlib/Analysis/Analytic/Inverse.lean | 339 ++++++++++++------ .../Algebra/InfiniteSum/Constructions.lean | 30 +- 4 files changed, 329 insertions(+), 137 deletions(-) diff --git a/Mathlib/Analysis/Analytic/Basic.lean b/Mathlib/Analysis/Analytic/Basic.lean index 011fa34428c159..19befbc09fbe95 100644 --- a/Mathlib/Analysis/Analytic/Basic.lean +++ b/Mathlib/Analysis/Analytic/Basic.lean @@ -822,6 +822,13 @@ theorem HasFPowerSeriesOnBall.tendsto_partialSum Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y))) := (hf.hasSum hy).tendsto_sum_nat +theorem HasFPowerSeriesAt.tendsto_partialSum + (hf : HasFPowerSeriesAt f p x) : + βˆ€αΆ  y in 𝓝 0, Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y))) := by + rcases hf with ⟨r, hr⟩ + filter_upwards [EMetric.ball_mem_nhds (0 : E) hr.r_pos] with y hy + exact hr.tendsto_partialSum hy + open Finset in /-- If a function admits a power series expansion within a ball, then the partial sums `p.partialSum n z` converge to `f (x + y)` as `n β†’ ∞` and `z β†’ y`. Note that `x + z` doesn't need diff --git a/Mathlib/Analysis/Analytic/Composition.lean b/Mathlib/Analysis/Analytic/Composition.lean index 08f88f4cedb1f4..d9bd84e10d143e 100644 --- a/Mathlib/Analysis/Analytic/Composition.lean +++ b/Mathlib/Analysis/Analytic/Composition.lean @@ -331,29 +331,34 @@ section variable (π•œ E) /-- The identity formal multilinear series, with all coefficients equal to `0` except for `n = 1` -where it is (the continuous multilinear version of) the identity. -/ -def id : FormalMultilinearSeries π•œ E E - | 0 => 0 +where it is (the continuous multilinear version of) the identity. We allow an arbitrary +constant coefficient `x`. -/ +def id (x : E) : FormalMultilinearSeries π•œ E E + | 0 => ContinuousMultilinearMap.uncurry0 π•œ _ x | 1 => (continuousMultilinearCurryFin1 π•œ E E).symm (ContinuousLinearMap.id π•œ E) | _ => 0 +@[simp] theorem id_apply_zero (x : E) (v : Fin 0 β†’ E) : + (FormalMultilinearSeries.id π•œ E x) 0 v = x := rfl + /-- The first coefficient of `id π•œ E` is the identity. -/ @[simp] -theorem id_apply_one (v : Fin 1 β†’ E) : (FormalMultilinearSeries.id π•œ E) 1 v = v 0 := +theorem id_apply_one (x : E) (v : Fin 1 β†’ E) : (FormalMultilinearSeries.id π•œ E x) 1 v = v 0 := rfl /-- The `n`th coefficient of `id π•œ E` is the identity when `n = 1`. We state this in a dependent way, as it will often appear in this form. -/ -theorem id_apply_one' {n : β„•} (h : n = 1) (v : Fin n β†’ E) : - (id π•œ E) n v = v ⟨0, h.symm β–Έ zero_lt_one⟩ := by +theorem id_apply_one' (x : E) {n : β„•} (h : n = 1) (v : Fin n β†’ E) : + (id π•œ E x) n v = v ⟨0, h.symm β–Έ zero_lt_one⟩ := by subst n apply id_apply_one /-- For `n β‰  1`, the `n`-th coefficient of `id π•œ E` is zero, by definition. -/ @[simp] -theorem id_apply_ne_one {n : β„•} (h : n β‰  1) : (FormalMultilinearSeries.id π•œ E) n = 0 := by +theorem id_apply_of_one_lt (x : E) {n : β„•} (h : 1 < n) : + (FormalMultilinearSeries.id π•œ E x) n = 0 := by cases' n with n - Β· rfl + Β· contradiction Β· cases n Β· contradiction Β· rfl @@ -361,11 +366,11 @@ theorem id_apply_ne_one {n : β„•} (h : n β‰  1) : (FormalMultilinearSeries.id end @[simp] -theorem comp_id (p : FormalMultilinearSeries π•œ E F) : p.comp (id π•œ E) = p := by +theorem comp_id (p : FormalMultilinearSeries π•œ E F) (x : E) : p.comp (id π•œ E x) = p := by ext1 n dsimp [FormalMultilinearSeries.comp] rw [Finset.sum_eq_single (Composition.ones n)] - Β· show compAlongComposition p (id π•œ E) (Composition.ones n) = p n + Β· show compAlongComposition p (id π•œ E x) (Composition.ones n) = p n ext v rw [compAlongComposition_apply] apply p.congr (Composition.ones_length n) @@ -375,50 +380,60 @@ theorem comp_id (p : FormalMultilinearSeries π•œ E F) : p.comp (id π•œ E) = p rw [Fin.ext_iff, Fin.coe_castLE, Fin.val_mk] Β· show βˆ€ b : Composition n, - b ∈ Finset.univ β†’ b β‰  Composition.ones n β†’ compAlongComposition p (id π•œ E) b = 0 + b ∈ Finset.univ β†’ b β‰  Composition.ones n β†’ compAlongComposition p (id π•œ E x) b = 0 intro b _ hb obtain ⟨k, hk, lt_k⟩ : βˆƒ (k : β„•), k ∈ Composition.blocks b ∧ 1 < k := Composition.ne_ones_iff.1 hb obtain ⟨i, hi⟩ : βˆƒ (i : Fin b.blocks.length), b.blocks[i] = k := List.get_of_mem hk - let j : Fin b.length := ⟨i.val, b.blocks_length β–Έ i.prop⟩ have A : 1 < b.blocksFun j := by convert lt_k ext v rw [compAlongComposition_apply, ContinuousMultilinearMap.zero_apply] apply ContinuousMultilinearMap.map_coord_zero _ j dsimp [applyComposition] - rw [id_apply_ne_one _ _ (ne_of_gt A)] + rw [id_apply_of_one_lt _ _ _ A] rfl Β· simp @[simp] -theorem id_comp (p : FormalMultilinearSeries π•œ E F) (h : p 0 = 0) : (id π•œ F).comp p = p := by +theorem id_comp (p : FormalMultilinearSeries π•œ E F) (v0 : Fin 0 β†’ E) : + (id π•œ F (p 0 v0)).comp p = p := by ext1 n by_cases hn : n = 0 - Β· rw [hn, h] + Β· rw [hn] ext v - rw [comp_coeff_zero', id_apply_ne_one _ _ zero_ne_one] - rfl + simp only [comp_coeff_zero', id_apply_zero] + congr with i + exact i.elim0 Β· dsimp [FormalMultilinearSeries.comp] have n_pos : 0 < n := bot_lt_iff_ne_bot.mpr hn rw [Finset.sum_eq_single (Composition.single n n_pos)] - Β· show compAlongComposition (id π•œ F) p (Composition.single n n_pos) = p n + Β· show compAlongComposition (id π•œ F (p 0 v0)) p (Composition.single n n_pos) = p n ext v - rw [compAlongComposition_apply, id_apply_one' _ _ (Composition.single_length n_pos)] + rw [compAlongComposition_apply, id_apply_one' _ _ _ (Composition.single_length n_pos)] dsimp [applyComposition] refine p.congr rfl fun i him hin => congr_arg v <| ?_ ext; simp Β· show - βˆ€ b : Composition n, - b ∈ Finset.univ β†’ b β‰  Composition.single n n_pos β†’ compAlongComposition (id π•œ F) p b = 0 + βˆ€ b : Composition n, b ∈ Finset.univ β†’ b β‰  Composition.single n n_pos β†’ + compAlongComposition (id π•œ F (p 0 v0)) p b = 0 intro b _ hb - have A : b.length β‰  1 := by simpa [Composition.eq_single_iff_length] using hb + have A : 1 < b.length := by + have : b.length β‰  1 := by simpa [Composition.eq_single_iff_length] using hb + have : 0 < b.length := Composition.length_pos_of_pos b n_pos + omega ext v - rw [compAlongComposition_apply, id_apply_ne_one _ _ A] + rw [compAlongComposition_apply, id_apply_of_one_lt _ _ _ A] rfl Β· simp +/-- Variant of `id_comp` in which the zero coefficient is given by an equality hypothesis instead +of a definitional equality. Useful for rewriting or simplifying out in some situations. -/ +theorem id_comp' (p : FormalMultilinearSeries π•œ E F) (x : F) (v0 : Fin 0 β†’ E) (h : x = p 0 v0) : + (id π•œ F x).comp p = p := by + simp [h] + /-! ### Summability properties of the composition of formal power series -/ @@ -634,11 +649,12 @@ theorem compChangeOfVariables_sum {Ξ± : Type*} [AddCommMonoid Ξ±] (m M N : β„•) /-- The auxiliary set corresponding to the composition of partial sums asymptotically contains all possible compositions. -/ -theorem compPartialSumTarget_tendsto_atTop : - Tendsto (fun N => compPartialSumTarget 0 N N) atTop atTop := by +theorem compPartialSumTarget_tendsto_prod_atTop : + Tendsto (fun (p : β„• Γ— β„•) => compPartialSumTarget 0 p.1 p.2) atTop atTop := by apply Monotone.tendsto_atTop_finset Β· intro m n hmn a ha - have : βˆ€ i, i < m β†’ i < n := fun i hi => lt_of_lt_of_le hi hmn + have : βˆ€ i, i < m.1 β†’ i < n.1 := fun i hi => lt_of_lt_of_le hi hmn.1 + have : βˆ€ i, i < m.2 β†’ i < n.2 := fun i hi => lt_of_lt_of_le hi hmn.2 aesop Β· rintro ⟨n, c⟩ simp only [mem_compPartialSumTarget_iff] @@ -650,29 +666,35 @@ theorem compPartialSumTarget_tendsto_atTop : apply hn simp only [Finset.mem_image_of_mem, Finset.mem_coe, Finset.mem_univ] +/-- The auxiliary set corresponding to the composition of partial sums asymptotically contains +all possible compositions. -/ +theorem compPartialSumTarget_tendsto_atTop : + Tendsto (fun N => compPartialSumTarget 0 N N) atTop atTop := by + apply Tendsto.comp compPartialSumTarget_tendsto_prod_atTop tendsto_atTop_diagonal + /-- Composing the partial sums of two multilinear series coincides with the sum over all compositions in `compPartialSumTarget 0 N N`. This is precisely the motivation for the definition of `compPartialSumTarget`. -/ theorem comp_partialSum (q : FormalMultilinearSeries π•œ F G) (p : FormalMultilinearSeries π•œ E F) - (N : β„•) (z : E) : - q.partialSum N (βˆ‘ i ∈ Finset.Ico 1 N, p i fun _j => z) = - βˆ‘ i ∈ compPartialSumTarget 0 N N, q.compAlongComposition p i.2 fun _j => z := by + (M N : β„•) (z : E) : + q.partialSum M (βˆ‘ i ∈ Finset.Ico 1 N, p i fun _j => z) = + βˆ‘ i ∈ compPartialSumTarget 0 M N, q.compAlongComposition p i.2 fun _j => z := by -- we expand the composition, using the multilinearity of `q` to expand along each coordinate. suffices H : - (βˆ‘ n ∈ Finset.range N, + (βˆ‘ n ∈ Finset.range M, βˆ‘ r ∈ Fintype.piFinset fun i : Fin n => Finset.Ico 1 N, q n fun i : Fin n => p (r i) fun _j => z) = - βˆ‘ i ∈ compPartialSumTarget 0 N N, q.compAlongComposition p i.2 fun _j => z by + βˆ‘ i ∈ compPartialSumTarget 0 M N, q.compAlongComposition p i.2 fun _j => z by simpa only [FormalMultilinearSeries.partialSum, ContinuousMultilinearMap.map_sum_finset] using H -- rewrite the first sum as a big sum over a sigma type, in the finset -- `compPartialSumTarget 0 N N` rw [Finset.range_eq_Ico, Finset.sum_sigma'] -- use `compChangeOfVariables_sum`, saying that this change of variables respects sums - apply compChangeOfVariables_sum 0 N N + apply compChangeOfVariables_sum 0 M N rintro ⟨k, blocks_fun⟩ H - apply congr _ (compChangeOfVariables_length 0 N N H).symm + apply congr _ (compChangeOfVariables_length 0 M N H).symm intros - rw [← compChangeOfVariables_blocksFun 0 N N H] + rw [← compChangeOfVariables_blocksFun 0 M N H] rfl end FormalMultilinearSeries diff --git a/Mathlib/Analysis/Analytic/Inverse.lean b/Mathlib/Analysis/Analytic/Inverse.lean index ccd47d8263a54a..eadc577c91124c 100644 --- a/Mathlib/Analysis/Analytic/Inverse.lean +++ b/Mathlib/Analysis/Analytic/Inverse.lean @@ -4,36 +4,43 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: SΓ©bastien GouΓ«zel -/ import Mathlib.Analysis.Analytic.Composition +import Mathlib.Analysis.Analytic.Linear /-! # Inverse of analytic functions We construct the left and right inverse of a formal multilinear series with invertible linear term, -we prove that they coincide and study their properties (notably convergence). +we prove that they coincide and study their properties (notably convergence). We deduce that the +inverse of an analytic partial homeomorphism is analytic. ## Main statements -* `p.leftInv i`: the formal left inverse of the formal multilinear series `p`, - for `i : E ≃L[π•œ] F` which coincides with `p₁`. -* `p.rightInv i`: the formal right inverse of the formal multilinear series `p`, - for `i : E ≃L[π•œ] F` which coincides with `p₁`. -* `p.leftInv_comp` says that `p.leftInv i` is indeed a left inverse to `p` when `p₁ = i`. -* `p.rightInv_comp` says that `p.rightInv i` is indeed a right inverse to `p` when `p₁ = i`. +* `p.leftInv i x`: the formal left inverse of the formal multilinear series `p`, with constant + coefficient `x`, for `i : E ≃L[π•œ] F` which coincides with `p₁`. +* `p.rightInv i x`: the formal right inverse of the formal multilinear series `p`, with constant + coefficient `x`, for `i : E ≃L[π•œ] F` which coincides with `p₁`. +* `p.leftInv_comp` says that `p.leftInv i x` is indeed a left inverse to `p` when `p₁ = i`. +* `p.rightInv_comp` says that `p.rightInv i x` is indeed a right inverse to `p` when `p₁ = i`. * `p.leftInv_eq_rightInv`: the two inverses coincide. * `p.radius_rightInv_pos_of_radius_pos`: if a power series has a positive radius of convergence, then so does its inverse. +* `PartialHomeomorph.hasFPowerSeriesAt_symm` shows that, if a partial homeomorph has a power series + `p` at a point, with invertible linear part, then the inverse also has a power series at the + image point, given by `p.leftInv`. -/ -open scoped Topology +open scoped Topology ENNReal open Finset Filter -namespace FormalMultilinearSeries +variable {π•œ : Type*} [NontriviallyNormedField π•œ] + {E : Type*} [NormedAddCommGroup E] [NormedSpace π•œ E] + {F : Type*} [NormedAddCommGroup F] [NormedSpace π•œ F] + {G : Type*} [NormedAddCommGroup G] [NormedSpace π•œ G] -variable {π•œ : Type*} [NontriviallyNormedField π•œ] {E : Type*} [NormedAddCommGroup E] - [NormedSpace π•œ E] {F : Type*} [NormedAddCommGroup F] [NormedSpace π•œ F] +namespace FormalMultilinearSeries /-! ### The left inverse of a formal multilinear series -/ @@ -51,27 +58,27 @@ term compensates the rest of the sum, using `i⁻¹` as an inverse to `p₁`. These formulas only make sense when the constant term `pβ‚€` vanishes. The definition we give is general, but it ignores the value of `pβ‚€`. -/ -noncomputable def leftInv (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) : +noncomputable def leftInv (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) (x : E) : FormalMultilinearSeries π•œ F E - | 0 => 0 + | 0 => ContinuousMultilinearMap.uncurry0 π•œ _ x | 1 => (continuousMultilinearCurryFin1 π•œ F E).symm i.symm | n + 2 => -βˆ‘ c : { c : Composition (n + 2) // c.length < n + 2 }, - (leftInv p i (c : Composition (n + 2)).length).compAlongComposition + (leftInv p i x (c : Composition (n + 2)).length).compAlongComposition (p.compContinuousLinearMap i.symm) c @[simp] -theorem leftInv_coeff_zero (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) : - p.leftInv i 0 = 0 := by rw [leftInv] +theorem leftInv_coeff_zero (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) (x : E) : + p.leftInv i x 0 = ContinuousMultilinearMap.uncurry0 π•œ _ x := by rw [leftInv] @[simp] -theorem leftInv_coeff_one (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) : - p.leftInv i 1 = (continuousMultilinearCurryFin1 π•œ F E).symm i.symm := by rw [leftInv] +theorem leftInv_coeff_one (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) (x : E) : + p.leftInv i x 1 = (continuousMultilinearCurryFin1 π•œ F E).symm i.symm := by rw [leftInv] /-- The left inverse does not depend on the zeroth coefficient of a formal multilinear series. -/ -theorem leftInv_removeZero (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) : - p.removeZero.leftInv i = p.leftInv i := by +theorem leftInv_removeZero (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) (x : E) : + p.removeZero.leftInv i x = p.leftInv i x := by ext1 n induction' n using Nat.strongRec' with n IH match n with @@ -87,14 +94,15 @@ theorem leftInv_removeZero (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[ /-- The left inverse to a formal multilinear series is indeed a left inverse, provided its linear term is invertible. -/ -theorem leftInv_comp (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) - (h : p 1 = (continuousMultilinearCurryFin1 π•œ E F).symm i) : (leftInv p i).comp p = id π•œ E := by - ext (n v) +theorem leftInv_comp (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) (x : E) + (h : p 1 = (continuousMultilinearCurryFin1 π•œ E F).symm i) : + (leftInv p i x).comp p = id π•œ E x := by + ext n v classical match n with | 0 => - simp only [leftInv_coeff_zero, ContinuousMultilinearMap.zero_apply, id_apply_ne_one, Ne, - not_false_iff, zero_ne_one, comp_coeff_zero'] + simp only [comp_coeff_zero', leftInv_coeff_zero, ContinuousMultilinearMap.uncurry0_apply, + id_apply_zero] | 1 => simp only [leftInv_coeff_one, comp_coeff_one, h, id_apply_one, ContinuousLinearEquiv.coe_apply, ContinuousLinearEquiv.symm_apply_apply, continuousMultilinearCurryFin1_symm_apply] @@ -111,16 +119,16 @@ theorem leftInv_comp (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) {Composition.ones (n + 2)} := by simp [Set.mem_toFinset (s := {c | Composition.length c < n + 2})] have C : - ((p.leftInv i (Composition.ones (n + 2)).length) + ((p.leftInv i x (Composition.ones (n + 2)).length) fun j : Fin (Composition.ones n.succ.succ).length => p 1 fun _ => v ((Fin.castLE (Composition.length_le _)) j)) = - p.leftInv i (n + 2) fun j : Fin (n + 2) => p 1 fun _ => v j := by + p.leftInv i x (n + 2) fun j : Fin (n + 2) => p 1 fun _ => v j := by apply FormalMultilinearSeries.congr _ (Composition.ones_length _) fun j hj1 hj2 => ?_ exact FormalMultilinearSeries.congr _ rfl fun k _ _ => by congr have D : - (p.leftInv i (n + 2) fun j : Fin (n + 2) => p 1 fun _ => v j) = + (p.leftInv i x (n + 2) fun j : Fin (n + 2) => p 1 fun _ => v j) = -βˆ‘ c ∈ {c : Composition (n + 2) | c.length < n + 2}.toFinset, - (p.leftInv i c.length) (p.applyComposition c v) := by + (p.leftInv i x c.length) (p.applyComposition c v) := by simp only [leftInv, ContinuousMultilinearMap.neg_apply, neg_inj, ContinuousMultilinearMap.sum_apply] convert @@ -128,7 +136,7 @@ theorem leftInv_comp (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) (fun c : Composition (n + 2) => c.length < n + 2) (fun c : Composition (n + 2) => (ContinuousMultilinearMap.compAlongComposition - (p.compContinuousLinearMap (i.symm : F β†’L[π•œ] E)) c (p.leftInv i c.length)) + (p.compContinuousLinearMap (i.symm : F β†’L[π•œ] E)) c (p.leftInv i x c.length)) fun j : Fin (n + 2) => p 1 fun _ : Fin 1 => v j)).symm.trans _ simp only [compContinuousLinearMap_applyComposition, @@ -157,26 +165,26 @@ term compensates the rest of the sum, using `i⁻¹` as an inverse to `p₁`. These formulas only make sense when the constant term `pβ‚€` vanishes. The definition we give is general, but it ignores the value of `pβ‚€`. -/ -noncomputable def rightInv (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) : +noncomputable def rightInv (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) (x : E) : FormalMultilinearSeries π•œ F E - | 0 => 0 + | 0 => ContinuousMultilinearMap.uncurry0 π•œ _ x | 1 => (continuousMultilinearCurryFin1 π•œ F E).symm i.symm | n + 2 => - let q : FormalMultilinearSeries π•œ F E := fun k => if k < n + 2 then rightInv p i k else 0; + let q : FormalMultilinearSeries π•œ F E := fun k => if k < n + 2 then rightInv p i x k else 0; -(i.symm : F β†’L[π•œ] E).compContinuousMultilinearMap ((p.comp q) (n + 2)) @[simp] -theorem rightInv_coeff_zero (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) : - p.rightInv i 0 = 0 := by rw [rightInv] +theorem rightInv_coeff_zero (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) (x : E) : + p.rightInv i x 0 = ContinuousMultilinearMap.uncurry0 π•œ _ x := by rw [rightInv] @[simp] -theorem rightInv_coeff_one (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) : - p.rightInv i 1 = (continuousMultilinearCurryFin1 π•œ F E).symm i.symm := by rw [rightInv] +theorem rightInv_coeff_one (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) (x : E) : + p.rightInv i x 1 = (continuousMultilinearCurryFin1 π•œ F E).symm i.symm := by rw [rightInv] /-- The right inverse does not depend on the zeroth coefficient of a formal multilinear series. -/ -theorem rightInv_removeZero (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) : - p.removeZero.rightInv i = p.rightInv i := by +theorem rightInv_removeZero (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) (x : E) : + p.removeZero.rightInv i x = p.rightInv i x := by ext1 n induction' n using Nat.strongRec' with n IH match n with @@ -216,12 +224,12 @@ theorem comp_rightInv_aux1 {n : β„•} (hn : 0 < n) (p : FormalMultilinearSeries simp [FormalMultilinearSeries.comp, A, Finset.sum_union B, C, -Set.toFinset_setOf, -add_right_inj, -Composition.single_length] -theorem comp_rightInv_aux2 (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) (n : β„•) +theorem comp_rightInv_aux2 (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) (x : E) (n : β„•) (v : Fin (n + 2) β†’ F) : βˆ‘ c ∈ {c : Composition (n + 2) | 1 < c.length}.toFinset, - p c.length (applyComposition (fun k : β„• => ite (k < n + 2) (p.rightInv i k) 0) c v) = + p c.length (applyComposition (fun k : β„• => ite (k < n + 2) (p.rightInv i x k) 0) c v) = βˆ‘ c ∈ {c : Composition (n + 2) | 1 < c.length}.toFinset, - p c.length ((p.rightInv i).applyComposition c v) := by + p c.length ((p.rightInv i x).applyComposition c v) := by have N : 0 < n + 2 := by norm_num refine sum_congr rfl fun c hc => p.congr rfl fun j hj1 hj2 => ?_ have : βˆ€ k, c.blocksFun k < n + 2 := by @@ -232,14 +240,16 @@ theorem comp_rightInv_aux2 (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[ /-- The right inverse to a formal multilinear series is indeed a right inverse, provided its linear term is invertible and its constant term vanishes. -/ -theorem comp_rightInv (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) - (h : p 1 = (continuousMultilinearCurryFin1 π•œ E F).symm i) (h0 : p 0 = 0) : - p.comp (rightInv p i) = id π•œ F := by +theorem comp_rightInv (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) (x : E) + (h : p 1 = (continuousMultilinearCurryFin1 π•œ E F).symm i) : + p.comp (rightInv p i x) = id π•œ F (p 0 0) := by ext (n v) match n with | 0 => - simp only [h0, ContinuousMultilinearMap.zero_apply, id_apply_ne_one, Ne, not_false_iff, - zero_ne_one, comp_coeff_zero'] + simp only [comp_coeff_zero', Matrix.zero_empty, id_apply_zero] + congr + ext i + exact i.elim0 | 1 => simp only [comp_coeff_one, h, rightInv_coeff_one, ContinuousLinearEquiv.apply_symm_apply, id_apply_one, ContinuousLinearEquiv.coe_apply, continuousMultilinearCurryFin1_symm_apply] @@ -248,11 +258,12 @@ theorem comp_rightInv (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F simp [comp_rightInv_aux1 N, h, rightInv, lt_irrefl n, show n + 2 β‰  1 by omega, ← sub_eq_add_neg, sub_eq_zero, comp_rightInv_aux2, -Set.toFinset_setOf] -theorem rightInv_coeff (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) (n : β„•) (hn : 2 ≀ n) : - p.rightInv i n = +theorem rightInv_coeff (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) (x : E) + (n : β„•) (hn : 2 ≀ n) : + p.rightInv i x n = -(i.symm : F β†’L[π•œ] E).compContinuousMultilinearMap (βˆ‘ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition n)), - p.compAlongComposition (p.rightInv i) c) := by + p.compAlongComposition (p.rightInv i x) c) := by match n with | 0 => exact False.elim (zero_lt_two.not_le hn) | 1 => exact False.elim (one_lt_two.not_le hn) @@ -267,26 +278,15 @@ theorem rightInv_coeff (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] /-! ### Coincidence of the left and the right inverse -/ -private theorem leftInv_eq_rightInv_aux (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) - (h : p 1 = (continuousMultilinearCurryFin1 π•œ E F).symm i) (h0 : p 0 = 0) : - leftInv p i = rightInv p i := - calc - leftInv p i = (leftInv p i).comp (id π•œ F) := by simp - _ = (leftInv p i).comp (p.comp (rightInv p i)) := by rw [comp_rightInv p i h h0] - _ = ((leftInv p i).comp p).comp (rightInv p i) := by rw [comp_assoc] - _ = (id π•œ E).comp (rightInv p i) := by rw [leftInv_comp p i h] - _ = rightInv p i := by simp - -/-- The left inverse and the right inverse of a formal multilinear series coincide. This is not at -all obvious from their definition, but it follows from uniqueness of inverses (which comes from the -fact that composition is associative on formal multilinear series). -/ -theorem leftInv_eq_rightInv (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) - (h : p 1 = (continuousMultilinearCurryFin1 π•œ E F).symm i) : leftInv p i = rightInv p i := +theorem leftInv_eq_rightInv (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) (x : E) + (h : p 1 = (continuousMultilinearCurryFin1 π•œ E F).symm i) : + leftInv p i x = rightInv p i x := calc - leftInv p i = leftInv p.removeZero i := by rw [leftInv_removeZero] - _ = rightInv p.removeZero i := by - apply leftInv_eq_rightInv_aux _ _ (by simpa using h) (by simp) - _ = rightInv p i := by rw [rightInv_removeZero] + leftInv p i x = (leftInv p i x).comp (id π•œ F (p 0 0)) := by simp + _ = (leftInv p i x).comp (p.comp (rightInv p i x)) := by rw [comp_rightInv p i _ h] + _ = ((leftInv p i x).comp p).comp (rightInv p i x) := by rw [comp_assoc] + _ = (id π•œ E x).comp (rightInv p i x) := by rw [leftInv_comp p i _ h] + _ = rightInv p i x := by simp [id_comp' _ _ 0] /-! ### Convergence of the inverse of a power series @@ -423,17 +423,17 @@ theorem radius_right_inv_pos_of_radius_pos_aux1 (n : β„•) (p : β„• β†’ ℝ) (hp expression for `βˆ‘_{k β€–p.rightInv i kβ€–) + radius_right_inv_pos_of_radius_pos_aux1 n (fun k => β€–p.rightInv i x kβ€–) (fun k => norm_nonneg _) hr ha /-- If a a formal multilinear series has a positive radius of convergence, then its right inverse also has a positive radius of convergence. -/ -theorem radius_rightInv_pos_of_radius_pos (p : FormalMultilinearSeries π•œ E F) (i : E ≃L[π•œ] F) - (hp : 0 < p.radius) : 0 < (p.rightInv i).radius := by +theorem radius_rightInv_pos_of_radius_pos + {p : FormalMultilinearSeries π•œ E F} {i : E ≃L[π•œ] F} {x : E} + (hp : 0 < p.radius) : 0 < (p.rightInv i x).radius := by obtain ⟨C, r, Cpos, rpos, ple⟩ : βˆƒ (C r : _) (_ : 0 < C) (_ : 0 < r), βˆ€ n : β„•, β€–p nβ€– ≀ C * r ^ n := le_mul_pow_of_radius_pos p hp @@ -508,7 +505,7 @@ theorem radius_rightInv_pos_of_radius_pos (p : FormalMultilinearSeries π•œ E F) exact ⟨a, ha.1, ha.2.1.le, ha.2.2.le⟩ -- check by induction that the partial sums are suitably bounded, using the choice of `a` and the -- inductive control from Lemma `radius_rightInv_pos_of_radius_pos_aux2`. - let S n := βˆ‘ k ∈ Ico 1 n, a ^ k * β€–p.rightInv i kβ€– + let S n := βˆ‘ k ∈ Ico 1 n, a ^ k * β€–p.rightInv i x kβ€– have IRec : βˆ€ n, 1 ≀ n β†’ S n ≀ (I + 1) * a := by apply Nat.le_induction Β· simp only [S] @@ -536,21 +533,159 @@ theorem radius_rightInv_pos_of_radius_pos (p : FormalMultilinearSeries π•œ E F) _ ≀ (I + 1) * a := by gcongr -- conclude that all coefficients satisfy `aⁿ Qβ‚™ ≀ (I + 1) a`. let a' : NNReal := ⟨a, apos.le⟩ - suffices H : (a' : ENNReal) ≀ (p.rightInv i).radius by + suffices H : (a' : ENNReal) ≀ (p.rightInv i x).radius by apply lt_of_lt_of_le _ H -- Prior to leanprover/lean4#2734, this was `exact_mod_cast apos`. simpa only [ENNReal.coe_pos] - apply le_radius_of_bound _ ((I + 1) * a) fun n => ?_ - by_cases hn : n = 0 - Β· have : β€–p.rightInv i nβ€– = β€–p.rightInv i 0β€– := by congr <;> try rw [hn] - simp only [this, norm_zero, zero_mul, rightInv_coeff_zero] - positivity - Β· have one_le_n : 1 ≀ n := bot_lt_iff_ne_bot.2 hn - calc - β€–p.rightInv i nβ€– * (a' : ℝ) ^ n = a ^ n * β€–p.rightInv i nβ€– := mul_comm _ _ - _ ≀ βˆ‘ k ∈ Ico 1 (n + 1), a ^ k * β€–p.rightInv i kβ€– := - (haveI : βˆ€ k ∈ Ico 1 (n + 1), 0 ≀ a ^ k * β€–p.rightInv i kβ€– := fun k _ => by positivity - single_le_sum this (by simp [one_le_n])) - _ ≀ (I + 1) * a := IRec (n + 1) (by norm_num) + apply le_radius_of_eventually_le _ ((I + 1) * a) + filter_upwards [Ici_mem_atTop 1] with n (hn : 1 ≀ n) + calc + β€–p.rightInv i x nβ€– * (a' : ℝ) ^ n = a ^ n * β€–p.rightInv i x nβ€– := mul_comm _ _ + _ ≀ βˆ‘ k ∈ Ico 1 (n + 1), a ^ k * β€–p.rightInv i x kβ€– := + (haveI : βˆ€ k ∈ Ico 1 (n + 1), 0 ≀ a ^ k * β€–p.rightInv i x kβ€– := fun k _ => by positivity + single_le_sum this (by simp [hn])) + _ ≀ (I + 1) * a := IRec (n + 1) (by norm_num) + +/-- If a a formal multilinear series has a positive radius of convergence, then its left inverse +also has a positive radius of convergence. -/ +theorem radius_leftInv_pos_of_radius_pos + {p : FormalMultilinearSeries π•œ E F} {i : E ≃L[π•œ] F} {x : E} + (hp : 0 < p.radius) (h : p 1 = (continuousMultilinearCurryFin1 π•œ E F).symm i) : + 0 < (p.leftInv i x).radius := by + rw [leftInv_eq_rightInv _ _ _ h] + exact radius_rightInv_pos_of_radius_pos hp end FormalMultilinearSeries + +/-! +### The inverse of an analytic partial homeomorphism is analytic +-/ + +open FormalMultilinearSeries List + +lemma HasFPowerSeriesAt.tendsto_partialSum_prod_of_comp + {f : E β†’ G} {q : FormalMultilinearSeries π•œ F G} + {p : FormalMultilinearSeries π•œ E F} {x : E} + (hf : HasFPowerSeriesAt f (q.comp p) x) (hq : 0 < q.radius) (hp : 0 < p.radius) : + βˆ€αΆ  y in 𝓝 0, Tendsto (fun (a : β„• Γ— β„•) ↦ q.partialSum a.1 (p.partialSum a.2 y + - p 0 (fun _ ↦ 0))) atTop (𝓝 (f (x + y))) := by + rcases hf with ⟨r0, h0⟩ + rcases q.comp_summable_nnreal p hq hp with ⟨r1, r1_pos : 0 < r1, hr1⟩ + let r : ℝβ‰₯0∞ := min r0 r1 + have : EMetric.ball (0 : E) r ∈ 𝓝 0 := + EMetric.ball_mem_nhds 0 (lt_min h0.r_pos (by exact_mod_cast r1_pos)) + filter_upwards [this] with y hy + have hy0 : y ∈ EMetric.ball 0 r0 := EMetric.ball_subset_ball (min_le_left _ _) hy + have A : HasSum (fun i : Ξ£ n, Composition n => q.compAlongComposition p i.2 fun _j => y) + (f (x + y)) := by + have cau : CauchySeq fun s : Finset (Ξ£ n, Composition n) => + βˆ‘ i ∈ s, q.compAlongComposition p i.2 fun _j => y := by + apply cauchySeq_finset_of_norm_bounded _ (NNReal.summable_coe.2 hr1) _ + simp only [coe_nnnorm, NNReal.coe_mul, NNReal.coe_pow] + rintro ⟨n, c⟩ + calc + β€–(compAlongComposition q p c) fun _j : Fin n => yβ€– ≀ + β€–compAlongComposition q p cβ€– * ∏ _j : Fin n, β€–yβ€– := by + apply ContinuousMultilinearMap.le_opNorm + _ ≀ β€–compAlongComposition q p cβ€– * (r1 : ℝ) ^ n := by + apply mul_le_mul_of_nonneg_left _ (norm_nonneg _) + rw [Finset.prod_const, Finset.card_fin] + apply pow_le_pow_left (norm_nonneg _) + rw [EMetric.mem_ball, edist_eq_coe_nnnorm] at hy + have := le_trans (le_of_lt hy) (min_le_right _ _) + rwa [ENNReal.coe_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this + apply HasSum.of_sigma (fun b ↦ hasSum_fintype _) ?_ cau + simpa [FormalMultilinearSeries.comp] using h0.hasSum hy0 + have B : Tendsto (fun (n : β„• Γ— β„•) => βˆ‘ i ∈ compPartialSumTarget 0 n.1 n.2, + q.compAlongComposition p i.2 fun _j => y) atTop (𝓝 (f (x + y))) := by + apply Tendsto.comp A compPartialSumTarget_tendsto_prod_atTop + have C : Tendsto (fun (n : β„• Γ— β„•) => q.partialSum n.1 (βˆ‘ a ∈ Finset.Ico 1 n.2, p a fun _b ↦ y)) + atTop (𝓝 (f (x + y))) := by simpa [comp_partialSum] using B + apply C.congr' + filter_upwards [Ici_mem_atTop (0, 1)] + rintro ⟨-, n⟩ ⟨-, (hn : 1 ≀ n)⟩ + congr + rw [partialSum, eq_sub_iff_add_eq', Finset.range_eq_Ico, + Finset.sum_eq_sum_Ico_succ_bot hn] + congr with i + exact i.elim0 + +lemma HasFPowerSeriesAt.eventually_hasSum_of_comp {f : E β†’ F} {g : F β†’ G} + {q : FormalMultilinearSeries π•œ F G} {p : FormalMultilinearSeries π•œ E F} {x : E} + (hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x) (hf : HasFPowerSeriesAt f p x) + (hq : 0 < q.radius) : + βˆ€αΆ  y in 𝓝 0, HasSum (fun n : β„• => q n fun _ : Fin n => (f (x + y) - f x)) (g (f (x + y))) := by + have : βˆ€αΆ  y in 𝓝 (0 : E), f (x + y) - f x ∈ EMetric.ball 0 q.radius := by + have A : ContinuousAt (fun y ↦ f (x + y) - f x) 0 := by + apply ContinuousAt.sub _ continuousAt_const + exact hf.continuousAt.comp_of_eq (continuous_add_left x).continuousAt (by simp) + have B : EMetric.ball 0 q.radius ∈ 𝓝 (f (x + 0) - f x) := by + simpa using EMetric.ball_mem_nhds _ hq + exact A.preimage_mem_nhds B + filter_upwards [hgf.tendsto_partialSum_prod_of_comp hq (hf.radius_pos), + hf.tendsto_partialSum, this] with y hy h'y h''y + have L : Tendsto (fun n ↦ q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y)))) := by + apply (closed_nhds_basis (g (f (x + y)))).tendsto_right_iff.2 + rintro u ⟨hu, u_closed⟩ + simp only [id_eq, eventually_atTop, ge_iff_le] + rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩ + obtain ⟨aβ‚€, bβ‚€, hab⟩ : βˆƒ aβ‚€ bβ‚€, βˆ€ (a b : β„•), aβ‚€ ≀ a β†’ bβ‚€ ≀ b β†’ + q.partialSum a (p.partialSum b y - (p 0) fun x ↦ 0) ∈ v := by + simpa using hy (v_open.mem_nhds hv) + refine ⟨aβ‚€, fun a ha ↦ ?_⟩ + have : Tendsto (fun b ↦ q.partialSum a (p.partialSum b y - (p 0) fun x ↦ 0)) atTop + (𝓝 (q.partialSum a (f (x + y) - f x))) := by + have : ContinuousAt (q.partialSum a) (f (x + y) - f x) := + (partialSum_continuous q a).continuousAt + apply this.tendsto.comp + apply Tendsto.sub h'y + convert tendsto_const_nhds + exact (HasFPowerSeriesAt.coeff_zero hf fun _ ↦ 0).symm + apply u_closed.mem_of_tendsto this + filter_upwards [Ici_mem_atTop bβ‚€] with b hb using vu (hab _ _ ha hb) + have C : CauchySeq (fun (s : Finset β„•) ↦ βˆ‘ n ∈ s, q n fun _ : Fin n => (f (x + y) - f x)) := by + have Z := q.summable_norm_apply (x := f (x + y) - f x) h''y + exact cauchySeq_finset_of_norm_bounded _ Z (fun i ↦ le_rfl) + exact tendsto_nhds_of_cauchySeq_of_subseq C tendsto_finset_range L + +/-- If a partial homeomorphism `f` is defined at `a` and has a power series expansion there with +invertible linear term, then `f.symm` has a power series expansion at `f a`, given by the inverse +of the initial power series. -/ +theorem PartialHomeomorph.hasFPowerSeriesAt_symm (f : PartialHomeomorph E F) {a : E} + {i : E ≃L[π•œ] F} (h0 : a ∈ f.source) {p : FormalMultilinearSeries π•œ E F} + (h : HasFPowerSeriesAt f p a) (hp : p 1 = (continuousMultilinearCurryFin1 π•œ E F).symm i) : + HasFPowerSeriesAt f.symm (p.leftInv i a) (f a) := by + have A : HasFPowerSeriesAt (f.symm ∘ f) ((p.leftInv i a).comp p) a := by + have : HasFPowerSeriesAt (ContinuousLinearMap.id π•œ E) ((p.leftInv i a).comp p) a := by + rw [leftInv_comp _ _ _ hp] + exact (ContinuousLinearMap.id π•œ E).hasFPowerSeriesAt a + apply this.congr + filter_upwards [f.open_source.mem_nhds h0] with x hx using by simp [hx] + have B : βˆ€αΆ  (y : E) in 𝓝 0, HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ f (a + y) - f a) + (f.symm (f (a + y))) := by + simpa using A.eventually_hasSum_of_comp h (radius_leftInv_pos_of_radius_pos h.radius_pos hp) + have C : βˆ€αΆ  (y : E) in 𝓝 a, HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ f y - f a) + (f.symm (f y)) := by + rw [← sub_eq_zero_of_eq (a := a) rfl] at B + have : ContinuousAt (fun x ↦ x - a) a := by fun_prop + simpa using this.preimage_mem_nhds B + have D : βˆ€αΆ  (y : E) in 𝓝 (f.symm (f a)), + HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ f y - f a) y := by + simp only [h0, PartialHomeomorph.left_inv] + filter_upwards [C, f.open_source.mem_nhds h0] with x hx h'x + simpa [h'x] using hx + have E : βˆ€αΆ  z in 𝓝 (f a), HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ f (f.symm z) - f a) + (f.symm z) := by + have : ContinuousAt f.symm (f a) := f.continuousAt_symm (f.map_source h0) + exact this D + have F : βˆ€αΆ  z in 𝓝 (f a), HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ z - f a) (f.symm z) := by + filter_upwards [f.open_target.mem_nhds (f.map_source h0), E] with z hz h'z + simpa [hz] using h'z + rcases EMetric.mem_nhds_iff.1 F with ⟨r, r_pos, hr⟩ + refine ⟨min r (p.leftInv i a).radius, min_le_right _ _, + lt_min r_pos (radius_leftInv_pos_of_radius_pos h.radius_pos hp), fun {y} hy ↦ ?_⟩ + have : y + f a ∈ EMetric.ball (f a) r := by + simp only [EMetric.mem_ball, edist_eq_coe_nnnorm_sub, sub_zero, lt_min_iff, + add_sub_cancel_right] at hy ⊒ + exact hy.1 + simpa [add_comm] using hr this diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean index c68372a5f2ce07..b47e95b56f4adf 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean @@ -146,7 +146,35 @@ end ContinuousMul section CompleteSpace -variable [CommGroup Ξ±] [UniformSpace Ξ±] [UniformGroup Ξ±] [CompleteSpace Ξ±] +variable [CommGroup Ξ±] [UniformSpace Ξ±] [UniformGroup Ξ±] + +@[to_additive] +theorem HasProd.of_sigma {Ξ³ : Ξ² β†’ Type*} {f : (Ξ£ b : Ξ², Ξ³ b) β†’ Ξ±} {g : Ξ² β†’ Ξ±} {a : Ξ±} + (hf : βˆ€ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b)) (hg : HasProd g a) + (h : CauchySeq (fun (s : Finset (Ξ£ b : Ξ², Ξ³ b)) ↦ ∏ i ∈ s, f i)) : + HasProd f a := by + classical + apply le_nhds_of_cauchy_adhp h + simp only [← mapClusterPt_def, mapClusterPt_iff, frequently_atTop, ge_iff_le, le_eq_subset] + intro u hu s + rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩ + obtain ⟨t0, st0, ht0⟩ : βˆƒ t0, ∏ i ∈ t0, g i ∈ v ∧ s.image Sigma.fst βŠ† t0 := by + have A : βˆ€αΆ  t0 in (atTop : Filter (Finset Ξ²)), ∏ i ∈ t0, g i ∈ v := hg (v_open.mem_nhds hv) + exact (A.and (Ici_mem_atTop _)).exists + have L : Tendsto (fun t : Finset (Ξ£b, Ξ³ b) ↦ ∏ p ∈ t.filter fun p ↦ p.1 ∈ t0, f p) atTop + (𝓝 <| ∏ b ∈ t0, g b) := by + simp only [← sigma_preimage_mk, prod_sigma] + refine tendsto_finset_prod _ fun b _ ↦ ?_ + change + Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b)) + exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective)) + have : βˆƒ t, ∏ p ∈ t.filter (fun p ↦ p.1 ∈ t0), f p ∈ v ∧ s βŠ† t := + ((Tendsto.eventually_mem L (v_open.mem_nhds st0)).and (Ici_mem_atTop _)).exists + obtain ⟨t, tv, st⟩ := this + refine ⟨t.filter (fun p ↦ p.1 ∈ t0), fun x hx ↦ ?_, vu tv⟩ + simpa only [mem_filter, st hx, true_and] using ht0 (mem_image_of_mem Sigma.fst hx) + +variable [CompleteSpace Ξ±] @[to_additive] theorem Multipliable.sigma_factor {Ξ³ : Ξ² β†’ Type*} {f : (Ξ£b : Ξ², Ξ³ b) β†’ Ξ±}