AngularGeometry.lean`

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Angular geometry of the conformal series.

def OAI.MahlerConformal.polar line 16
def OAI.MahlerConformal.Q line 17
def OAI.MahlerConformal.S line 18
def OAI.MahlerConformal.B line 19
lemma OAI.MahlerConformal.norm_polar line 21
lemma OAI.MahlerConformal.polar_ne_zero line 24
lemma OAI.MahlerConformal.polar_re line 27
lemma OAI.MahlerConformal.polar_im line 30
lemma OAI.MahlerConformal.hasDerivAt_polar_complex line 33
lemma OAI.MahlerConformal.hasDerivAt_Q_arg line 39
lemma OAI.MahlerConformal.arg_eq_arctan_of_re_pos line 54
Source documentation
The principal branch gives arctan, rather than an angle modulo pi.
```
lemma arg_eq_arctan_of_re_pos {z : ℂ} (hz : 0 < z.re) :
    z.arg = Real.arctan (z.im / z.re) := by
…
```
lemma OAI.MahlerConformal.cayley_im_div_re line 61
theorem OAI.MahlerConformal.arg_cayley_polar line 82
Source documentation
The branch-sensitive angular identity.
```
theorem arg_cayley_polar {r : ℝ} (hr : 0 < r) (hr1 : r < 1) (θ : ℝ) :
    (cayley (polar r θ)).arg = Real.arctan (2*r*Real.sin θ/(1-r^2)) := by
…
```
Mentions: OAI.MahlerConformal.cayley, OAI.MahlerConformal.polar
theorem OAI.MahlerConformal.hasDerivAt_Q line 91
Source documentation
The derivative of the series' real part is minus B.
```
theorem hasDerivAt_Q {r : ℝ} (hr : 0 < r) (hr1 : r < 1) (θ : ℝ) :
    HasDerivAt (Q r) (-B r θ) θ := by
…
```
Mentions: OAI.MahlerConformal.Q, OAI.MahlerConformal.B
theorem OAI.MahlerConformal.neg_deriv_Q_eq_B line 95
theorem OAI.MahlerConformal.B_pos line 98
theorem OAI.MahlerConformal.B_lt_two_div_pi line 106
theorem OAI.MahlerConformal.Q_strictAntiOn line 113
Source documentation
Strict decrease includes the semicircle endpoints, whose derivatives vanish.
```
theorem Q_strictAntiOn {r : ℝ} (hr : 0 < r) (hr1 : r < 1) :
    StrictAntiOn (Q r) (Icc 0 Real.pi) := by
…
```
Mentions: OAI.MahlerConformal.Q
lemma OAI.MahlerConformal.polar_zero line 122
lemma OAI.MahlerConformal.polar_pi line 124
lemma OAI.MahlerConformal.polar_pi_sub line 126
lemma OAI.MahlerConformal.F_real_im line 129
theorem OAI.MahlerConformal.Q_zero line 134
theorem OAI.MahlerConformal.Q_pi line 136
theorem OAI.MahlerConformal.Q_pi_sub line 139
theorem OAI.MahlerConformal.Q_pi_div_two line 142
theorem OAI.MahlerConformal.S_zero line 147
theorem OAI.MahlerConformal.S_pi line 149
theorem OAI.MahlerConformal.Q_mem_Ioo line 152
theorem OAI.MahlerConformal.existsUnique_angle line 162
Source documentation
Existence and uniqueness of the angle at a fixed radius. The endpoint condition is stated with F(r) itself, with no radial theorem assumed.
```
theorem existsUnique_angle {r q : ℝ} (hr : 0 < r) (hr1 : r < 1)
    (hq : -(F (r : ℂ)).re < q) (hq' : q < (F (r : ℂ)).re) :
    ∃! θ : ℝ, θ ∈ Ioo 0 Real.pi ∧ Q r θ = q := by
…
```
Mentions: OAI.MahlerConformal.F, OAI.MahlerConformal.Q
theorem OAI.MahlerConformal.Q_pos_iff line 185
theorem OAI.MahlerConformal.Q_min_angle line 198
Source documentation
Reflection reduces an upper-semicircle angle to [0, pi/2], and Q to |Q|.
```
theorem Q_min_angle {r θ : ℝ} (hr : 0 < r) (hr1 : r < 1)
    (hθ : θ ∈ Icc 0 Real.pi) :
    Q r (min θ (Real.pi-θ)) = |Q r θ| := by
…
```
Mentions: OAI.MahlerConformal.Q