theorem MeasureTheory.eLpNormEssSup_congr_measure {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {f : α → ε} {μ ν : Measure α} (h : ae ν = ae μ) : eLpNormEssSup f ν = eLpNormEssSup f μ

theorem MeasureTheory.eLpNormEssSup_withDensity {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [ENorm ε] {f : α → ε} {μ : Measure α} {d : α → ENNReal} (hd : AEMeasurable d μ) (hd' : ∀ᵐ (x : α) ∂μ, d x ≠ 0) : eLpNormEssSup f (μ.withDensity d) = eLpNormEssSup f μ

theorem MeasureTheory.eLpNormEssSup_nnreal_scale_constant' {f : NNReal → ENNReal} {a : NNReal} (h : a ≠ 0) (hf : AEStronglyMeasurable f volume) : eLpNormEssSup (fun (x : NNReal) => f (a * x)) volume = eLpNormEssSup f volume

theorem MeasureTheory.eLpNorm_withDensity_scale_constant' {f : NNReal → ENNReal} (hf : AEStronglyMeasurable f volume) {p : ENNReal} {a : NNReal} (h : a ≠ 0) : eLpNorm (fun (t : NNReal) => f (a * t)) p (volume.withDensity fun (t : NNReal) => (↑t)⁻¹) = eLpNorm f p (volume.withDensity fun (t : NNReal) => (↑t)⁻¹)