Theorems · Theorem · real analysis
Asymptotics.isTheta_refl
∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] (f : α → E) (l : Filter α), f =Θ[l] f- Defined in
- Mathlib.Analysis.Asymptotics.Theta
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Norm
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filterstatement and proof · cited by 8,121
- Normstatement and proof · cited by 512
- Asymptotics.IsThetastatement · cited by 115
- Asymptotics.isBigO_reflproof · cited by 51
Cited by12
Results whose statement or proof uses this declaration.
- Asymptotics.isTheta_rflproof · cited by 4
- AkraBazziRecurrence.isTheta_smoothingFn_sub_selfproof · cited by 2
- Complex.isTheta_cpow_rpowproof · cited by 1
- AkraBazziRecurrence.rpow_p_mul_one_add_smoothingFn_geproof · cited by 1
- AkraBazziRecurrence.rpow_p_mul_one_sub_smoothingFn_leproof · cited by 1
- AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_add_smoothingFnproof · cited by 1
- AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFnproof · cited by 1
- AkraBazziRecurrence.isTheta_deriv_rpow_p_mul_one_add_smoothingFnproof · cited by 1
- AkraBazziRecurrence.isTheta_deriv_rpow_p_mul_one_sub_smoothingFnproof · cited by 1
- EisensteinSeries.vec_add_const_isThetaproof · cited by 1
- Complex.isBigO_cpow_rpowproof · cited by 0
- Asymptotics.IsTheta.rpowproof · cited by 0