def MeasureTheory.Lorentz {α : Type u_1} {ε : Type u_2} (p q : ENNReal) {m0 : MeasurableSpace α} (μ : Measure α) [NoAtoms μ] [TopologicalSpace ε] [ESeminormedAddMonoid ε] [ContinuousAdd ε] : AddSubmonoid (α →ₘ[μ] ε)

TODO: basic results

Equations

• MeasureTheory.Lorentz p q μ = { carrier := {f : α →ₘ[μ] ε | MeasureTheory.eLorentzNorm (↑f) p q μ < ⊤}, add_mem' := ⋯, zero_mem' := ⋯ }