LeanPool.SardMoreira.ContDiff

theorem ContDiffOn.continuousAt_iteratedFDerivWithin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {n : WithTop ℕ∞} {k : ℕ} {a : E} (hf : ContDiffOn 𝕜 n f s) (hs : UniqueDiffOn 𝕜 s) (ha : s ∈ nhds a) (hk : ↑k ≤ n) : ContinuousAt (iteratedFDerivWithin 𝕜 k f s) a

theorem ContDiffAt.eventually_isInvertible_fderiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} {a : E} [CompleteSpace E] (hf : ContDiffAt 𝕜 n f a) (ha : (fderiv 𝕜 f a).IsInvertible) (hn : n ≠ 0) : ∀ᶠ (x : E) in nhds a, (fderiv 𝕜 f x).IsInvertible

@[simp]

theorem OrderedFinpartition.sum_partSize {n : ℕ} (c : OrderedFinpartition n) : ∑ i : Fin c.length, c.partSize i = n

@[simp]

theorem OrderedFinpartition.length_eq_zero {n : ℕ} (c : OrderedFinpartition n) : c.length = 0 ↔ n = 0

@[simp]

theorem OrderedFinpartition.length_pos_iff {n : ℕ} (c : OrderedFinpartition n) : 0 < c.length ↔ 0 < n

theorem OrderedFinpartition.length_eq_iff {n : ℕ} (c : OrderedFinpartition n) : c.length = n ↔ c = atomic n

theorem OrderedFinpartition.length_lt_iff {n : ℕ} (c : OrderedFinpartition n) : c.length < n ↔ c ≠ atomic n

theorem OrderedFinpartition.compContinuousLinearMap_compAlongOrderedFinpartition_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) {H : Type u_5} [NormedAddCommGroup H] [NormedSpace 𝕜 H] (f : F [×c.length]→L[𝕜] G) (g : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F) (h : H →L[𝕜] E) : ((c.compAlongOrderedFinpartition f g).compContinuousLinearMap fun (x : Fin n) => h) = c.compAlongOrderedFinpartition f fun (i : Fin c.length) => (g i).compContinuousLinearMap fun (x : Fin (c.partSize i)) => h

theorem OrderedFinpartition.compAlongOrderedFinpartition_sub_compAlongOrderedFinpartition_isBigO {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) {α : Type u_5} {l : Filter α} {p₁ p₂ : α → F [×c.length]→L[𝕜] G} {q₁ q₂ : α → (m : Fin c.length) → E [×c.partSize m]→L[𝕜] F} {B : α → ℝ} (hp_bdd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖p₁ x‖) (hpB : (fun (x : α) => p₁ x - p₂ x) =O[l] B) (hq₁_bdd : ∀ (m : Fin c.length), Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖q₁ x m‖) (hq₂_bdd : ∀ (m : Fin c.length), Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖q₂ x m‖) (hqB : ∀ (m : Fin c.length), (fun (x : α) => q₁ x m - q₂ x m) =O[l] B) : (fun (x : α) => (c.compAlongOrderedFinpartition (p₁ x) fun (m : Fin c.length) => q₁ x m) - c.compAlongOrderedFinpartition (p₂ x) fun (m : Fin c.length) => q₂ x m) =O[l] B

@[irreducible]

noncomputable def FormalMultilinearSeries.taylorLeftInv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (x : E) : FormalMultilinearSeries 𝕜 F E

The formal Taylor left inverse of a formal multilinear series at a point.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FormalMultilinearSeries.taylorLeftInv_coeff_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (x : E) : p.taylorLeftInv x 0 = ContinuousMultilinearMap.uncurry0 𝕜 F x

@[simp]

theorem ftaylorSeries_id {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : ftaylorSeries 𝕜 id x = FormalMultilinearSeries.id 𝕜 E x

theorem ContinuousLinearMap.IsInvertible.hasFDerivAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : (fderiv 𝕜 f x).IsInvertible) : HasFDerivAt f (↑(Exists.choose h)) x

theorem OpenPartialHomeomorph.hasFDerivAt_symm_inverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {y : F} (hy : y ∈ f.target) (hf' : (fderiv 𝕜 (↑f) (↑f.symm y)).IsInvertible) : HasFDerivAt (↑f.symm) (fderiv 𝕜 (↑f) (↑f.symm y)).inverse y

theorem OpenPartialHomeomorph.fderiv_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {y : F} (hy : y ∈ f.target) (hf' : (fderiv 𝕜 (↑f) (↑f.symm y)).IsInvertible) : fderiv 𝕜 (↑f.symm) y = (fderiv 𝕜 (↑f) (↑f.symm y)).inverse

theorem OpenPartialHomeomorph.bijective_fderiv_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {y : F} (hy : y ∈ f.target) (hf' : (fderiv 𝕜 (↑f) (↑f.symm y)).IsInvertible) : Function.Bijective ⇑(fderiv 𝕜 (↑f.symm) y)

theorem OpenPartialHomeomorph.surjective_fderiv_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {y : F} (hy : y ∈ f.target) (hf' : (fderiv 𝕜 (↑f) (↑f.symm y)).IsInvertible) : Function.Surjective ⇑(fderiv 𝕜 (↑f.symm) y)

theorem OpenPartialHomeomorph.injective_fderiv_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {y : F} (hy : y ∈ f.target) (hf' : (fderiv 𝕜 (↑f) (↑f.symm y)).IsInvertible) : Function.Injective ⇑(fderiv 𝕜 (↑f.symm) y)

theorem OpenPartialHomeomorph.contDiffAt_symm' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} [CompleteSpace E] (f : OpenPartialHomeomorph E F) {a : F} (ha : a ∈ f.target) (hf' : (fderiv 𝕜 (↑f) (↑f.symm a)).IsInvertible) (hf : ContDiffAt 𝕜 n (↑f) (↑f.symm a)) : ContDiffAt 𝕜 n (↑f.symm) a

theorem iteratedFDeriv_one_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (x : E) : iteratedFDeriv 𝕜 1 f x = (continuousMultilinearCurryFin1 𝕜 E F).symm (fderiv 𝕜 f x)

theorem OpenPartialHomeomorph.iteratedFDeriv_symm_eq_rec {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} [CompleteSpace E] (f : OpenPartialHomeomorph E F) {y : F} (hy : y ∈ f.target) (hf : ContDiffAt 𝕜 n (↑f) (↑f.symm y)) {i : ℕ} (hi : ↑i ≤ n) (hf' : 0 < i → (fderiv 𝕜 (↑f) (↑f.symm y)).IsInvertible) : iteratedFDeriv 𝕜 i (↑f.symm) y = (FormalMultilinearSeries.id 𝕜 E (↑f.symm y) i - ∑ c ∈ Finset.univ.erase (OrderedFinpartition.atomic i), c.compAlongOrderedFinpartition (iteratedFDeriv 𝕜 c.length (↑f.symm) y) fun (m : Fin c.length) => iteratedFDeriv 𝕜 (c.partSize m) (↑f) (↑f.symm y)).compContinuousLinearMap fun (x : Fin i) => fderiv 𝕜 (↑f.symm) y

theorem OpenPartialHomeomorph.iteratedFDeriv_symm_eq_taylorLeftInv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} [CompleteSpace E] (f : OpenPartialHomeomorph E F) {y : F} (hy : y ∈ f.target) (hf : ContDiffAt 𝕜 n (↑f) (↑f.symm y)) {i : ℕ} (hi : ↑i ≤ n) (hf' : 0 < i → (fderiv 𝕜 (↑f) (↑f.symm y)).IsInvertible) : iteratedFDeriv 𝕜 i (↑f.symm) y = (ftaylorSeries 𝕜 (↑f) (↑f.symm y)).taylorLeftInv (↑f.symm y) i

theorem FormalMultilinearSeries.compAlongOrderedFinpartition_sub_compAlongOrderedFinpartition_isBigO {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {α : Type u_5} {l : Filter α} {p₁ p₂ : α → FormalMultilinearSeries 𝕜 F G} {q₁ q₂ : α → FormalMultilinearSeries 𝕜 E F} {B : α → ℝ} {n : ℕ} (hp_bdd : ∀ k ≤ n, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖p₁ x k‖) (hpB : ∀ k ≤ n, (fun (x : α) => p₁ x k - p₂ x k) =O[l] B) (hq₁_bdd : ∀ k ≤ n, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖q₁ x k‖) (hq₂_bdd : ∀ k ≤ n, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖q₂ x k‖) (hqB : ∀ k ≤ n, (fun (x : α) => q₁ x k - q₂ x k) =O[l] B) (c : OrderedFinpartition n) : (fun (x : α) => (p₁ x).compAlongOrderedFinpartition (q₁ x) c - (p₂ x).compAlongOrderedFinpartition (q₂ x) c) =O[l] B