Fix definition of PreProofData.hasBoundedStrongType_Tstar (#212)

The definition of `PreProofData.hasBoundedStrongType_Tstar` said that `(nontangentialOperator K · · |>.toReal)` has bounded strong type, but I think the `toReal` is a mistake; with the `toReal` present, a case where the nontangential operator is ∞ everywhere would qualify as bounded strong type.
fpvandoorn · Jan 20, 2025 · 26325e3 · 26325e3
1 parent 0138d63
commit 26325e3
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Carleson/Defs.lean b/Carleson/Defs.lean
@@ -301,7 +301,7 @@ class PreProofData {X : Type*} (a : outParam ℕ) (q : outParam ℝ) (K : outPar
   c : IsCancellative X (defaultτ a)
   hcz : IsOneSidedKernel a K
   hasBoundedStrongType_Tstar :
-    HasBoundedStrongType (nontangentialOperator K · · |>.toReal) 2 2 volume volume (C_Ts a)
+    HasBoundedStrongType (nontangentialOperator K · ·) 2 2 volume volume (C_Ts a)
   measurableSet_F : MeasurableSet F
   measurableSet_G : MeasurableSet G
   measurable_σ₁ : Measurable σ₁

diff --git a/Carleson/MetricCarleson.lean b/Carleson/MetricCarleson.lean
@@ -26,7 +26,7 @@ theorem metric_carleson [CompatibleFunctions ℝ X (defaultA a)]
   [IsCancellative X (defaultτ a)] [IsOneSidedKernel a K]
     (ha : 4 ≤ a) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjExponent q')
     (hF : MeasurableSet F) (hG : MeasurableSet G)
-    (hT : HasBoundedStrongType (nontangentialOperator K · · |>.toReal) 2 2 volume volume (C_Ts a))
+    (hT : HasBoundedStrongType (nontangentialOperator K · ·) 2 2 volume volume (C_Ts a))
     (f : X → ℂ) (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
     ∫⁻ x in G, carlesonOperator K f x ≤
     ENNReal.ofReal (C1_0_2 a q) * (volume G) ^ q'⁻¹ * (volume F) ^ q⁻¹ := by