def ContinuousLinearMap.blocks {𝕜 : Type u₁} [NontriviallyNormedField 𝕜] {M₁ : Type u₂} [NormedAddCommGroup M₁] [NormedSpace 𝕜 M₁] {M₂ : Type u₃} [NormedAddCommGroup M₂] [NormedSpace 𝕜 M₂] {M₃ : Type u₄} [NormedAddCommGroup M₃] [NormedSpace 𝕜 M₃] {M₄ : Type u₅} [NormedAddCommGroup M₄] [NormedSpace 𝕜 M₄] (A : M₁ →L[𝕜] M₃) (B : M₂ →L[𝕜] M₃) (C : M₁ →L[𝕜] M₄) (D : M₂ →L[𝕜] M₄) : M₁ × M₂ →L[𝕜] M₃ × M₄

Defines continuous linear maps between two products by blocks: given (A : M₁ →L[𝕜] M₃), (B : M₂ →L[𝕜] M₃), (C : M₁ →L[𝕜] M₄) and (D : M₂ →L[𝕜] M₄), construct the continuous linear map with "matrix": A B C D.

Equations

• A.blocks B C D = (A.coprod B).prod (C.coprod D)

def ContinuousLinearEquiv.lowerTriangular {𝕜 : Type u₁} [NontriviallyNormedField 𝕜] {M₁ : Type u₂} [NormedAddCommGroup M₁] [NormedSpace 𝕜 M₁] {M₂ : Type u₃} [NormedAddCommGroup M₂] [NormedSpace 𝕜 M₂] {M₃ : Type u₄} [NormedAddCommGroup M₃] [NormedSpace 𝕜 M₃] {M₄ : Type u₅} [NormedAddCommGroup M₄] [NormedSpace 𝕜 M₄] (A : M₁ ≃L[𝕜] M₃) (C : M₁ →L[𝕜] M₄) (D : M₂ ≃L[𝕜] M₄) : (M₁ × M₂) ≃L[𝕜] M₃ × M₄

Given (A : M₁ ≃L[𝕜] M₃), (C : M₁ →L[𝕜] M₄) and (D : M₂ ≃L[𝕜] M₄), construct the continuous linear equiv with "matrix" A 0 C D.

Equations

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

theorem ContinuousLinearEquiv.continuous_lowerTriangular {𝕜 : Type u₁} [NontriviallyNormedField 𝕜] {M₁ : Type u₂} [NormedAddCommGroup M₁] [NormedSpace 𝕜 M₁] {M₂ : Type u₃} [NormedAddCommGroup M₂] [NormedSpace 𝕜 M₂] {M₃ : Type u₄} [NormedAddCommGroup M₃] [NormedSpace 𝕜 M₃] {M₄ : Type u₅} [NormedAddCommGroup M₄] [NormedSpace 𝕜 M₄] {X : Type u_1} [TopologicalSpace X] {A : X → M₁ ≃L[𝕜] M₃} {C : X → M₁ →L[𝕜] M₄} {D : X → M₂ ≃L[𝕜] M₄} (hA : Continuous fun (x : X) => ↑(A x)) (hC : Continuous C) (hD : Continuous fun (x : X) => ↑(D x)) : Continuous fun (x : X) => ↑((A x).lowerTriangular (C x) (D x))

def StrictDifferentiableAt (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (x : E) : Prop

The proposition that a function between two normed spaces has a strict derivative at a given point.

Equations

• StrictDifferentiableAt 𝕜 f x = ∃ (φ : E →L[𝕜] F), HasStrictFDerivAt f φ x

def StrictDifferentiable (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) : Prop

The proposition that a function between two normed spaces has a strict derivative at every point.

Equations

• StrictDifferentiable 𝕜 f = ∀ (x : E), StrictDifferentiableAt 𝕜 f x

theorem StrictDifferentiableAt.differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : StrictDifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 f x

@[simp]

theorem LinearMap.coprod_comp_inl_inr {R : Type u_5} {M : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M × M₂ →ₗ[R] M₃) : (f ∘ₗ inl R M M₂).coprod (f ∘ₗ inr R M M₂) = f

@[simp]

theorem ContinuousLinearMap.coprod_comp_inl_inr {R₁ : Type u_5} [Semiring R₁] {M₁ : Type u_6} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_7} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_8} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [ContinuousAdd M₃] (f : M₁ × M₂ →L[R₁] M₃) : (f.comp (inl R₁ M₁ M₂)).coprod (f.comp (inr R₁ M₁ M₂)) = f

theorem DifferentiableAt.hasFDerivAt_coprod_partial {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F → G} {x : E} {y : F} (hf : DifferentiableAt 𝕜 (Function.uncurry f) (x, y)) : HasFDerivAt (Function.uncurry f) ((partialFDerivFst 𝕜 f x y).coprod (partialFDerivSnd 𝕜 f x y)) (x, y)

theorem DifferentiableAt.hasFDerivAt_coprod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F → G} {x : E} {y : F} (hf : DifferentiableAt 𝕜 (Function.uncurry f) (x, y)) {φ : E →L[𝕜] G} {ψ : F →L[𝕜] G} (hφ : HasFDerivAt (fun (p : E) => f p y) φ x) (hψ : HasFDerivAt (f x) ψ y) : HasFDerivAt (Function.uncurry f) (φ.coprod ψ) (x, y)

theorem Homeomorph.contDiffAt_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} [CompleteSpace E] (f : E ≃ₜ F) {f₀' : E ≃L[𝕜] F} {a : F} (hf' : HasFDerivAt (⇑f) (↑f₀') (f.symm a)) (hf : ContDiffAt 𝕜 n (⇑f) (f.symm a)) : ContDiffAt 𝕜 n (⇑f.symm) a

theorem Equiv.continuous_symm_of_contDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] (φ : E ≃ F) {Dφ : E → E ≃L[𝕜] F} (hφ : ∀ (x : E), HasStrictFDerivAt (⇑φ) (↑(Dφ x)) x) : Continuous ⇑φ.symm

def Equiv.toHomeomorphOfContDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] (φ : E ≃ F) {Dφ : E → E ≃L[𝕜] F} (hφ : ∀ (x : E), HasStrictFDerivAt (⇑φ) (↑(Dφ x)) x) : E ≃ₜ F

A bijection that is strictly differentiable at every point is a homeomorphism.

Equations

• φ.toHomeomorphOfContDiff hφ = { toEquiv := φ, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem contDiff_parametric_symm {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CompleteSpace E] [CompleteSpace F] {f : E → F ≃ G} {f' : E → F → F ≃L[𝕜] G} (hf : ContDiff 𝕜 ↑⊤ fun (p : E × F) => (f p.1) p.2) (hf' : ∀ (x : E) (y : F), partialFDerivSnd 𝕜 (fun (x : E) (y : F) => (f x) y) x y = ↑(f' x y)) : ContDiff 𝕜 ↑⊤ fun (p : E × G) => (f p.1).symm p.2

theorem contDiff_parametric_symm_of_deriv_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : E → ℝ → ℝ} (hf : ContDiff ℝ ↑⊤ ↿f) (hderiv : ∀ (x : E) (t : ℝ), 0 < partialDerivSnd f x t) (hsurj : ∀ (x : E), Function.Surjective (f x)) : ContDiff ℝ ↑⊤ fun (p : E × ℝ) => (StrictMono.orderIsoOfSurjective (f p.1) ⋯ ⋯).symm p.2

theorem contDiff_toSpanSingleton (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace 𝕜 E] : ContDiff 𝕜 ⊤ (ContinuousLinearMap.toSpanSingleton 𝕜)

theorem orthogonalProjection_singleton' {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {v : E} : (Submodule.span 𝕜 {v}).subtypeL.comp (orthogonalProjection (Submodule.span 𝕜 {v})) = (1 / ↑‖v‖ ^ 2) • (ContinuousLinearMap.toSpanSingleton 𝕜 v).comp ((InnerProductSpace.toDual 𝕜 E) v)

theorem contDiffAt_orthogonalProjection_singleton {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {v₀ : E} (hv₀ : v₀ ≠ 0) : ContDiffAt ℝ ⊤ (fun (v : E) => (Submodule.span ℝ {v}).subtypeL.comp (orthogonalProjection (Submodule.span ℝ {v}))) v₀

The orthogonal projection onto a vector in a real inner product space E, considered as a map from E to E →L[ℝ] E, is analytic away from 0.

theorem ContDiffWithinAt.mul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {n : WithTop ℕ∞} {f : E → 𝔸} {s : Set E} {x : E} (hf : ContDiffWithinAt 𝕜 n f s x) {c : 𝔸} : ContDiffWithinAt 𝕜 n (fun (x : E) => f x * c) s x

theorem ContDiffAt.mul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {n : WithTop ℕ∞} {f : E → 𝔸} {x : E} (hf : ContDiffAt 𝕜 n f x) {c : 𝔸} : ContDiffAt 𝕜 n (fun (x : E) => f x * c) x

theorem ContDiffOn.mul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {n : WithTop ℕ∞} {f : E → 𝔸} {s : Set E} (hf : ContDiffOn 𝕜 n f s) {c : 𝔸} : ContDiffOn 𝕜 n (fun (x : E) => f x * c) s

theorem ContDiff.mul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {n : WithTop ℕ∞} {f : E → 𝔸} (hf : ContDiff 𝕜 n f) {c : 𝔸} : ContDiff 𝕜 n fun (x : E) => f x * c

theorem contDiffWithinAt_finsum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_4} {f : ι → E → F} (lf : LocallyFinite fun (i : ι) => Function.support (f i)) {n : WithTop ℕ∞} {s : Set E} {x₀ : E} (h : ∀ (i : ι), ContDiffWithinAt 𝕜 n (f i) s x₀) : ContDiffWithinAt 𝕜 n (fun (x : E) => ∑ᶠ (i : ι), f i x) s x₀

theorem contDiffAt_finsum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_4} {f : ι → E → F} (lf : LocallyFinite fun (i : ι) => Function.support (f i)) {n : WithTop ℕ∞} {x₀ : E} (h : ∀ (i : ι), ContDiffAt 𝕜 n (f i) x₀) : ContDiffAt 𝕜 n (fun (x : E) => ∑ᶠ (i : ι), f i x) x₀