Prove MeasureTheory.SublinearOn.maximalFunction

[js2357]

• The definition of SublinearOn was missing the requirement c ≥ 0.
• The statement of MeasureTheory.SublinearOn.maximalFunction had a spurious p; MB is defined with p=1, so there's no need for a general p.
• The blueprint says that 𝓑 is finite, so I used that assumption even though several theorems in the file assume 𝓑 is countable instead. I also changed the assumption in hasStrongType_MB.

[fpvandoorn]

Suggested change

	lemma setLaverage_add_left' {α : Type*} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
	lemma setLAverage_add_left' {α : Type*} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}

also elsewhere

[fpvandoorn]

Thanks!
I was hoping we could generalize this to countable 𝓑, but it's no problem if we cannot.