Theorems · Theorem · functional analysis
MeasureTheory.eLpNorm_exponent_top
∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [inst : ENorm ε] {μ : MeasureTheory.Measure α} {f : α → ε},
MeasureTheory.eLpNorm f ⊤ μ = MeasureTheory.eLpNormEssSup f μ- Cited by
- 36 results in Mathlib
- Foundations
- Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- ENorm
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.
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- ENNRealstatement · cited by 9,879
- Top.topstatement and proof · cited by 9,680
- ENNReal.toRealproof · cited by 859
- MeasureTheory.eLpNormstatement · cited by 329
- ENormstatement and proof · cited by 155
- MeasureTheory.eLpNorm'proof · cited by 73
- MeasureTheory.eLpNormEssSupstatement and proof · cited by 59
Cited by36
Results whose statement or proof uses this declaration.
- MeasureTheory.eLpNorm_negproof · cited by 15
- MeasureTheory.eLpNorm_zeroproof · cited by 14
- MeasureTheory.eLpNorm_measure_zeroproof · cited by 13
- MeasureTheory.eLpNorm_mono_measureproof · cited by 13
- MeasureTheory.memLp_top_of_boundproof · cited by 11
- MeasureTheory.MemLp.mono_exponentproof · cited by 11
- MeasureTheory.eLpNorm_add_leproof · cited by 10
- MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrictproof · cited by 8
- MeasureTheory.eLpNorm_constproof · cited by 5
- MeasureTheory.eLpNorm_eq_zero_iffproof · cited by 5
- MeasureTheory.eLpNorm_indicator_const_leproof · cited by 3
- MeasureTheory.eLpNorm_le_eLpNorm_mul_rpow_measure_univproof · cited by 3