Theorems · Theorem · computer science

AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn

∀ {p : ℝ},
  p ≠ 0 →
    Asymptotics.IsEquivalent Filter.atTop (deriv fun z => z ^ p * (1 - AkraBazziRecurrence.smoothingFn z)) fun z =>
      p * z ^ (p - 1)

Defined in: Mathlib.Computability.AkraBazzi.AkraBazzi
Cited by: 1 results in Mathlib
Foundations: Depth 216 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites26

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
Filter.Eventuallyproof · cited by 3,134
Nat.cast_oneproof · cited by 2,501
Filter.atTopstatement and proof · cited by 2,405
Real.logproof · cited by 939
div_eq_mul_invproof · cited by 715
derivstatement · cited by 676
div_oneproof · cited by 629
Filter.Tendsto.compproof · cited by 560
Asymptotics.IsLittleOproof · cited by 375
Asymptotics.IsEquivalentstatement · cited by 98
Asymptotics.isBigO_reflproof · cited by 51

Cited by1

Results whose statement or proof uses this declaration.

AkraBazziRecurrence.isTheta_deriv_rpow_p_mul_one_sub_smoothingFnproof · cited by 1