Commit 2025-12-17 18:19 c4c891f1

View on Github →

feat(Counterexamples): Weierstrass function is continuous and nowhere differentiable (#31954)

Estimated changes

Modified Counterexamples.lean

Created Counterexamples/NowhereDifferentiable.lean

added theorem NowhereDifferentiable.exists_uniformContinuous_and_not_differentiableAt

added theorem NowhereDifferentiable.hasSumUniformlyOn_weierstrass

added theorem NowhereDifferentiable.le_seq

added theorem NowhereDifferentiable.lt_seq

added theorem NowhereDifferentiable.not_differentiableAt_weierstrass

added theorem NowhereDifferentiable.not_differentiableAt_weierstrass_seven

added theorem NowhereDifferentiable.seq_le

added theorem NowhereDifferentiable.seq_mul_pow

added theorem NowhereDifferentiable.summable_weierstrass

added theorem NowhereDifferentiable.tendstoUniformly_weierstrass

added theorem NowhereDifferentiable.tendsto_seq

added theorem NowhereDifferentiable.tendsto_seq_sub_inv

added theorem NowhereDifferentiable.uniformContinuous_weierstrass

added def NowhereDifferentiable.weierstrass

added theorem NowhereDifferentiable.weierstrass_partial

added theorem NowhereDifferentiable.weierstrass_remainder

added theorem NowhereDifferentiable.weierstrass_slope

Modified docs/references.bib