Gradient

Main results

This file contains the following parts of gradient.

• the chain rule for the g : 𝕜 → 𝕜 composed with f : F → 𝕜.
• the gradient for the sum of two functions.
• the gradient for finite sum of functions.
• the gradient for the sum of a constant and a function.
• the gradient for the difference of two functions.
• the gradient for the difference of a constant and a function.
• the gradient for the product of two functions.
• the gradient for the product of a constant and a function.

theorem HasGradientAtFilter.comp {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' : F} {x : F} {L : Filter F} {g : 𝕜 → 𝕜} {g' : 𝕜} {L' : Filter 𝕜} (hg : HasGradientAtFilter g g' (f x) L') (hf : HasGradientAtFilter f f' x L) (hL : Filter.Tendsto f L L') : HasGradientAtFilter (g ∘ f) (g' • f') x L

theorem HasGradientWithinAt.comp {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' : F} {x : F} {s : Set F} {g : 𝕜 → 𝕜} {g' : 𝕜} {t : Set 𝕜} (hg : HasGradientWithinAt g g' t (f x)) (hf : HasGradientWithinAt f f' s x) (hst : Set.MapsTo f s t) : HasGradientWithinAt (g ∘ f) (g' • f') s x

theorem HasGradientAt.comp_hasGradientWithinAt {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' : F} {x : F} {s : Set F} {g : 𝕜 → 𝕜} {g' : 𝕜} (hg : HasGradientAt g g' (f x)) (hf : HasGradientWithinAt f f' s x) : HasGradientWithinAt (g ∘ f) (g' • f') s x

theorem HasGradientWithinAt.comp_of_mem {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' : F} {x : F} {s : Set F} {g : 𝕜 → 𝕜} {g' : 𝕜} {t : Set 𝕜} (hg : HasGradientWithinAt g g' t (f x)) (hf : HasGradientWithinAt f f' s x) (hst : Filter.Tendsto f (nhdsWithin x s) (nhdsWithin (f x) t)) : HasGradientWithinAt (g ∘ f) (g' • f') s x

theorem HasGradientAt.comp {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' : F} {x : F} {g : 𝕜 → 𝕜} {g' : 𝕜} (hg : HasGradientAt g g' (f x)) (hf : HasGradientAt f f' x) : HasGradientAt (g ∘ f) (g' • f') x

The chain rule.

theorem gradient.comp {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {x : F} {g : 𝕜 → 𝕜} (hg : DifferentiableAt 𝕜 g (f x)) (hf : DifferentiableAt 𝕜 f x) : gradient (g ∘ f) x = gradient g (f x) • gradient f x

theorem HasGradientAtFilter.const_smul {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' : F} {x : F} {L : Filter F} (h : HasGradientAtFilter f f' x L) (c : 𝕜) : HasGradientAtFilter (fun (x : F) => c • f x) ((starRingEnd 𝕜) c • f') x L

theorem HasGradientWithinAt.const_smul {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' : F} {x : F} {s : Set F} (h : HasGradientWithinAt f f' s x) (c : 𝕜) : HasGradientWithinAt (fun (x : F) => c • f x) ((starRingEnd 𝕜) c • f') s x

theorem HasGradientAt.const_smul {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' : F} {x : F} (h : HasGradientAt f f' x) (c : 𝕜) : HasGradientAt (fun (x : F) => c • f x) ((starRingEnd 𝕜) c • f') x

theorem gradient_const_smul {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {x : F} (h : DifferentiableAt 𝕜 f x) (c : 𝕜) : gradient (fun (y : F) => c • f y) x = (starRingEnd 𝕜) c • gradient f x

theorem HasGradientAtFilter.const_smul' {F : Type u_2} [NormedAddCommGroup F] [CompleteSpace F] {f' : F} {x : F} {L : Filter F} [InnerProductSpace ℝ F] {f : F → ℝ} (c : ℝ) (h : HasGradientAtFilter f f' x L) : HasGradientAtFilter (fun (x : F) => c • f x) (c • f') x L

theorem HasGradientWithinAt.const_smul' {F : Type u_2} [NormedAddCommGroup F] [CompleteSpace F] {f' : F} {x : F} {s : Set F} [InnerProductSpace ℝ F] {f : F → ℝ} (c : ℝ) (h : HasGradientWithinAt f f' s x) : HasGradientWithinAt (fun (x : F) => c • f x) (c • f') s x

theorem HasGradientAt.const_smul' {F : Type u_2} [NormedAddCommGroup F] [CompleteSpace F] {f' : F} {x : F} [InnerProductSpace ℝ F] {f : F → ℝ} (c : ℝ) (h : HasGradientAt f f' x) : HasGradientAt (fun (x : F) => c • f x) (c • f') x

theorem gradient_const_smul' {F : Type u_2} [NormedAddCommGroup F] [CompleteSpace F] {x : F} [InnerProductSpace ℝ F] {f : F → ℝ} (h : DifferentiableAt ℝ f x) (c : ℝ) : gradient (fun (y : F) => c • f y) x = c • gradient f x

theorem HasGradientAtFilter.add {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f' : F} {g : F → 𝕜} {x : F} {g' : F} {L : Filter F} {f : F → 𝕜} (hf : HasGradientAtFilter f f' x L) (hg : HasGradientAtFilter g g' x L) : HasGradientAtFilter (fun (y : F) => f y + g y) (f' + g') x L

theorem HasGradientWithinAt.add {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {s : Set F} {f' : F} {g : F → 𝕜} {x : F} {g' : F} {f : F → 𝕜} (hf : HasGradientWithinAt f f' s x) (hg : HasGradientWithinAt g g' s x) : HasGradientWithinAt (fun (y : F) => f y + g y) (f' + g') s x

theorem HasGradientAt.add {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f' : F} {g : F → 𝕜} {x : F} {g' : F} {f : F → 𝕜} (hf : HasGradientAt f f' x) (hg : HasGradientAt g g' x) : HasGradientAt (fun (x : F) => f x + g x) (f' + g') x

theorem gradient_add {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {g : F → 𝕜} {x : F} {f : F → 𝕜} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) : gradient (fun (y : F) => f y + g y) x = gradient f x + gradient g x

theorem HasGradientAtFilter.add_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f' : F} {x : F} {L : Filter F} {f : F → 𝕜} (hf : HasGradientAtFilter f f' x L) (c : 𝕜) : HasGradientAtFilter (fun (y : F) => f y + c) f' x L

theorem HasGradientWithinAt.add_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {s : Set F} {f' : F} {x : F} {f : F → 𝕜} (hf : HasGradientWithinAt f f' s x) (c : 𝕜) : HasGradientWithinAt (fun (y : F) => f y + c) f' s x

theorem HasGradientAt.add_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f' : F} {x : F} {f : F → 𝕜} (hf : HasGradientAt f f' x) (c : 𝕜) : HasGradientAt (fun (x : F) => f x + c) f' x

theorem gradient_add_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {x : F} {f : F → 𝕜} (c : 𝕜) : gradient (fun (y : F) => f y + c) x = gradient f x

theorem HasGradientAtFilter.const_add {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f' : F} {x : F} {L : Filter F} {f : F → 𝕜} (hf : HasGradientAtFilter f f' x L) (c : 𝕜) : HasGradientAtFilter (fun (y : F) => c + f y) f' x L

theorem HasGradientWithinAt.const_add {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {s : Set F} {f' : F} {x : F} {f : F → 𝕜} (hf : HasGradientWithinAt f f' s x) (c : 𝕜) : HasGradientWithinAt (fun (y : F) => c + f y) f' s x

theorem HasGradientAt.const_add {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f' : F} {x : F} {f : F → 𝕜} (hf : HasGradientAt f f' x) (c : 𝕜) : HasGradientAt (fun (x : F) => c + f x) f' x

theorem Gradient_const_add {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {x : F} {f : F → 𝕜} (c : 𝕜) : gradient (fun (y : F) => c + f y) x = gradient f x

Derivative of a finite sum of functions

theorem HasGradientAtFilter.sum {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {x : F} {L : Filter F} {ι : Type u_3} {u : Finset ι} {A : ι → F → 𝕜} {A' : ι → F} (h : ∀ i ∈ u, HasGradientAtFilter (A i) (A' i) x L) : HasGradientAtFilter (fun (y : F) => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x L

theorem HasGradientWithinAt.sum {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {x : F} {s : Set F} {ι : Type u_3} {u : Finset ι} {A : ι → F → 𝕜} {A' : ι → F} (h : ∀ i ∈ u, HasGradientWithinAt (A i) (A' i) s x) : HasGradientWithinAt (fun (y : F) => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) s x

theorem HasGradientAt.sum {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {x : F} {ι : Type u_3} {u : Finset ι} {A : ι → F → 𝕜} {A' : ι → F} (h : ∀ i ∈ u, HasGradientAt (A i) (A' i) x) : HasGradientAt (fun (y : F) => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x

theorem gradient_sum {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {x : F} {ι : Type u_3} {u : Finset ι} {A : ι → F → 𝕜} (h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) : gradient (fun (y : F) => ∑ i ∈ u, A i y) x = ∑ i ∈ u, gradient (A i) x

Gradient of the negative of a function

theorem HasGradientAtFilter.neg {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' : F} {x : F} {L : Filter F} (h : HasGradientAtFilter f f' x L) : HasGradientAtFilter (fun (x : F) => -f x) (-f') x L

theorem HasGradientWithinAt.neg {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' : F} {x : F} {s : Set F} (h : HasGradientWithinAt f f' s x) : HasGradientWithinAt (fun (x : F) => -f x) (-f') s x

theorem HasGradientAt.neg {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {f' : F} {x : F} (h : HasGradientAt f f' x) : HasGradientAt (fun (x : F) => -f x) (-f') x

theorem gradient_neg {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {x : F} : gradient (fun (y : F) => -f y) x = -gradient f x

Derivative of the difference of two functions

theorem HasGradientAtFilter.sub {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f' : F} {g : F → 𝕜} {x : F} {g' : F} {L : Filter F} {f : F → 𝕜} (hf : HasGradientAtFilter f f' x L) (hg : HasGradientAtFilter g g' x L) : HasGradientAtFilter (fun (x : F) => f x - g x) (f' - g') x L

theorem HasGradientWithinAt.sub {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {s : Set F} {f' : F} {g : F → 𝕜} {x : F} {g' : F} {f : F → 𝕜} (hf : HasGradientWithinAt f f' s x) (hg : HasGradientWithinAt g g' s x) : HasGradientWithinAt (fun (x : F) => f x - g x) (f' - g') s x

theorem HasGradientAt.sub {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f' : F} {g : F → 𝕜} {x : F} {g' : F} {f : F → 𝕜} (hf : HasGradientAt f f' x) (hg : HasGradientAt g g' x) : HasGradientAt (fun (x : F) => f x - g x) (f' - g') x

theorem gradient_sub {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {g : F → 𝕜} {x : F} {f : F → 𝕜} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) : gradient (fun (y : F) => f y - g y) x = gradient f x - gradient g x

theorem HasGradientAtFilter.sub_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f' : F} {x : F} {L : Filter F} {f : F → 𝕜} (hf : HasGradientAtFilter f f' x L) (c : 𝕜) : HasGradientAtFilter (fun (x : F) => f x - c) f' x L

theorem HasGradientWithinAt.sub_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {s : Set F} {f' : F} {x : F} {f : F → 𝕜} (hf : HasGradientWithinAt f f' s x) (c : 𝕜) : HasGradientWithinAt (fun (x : F) => f x - c) f' s x

theorem HasGradientAt.sub_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f' : F} {x : F} {f : F → 𝕜} (hf : HasGradientAt f f' x) (c : 𝕜) : HasGradientAt (fun (x : F) => f x - c) f' x

theorem Gradient_sub_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {x : F} {f : F → 𝕜} (c : 𝕜) : gradient (fun (y : F) => f y - c) x = gradient f x

theorem HasGradientAtFilter.const_sub {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f' : F} {x : F} {L : Filter F} {f : F → 𝕜} (hf : HasGradientAtFilter f f' x L) (c : 𝕜) : HasGradientAtFilter (fun (x : F) => c - f x) (-f') x L

theorem HasGradientWithinAt.const_sub {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {s : Set F} {f' : F} {x : F} {f : F → 𝕜} (hf : HasGradientWithinAt f f' s x) (c : 𝕜) : HasGradientWithinAt (fun (x : F) => c - f x) (-f') s x

theorem HasGradientAt.const_sub {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f' : F} {x : F} {f : F → 𝕜} (hf : HasGradientAt f f' x) (c : 𝕜) : HasGradientAt (fun (x : F) => c - f x) (-f') x

theorem gradient_const_sub {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {x : F} {f : F → 𝕜} (c : 𝕜) : gradient (fun (y : F) => c - f y) x = -gradient f x

theorem equiv_lemma_mul {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {c' : F} {d' : F} {c : F → 𝕜} {d : F → 𝕜} {x : F} : c x • (InnerProductSpace.toDual 𝕜 F) d' + d x • (InnerProductSpace.toDual 𝕜 F) c' = (InnerProductSpace.toDual 𝕜 F) ((starRingEnd 𝕜) (c x) • d' + (starRingEnd 𝕜) (d x) • c')

theorem HasGradientAt.mul {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {c' : F} {d' : F} {c : F → 𝕜} {d : F → 𝕜} {x : F} (hc : HasGradientAt c c' x) (hd : HasGradientAt d d' x) : HasGradientAt (fun (y : F) => c y * d y) ((starRingEnd 𝕜) (c x) • d' + (starRingEnd 𝕜) (d x) • c') x

theorem HasGradientWithinAt.mul {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {s : Set F} {c' : F} {d' : F} {c : F → 𝕜} {d : F → 𝕜} {x : F} (hc : HasGradientWithinAt c c' s x) (hd : HasGradientWithinAt d d' s x) : HasGradientWithinAt (fun (y : F) => c y * d y) ((starRingEnd 𝕜) (c x) • d' + (starRingEnd 𝕜) (d x) • c') s x

theorem gradient_mul {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {c : F → 𝕜} {d : F → 𝕜} {x : F} (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) : gradient (fun (y : F) => c y * d y) x = (starRingEnd 𝕜) (c x) • gradient d x + (starRingEnd 𝕜) (d x) • gradient c x

theorem HasGradientAt.mul' {F : Type u_2} [NormedAddCommGroup F] [CompleteSpace F] [InnerProductSpace ℝ F] {c' : F} {d' : F} {c : F → ℝ} {d : F → ℝ} {x : F} (hc : HasGradientAt c c' x) (hd : HasGradientAt d d' x) : HasGradientAt (fun (y : F) => c y * d y) (c x • d' + d x • c') x

theorem HasGradientWithinAt.mul' {F : Type u_2} [NormedAddCommGroup F] [CompleteSpace F] {s : Set F} [InnerProductSpace ℝ F] {c' : F} {d' : F} {c : F → ℝ} {d : F → ℝ} {x : F} (hc : HasGradientWithinAt c c' s x) (hd : HasGradientWithinAt d d' s x) : HasGradientWithinAt (fun (y : F) => c y * d y) (c x • d' + d x • c') s x

theorem gradient_mul' {F : Type u_2} [NormedAddCommGroup F] [CompleteSpace F] [InnerProductSpace ℝ F] {c : F → ℝ} {d : F → ℝ} {x : F} (hc : DifferentiableAt ℝ c x) (hd : DifferentiableAt ℝ d x) : gradient (fun (y : F) => c y * d y) x = c x • gradient d x + d x • gradient c x

theorem equiv_lemma_mul_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {c' : F} (d : 𝕜) : d • (InnerProductSpace.toDual 𝕜 F) c' = (InnerProductSpace.toDual 𝕜 F) ((starRingEnd 𝕜) d • c')

theorem HasGradientWithinAt.mul_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {s : Set F} {c' : F} {c : F → 𝕜} {x : F} (d : 𝕜) (hc : HasGradientWithinAt c c' s x) : HasGradientWithinAt (fun (y : F) => c y * d) ((starRingEnd 𝕜) d • c') s x

theorem HasGradientAt.mul_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {c' : F} {c : F → 𝕜} {x : F} (d : 𝕜) (hc : HasGradientAt c c' x) : HasGradientAt (fun (y : F) => c y * d) ((starRingEnd 𝕜) d • c') x

theorem gradient_mul_const {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {c : F → 𝕜} {x : F} (d : 𝕜) (hc : DifferentiableAt 𝕜 c x) : gradient (fun (y : F) => c y * d) x = (starRingEnd 𝕜) d • gradient c x

theorem equiv_lemma_const_mul {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {a' : F} (b : 𝕜) : b • (InnerProductSpace.toDual 𝕜 F) a' = (InnerProductSpace.toDual 𝕜 F) ((starRingEnd 𝕜) b • a')

theorem HasGradientWithinAt.const_mul {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {s : Set F} {a' : F} {a : F → 𝕜} {x : F} (b : 𝕜) (ha : HasGradientWithinAt a a' s x) : HasGradientWithinAt (fun (y : F) => b * a y) ((starRingEnd 𝕜) b • a') s x

theorem HasGradientAt.const_mul {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {a' : F} {a : F → 𝕜} {x : F} (b : 𝕜) (ha : HasGradientAt a a' x) : HasGradientAt (fun (y : F) => b * a y) ((starRingEnd 𝕜) b • a') x

theorem gradient_const_mul {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {a : F → 𝕜} {x : F} (b : 𝕜) (ha : DifferentiableAt 𝕜 a x) : gradient (fun (y : F) => b * a y) x = (starRingEnd 𝕜) b • gradient a x

theorem HasGradientWithinAt.mul_const' {F : Type u_2} [NormedAddCommGroup F] [CompleteSpace F] {s : Set F} [InnerProductSpace ℝ F] {c' : F} {c : F → ℝ} {x : F} (d : ℝ) (hc : HasGradientWithinAt c c' s x) : HasGradientWithinAt (fun (y : F) => c y * d) (d • c') s x

theorem HasGradientAt.mul_const' {F : Type u_2} [NormedAddCommGroup F] [CompleteSpace F] [InnerProductSpace ℝ F] {c' : F} {c : F → ℝ} {x : F} (d : ℝ) (hc : HasGradientAt c c' x) : HasGradientAt (fun (y : F) => c y * d) (d • c') x

theorem gradient_mul_const' {F : Type u_2} [NormedAddCommGroup F] [CompleteSpace F] [InnerProductSpace ℝ F] {c : F → ℝ} {x : F} (d : ℝ) (hc : DifferentiableAt ℝ c x) : gradient (fun (y : F) => c y * d) x = d • gradient c x

theorem HasGradientWithinAt.const_mul' {F : Type u_2} [NormedAddCommGroup F] [CompleteSpace F] {s : Set F} [InnerProductSpace ℝ F] {a' : F} {a : F → ℝ} {x : F} (b : ℝ) (ha : HasGradientWithinAt a a' s x) : HasGradientWithinAt (fun (y : F) => b * a y) (b • a') s x

theorem HasGradientAt.const_mul' {F : Type u_2} [NormedAddCommGroup F] [CompleteSpace F] [InnerProductSpace ℝ F] {a' : F} {a : F → ℝ} {x : F} (b : ℝ) (ha : HasGradientAt a a' x) : HasGradientAt (fun (y : F) => b * a y) (b • a') x

theorem gradient_const_mul' {F : Type u_2} [NormedAddCommGroup F] [CompleteSpace F] [InnerProductSpace ℝ F] {a : F → ℝ} {x : F} (b : ℝ) (ha : DifferentiableAt ℝ a x) : gradient (fun (y : F) => b * a y) x = b • gradient a x