PrimeNumberTheoremAnd.Auxiliary

Auxiliary lemmas #

source

theorem Complex.hasDerivAt_ofReal (x : ℝ) :

HasDerivAt ofReal 1 x

Inspect dependencies

Complex.hasDerivAt_ofReal · compiled type and proof/definition references.

source

theorem Complex.deriv_ofReal (x : ℝ) :

deriv ofReal x = 1

Inspect dependencies

Complex.deriv_ofReal · compiled type and proof/definition references.

source

theorem Complex.differentiableAt_ofReal (x : ℝ) :

DifferentiableAt ℝ ofReal x

Inspect dependencies

Complex.differentiableAt_ofReal · compiled type and proof/definition references.

source

theorem DifferentiableAt.comp_ofReal {e : ℂ → ℂ} {z : ℝ} (hf : DifferentiableAt ℂ e ↑z) :

DifferentiableAt ℝ (fun (x : ℝ) => e ↑x) z

Inspect dependencies

DifferentiableAt.comp_ofReal · compiled type and proof/definition references.

source

theorem deriv.comp_ofReal {e : ℂ → ℂ} {z : ℝ} (hf : DifferentiableAt ℂ e ↑z) :

deriv (fun (x : ℝ) => e ↑x) z = deriv e ↑z

Inspect dependencies

deriv.comp_ofReal · compiled type and proof/definition references.

source

theorem Differentiable.comp_ofReal {e : ℂ → ℂ} (h : Differentiable ℂ e) :

Differentiable ℝ fun (x : ℝ) => e ↑x

Inspect dependencies

Differentiable.comp_ofReal · compiled type and proof/definition references.

source

theorem DifferentiableAt.ofReal_comp {z : ℝ} {f : ℝ → ℝ} (hf : DifferentiableAt ℝ f z) :

DifferentiableAt ℝ (fun (y : ℝ) => ↑(f y)) z

Inspect dependencies

DifferentiableAt.ofReal_comp · compiled type and proof/definition references.

source

theorem Differentiable.ofReal_comp {f : ℝ → ℝ} (hf : Differentiable ℝ f) :

Differentiable ℝ fun (y : ℝ) => ↑(f y)

Inspect dependencies

Differentiable.ofReal_comp · compiled type and proof/definition references.

source

theorem HasDerivAt.of_hasDerivAt_ofReal_comp {z : ℝ} {f : ℝ → ℝ} {u : ℂ} (hf : HasDerivAt (fun (y : ℝ) => ↑(f y)) u z) :

∃ (u' : ℝ), u = ↑u' ∧ HasDerivAt f u' z

Inspect dependencies

HasDerivAt.of_hasDerivAt_ofReal_comp · compiled type and proof/definition references.

source

theorem DifferentiableAt.ofReal_comp_iff {z : ℝ} {f : ℝ → ℝ} :

DifferentiableAt ℝ (fun (y : ℝ) => ↑(f y)) z ↔ DifferentiableAt ℝ f z

Inspect dependencies

DifferentiableAt.ofReal_comp_iff · compiled type and proof/definition references.

source

theorem Differentiable.ofReal_comp_iff {f : ℝ → ℝ} :

(Differentiable ℝ fun (y : ℝ) => ↑(f y)) ↔ Differentiable ℝ f

Inspect dependencies

Differentiable.ofReal_comp_iff · compiled type and proof/definition references.

source

theorem deriv.ofReal_comp {z : ℝ} {f : ℝ → ℝ} :

deriv (fun (y : ℝ) => ↑(f y)) z = ↑(deriv f z)

Inspect dependencies

deriv.ofReal_comp · compiled type and proof/definition references.