Basic API for the centred maximal function and its weak type constant

• le_maximalFunction: every cube average is at most the maximal function;
• exists_lt_average_of_lt_maximalFunction: a level below the maximal function is exceeded by some cube average;
• volume_closedBall_eq: the cube of radius r has volume (2r)ᵈ;
• weakTypeConstant_le, le_weakTypeConstant: the constant is the least weak type bound.

theorem LeanPool.CenteredMaximal.le_maximalFunction {d : ℕ} (f : (Fin d → ℝ) → ℝ) (x : Fin d → ℝ) {r : ℝ} (hr : 0 < r) : (MeasureTheory.volume (Metric.closedBall x r))⁻¹ * ∫⁻ (y : Fin d → ℝ) in Metric.closedBall x r, ‖f y‖ₑ ≤ maximalFunction f x

Every cube average is at most the maximal function.

theorem LeanPool.CenteredMaximal.exists_lt_average_of_lt_maximalFunction {d : ℕ} {f : (Fin d → ℝ) → ℝ} {x : Fin d → ℝ} {α : ENNReal} (h : α < maximalFunction f x) : ∃ (r : ℝ), 0 < r ∧ α < (MeasureTheory.volume (Metric.closedBall x r))⁻¹ * ∫⁻ (y : Fin d → ℝ) in Metric.closedBall x r, ‖f y‖ₑ

A level strictly below the maximal function is exceeded by some cube average.

theorem LeanPool.CenteredMaximal.volume_closedBall_eq {d : ℕ} (x : Fin d → ℝ) {r : ℝ} (hr : 0 ≤ r) : MeasureTheory.volume (Metric.closedBall x r) = ENNReal.ofReal ((2 * r) ^ d)

The closed cube of radius r (side 2r) in ℝᵈ has volume (2r)ᵈ.

theorem LeanPool.CenteredMaximal.IsWeakTypeBound.mono {d : ℕ} {C C' : ENNReal} (h : IsWeakTypeBound d C) (hCC' : C ≤ C') : IsWeakTypeBound d C'

A weak type bound stays a weak type bound when it is increased.

theorem LeanPool.CenteredMaximal.weakTypeConstant_le {d : ℕ} {C : ENNReal} (h : IsWeakTypeBound d C) : weakTypeConstant d ≤ C

The weak type constant is at most every weak type bound.

theorem LeanPool.CenteredMaximal.le_weakTypeConstant {d : ℕ} {c : ENNReal} (h : ∀ (C : ENNReal), IsWeakTypeBound d C → c ≤ C) : c ≤ weakTypeConstant d

A lower bound for every weak type bound is a lower bound for the weak type constant.