AngularIntegrals.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Angular integral and sine estimate.

lemma OAI.MahlerConformal.continuous_B line 14
theorem OAI.MahlerConformal.integral_B line 19
Source documentation
Fundamental theorem of calculus for the actual angular derivative.
```
theorem integral_B {r : ℝ} (hr : 0 < r) (hr1 : r < 1) (a b : ℝ) :
    (∫ θ in a..b, B r θ) = Q r a - Q r b := by
…
```
Mentions: OAI.MahlerConformal.B, OAI.MahlerConformal.Q
theorem OAI.MahlerConformal.integral_B_semicircle line 30
Source documentation
The normalization identity for the angular integral.
```
theorem integral_B_semicircle {r : ℝ} (hr : 0 < r) (hr1 : r < 1) :
    (∫ θ in (0 : ℝ)..Real.pi, B r θ) = 2*(F (r : ℂ)).re := by
…
```
Mentions: OAI.MahlerConformal.B, OAI.MahlerConformal.F
lemma OAI.MahlerConformal.arctan_le_self_nonneg line 35
lemma OAI.MahlerConformal.B_le_linear line 39
theorem OAI.MahlerConformal.Q_drop_le_quadratic line 54
Source documentation
The quadratic angular estimate, with C=4/pi².
```
theorem Q_drop_le_quadratic {r d : ℝ} (hr : 0 < r) (hr1 : r < 1)
    (hd : d ∈ Icc 0 Real.pi) :
    (F (r : ℂ)).re - Q r d ≤ 4*r*d^2/(Real.pi^2*(1-r^2)) := by
…
```
Mentions: OAI.MahlerConformal.F, OAI.MahlerConformal.Q
theorem OAI.MahlerConformal.sine_bound line 78
Source documentation
The reflected angle gives the sine estimate with the explicit absolute constant c=1. This theorem is about F itself and assumes no inverse map.
```
theorem sine_bound {r θ : ℝ} (hr : 0 < r) (hr1 : r < 1)
    (hθ : θ ∈ Icc 0 Real.pi) :
    Real.sqrt ((1-r^2)*((F (r : ℂ)).re - |Q r θ|)/r) ≤ Real.sin θ := by
…
```
Mentions: OAI.MahlerConformal.F, OAI.MahlerConformal.Q