LeanPool.SardMoreira.Unused #

source

theorem HasFDerivWithinAt.of_local_leftInverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {g : F → E} {a : F} {s : Set E} {t : Set F} (hg : Filter.Tendsto g (nhdsWithin a t) (nhdsWithin (g a) s)) (hf : HasFDerivWithinAt f (↑f') s (g a)) (ha : a ∈ t) (hfg : ∀ᶠ (y : F) in nhdsWithin a t, f (g y) = y) :

HasFDerivWithinAt g (↑f'.symm) t a

source

def Submodule.continuousEquivSubtypeMap {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] (p : Submodule R M) (q : Submodule R ↥p) :

↥q ≃L[R] ↥(map p.subtype q)

Continuous linear equivalence between a submodule of a submodule and its mapped subtype.

Equations

p.continuousEquivSubtypeMap q = { toLinearEquiv := p.equivSubtypeMap q, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source

@[simp]

theorem Submodule.continuousEquivSubtypeMap_symm_apply_coe_coe {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] (p : Submodule R M) (q : Submodule R ↥p) (a✝ : ↥(map p.subtype q)) :

↑↑((p.continuousEquivSubtypeMap q).symm a✝) = ↑a✝

source

@[simp]

theorem Submodule.continuousEquivSubtypeMap_apply_coe {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] (p : Submodule R M) (q : Submodule R ↥p) (c : ↥q) :

↑((p.continuousEquivSubtypeMap q) c) = ↑↑c

source

def Submodule.topContinuousEquiv {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] :

↥⊤ ≃L[R] M

Continuous linear equivalence from the top submodule to the ambient module.

Equations

Submodule.topContinuousEquiv = { toLinearEquiv := Submodule.topEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source

@[simp]

theorem Submodule.topContinuousEquiv_apply {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] (x : ↥⊤) :

topContinuousEquiv x = ↑x

source

@[simp]

theorem Submodule.topContinuousEquiv_symm_apply_coe {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] (x : M) :

↑(topContinuousEquiv.symm x) = x

source

theorem ContinuousLinearEquiv.map_nhdsWithin_eq {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (e : M ≃L[R] N) (s : Set M) (x : M) :

Filter.map (⇑e) (nhdsWithin x s) = nhdsWithin (e x) (⇑e '' s)

source

theorem ContinuousLinearEquiv.map_nhdsWithin_preimage_eq {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (e : M ≃L[R] N) (s : Set N) (x : M) :

Filter.map (⇑e) (nhdsWithin x (⇑e ⁻¹' s)) = nhdsWithin (e x) s

source

def Submodule.prodEquiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (s : Submodule R M) (t : Submodule R N) :

↥(s.prod t) ≃ₗ[R] ↥s × ↥t

Linear equivalence between a product submodule and the product of submodules.

Equations

s.prodEquiv t = { toFun := (Equiv.Set.prod ↑s ↑t).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (Equiv.Set.prod ↑s ↑t).invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem Submodule.rank_prod_eq_lift {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [StrongRankCondition R] (s : Submodule R M) (t : Submodule R N) [Module.Free R ↥s] [Module.Free R ↥t] :

Module.rank R ↥(s.prod t) = Cardinal.lift.{u_3, u_2} (Module.rank R ↥s) + Cardinal.lift.{u_2, u_3} (Module.rank R ↥t)

source

@[simp]

theorem Submodule.finrank_prod {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [StrongRankCondition R] (s : Submodule R M) (t : Submodule R N) [Module.Free R ↥s] [Module.Free R ↥t] [Module.Finite R ↥s] [Module.Finite R ↥t] :

Module.finrank R ↥(s.prod t) = Module.finrank R ↥s + Module.finrank R ↥t

source

theorem UniqueDiffOn.frequently_smallSets {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} (hs : UniqueDiffOn 𝕜 s) (a : E) :

∃ᶠ (t : Set E) in (nhdsWithin a s).smallSets, t ∈ nhdsWithin a s ∧ UniqueDiffOn 𝕜 t

source

theorem iteratedFDeriv_apply_congr_order {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k l : ℕ} (h : k = l) (f : E → F) (x : E) (m : Fin k → E) :

(iteratedFDeriv 𝕜 k f x) m = (iteratedFDeriv 𝕜 l f x) (m ∘ Fin.cast ⋯)

source

theorem iteratedFDerivWithin_comp_of_eventually {𝕜 : 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 : WithTop ℕ∞} {g : F → G} {f : E → F} {t : Set F} {s : Set E} {a : E} (hg : ContDiffWithinAt 𝕜 n g t (f a)) (hf : ContDiffWithinAt 𝕜 n f s a) (ht : UniqueDiffOn 𝕜 t) (hs : UniqueDiffOn 𝕜 s) (ha : a ∈ s) (hst : ∀ᶠ (x : E) in nhdsWithin a s, f x ∈ t) {i : ℕ} (hi : ↑i ≤ n) :

iteratedFDerivWithin 𝕜 i (g ∘ f) s a = (ftaylorSeriesWithin 𝕜 g t (f a)).taylorComp (ftaylorSeriesWithin 𝕜 f s a) i

source

def OrderedFinpartition.single (n : ℕ) (hn : n ≠ 0) :

OrderedFinpartition n

Cover [0, n), n ≠ 0, by a single subset.

Equations

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

Instances For

source

@[simp]

theorem OrderedFinpartition.single_length (n : ℕ) (hn : n ≠ 0) :

(single n hn).length = 1

source

@[simp]

theorem OrderedFinpartition.single_partSize (n : ℕ) (hn : n ≠ 0) :

(single n hn).partSize = fun (x : Fin 1) => n

source

@[simp]

theorem OrderedFinpartition.single_emb (n : ℕ) (hn : n ≠ 0) :

(single n hn).emb = fun (x : Fin 1) => id

source

@[simp]

theorem OrderedFinpartition.applyOrderedFinpartition_single {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (hn : n ≠ 0) (p : (i : Fin (single n hn).length) → E [×(single n hn).partSize i]→L[𝕜] F) (m : Fin n → E) (i : Fin (single n hn).length) :

(single n hn).applyOrderedFinpartition p m i = (p i) m

source

theorem OrderedFinpartition.length_eq_one_iff {n : ℕ} (c : OrderedFinpartition n) (hn : n ≠ 0) :

c.length = 1 ↔ c = single n hn

source

theorem OrderedFinpartition.length_eq_one_iff_exists {n : ℕ} (c : OrderedFinpartition n) :

c.length = 1 ↔ ∃ (h : n ≠ 0), c = single n h

source

theorem OrderedFinpartition.partSize_eq_iff_length_eq_one {n : ℕ} (c : OrderedFinpartition n) (i : Fin c.length) :

c.partSize i = n ↔ c.length = 1

source

theorem OrderedFinpartition.partSize_eq_iff_eq_single {n : ℕ} (c : OrderedFinpartition n) (i : Fin c.length) :

c.partSize i = n ↔ c = single n ⋯