Source indexedtheorem · leanprover/lean4:v4.32.0

hasWeakType_maximalFunction

Carleson.ToMathlib.HardyLittlewood · Carleson/ToMathlib/HardyLittlewood.lean:364 to 374

Source documentation

hasStrongType_maximalFunction minus the assumption hR, but where p₁ = p₂ is possible and we only conclude a weak-type estimate.

Exact Lean statement

public theorem hasWeakType_maximalFunction
    [BorelSpace X] [IsFiniteMeasureOnCompacts μ] [ProperSpace X] [μ.IsOpenPosMeasure]
    {p₁ p₂ : ℝ≥0} (hp₁ : 0 < p₁) (hp₁₂ : p₁ ≤ p₂) :
    HasWeakType (fun (u : X → E) (x : X) ↦ maximalFunction μ 𝓑 c r p₁ u x)
      p₂ p₂ μ μ (C_weakType_maximalFunction A p₁ p₂)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

public theorem hasWeakType_maximalFunction    [BorelSpace X] [IsFiniteMeasureOnCompacts μ] [ProperSpace X] [μ.IsOpenPosMeasure]    {p₁ p₂ : ℝ≥0} (hp₁ : 0 < p₁) (hp₁₂ : p₁ ≤ p₂) :    HasWeakType (fun (u : X → E) (x : X) ↦ maximalFunction μ 𝓑 c r p₁ u x)      p₂ p₂ μ μ (C_weakType_maximalFunction A p₁ p₂) := by  unfold C_weakType_maximalFunction  split_ifs with hps  · rw [← hps]    exact hasWeakType_maximalFunction_equal_exponents (A := A) hp₁  · apply HasStrongType.hasWeakType (coe_lt_coe_of_lt (hp₁.trans_le hp₁₂))    exact hasStrongType_maximalFunction hp₁ (lt_of_le_of_ne hp₁₂ hps)