Definitions in the public statement

The maximal operator is defined on real-valued integrable functions using Lebesgue measure. These definitions agree with the independently stated upstream comparator challenge.

noncomputable def LeanPool.CenteredMaximal.maximalFunction {d : ℕ} (f : (Fin d → ℝ) → ℝ) (x : Fin d → ℝ) : ENNReal

The centred Hardy–Littlewood maximal function of f : ℝᵈ → ℝ over axis-parallel cubes: M f (x) = sup_{r > 0} |Q(x, r)|⁻¹ ∫_{Q(x, r)} |f|, with values in [0, ∞].

Since Fin d → ℝ carries the sup norm, closedBall x r is the closed cube ∏ᵢ [xᵢ - r, xᵢ + r] of side length 2r centred at x; volume is Lebesgue measure.

Equations

• LeanPool.CenteredMaximal.maximalFunction f x = ⨆ (r : ℝ), ⨆ (_ : 0 < r), (MeasureTheory.volume (Metric.closedBall x r))⁻¹ * ∫⁻ (y : Fin d → ℝ) in Metric.closedBall x r, ‖f y‖ₑ

def LeanPool.CenteredMaximal.IsWeakTypeBound (d : ℕ) (C : ENNReal) : Prop

C is a weak type (1, 1) bound for the centred maximal operator in dimension d: for every integrable f : ℝᵈ → ℝ and every level α ∈ [0, ∞], α · |{x : M f (x) > α}| ≤ C · ‖f‖₁.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.CenteredMaximal.weakTypeConstant (d : ℕ) : ENNReal

The weak type (1, 1) constant c_d of the centred Hardy–Littlewood maximal operator over axis-parallel cubes in ℝᵈ: the least weak type bound.

Equations

• LeanPool.CenteredMaximal.weakTypeConstant d = sInf {C : ENNReal | LeanPool.CenteredMaximal.IsWeakTypeBound d C}

noncomputable def LeanPool.CenteredMaximal.phi : ℝ

The constant Φ = 1.68550999335552518…, an explicit radical expression: Φ = ((77 + 16√22)/2 - (8 + √22 - √(70 + 8√22)) (11 + √22 - 2√2 - 2√11 - √(17 + 4√22))) / (26 + 4√22).

It bounds the covered area per unit mass of a periodic measure from below: unit masses and masses w = (17 + 4√22)/9 alternate along the columns x = i h, h = (5 + √22)/6, and the rows are y = j V, V = (11 + √22)/6.

Equations

• LeanPool.CenteredMaximal.phi = ((77 + 16 * √22) / 2 - (8 + √22 - √(70 + 8 * √22)) * (11 + √22 - 2 * √2 - 2 * √11 - √(17 + 4 * √22))) / (26 + 4 * √22)