Theorems · Theorem · information theory
InformationTheory.not_differentiableWithinAt_klFun_Iio_zero
¬DifferentiableWithinAt ℝ InformationTheory.klFun (Set.Iio 0) 0
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 213 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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.Tendstoproof · cited by 3,814
- nhdsWithinproof · cited by 1,912
- Set.Iiostatement and proof · cited by 1,166
- Filter.atBotproof · cited by 512
- DifferentiableWithinAtstatement · cited by 453
- InformationTheory.klFunstatement and proof · cited by 36
- InformationTheory.deriv_klFunproof · cited by 2
- not_differentiableWithinAt_of_deriv_tendsto_atBot_Iioproof · cited by 2
- Real.tendsto_log_nhdsLT_zeroproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- InformationTheory.leftDeriv_klFunproof · cited by 1