add_pos (#112)

Hi, I wanna join your project!
fpvandoorn · Sep 9, 2024 · 3aa1515 · 3aa1515
1 parent cbd59e1
commit 3aa1515
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Carleson/Discrete/Forests.lean b/Carleson/Discrete/Forests.lean
@@ -669,7 +669,7 @@ lemma forest_complement {f : X → ℂ} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1
 which has value `2 ^ (440 * a ^ 3) / (q - 1) ^ 5` in the blueprint. -/
 def C2_0_2 (a : ℝ) (q : ℝ≥0) : ℝ≥0 := C5_1_2 a q + C5_1_3 a q
 
-lemma C2_0_2_pos : C2_0_2 a nnq > 0 := sorry
+lemma C2_0_2_pos : C2_0_2 a nnq > 0 := add_pos C5_1_2_pos C5_1_3_pos
 
 variable (X) in
 theorem discrete_carleson :