AngularEndpoint.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The bounded-convergence normalization M(r) → 1.

lemma OAI.MahlerConformal.eventually_radius line 13
lemma OAI.MahlerConformal.B_nonneg line 15
theorem OAI.MahlerConformal.B_tendsto_one line 25
Source documentation
Pointwise interior-angle limit; the endpoint angles are intentionally excluded.
```
theorem B_tendsto_one {θ : ℝ} (hθ : 0 < θ) (hθπ : θ < Real.pi) :
    Tendsto (fun r => B r θ) (𝓝[<] 1) (𝓝 (2/Real.pi)) := by
…
```
Mentions: OAI.MahlerConformal.B
theorem OAI.MahlerConformal.integral_B_tendsto_one line 48
Source documentation
Bounded convergence applied to the actual angular speed of F.
```
theorem integral_B_tendsto_one :
    Tendsto (fun r => ∫ θ in (0 : ℝ)..Real.pi, B r θ) (𝓝[<] 1) (𝓝 2) := by
…
```
Mentions: OAI.MahlerConformal.B
theorem OAI.MahlerConformal.F_real_tendsto_one line 73
Source documentation
The real part of M(r)=F(r) tends to 1. No radial derivative or assumed endpoint normalization is used.
```
theorem F_real_tendsto_one :
    Tendsto (fun r : ℝ => (F (r : ℂ)).re) (𝓝[<] 1) (𝓝 1) := by
…
```
Mentions: OAI.MahlerConformal.F