Theorems · Theorem · real analysis
norm_iteratedFDeriv_zero
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
{x : E}, ‖iteratedFDeriv 𝕜 0 f x‖ = ‖f x‖- Cited by
- 14 results in Mathlib
- Foundations
- Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- Norm.normstatement and proof · cited by 5,413
- ContinuousMultilinearMapstatement and proof · cited by 1,016
- LinearIsometryEquiv.symmproof · cited by 287
- iteratedFDerivstatement · cited by 211
- LinearIsometryEquiv.norm_mapproof · cited by 39
- continuousMultilinearCurryFin0proof · cited by 34
- iteratedFDeriv_zero_eq_compproof · cited by 4
Cited by14
Results whose statement or proof uses this declaration.
- Function.HasTemperateGrowth.of_fderivproof · cited by 4
- IsOpen.exists_contDiff_support_eqproof · cited by 2
- Function.HasTemperateGrowth.comp'proof · cited by 2
- SchwartzMap.integrable_pow_mulproof · cited by 2
- SchwartzMap.eLpNorm_le_seminormproof · cited by 2
- SchwartzMap.memLp_topproof · cited by 1
- contDiff_tsum_of_eventuallyproof · cited by 1
- SchwartzMap.isBigO_cocompact_zpow_neg_natproof · cited by 1
- SchwartzMap.norm_pow_mul_le_seminormproof · cited by 1
- ContDiffMapSupportedIn.norm_apply_le_seminormproof · cited by 1
- VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegralproof · cited by 1
- SchwartzMap.norm_fourier_Lp_top_leq_toLp_oneproof · cited by 0