Theorems · Definition · computer science
AkraBazziRecurrence.smoothingFn
ℝ → ℝ
The "smoothing function" is defined as 1 / log n. This is defined as an ℝ → ℝ function
as opposed to ℕ → ℝ since this is more convenient for the proof, where we need to e.g. take
derivatives.
- Cited by
- 45 results in Mathlib
- Foundations
- Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by45
Results whose statement or proof uses this declaration.
- AkraBazziRecurrence.differentiableAt_smoothingFnstatement · cited by 8
- AkraBazziRecurrence.isEquivalent_one_sub_smoothingFn_onestatement · cited by 5
- AkraBazziRecurrence.strictAntiOn_smoothingFnstatement · cited by 4
- AkraBazziRecurrence.isEquivalent_one_add_smoothingFn_onestatement · cited by 4
- AkraBazziRecurrence.deriv_smoothingFnstatement · cited by 3
- AkraBazziRecurrence.eventually_one_add_smoothingFn_posstatement and proof · cited by 3
- AkraBazziRecurrence.isLittleO_smoothingFn_onestatement · cited by 3
- AkraBazziRecurrence.differentiableAt_one_add_smoothingFnstatement · cited by 2
- AkraBazziRecurrence.differentiableAt_one_sub_smoothingFnstatement · cited by 2
- AkraBazziRecurrence.eventually_deriv_one_add_smoothingFnstatement and proof · cited by 2
- AkraBazziRecurrence.eventually_deriv_one_sub_smoothingFnstatement and proof · cited by 2
- AkraBazziRecurrence.eventually_one_sub_smoothingFn_gt_conststatement · cited by 2