Theorems · Definition · real analysis
minSmoothness
(𝕜 : Type u_4) → [NontriviallyNormedField 𝕜] → WithTop ℕ∞ → WithTop ℕ∞
minSmoothness 𝕜 n is the minimal smoothness exponent larger than or equal to n for which
one can do serious calculus in 𝕜. If 𝕜 is ℝ or ℂ, this is just n. Otherwise,
this is ω as only analytic functions are well behaved on ℚₚ, say.
- Cited by
- 50 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NontriviallyNormedField
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NontriviallyNormedFieldstatement · cited by 8,742
- ENatstatement · cited by 4,985
- WithTopstatement · cited by 3,754
Cited by50
Results whose statement or proof uses this declaration.
- le_minSmoothnessstatement · cited by 23
- minSmoothness_defstatement · cited by 7
- ContDiffWithinAt.isSymmSndFDerivWithinAtstatement and proof · cited by 6
- ContDiffAt.isSymmSndFDerivAtstatement and proof · cited by 4
- VectorField.mpullback_mlieBracketWithinstatement and proof · cited by 3
- ContMDiffWithinAt.mlieBracketWithin_vectorFieldstatement and proof · cited by 3
- minSmoothness_addstatement · cited by 3
- minSmoothness_monotonestatement · cited by 3
- VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symmstatement · cited by 3
- VectorField.mpullbackWithin_mlieBracketWithin'statement and proof · cited by 2
- VectorField.mpullback_mlieBracketstatement and proof · cited by 2
- minSmoothness_of_isRCLikeNormedFieldstatement · cited by 2