a few comments

fpvandoorn · Feb 26, 2025 · f8d081b · f8d081b
1 parent a1a092a
commit f8d081b
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 2 deletions.
diff --git a/Carleson/ToMathlib/HardyLittlewood.lean b/Carleson/ToMathlib/HardyLittlewood.lean
@@ -71,7 +71,8 @@ variable {X E : Type*} {A : ℝ≥0} [MetricSpace X] [MeasurableSpace X]
   {f : X → E} {x : X} {ι : Type*} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ}
   -- feel free to assume `A ≥ 16` or similar
 
-/-- Use the dominated convergence theorem [Folland, Lemma 3.16] -/
+/-- Use the dominated convergence theorem
+e.g. [Folland, Real Analysis. Modern Techniques and Their Applications, Lemma 3.16] -/
 lemma continuous_average_ball (hf : LocallyIntegrable f μ) :
     ContinuousOn (fun x : X × ℝ ↦ ⨍⁻ y in ball x.1 x.2, ‖f y‖ₑ ∂μ) (univ ×ˢ Ioi 0) := by
   sorry

diff --git a/Carleson/ToMathlib/WeakType.lean b/Carleson/ToMathlib/WeakType.lean
@@ -596,6 +596,8 @@ lemma HasWeakType.const_smul {𝕜 E' α α' : Type*} [NormedAddCommGroup E']
     {p p' : ℝ≥0∞} {μ : Measure α} {ν : Measure α'} {c : ℝ≥0} (h : HasWeakType T p p' μ ν c)
     [NormedRing 𝕜] [MulActionWithZero 𝕜 E'] [BoundedSMul 𝕜 E'] (k : 𝕜) :
     HasWeakType (k • T) p p' μ ν (‖k‖₊ * c) := by
+  intro f hf
+  refine ⟨aestronglyMeasurable_const.smul (h f hf).1, ?_⟩
   sorry
 
 lemma HasWeakType.const_mul {E' α α' : Type*} [NormedRing E']

diff --git a/Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean b/Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean
@@ -60,7 +60,7 @@ theorem ball_covering {O : Set X} (hO : IsOpen O ∧ O ≠ univ) :
       ∀ x ∈ O, Cardinal.mk { i | x ∈ ball (c i) (3 * r i)} ≤ (2 ^ (6 * a) : ℕ) := by
   sorry
 
-/-! ### Remarks about Lemma 10.2.5
+/-! ### Lemma 10.2.5
 
 Lemma 10.2.5 has an annoying case distinction between the case `E_α ≠ X` (general case) and
 `E_α = X` (finite case). It isn't easy to get rid of this case distinction.