Measure-theoretic bridge for finite L^p norms

On a nonempty finite type α with measurable singletons and 0 < p, Cslib.lpNorm p f agrees with Mathlib's MeasureTheory.lpNorm with respect to both ProbabilityTheory.uniformOn Set.univ (Cslib.lpNorm_eq_measureTheory_lpNorm_uniformOn) and CSLib's (Probability.PMF.uniformOfFintype α).toMeasure (Cslib.lpNorm_eq_measureTheory_lpNorm).

Main results

• Cslib.lpNorm_eq_measureTheory_lpNorm_uniformOn: agreement with MeasureTheory.lpNorm under ProbabilityTheory.uniformOn Set.univ.
• Cslib.lpNorm_eq_measureTheory_lpNorm: agreement with MeasureTheory.lpNorm under (Probability.PMF.uniformOfFintype α).toMeasure.

theorem Cslib.lpNorm_eq_measureTheory_lpNorm_uniformOn {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {p : ℝ} (hp : 0 < p) (f : α → ℝ) : lpNorm p f = MeasureTheory.lpNorm f (ENNReal.ofReal p) (ProbabilityTheory.uniformOn Set.univ)

For 0 < p on a nonempty finite type with measurable singletons, lpNorm p f is Mathlib's MeasureTheory.lpNorm with respect to ProbabilityTheory.uniformOn Set.univ.

theorem Cslib.lpNorm_eq_measureTheory_lpNorm {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {p : ℝ} (hp : 0 < p) (f : α → ℝ) : lpNorm p f = MeasureTheory.lpNorm f (ENNReal.ofReal p) (Probability.PMF.uniformOfFintype α).toMeasure

For 0 < p on a nonempty finite type with measurable singletons, lpNorm p f is Mathlib's MeasureTheory.lpNorm with respect to (PMF.uniformOfFintype α).toMeasure.