scilib documentation

theorem fun_split (f g : ℝ → ℝ) :

theorem antideriv_const (f : ℝ → ℝ) (k : ℝ) (hf : ∀ (x : ℝ), has_deriv_at f k x) :

theorem antideriv_pow (f : ℝ → ℝ) (hf : ∀ (x : ℝ) (n : ℕ), has_deriv_at f (x ^ n) x) (n : ℕ) :

theorem antideriv_zpow (f : ℝ → ℝ) (hf : ∀ (x : ℝ), x ≠ 0 ∧ ∀ (z : ℤ), has_deriv_at f (x ^ z) x) (z : ℤ) :

theorem antideriv_first_order_poly {k j : ℝ} (f : ℝ → ℝ) (hf : ∀ (x : ℝ), has_deriv_at f (j * x + k) x) :

theorem constant_of_has_deriv_right_zero' {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} (hderiv : ∀ (x : ℝ), x ∈ set.Icc a b → has_deriv_at f 0 x) (h : a ≤ b) :

theorem antideriv {E : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] {f F G : 𝕜 → E} (hf : ∀ (t : 𝕜), has_deriv_at F (f t) t) (hg : ∀ (t : 𝕜), has_deriv_at G (f t) t) (hg' : G 0 = 0) :

theorem has_deriv_at_linear_no_pow {𝕜 : Type u_3} [is_R_or_C 𝕜] (x : 𝕜) :

theorem antideriv_const' {E : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] (f : 𝕜 → E) {k : E} (hf : ∀ (x : 𝕜), has_deriv_at f k x) :

theorem antideriv_first_order_poly' {E : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] {k j : E} (f : 𝕜 → E) (hf : ∀ (x : 𝕜), has_deriv_at f (x • j + k) x) :