Theorems · Definition · functional analysis

MeasureTheory.eLpNormLESNormFDerivOneConst

{E : Type u_5} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      [inst_2 : MeasurableSpace E] →
        [BorelSpace E] → [FiniteDimensional ℝ E] → (μ : MeasureTheory.Measure E) → [μ.IsAddHaarMeasure] → ℝ → NNReal

The constant factor occurring in the conclusion of eLpNorm_le_eLpNorm_fderiv_one. It only depends on E, μ and p.

Defined in: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Cited by: 4 results in Mathlib
Foundations: Depth 278 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup NormedSpace MeasurableSpace BorelSpace FiniteDimensional MeasureTheory.Measure.IsAddHaarMeasure

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement · cited by 25,697
NormedAddCommGroupstatement · cited by 15,752
MeasurableSpacestatement · cited by 13,106
NormedSpacestatement · cited by 12,499
MeasureTheory.Measurestatement · cited by 10,939
NNRealstatement · cited by 4,310
FiniteDimensionalstatement · cited by 1,854
BorelSpacestatement · cited by 1,602
MeasureTheory.Measure.IsAddHaarMeasurestatement · cited by 255

Cited by5

Results whose statement or proof uses this declaration.

MeasureTheory.eLpNormLESNormFDerivOfEqInnerConstproof · cited by 4
MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq_innerproof · cited by 1
MeasureTheory.eLpNormLESNormFDerivOneConst_defstatement · cited by 1
MeasureTheory.eLpNorm_le_eLpNorm_fderiv_onestatement and proof · cited by 1
MeasureTheory.eLpNormLESNormFDerivOneConst.congr_simpstatement and proof · cited by 0