theorem Real.smoothTransition_projI {x : ℝ} : (projI x).smoothTransition = x.smoothTransition

theorem fderiv_prod_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x₀ : E} {y₀ : F} : fderiv 𝕜 (fun (x : E) => (x, y₀)) x₀ = ContinuousLinearMap.inl 𝕜 E F

theorem fderiv_prod_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x₀ : E} {y₀ : F} : fderiv 𝕜 (fun (y : F) => (x₀, y)) y₀ = ContinuousLinearMap.inr 𝕜 E F

theorem HasFDerivAt.partial_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} {φ' : E × F →L[𝕜] G} {e₀ : E} {f₀ : F} (h : HasFDerivAt (Function.uncurry φ) φ' (e₀, f₀)) : HasFDerivAt (fun (e : E) => φ e f₀) (φ'.comp (ContinuousLinearMap.inl 𝕜 E F)) e₀

theorem HasFDerivAt.partial_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} {φ' : E × F →L[𝕜] G} {e₀ : E} {f₀ : F} (h : HasFDerivAt (Function.uncurry φ) φ' (e₀, f₀)) : HasFDerivAt (fun (f : F) => φ e₀ f) (φ'.comp (ContinuousLinearMap.inr 𝕜 E F)) f₀

theorem fderiv_prod_eq_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × F → G} {p : E × F} (hf : DifferentiableAt 𝕜 f p) : fderiv 𝕜 f p = fderiv 𝕜 (fun (z : E × F) => f (z.1, p.2)) p + fderiv 𝕜 (fun (z : E × F) => f (p.1, z.2)) p

def partialFDerivFst (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {F : Type u_8} (φ : E → F → G) : E → F → E →L[𝕜] G

The first partial derivative of a binary function.

Equations

• partialFDerivFst 𝕜 φ e₀ f₀ = fderiv 𝕜 (fun (e : E) => φ e f₀) e₀

def partialFDerivSnd (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {E : Type u_8} (φ : E → F → G) : E → F → F →L[𝕜] G

The second partial derivative of a binary function.

Equations

• partialFDerivSnd 𝕜 φ e₀ f₀ = fderiv 𝕜 (fun (f : F) => φ e₀ f) f₀

theorem fderiv_partial_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} {φ' : E × F →L[𝕜] G} {e₀ : E} {f₀ : F} (h : HasFDerivAt (Function.uncurry φ) φ' (e₀, f₀)) : partialFDerivFst 𝕜 φ e₀ f₀ = φ'.comp (ContinuousLinearMap.inl 𝕜 E F)

theorem fderiv_partial_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} {φ' : E × F →L[𝕜] G} {e₀ : E} {f₀ : F} (h : HasFDerivAt (Function.uncurry φ) φ' (e₀, f₀)) : partialFDerivSnd 𝕜 φ e₀ f₀ = φ'.comp (ContinuousLinearMap.inr 𝕜 E F)

theorem DifferentiableAt.hasFDerivAt_partial_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} {e₀ : E} {f₀ : F} (h : DifferentiableAt 𝕜 (Function.uncurry φ) (e₀, f₀)) : HasFDerivAt (fun (e : E) => φ e f₀) (partialFDerivFst 𝕜 φ e₀ f₀) e₀

theorem DifferentiableAt.hasFDerivAt_partial_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} {e₀ : E} {f₀ : F} (h : DifferentiableAt 𝕜 (Function.uncurry φ) (e₀, f₀)) : HasFDerivAt (fun (f : F) => φ e₀ f) (partialFDerivSnd 𝕜 φ e₀ f₀) f₀

theorem ContDiff.partial_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} {n : ℕ∞} (h : ContDiff 𝕜 (↑n) (Function.uncurry φ)) (f₀ : F) : ContDiff 𝕜 ↑n fun (e : E) => φ e f₀

theorem ContDiff.partial_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} {n : ℕ∞} (h : ContDiff 𝕜 (↑n) (Function.uncurry φ)) (e₀ : E) : ContDiff 𝕜 ↑n fun (f : F) => φ e₀ f

def ContinuousLinearMap.compRightL {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (φ : E →L[𝕜] F) : (F →L[𝕜] G) →L[𝕜] E →L[𝕜] G

Precomposition by a continuous linear map as a continuous linear map between spaces of continuous linear maps.

Equations

• φ.compRightL = ContinuousLinearMap.precomp G φ

def ContinuousLinearMap.compLeftL {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (φ : F →L[𝕜] G) : (E →L[𝕜] F) →L[𝕜] E →L[𝕜] G

Postcomposition by a continuous linear map as a continuous linear map between spaces of continuous linear maps.

Equations

• φ.compLeftL = ContinuousLinearMap.postcomp E φ

theorem Differentiable.fderiv_partial_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} (hF : Differentiable 𝕜 (Function.uncurry φ)) : ↿(partialFDerivFst 𝕜 φ) = ⇑(ContinuousLinearMap.precomp G (ContinuousLinearMap.inl 𝕜 E F)) ∘ fderiv 𝕜 (Function.uncurry φ)

theorem Differentiable.fderiv_partial_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} (hF : Differentiable 𝕜 (Function.uncurry φ)) : ↿(partialFDerivSnd 𝕜 φ) = ⇑(ContinuousLinearMap.precomp G (ContinuousLinearMap.inr 𝕜 E F)) ∘ fderiv 𝕜 (Function.uncurry φ)

def partialDerivFst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (φ : 𝕜 → F → G) : 𝕜 → F → G

The first partial derivative of φ : 𝕜 → F → G seen as a function from 𝕜 → F → G

Equations

• partialDerivFst φ k f = (partialFDerivFst 𝕜 φ k f) 1

def partialDerivSnd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (φ : E → 𝕜 → G) : E → 𝕜 → G

The second partial derivative of φ : E → 𝕜 → G seen as a function from E → 𝕜 → G

Equations

• partialDerivSnd φ e k = (partialFDerivSnd 𝕜 φ e k) 1

theorem partialFDerivFst_eq_smulRight {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (φ : 𝕜 → F → G) (k : 𝕜) (f : F) : partialFDerivFst 𝕜 φ k f = ContinuousLinearMap.smulRight 1 (partialDerivFst φ k f)

@[simp]

theorem partialFDerivFst_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (φ : 𝕜 → F → G) (k : 𝕜) (f : F) : (partialFDerivFst 𝕜 φ k f) 1 = partialDerivFst φ k f

theorem partialFDerivSnd_eq_smulRight {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (φ : E → 𝕜 → G) (e : E) (k : 𝕜) : partialFDerivSnd 𝕜 φ e k = ContinuousLinearMap.smulRight 1 (partialDerivSnd φ e k)

theorem partialFDerivSnd_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (φ : E → 𝕜 → G) (e : E) (k : 𝕜) : (partialFDerivSnd 𝕜 φ e k) 1 = partialDerivSnd φ e k

theorem WithTop.le_mul_self {α : Type u_8} [OrderedCommMonoid α] [CanonicallyOrderedMul α] (n m : α) : ↑n ≤ ↑(m * n)

theorem WithTop.le_add_self {α : Type u_8} [OrderedAddCommMonoid α] [CanonicallyOrderedAdd α] (n m : α) : ↑n ≤ ↑(m + n)

theorem WithTop.le_self_mul {α : Type u_8} [OrderedCommMonoid α] [CanonicallyOrderedMul α] (n m : α) : ↑n ≤ ↑(n * m)

theorem WithTop.le_self_add {α : Type u_8} [OrderedAddCommMonoid α] [CanonicallyOrderedAdd α] (n m : α) : ↑n ≤ ↑(n + m)

theorem ContDiff.contDiff_partial_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} {n : ℕ} (hF : ContDiff 𝕜 (↑n + 1) (Function.uncurry φ)) : ContDiff 𝕜 ↑n ↿(partialFDerivFst 𝕜 φ)

theorem ContDiff.contDiff_partial_fst_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} {n : ℕ} (hF : ContDiff 𝕜 (↑n + 1) (Function.uncurry φ)) {x : E} : ContDiff 𝕜 ↑n ↿fun (x' : E) (y : F) => (partialFDerivFst 𝕜 φ x' y) x

theorem ContDiff.continuous_partial_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} {n : ℕ} (h : ContDiff 𝕜 (↑↑(n + 1)) (Function.uncurry φ)) : Continuous ↿(partialFDerivFst 𝕜 φ)

theorem ContDiff.contDiff_top_partial_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} (hF : ContDiff 𝕜 (↑⊤) (Function.uncurry φ)) : ContDiff 𝕜 ↑⊤ ↿(partialFDerivFst 𝕜 φ)

theorem ContDiff.contDiff_partial_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} {n : ℕ} (hF : ContDiff 𝕜 (↑n + 1) (Function.uncurry φ)) : ContDiff 𝕜 ↑n ↿(partialFDerivSnd 𝕜 φ)

theorem ContDiff.contDiff_partial_snd_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} {n : ℕ} (hF : ContDiff 𝕜 (↑n + 1) (Function.uncurry φ)) {y : F} : ContDiff 𝕜 ↑n ↿fun (x : E) (y' : F) => (partialFDerivSnd 𝕜 φ x y') y

theorem ContDiff.continuous_partial_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} {n : ℕ} (h : ContDiff 𝕜 (↑↑(n + 1)) (Function.uncurry φ)) : Continuous ↿(partialFDerivSnd 𝕜 φ)

theorem ContDiff.contDiff_top_partial_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {φ : E → F → G} (hF : ContDiff 𝕜 (↑⊤) (Function.uncurry φ)) : ContDiff 𝕜 ↑⊤ ↿(partialFDerivSnd 𝕜 φ)

theorem ContDiff.lipschitzOnWith {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} {f : E → F} {n : WithTop ℕ∞} (hf : ContDiff ℝ n f) (hn : 1 ≤ n) (hs : Convex ℝ s) (hs' : IsCompact s) : ∃ (K : NNReal), LipschitzOnWith K f s

theorem const_mul_one_div_lt {ε : ℝ} (ε_pos : 0 < ε) (C : ℝ) : ∀ᶠ (N : ℝ) in Filter.atTop, C * ‖1 / N‖ < ε