9 lines
250 B
Lean4
9 lines
250 B
Lean4
import Mathlib
|
||
|
||
open ComplexConjugate Metric Real
|
||
|
||
theorem test :
|
||
∃ k > 0, ∃ r ∈ Set.Ioo 0 4⁻¹, ∀ ρ ∈ Set.Ioo r 4⁻¹, ∀ θ ≠ 0,
|
||
|log ‖circleMap 0 ρ θ - 1‖| ≤ k * |log ‖circleMap 0 4⁻¹ θ - 1‖| := by
|
||
sorry
|