Endpoints.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.StrictInverseFirstPower.uniform_inverse_first_power_gap line 13
Source documentation
A single, strictly positive gap works for every normalized univalent map, and hence for the supremum of the individual bounded-map exponents.
```
theorem uniform_inverse_first_power_gap :
    ∃ ε C : ℝ, 0 < ε ∧ ε < 1 / 4 ∧ 0 < C ∧
      (∀ (f : ℂ → ℂ), NormalizedUnivalent f →
        ∀ r : ℝ, 1 / 2 ≤ r → r < 1 →
          integralMean (-1) f r ≤ C * (1 - r) ^ (-(1 / 4 : ℝ) + ε)) ∧
      boundedSpectrum (-1) ≤ ((1 / 4 - ε : ℝ) : EReal) := by
…
```
Mentions: OAI.StrictInverseFirstPower.NormalizedUnivalent, OAI.StrictInverseFirstPower.integralMean, OAI.StrictInverseFirstPower.boundedSpectrum
theorem OAI.StrictInverseFirstPower.uniform_inverse_first_power line 34
theorem OAI.StrictInverseFirstPower.bounded_spectrum_strict line 42
theorem OAI.StrictInverseFirstPower.kraetzer_identity_false line 48