The upper bound c_d ≤ 2ᵈ

Let E = {M f > α}. Every x ∈ E is the centre of a cube Q_x with α |Q_x| < ∫_{Q_x} |f|; these cubes have bounded radii. Mathlib's Vitali lemma with enlargement τ > 1 selects a disjoint subfamily such that every Q_x meets a selected Q_b with r_x ≤ τ r_b. Then the centre x lies in the cube of radius (1 + τ) r_b about b; covering only the centres is what saves the factor 3ᵈ of the uncentred argument. Summing over the disjoint selected cubes gives α |E| ≤ (1 + τ)ᵈ ‖f‖₁, and letting τ → 1 gives 2ᵈ (Tao, 245A Notes 5, Exercise 42, whose hint notes that one needs an epsilon of room).

theorem LeanPool.CenteredMaximal.isWeakTypeBound_zero_one : IsWeakTypeBound 0 1

In dimension 0 the space Fin 0 → ℝ is a single point of volume 1, and 1 is a weak type bound. This is the case d = 0 of isWeakTypeBound_two_pow.

theorem LeanPool.CenteredMaximal.radius_le_of_mul_volume_lt {d : ℕ} (hd : 0 < d) {α K : ENNReal} (hα : 0 < α) (hα' : α ≠ ⊤) (hK : K ≠ ⊤) {x : Fin d → ℝ} {r : ℝ} (hr : 0 < r) (h : α * MeasureTheory.volume (Metric.closedBall x r) < K) : r ≤ max 1 (K / α).toReal

In positive dimension, a cube whose volume times α ∈ (0, ∞) stays below a finite K has radius at most max 1 (K / α). With K = ‖f‖₁ this is the uniform bound on the radii of the cubes in mul_volume_le_of_one_lt, which the Vitali covering lemma requires.

theorem LeanPool.CenteredMaximal.mul_volume_le_of_one_lt {d : ℕ} (hd : 0 < d) {f : (Fin d → ℝ) → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (α : ENNReal) {τ : ℝ} (hτ : 1 < τ) : α * MeasureTheory.volume {x : Fin d → ℝ | α < maximalFunction f x} ≤ ENNReal.ofReal ((1 + τ) ^ d) * ∫⁻ (x : Fin d → ℝ), ‖f x‖ₑ

Weak type bound with an epsilon of room: in positive dimension, α |{M f > α}| ≤ (1 + τ)ᵈ ‖f‖₁ for every τ > 1. Letting τ → 1 gives the bound 2ᵈ of isWeakTypeBound_two_pow; the case d = 0 is isWeakTypeBound_zero_one.

theorem LeanPool.CenteredMaximal.isWeakTypeBound_two_pow (d : ℕ) : IsWeakTypeBound d (2 ^ d)

2ᵈ is a weak type bound in dimension d, so weakTypeConstant d ≤ 2 ^ d by weakTypeConstant_le. Compare mul_volume_le_of_one_lt, which gives only the weaker bound (1 + τ)ᵈ for each fixed τ > 1, and only in positive dimension.