1 parent 2bfb7ce commit dd587e5Copy full SHA for dd587e5
1 file changed
Ray/Dynamics/Multibrot/Potential.lean
@@ -235,7 +235,7 @@ public lemma potential_error_le_of_z4 (d : ℕ) [Fact (2 ≤ d)] {c z : ℂ}
235
· norm_num; exact (exp_div_lt).le
236
237
/-- `potential_error` bound for `6 ≤ abs z` -/
238
-lemma potential_error_le_of_z6 (d : ℕ) [Fact (2 ≤ d)] {c z : ℂ}
+public lemma potential_error_le_of_z6 (d : ℕ) [Fact (2 ≤ d)] {c z : ℂ}
239
(z6 : 6 ≤ ‖z‖) (cz : ‖c‖ ≤ ‖z‖) :
240
potential_error d c z ≤ 0.8095 / ‖z‖ ^ (1.927 : ℝ) := by
241
apply potential_error_le' d _ (j := 0.0753) (b := 6) (by norm_num) z6 cz (by norm_num)
0 commit comments