Theorems · Theorem · functional analysis

MeasureTheory.lintegralPowLePowLIntegralFDerivConst_def

∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [inst_5 : μ.IsAddHaarMeasure]
  (p : ℝ),
  MeasureTheory.lintegralPowLePowLIntegralFDerivConst μ p =
    let ι := Fin (Module.finrank ℝ E);
    have this := ⋯;
    let e := ContinuousLinearEquiv.ofFinrankEq this;
    have c := μ.addHaarScalarFactor (MeasureTheory.Measure.map (⇑e.symm) MeasureTheory.volume);
    c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹

Defined in

Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Cited by

1 results in Mathlib

Foundations

Depth 275 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceFiniteDimensionalMeasureTheory.Measure.IsAddHaarMeasure