Update RemainingTiles.lean

fpvandoorn · Nov 10, 2024 · f0d40b1 · f0d40b1
1 parent a5fb290
commit f0d40b1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Carleson/ForestOperator/RemainingTiles.lean b/Carleson/ForestOperator/RemainingTiles.lean
@@ -121,7 +121,7 @@ lemma square_function_count (hJ : J ∈ 𝓙₆ t u₁) (s' : ℤ) :
       (fun _ _ ↦ measurableSet_ball) (fun _ _ ↦ measure_ball_ne_top _ _)]
     simp only [Nat.cast_pow, Nat.cast_ofNat]
     gcongr
-    · sorry -- TODO fix, max application depth! finiteness
+    · exact measure_ball_ne_top _ _ -- TODO fix, max application depth! finiteness
     · simp only [mem_toFinset, iUnion_subset_iff]
       intro I hI
       apply ball_subset_ball'