AngularStrip.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Real-part image and real preimages of the conformal map.

lemma OAI.MahlerConformal.F_real_pos line 12
lemma OAI.MahlerConformal.F_real_lt_one line 17
lemma OAI.MahlerConformal.polar_neg_angle line 28
lemma OAI.MahlerConformal.Q_neg_angle line 31
lemma OAI.MahlerConformal.Q_mem_Icc line 34
theorem OAI.MahlerConformal.F_re_mem_strip line 42
Source documentation
Every image point has real part in the strip.
```
theorem F_re_mem_strip {w : ℂ} (hw : ‖w‖ < 1) : (F w).re ∈ Ioo (-1 : ℝ) 1 := by
…
```
Mentions: OAI.MahlerConformal.F
theorem OAI.MahlerConformal.eventually_existsUnique_angle line 61
Source documentation
Every strip real part has its unique angular preimage for all sufficiently large radii below one. No radial monotonicity theorem is assumed.
```
theorem eventually_existsUnique_angle {q : ℝ} (hq : q ∈ Ioo (-1 : ℝ) 1) :
    ∀ᶠ r : ℝ in 𝓝[<] 1, ∃! θ : ℝ, θ ∈ Ioo 0 Real.pi ∧ Q r θ = q := by
…
```
Mentions: OAI.MahlerConformal.Q
lemma OAI.MahlerConformal.continuousOn_F_real line 69
theorem OAI.MahlerConformal.exists_real_preimage line 79
Source documentation
Every point on the real interval (-1,1) is the actual value F(t) at a real point t in the disk. This is existence only; it does not assert univalence.
```
theorem exists_real_preimage {q : ℝ} (hq : q ∈ Ioo (-1 : ℝ) 1) :
    ∃ t : ℝ, t ∈ Ioo (-1 : ℝ) 1 ∧ F (t : ℂ) = (q : ℂ) := by
…
```
Mentions: OAI.MahlerConformal.F
theorem OAI.MahlerConformal.image_re_F_disk line 100
Source documentation
The set of real parts of the image is exactly (-1,1). This does not assert that each vertical fiber is an interval.
```
theorem image_re_F_disk : Complex.re '' (F '' ball (0 : ℂ) 1) = Ioo (-1 : ℝ) 1 := by
…
```
Mentions: OAI.MahlerConformal.F