Lemmas

Main results

This file contains the following parts of basic properties of continuous and differentiable lemmas

• the equivalent definition of continuous functions
• the equivalent definition of fderiv and gradient
• the deriv of composed function on a segment
• the gradient of special functions with inner product and norm
• the taylor expansion of a differentiable function locally
• the langrange interpolation of a differentiable function

theorem ContinuousAt_Convergence {E : Type u_1} [NormedAddCommGroup E] {f : E → ℝ} {x : E} (h : ContinuousAt f x) (ε : ℝ) : ε > 0 → ∃ δ > 0, ∀ (x' : E), ‖x - x'‖ ≤ δ → ‖f x' - f x‖ ≤ ε

theorem Convergence_ContinuousAt {E : Type u_1} [NormedAddCommGroup E] {f : E → ℝ} {x : E} (h : ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x - x'‖ ≤ δ → ‖f x' - f x‖ ≤ ε) : ContinuousAt f x

theorem ContinuousAt_iff_Convergence {E : Type u_1} [NormedAddCommGroup E] {f : E → ℝ} {x : E} : ContinuousAt f x ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x - x'‖ ≤ δ → ‖f x' - f x‖ ≤ ε

theorem continuous {E : Type u_1} [NormedAddCommGroup E] {f : E → ℝ} {x : E} (h : ContinuousAt f x) (ε : ℝ) : ε > 0 → ∃ δ > 0, ∀ (y : E), ‖y - x‖ < δ → ‖f y - f x‖ < ε

theorem deriv_function_comp_segment {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E → E →L[ℝ] ℝ} (x : E) (y : E) (h₁ : ∀ (x₁ : E), HasFDerivAt f (f' x₁) x₁) (t₀ : ℝ) : HasDerivAt (fun (t : ℝ) => f (x + t • (y - x))) ((fun (t : ℝ) => (f' (x + t • (y - x))) (y - x)) t₀) t₀

theorem HasFDeriv_Convergence {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E → E →L[ℝ] ℝ} {x : E} (h : HasFDerivAt f (f' x) x) (ε : ℝ) : ε > 0 → ∃ δ > 0, ∀ (x' : E), ‖x - x'‖ ≤ δ → ‖f x' - f x - (f' x) (x' - x)‖ ≤ ε * ‖x - x'‖

theorem Convergence_HasFDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E → E →L[ℝ] ℝ} {x : E} (h : ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x - x'‖ ≤ δ → ‖f x' - f x - (f' x) (x' - x)‖ ≤ ε * ‖x - x'‖) : HasFDerivAt f (f' x) x

theorem HasFDeriv_iff_Convergence_Point {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {f'x : E →L[ℝ] ℝ} : HasFDerivAt f f'x x ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x - x'‖ ≤ δ → ‖f x' - f x - f'x (x' - x)‖ ≤ ε * ‖x - x'‖

theorem HasFDeriv_iff_Convergence {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E → E →L[ℝ] ℝ} {x : E} : HasFDerivAt f (f' x) x ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x - x'‖ ≤ δ → ‖f x' - f x - (f' x) (x' - x)‖ ≤ ε * ‖x - x'‖

theorem HasGradient_Convergence {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {x : E} {f : E → ℝ} {f' : E → E} (h : HasGradientAt f (f' x) x) (ε : ℝ) : ε > 0 → ∃ δ > 0, ∀ (x' : E), ‖x - x'‖ ≤ δ → ‖f x' - f x - ⟪f' x, x' - x⟫_ℝ‖ ≤ ε * ‖x - x'‖

theorem Convergence_HasGradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {x : E} {f : E → ℝ} {f' : E → E} (h : ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x - x'‖ ≤ δ → ‖f x' - f x - ⟪f' x, x' - x⟫_ℝ‖ ≤ ε * ‖x - x'‖) : HasGradientAt f (f' x) x

theorem HasGradient_iff_Convergence_Point {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {x : E} {f : E → ℝ} {f'x : E} : HasGradientAt f f'x x ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x - x'‖ ≤ δ → ‖f x' - f x - ⟪f'x, x' - x⟫_ℝ‖ ≤ ε * ‖x - x'‖

theorem HasGradient_iff_Convergence {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {x : E} {f : E → ℝ} {f' : E → E} : HasGradientAt f (f' x) x ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x - x'‖ ≤ δ → ‖f x' - f x - ⟪f' x, x' - x⟫_ℝ‖ ≤ ε * ‖x - x'‖

theorem gradient_norm_sq_eq_two_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (x : E) : HasGradientAt (fun (x : E) => ‖x‖ ^ 2) (2 • x) x

theorem gradient_of_inner_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (x : E) (a : E) : HasGradientAt (fun (x : E) => ⟪a, x⟫_ℝ) a x

theorem gradient_of_const_mul_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (l : ℝ) (z : E) : HasGradientAt (fun (x : E) => l / 2 * ‖x‖ ^ 2) (l • z) z

theorem gradient_of_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {x : E} (u : E) : HasGradientAt (fun (u : E) => ‖u - x‖ ^ 2 / 2) (u - x) u

theorem sub_normsquare_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {f' : E → E} {s : Set E} (hf : ∀ x ∈ s, HasGradientAt f (f' x) x) (m : ℝ) (x : E) : x ∈ s → HasGradientAt (fun (x : E) => f x - m / 2 * ‖x‖ ^ 2) (f' x - m • x) x

theorem gradient_continuous_of_contdiff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {x : E} {ε : ℝ} (f : E → ℝ) (he : ε > 0) (hf : ContDiffOn ℝ 1 f (Metric.ball x ε)) : ContinuousAt (fun (x : E) => gradient f x) x

theorem expansion {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {f' : E → E} (hf : ∀ (x : E), HasGradientAt f (f' x) x) (x : E) (p : E) : ∃ t > 0, t < 1 ∧ f (x + p) = f x + ⟪f' (x + t • p), p⟫_ℝ

theorem general_expansion {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {f' : E → E} (x : E) (p : E) (hf : ∀ y ∈ Metric.closedBall x ‖p‖, HasGradientAt f (f' y) y) : ∃ t > 0, t < 1 ∧ f (x + p) = f x + ⟪f' (x + t • p), p⟫_ℝ

theorem lagrange {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {f' : E → E} {s : Set E} (hs : Convex ℝ s) (hf : ∀ x ∈ s, HasGradientAt f (f' x) x) (x : E) : x ∈ s → ∀ y ∈ s, ∃ c ∈ Set.Ioo 0 1, ⟪f' (x + c • (y - x)), y - x⟫_ℝ = f y - f x