LeanPool.SardMoreira.ImplicitFunction

@[irreducible]

noncomputable def HasStrictFDerivAt.implicitFunctionDataOfComplementedKerRange {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (f : E → F) (f' : E →L[𝕜] F) {a : E} (hf : HasStrictFDerivAt f f' a) (hker : (↑f').ker.ClosedComplemented) (hrange : (↑f').range.ClosedComplemented) : have this := ⋯; ImplicitFunctionData 𝕜 E ↥(↑f').range ↥(↑f').ker

An ImplicitFunctionData from a strict Fréchet derivative f' with both its kernel and its range closed-complemented.

Equations

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

@[simp]

theorem HasStrictFDerivAt.implicitFunctionDataOfComplementedKerRange_pt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (f : E → F) (f' : E →L[𝕜] F) {a : E} (hf : HasStrictFDerivAt f f' a) (hker : (↑f').ker.ClosedComplemented) (hrange : (↑f').range.ClosedComplemented) : (implicitFunctionDataOfComplementedKerRange f f' hf hker hrange).pt = a

noncomputable def HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplementedKerRange {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (f : E → F) (f' : E →L[𝕜] F) {a : E} (hf : HasStrictFDerivAt f f' a) (hker : (↑f').ker.ClosedComplemented) (hrange : (↑f').range.ClosedComplemented) : OpenPartialHomeomorph E (↥(↑f').range × ↥(↑f').ker)

The OpenPartialHomeomorph associated to implicitFunctionDataOfComplementedKerRange.

Equations

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

@[simp]

theorem HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplementedKerRange_source {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hker : (↑f').ker.ClosedComplemented) (hrange : (↑f').range.ClosedComplemented) : a ∈ (implicitToOpenPartialHomeomorphOfComplementedKerRange f f' hf hker hrange).source

theorem HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplementedKerRange_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hker : (↑f').ker.ClosedComplemented) (hrange : (↑f').range.ClosedComplemented) (x : E) : ↑(implicitToOpenPartialHomeomorphOfComplementedKerRange f f' hf hker hrange) x = ((Exists.choose hrange) (f x), (Exists.choose hker) x)

theorem HasStrictFDerivAt.coe_implicitToOpenPartialHomeomorphOfComplementedKerRange {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hker : (↑f').ker.ClosedComplemented) (hrange : (↑f').range.ClosedComplemented) : ↑(implicitToOpenPartialHomeomorphOfComplementedKerRange f f' hf hker hrange) = fun (x : E) => ((Exists.choose hrange) (f x), (Exists.choose hker) x)

@[simp]

theorem HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplementedKerRange_apply_fst {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hker : (↑f').ker.ClosedComplemented) (hrange : (↑f').range.ClosedComplemented) (x : E) : (↑(implicitToOpenPartialHomeomorphOfComplementedKerRange f f' hf hker hrange) x).1 = (Exists.choose hrange) (f x)