update comment

Author: fpvandoorn

Carleson/Defs.lean

@@ -243,7 +243,7 @@ def ClassicalCarleson : Prop :=
   ∀ {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * π)),
     ∀ᵐ x, Filter.Tendsto (S_ · f x) Filter.atTop (nhds (f x))
 
-/-- The constant used in the statement of `MetricSpaceCarleson`.
+/-- The constant used in `MetricSpaceCarleson` and `LinearizedMetricCarleson`.
 Has value `2 ^ (443 * a ^ 3)` in the blueprint. -/
 def C1_0_2 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := 2 ^ ((3 * 𝕔 + 18 + 5 * (𝕔 / 4)) * a ^ 3) / (q - 1) ^ 6