Structures · Analysis
ENorm
Auxiliary class, endowing a type α with a function enorm : α → ℝ≥0∞ with notation ‖x‖ₑ.
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Shape
- One type argument · adds enorm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances1
- ENNReal
How is a type an instance?
Loading the hierarchy index…
Assumed by114
- ENorm.enorm
- MeasureTheory.MemLp
- MeasureTheory.eLpNorm
- MeasureTheory.HasFiniteIntegral
- egauge
- MeasureTheory.eLpNorm'
- MeasureTheory.eLpNormEssSup
- MeasureTheory.eLpNorm_congr_ae
- MeasureTheory.eLpNorm_exponent_zero
- MeasureTheory.eLpNorm_exponent_top
- MeasureTheory.MemLp.aestronglyMeasurable
- MeasureTheory.eLpNorm_eq_eLpNorm'
- MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal
- Manifold.pathELength
- Asymptotics.IsThetaTVS
- MeasureTheory.MemLp.eLpNorm_ne_top
- MeasureTheory.eLpNorm_one_eq_lintegral_enorm
- Manifold.riemannianEDist
- enorm_smul
- MeasureTheory.eLpNorm_measure_zero
- MeasureTheory.MemLp.eLpNorm_lt_top
- MeasureTheory.MemLp.aemeasurable
- MeasureTheory.MemLp.ae_eq
- MeasureTheory.hasFiniteIntegral_iff_enorm
- MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top
- MeasureTheory.eLpNorm_mono_enorm_ae
- MeasureTheory.eLpNorm'_eq_lintegral_enorm
- Asymptotics.IsLittleOTVS.exists_eventuallyLE_mul
- MeasureTheory.eLpNorm_const
- MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top
- MeasureTheory.HasFiniteIntegral.mono_enorm
- Manifold.pathELength_eq_lintegral_mfderivWithin_Icc
- Asymptotics.IsBigOTVS.exists_eventuallyLE
- MeasureTheory.hasFiniteIntegral_const_iff_enorm
- MeasureTheory.eLpNorm_mono_enorm
- MeasureTheory.memLp_congr_ae
- Manifold.riemannianEDist_le_pathELength
- MeasureTheory.HasFiniteIntegral.mono_measure
- MeasureTheory.eLpNorm_congr_enorm_ae
- Manifold.exists_lt_locally_constant_of_riemannianEDist_lt
- MeasureTheory.eLpNormEssSup_measure_zero
- Asymptotics.isLittleOTVS_iff
- MeasureTheory.memLp_zero_iff_aestronglyMeasurable
- MeasureTheory.eLpNorm'_mono_enorm_ae
- Manifold.pathELength_def
- MeasureTheory.enorm_ae_le_eLpNormEssSup
- MeasureTheory.ae_le_eLpNormEssSup
- MeasureTheory.hasFiniteIntegral_congr
- Manifold.pathELength_eq_lintegral_mfderiv_Icc
- MeasureTheory.eLpNorm_const'
Ancestors0
No ancestors.